From 11cb915e7954f7a2afbaa2da4cb8db8d709c04af Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Thu, 8 Oct 2026 19:59:52 +0100 Subject: [PATCH 1/2] fix(dispatch): send echidnabot proof obligations as GraphQL variables Both senders of echidnabot's submitProofObligation now share one module, Hypatia.EchidnabotObligation: a static mutation document plus a variables map. Claim, context and prover never enter the document. - FleetDispatcher no longer splices claim/context into an inline string literal through escape_quotes/1, which escaped only `"`: a raw newline or a backslash in a claim produced an invalid or altered document. escape_quotes/1 stays: eight other bot mutations use it. - LearningScheduler.submit_requeue/4 reuses normalise_prover_hint/1 and omits `prover` when the hint has no ProverKind. It used to upcase any name (`lean4` -> `LEAN4`), an invalid enum value that fails the whole request. - HYPATIA_ECHIDNABOT_URL is a base URL for both senders; each appends /graphql. LearningScheduler used to POST to the value as given, with a default that already ended in /graphql. No port default changes. - LearningScheduler.requeue_candidates/3 is public, so the re-queue request can be tested on the wire. New test/echidnabot_dispatch_test.exs captures the HTTP request each sender puts on the wire. Its four sender tests fail on the old code. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015bTuGfwCcvjrmNFejydTML --- lib/echidnabot_obligation.ex | 105 ++++++++++++ lib/fleet_dispatcher.ex | 130 +++++++-------- lib/learning_scheduler.ex | 59 ++++--- test/echidnabot_dispatch_test.exs | 254 ++++++++++++++++++++++++++++++ 4 files changed, 447 insertions(+), 101 deletions(-) create mode 100644 lib/echidnabot_obligation.ex create mode 100644 test/echidnabot_dispatch_test.exs diff --git a/lib/echidnabot_obligation.ex b/lib/echidnabot_obligation.ex new file mode 100644 index 00000000..0672ad11 --- /dev/null +++ b/lib/echidnabot_obligation.ex @@ -0,0 +1,105 @@ +# SPDX-License-Identifier: MPL-2.0 + +defmodule Hypatia.EchidnabotObligation do + @moduledoc """ + The one place hypatia builds echidnabot's `submitProofObligation` request. + + Two senders use it: `Hypatia.FleetDispatcher` (proof obligations routed + from findings) and `Hypatia.LearningScheduler` (re-queues after a strategy + shift). Both send the same static GraphQL document and pass every value as + a GraphQL variable, so a claim or context holding a newline, a backslash or + a quote reaches echidnabot byte for byte and cannot change the document. + + The contract is echidnabot's `SubmitProofObligationInput` in + `src/api/graphql.rs` (added by hyperpolymath/echidnabot#169, on `main` at + `faeb280`): `repo`, `claim` and `context` are strings, `prover` is an + optional `ProverKind` enum value, and `inline` is an optional boolean. + + `HYPATIA_ECHIDNABOT_URL` has one meaning for both senders: the base URL of + echidnabot's HTTP server. Each sender appends `/graphql` (see + `graphql_url/1`). + """ + + @mutation """ + mutation SubmitProofObligation($input: SubmitProofObligationInput!) { + submitProofObligation(input: $input) { + success + proofId + } + } + """ + + # VeriSimDB / ProofStrategySelection prover names (lowercase snake) mapped + # to echidnabot's ProverKind enum values. Anything else has no ProverKind. + @prover_kinds %{ + "coq" => "COQ", + "lean" => "LEAN", + "agda" => "AGDA", + "isabelle" => "ISABELLE", + "z3" => "Z3", + "cvc5" => "CVC5", + "metamath" => "METAMATH", + "hol_light" => "HOL_LIGHT", + "mizar" => "MIZAR", + "pvs" => "PVS", + "acl2" => "ACL2", + "hol4" => "HOL4" + } + + @doc """ + The static `submitProofObligation` GraphQL document. Every value travels in + the `variables` map built by `variables/5`; nothing is interpolated here. + """ + @spec mutation() :: String.t() + def mutation, do: @mutation + + @doc """ + Build the GraphQL `variables` map for `mutation/0`. + + `prover_hint` is passed through `normalise_prover_hint/1`; when it has no + `ProverKind` the `prover` field is omitted, and echidnabot falls back to its + default prover. Pass `inline: true` (or `false`) in `opts` to set the + optional `inline` field; it is omitted otherwise. + """ + @spec variables(String.t(), String.t(), String.t(), String.t() | nil, keyword()) :: map() + def variables(repo, claim, context, prover_hint, opts \\ []) do + input = + %{"repo" => repo, "claim" => claim, "context" => context} + |> put_prover(normalise_prover_hint(prover_hint)) + |> put_inline(Keyword.fetch(opts, :inline)) + + %{"input" => input} + end + + @doc """ + Map a lowercase prover name (`"lean"`, `"hol_light"`, ...) to echidnabot's + `ProverKind` enum value (`"LEAN"`, `"HOL_LIGHT"`, ...). + + Returns `nil` for `nil` and for any name that is not a `ProverKind`, such as + `"lean4"` or `"idris2"`. Unknown names are dropped, not guessed at, because + echidnabot rejects the whole request when an enum value is invalid. + """ + @spec normalise_prover_hint(term()) :: String.t() | nil + def normalise_prover_hint(hint) when is_binary(hint), do: Map.get(@prover_kinds, hint) + def normalise_prover_hint(_hint), do: nil + + @doc """ + The GraphQL endpoint for an echidnabot base URL: `base_url <> "/graphql"`. + + This is the rule `Hypatia.FleetDispatcher` applies to every + `HYPATIA__URL`, so `HYPATIA_ECHIDNABOT_URL` means the same thing to + both senders. + """ + @spec graphql_url(String.t()) :: String.t() + def graphql_url(base_url) when is_binary(base_url), do: base_url <> "/graphql" + + # Add the optional `prover` field when there is a ProverKind for it. + defp put_prover(input, nil), do: input + defp put_prover(input, kind), do: Map.put(input, "prover", kind) + + # Add the optional `inline` field when the caller passed a boolean for it. + defp put_inline(input, {:ok, inline}) when is_boolean(inline), + do: Map.put(input, "inline", inline) + + defp put_inline(input, _), do: input +end diff --git a/lib/fleet_dispatcher.ex b/lib/fleet_dispatcher.ex index d931b67f..1b22e3cb 100644 --- a/lib/fleet_dispatcher.ex +++ b/lib/fleet_dispatcher.ex @@ -13,6 +13,7 @@ defmodule Hypatia.FleetDispatcher do alias Hypatia.DirectGitHubPR alias Hypatia.Rules.ProofObligation alias Hypatia.Rules.DependabotAlerts + alias Hypatia.EchidnabotObligation require Logger @@ -381,6 +382,8 @@ defmodule Hypatia.FleetDispatcher do execute_graphql(mutation, "sustainabot") end + # Submit a proof-obligation finding to echidnabot's submitProofObligation, + # with the claim, context and prover hint sent as GraphQL variables. defp dispatch_to_echidnabot(finding) do # Closes the proof learning loop: classify this obligation, ask VeriSimDB # which prover has historically worked best on that class, and pass the @@ -404,19 +407,24 @@ defmodule Hypatia.FleetDispatcher do override -> # Already resolved by ProofObligation.to_recipe/2 -- pass through - # the lowercase string; normalise_prover_hint/1 handles the mapping. + # the lowercase string; EchidnabotObligation.normalise_prover_hint/1 + # handles the mapping. override end - mutation = - build_proof_obligation_mutation( - finding_field(finding, :repo), + # Claim and context travel as GraphQL variables, never spliced into the + # document, so newlines, backslashes and quotes arrive byte for byte. A + # hint with no echidnabot ProverKind (e.g. "idris2") omits the prover + # field and echidnabot uses its own default. + variables = + EchidnabotObligation.variables( + finding_field(finding, :repo, ""), claim, context, prover_hint ) - execute_graphql(mutation, "echidnabot") + execute_graphql(EchidnabotObligation.mutation(), "echidnabot", variables) end # Look up the historically-best prover for an obligation class from @@ -443,62 +451,6 @@ defmodule Hypatia.FleetDispatcher do end end - # Build the submitProofObligation mutation (input-object syntax). - # - # CONTRACT GAP (2026-10-07): echidnabot's MutationRoot (src/api/graphql.rs) - # has no submitProofObligation and no ProofObligationInput; it only offers - # triggerCheck(repoId, commitSha, provers) on a registered repo. A live - # dispatch of this mutation therefore returns GraphQL `errors`, which - # execute_graphql/2 now reports as {:error, _}. Which side changes is an - # open owner decision. The prover field is omitted when - # prover_hint is nil OR the hint names a prover echidnabot's GraphQL - # schema doesn't know about (VeriSimDB tracks more provers than echidnabot - # currently exposes). In either case echidnabot uses its own default. - defp build_proof_obligation_mutation(repo, claim, context, prover_hint) do - prover_line = - case normalise_prover_hint(prover_hint) do - nil -> "" - enum_value -> " prover: #{enum_value},\n" - end - - """ - mutation { - submitProofObligation(input: { - repo: "#{repo}", - claim: "#{escape_quotes(claim)}", - context: "#{escape_quotes(context)}", - #{prover_line} }) { - success - proofId - } - } - """ - end - - # Map a VeriSimDB prover string to echidnabot's GraphQL ProverKind enum - # variant name. Returns nil for provers echidnabot doesn't expose (idris2, - # fstar, altergo, dafny, why3, tlaps, vampire, eprover, other) -- caller - # falls back to echidnabot's own default (Lean). - defp normalise_prover_hint(nil), do: nil - - defp normalise_prover_hint(hint) when is_binary(hint) do - case hint do - "coq" -> "COQ" - "lean" -> "LEAN" - "agda" -> "AGDA" - "isabelle" -> "ISABELLE" - "z3" -> "Z3" - "cvc5" -> "CVC5" - "metamath" -> "METAMATH" - "hol_light" -> "HOL_LIGHT" - "mizar" -> "MIZAR" - "pvs" -> "PVS" - "acl2" -> "ACL2" - "hol4" -> "HOL4" - _ -> nil - end - end - defp dispatch_to_rhodibot(finding) do mutation = """ mutation { @@ -770,14 +722,21 @@ defmodule Hypatia.FleetDispatcher do # when no URL is configured and the manifest write succeeded, and # `{:error, reason}` otherwise. A configured URL that fails is an error even # though the manifest line was written: the caller asked for live dispatch. - defp execute_graphql(query, bot_name) do + # + # `variables` (default nil) is the GraphQL variables map for a document + # that declares them, as echidnabot's submitProofObligation does. When + # given, it is recorded in the manifest line next to `query` and sent in + # the request's JSON envelope. + defp execute_graphql(query, bot_name, variables \\ nil) do # Dual dispatch: file-based (immediate) + HTTP (when fleet API available) - dispatch_record = %{ - "bot" => bot_name, - "query" => query, - "dispatched_at" => DateTime.utc_now() |> DateTime.to_iso8601(), - "status" => "pending" - } + dispatch_record = + %{ + "bot" => bot_name, + "query" => query, + "dispatched_at" => DateTime.utc_now() |> DateTime.to_iso8601(), + "status" => "pending" + } + |> maybe_put_variables(variables) # 1. Always write to dispatch manifest (dispatch-runner.sh reads this) manifest_result = write_manifest(dispatch_record) @@ -793,7 +752,7 @@ defmodule Hypatia.FleetDispatcher do # GraphQL endpoint instead of routing through a fleet coordinator that may # not exist. The fleet-coordinator path is kept as a fallback for # deployments that front multiple bots behind one dispatcher. - {target_url, description, body} = resolve_dispatch_url(bot_name, query) + {target_url, description, body} = resolve_dispatch_url(bot_name, query, variables) graphql_envelope? = description != :none and String.starts_with?(description, "via per-bot") @@ -874,11 +833,14 @@ defmodule Hypatia.FleetDispatcher do # Resolve the HTTP dispatch target for a bot. # Returns {url, description, body} on success, {nil, _, _} when no URL configured. # - # - Per-bot URLs hit the bot's own GraphQL endpoint, so we wrap the query in - # a GraphQL-over-HTTP JSON envelope: {"query": "..."}. + # - Per-bot URLs are base URLs. We POST to {url}/graphql, the bot's own + # GraphQL endpoint, with a GraphQL-over-HTTP JSON envelope: + # {"query": "..."}, plus "variables" when the document declares them. # - Fleet-coordinator URLs hit /dispatch/{bot_name} with the raw query as - # body, preserving legacy fleet-coordinator semantics. - defp resolve_dispatch_url(bot_name, query) do + # body, preserving legacy fleet-coordinator semantics. A raw document + # cannot carry variables, so a dispatch that has them sends the same JSON + # envelope there instead. + defp resolve_dispatch_url(bot_name, query, variables) do per_bot_env = "HYPATIA_" <> String.upcase(bot_name) <> "_URL" case System.get_env(per_bot_env) do @@ -887,16 +849,32 @@ defmodule Hypatia.FleetDispatcher do nil -> {nil, :none, nil} - fleet_url -> + fleet_url when is_nil(variables) -> {fleet_url <> "/dispatch/" <> bot_name, "via fleet coordinator", query} + + fleet_url -> + {fleet_url <> "/dispatch/" <> bot_name, "via fleet coordinator", + graphql_envelope(query, variables)} end bot_url -> - envelope = Jason.encode!(%{"query" => query}) - {bot_url <> "/graphql", "via per-bot URL #{per_bot_env}", envelope} + {bot_url <> "/graphql", "via per-bot URL #{per_bot_env}", + graphql_envelope(query, variables)} end end + # Encode a GraphQL-over-HTTP request body: {"query": ...}, with + # "variables" added when the document has any. + defp graphql_envelope(query, variables) do + %{"query" => query} + |> maybe_put_variables(variables) + |> Jason.encode!() + end + + # Add a "variables" key to a map when there are variables to carry. + defp maybe_put_variables(map, nil), do: map + defp maybe_put_variables(map, variables), do: Map.put(map, "variables", variables) + # POST a JSON body. Returns `{:ok, status, body}` for a 2xx response, # `{:error, {:http_status, status}}` for any other status, or the :httpc error. defp http_post(url, body) do diff --git a/lib/learning_scheduler.ex b/lib/learning_scheduler.ex index d4dfffd9..21a44159 100644 --- a/lib/learning_scheduler.ex +++ b/lib/learning_scheduler.ex @@ -20,6 +20,7 @@ defmodule Hypatia.LearningScheduler do require Logger alias Hypatia.ConfidenceAnnealing + alias Hypatia.EchidnabotObligation # 5 minutes @poll_interval_ms 5 * 60 * 1_000 @@ -392,14 +393,28 @@ defmodule Hypatia.LearningScheduler do end end - # Re-queue each candidate attempt_id via echidnabot. We construct a - # fresh submitProofObligation mutation with the class and new prover - # hint. Failures logged but non-fatal -- the scheduler must keep - # running even if echidnabot is unreachable. - defp requeue_candidates(_class, _new_top, []), do: :ok + @doc """ + Re-queue failed proof attempts with echidnabot after a strategy shift. - defp requeue_candidates(class, new_top, candidates) do - echidnabot_url = System.get_env("HYPATIA_ECHIDNABOT_URL") || "http://localhost:9001/graphql" + Sends one `submitProofObligation` per attempt id (at most 20 per call) with + `new_top` as the prover hint, and returns `:ok`. Failures are logged and + never raised: the scheduler must keep running when echidnabot is + unreachable. + + `HYPATIA_ECHIDNABOT_URL` is echidnabot's base URL, the same meaning + `Hypatia.FleetDispatcher` gives it, and `/graphql` is appended. It defaults + to `http://localhost:9001`. `new_top` goes through + `Hypatia.EchidnabotObligation.normalise_prover_hint/1`, so a name with no + echidnabot `ProverKind` (such as `"lean4"`) sends no prover instead of an + invalid enum value. + """ + @spec requeue_candidates(String.t(), String.t() | nil, [String.t()]) :: :ok + def requeue_candidates(_class, _new_top, []), do: :ok + + def requeue_candidates(class, new_top, candidates) do + echidnabot_url = + (System.get_env("HYPATIA_ECHIDNABOT_URL") || "http://localhost:9001") + |> EchidnabotObligation.graphql_url() success_count = candidates @@ -418,27 +433,21 @@ defmodule Hypatia.LearningScheduler do :ok end + # Send one best-effort submitProofObligation for a failed attempt and + # report whether echidnabot accepted it. The document is static; the class, + # attempt id and prover travel as GraphQL variables built by + # EchidnabotObligation, so no value can change the document. defp submit_requeue(url, class, prover, attempt_id) do - # Best-effort GraphQL mutation. The prover field is an enum in - # echidnabot's schema; we send it unquoted as the enum literal. - prover_upper = prover |> String.upcase() |> String.replace("-", "_") - - claim = "requeue-of-#{attempt_id}" - context = "strategy-shift class=#{class}" - - mutation = """ - mutation { - submitProofObligation(input: { - repo: "hyperpolymath/requeue", - claim: "#{claim}", - context: "#{context}", - prover: #{prover_upper}, + variables = + EchidnabotObligation.variables( + "hyperpolymath/requeue", + "requeue-of-#{attempt_id}", + "strategy-shift class=#{class}", + prover, inline: true - }) { success proofId } - } - """ + ) - body = Jason.encode!(%{query: mutation}) + body = Jason.encode!(%{"query" => EchidnabotObligation.mutation(), "variables" => variables}) case http_post_json(url, body, 5_000) do {:ok, response_body} -> diff --git a/test/echidnabot_dispatch_test.exs b/test/echidnabot_dispatch_test.exs new file mode 100644 index 00000000..a7edb472 --- /dev/null +++ b/test/echidnabot_dispatch_test.exs @@ -0,0 +1,254 @@ +# SPDX-License-Identifier: MPL-2.0 + +defmodule Hypatia.EchidnabotDispatchTest do + # Both senders of echidnabot's `submitProofObligation`: FleetDispatcher and + # LearningScheduler. Each test captures the request a sender actually puts + # on the wire and checks the GraphQL-over-HTTP envelope, not the sender's + # return value alone. + # + # Mutates process-global env (HYPATIA_ECHIDNABOT_URL), so it cannot run + # concurrently with other tests. + use ExUnit.Case, async: false + + alias Hypatia.FleetDispatcher + alias Hypatia.LearningScheduler + + @accepted ~s({"data":{"submitProofObligation":{"success":true,"proofId":"p-1"}}}) + + # A claim that an inline GraphQL string literal cannot carry when only `"` + # is escaped: a raw newline, a tab, a backslash and a quote. + @hostile_claim "line one\nline two\twith \\ backslash and \"quotes\"" + + setup do + # A fresh manifest directory per test, so a manifest assertion reads only + # this test's line. + original_path = Application.get_env(:hypatia, :verisimdb_data_path) + + data_path = + Path.join(["_build", "test", "echidnabot-dispatch-#{System.unique_integer([:positive])}"]) + + Application.put_env(:hypatia, :verisimdb_data_path, data_path) + + on_exit(fn -> + System.delete_env("HYPATIA_ECHIDNABOT_URL") + System.delete_env("HYPATIA_FLEET_URL") + Application.put_env(:hypatia, :verisimdb_data_path, original_path) + File.rm_rf!(data_path) + end) + + {:ok, manifest: Path.join([data_path, "dispatch", "pending.jsonl"])} + end + + # Serve exactly one HTTP request on an ephemeral localhost port. The request + # line and the full body (read to its Content-Length) are sent to the test + # process as `{:captured, request_line, body}`. Returns the base URL. + defp capturing_server(status, reply) do + test_pid = self() + {:ok, listen} = :gen_tcp.listen(0, [:binary, packet: :raw, active: false, reuseaddr: true]) + {:ok, port} = :inet.port(listen) + + spawn_link(fn -> + {:ok, sock} = :gen_tcp.accept(listen) + {head, body_start} = recv_head(sock, "") + [request_line | header_lines] = String.split(head, "\r\n") + body = recv_body(sock, body_start, content_length(header_lines)) + send(test_pid, {:captured, request_line, body}) + + :gen_tcp.send( + sock, + "HTTP/1.1 #{status} X\r\ncontent-type: application/json\r\n" <> + "content-length: #{byte_size(reply)}\r\nconnection: close\r\n\r\n" <> reply + ) + + :gen_tcp.close(sock) + :gen_tcp.close(listen) + end) + + "http://127.0.0.1:#{port}" + end + + # Read until the end of the HTTP header block; returns {head, body_so_far}. + defp recv_head(sock, acc) do + case :binary.split(acc, "\r\n\r\n") do + [head, rest] -> + {head, rest} + + [_] -> + {:ok, data} = :gen_tcp.recv(sock, 0, 5_000) + recv_head(sock, acc <> data) + end + end + + # Read until the body holds `length` bytes. + defp recv_body(_sock, acc, length) when byte_size(acc) >= length, do: acc + + defp recv_body(sock, acc, length) do + {:ok, data} = :gen_tcp.recv(sock, 0, 5_000) + recv_body(sock, acc <> data, length) + end + + # The Content-Length header value, or 0 when absent. + defp content_length(header_lines) do + Enum.find_value(header_lines, 0, fn line -> + case String.split(line, ":", parts: 2) do + [name, value] -> + if String.downcase(String.trim(name)) == "content-length", + do: value |> String.trim() |> String.to_integer() + + _ -> + nil + end + end) + end + + # Wait for the capturing server's request; returns {request_line, decoded JSON body}. + defp captured! do + assert_receive {:captured, request_line, body}, 5_000 + {request_line, Jason.decode!(body)} + end + + # A :proof_obligation finding carrying the hostile claim, with `overrides` merged in. + defp obligation(overrides) do + Map.merge( + %{ + type: :proof_obligation, + repo: "hyperpolymath/hypatia", + claim: @hostile_claim, + context: "context\nacross lines", + prover_hint_override: "lean" + }, + overrides + ) + end + + describe "FleetDispatcher -> echidnabot" do + test "sends claim and context as GraphQL variables, byte for byte" do + System.put_env("HYPATIA_ECHIDNABOT_URL", capturing_server(200, @accepted)) + + assert {:ok, :dispatched} = FleetDispatcher.dispatch_finding(obligation(%{})) + + {request_line, envelope} = captured!() + assert request_line =~ ~r{^POST /graphql HTTP/1\.[01]$} + + assert envelope["variables"] == %{ + "input" => %{ + "repo" => "hyperpolymath/hypatia", + "claim" => @hostile_claim, + "context" => "context\nacross lines", + "prover" => "LEAN" + } + } + + # The document is static: no part of the claim is spliced into it. + refute envelope["query"] =~ "line one" + assert envelope["query"] =~ "$input: SubmitProofObligationInput!" + end + + test "omits the prover when the hint is not a ProverKind value" do + System.put_env("HYPATIA_ECHIDNABOT_URL", capturing_server(200, @accepted)) + + assert {:ok, :dispatched} = + FleetDispatcher.dispatch_finding(obligation(%{prover_hint_override: "lean4"})) + + {_request_line, envelope} = captured!() + refute Map.has_key?(envelope["variables"]["input"], "prover") + end + + test "records the variables in the manifest line next to the static query", %{ + manifest: manifest + } do + System.put_env("HYPATIA_ECHIDNABOT_URL", capturing_server(200, @accepted)) + + assert {:ok, :dispatched} = FleetDispatcher.dispatch_finding(obligation(%{})) + _ = captured!() + + [line] = manifest |> File.read!() |> String.split("\n", trim: true) + record = Jason.decode!(line) + assert record["bot"] == "echidnabot" + assert record["query"] == Hypatia.EchidnabotObligation.mutation() + assert record["variables"]["input"]["claim"] == @hostile_claim + end + + test "sends the JSON envelope, variables included, on the fleet-coordinator path" do + System.put_env("HYPATIA_FLEET_URL", capturing_server(200, "{}")) + + assert {:ok, :dispatched} = FleetDispatcher.dispatch_finding(obligation(%{})) + + {request_line, envelope} = captured!() + assert request_line =~ ~r{^POST /dispatch/echidnabot HTTP/1\.[01]$} + assert envelope["query"] == Hypatia.EchidnabotObligation.mutation() + assert envelope["variables"]["input"]["claim"] == @hostile_claim + end + end + + describe "EchidnabotObligation" do + alias Hypatia.EchidnabotObligation + + test "normalise_prover_hint/1 maps ProverKind names and drops everything else" do + assert EchidnabotObligation.normalise_prover_hint("lean") == "LEAN" + assert EchidnabotObligation.normalise_prover_hint("hol_light") == "HOL_LIGHT" + assert EchidnabotObligation.normalise_prover_hint("hol4") == "HOL4" + assert EchidnabotObligation.normalise_prover_hint("lean4") == nil + assert EchidnabotObligation.normalise_prover_hint("idris2") == nil + assert EchidnabotObligation.normalise_prover_hint("LEAN") == nil + assert EchidnabotObligation.normalise_prover_hint(nil) == nil + end + + test "variables/5 sets inline only when asked and never splices values" do + assert EchidnabotObligation.variables("o/r", "c", "x", nil) == + %{"input" => %{"repo" => "o/r", "claim" => "c", "context" => "x"}} + + assert EchidnabotObligation.variables("o/r", "c", "x", "coq", inline: true) == + %{ + "input" => %{ + "repo" => "o/r", + "claim" => "c", + "context" => "x", + "prover" => "COQ", + "inline" => true + } + } + + # The document holds no string literal for a value to be spliced into. + refute EchidnabotObligation.mutation() =~ "\"" + end + + test "graphql_url/1 treats the env value as a base URL" do + assert EchidnabotObligation.graphql_url("http://localhost:9001") == + "http://localhost:9001/graphql" + end + end + + describe "LearningScheduler -> echidnabot" do + test "re-queues with variables, a normalised prover, and the base URL + /graphql" do + System.put_env("HYPATIA_ECHIDNABOT_URL", capturing_server(200, @accepted)) + + assert :ok = LearningScheduler.requeue_candidates("cls \"a\"\nb", "hol_light", ["att-1"]) + + {request_line, envelope} = captured!() + assert request_line =~ ~r{^POST /graphql HTTP/1\.[01]$} + + assert envelope["variables"] == %{ + "input" => %{ + "repo" => "hyperpolymath/requeue", + "claim" => "requeue-of-att-1", + "context" => "strategy-shift class=cls \"a\"\nb", + "prover" => "HOL_LIGHT", + "inline" => true + } + } + + refute envelope["query"] =~ "requeue-of" + end + + test "drops a prover name that is not a ProverKind value instead of upcasing it" do + System.put_env("HYPATIA_ECHIDNABOT_URL", capturing_server(200, @accepted)) + + assert :ok = LearningScheduler.requeue_candidates("cls", "lean4", ["att-2"]) + + {_request_line, envelope} = captured!() + refute Map.has_key?(envelope["variables"]["input"], "prover") + refute inspect(envelope) =~ "LEAN4" + end + end +end From 83a0c597334569020c3d9874e360117ca7d68a67 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Thu, 8 Oct 2026 20:10:13 +0100 Subject: [PATCH 2/2] fix(dispatch): accept echidnabot's hol-light prover slug normalise_prover_hint/1 mapped only hypatia's own snake-case name, hol_light. echidnabot's ProverKind slug is hol-light (map_prover_kind in its src/api/graphql.rs), so a prover hint that originated from echidnabot was dropped and the obligation went out with no prover. Map both names to HOL_LIGHT and assert it in the normaliser test. Addresses the CodeRabbit review thread on lib/echidnabot_obligation.ex. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015bTuGfwCcvjrmNFejydTML --- lib/echidnabot_obligation.ex | 6 +++++- test/echidnabot_dispatch_test.exs | 1 + 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/lib/echidnabot_obligation.ex b/lib/echidnabot_obligation.ex index 0672ad11..452c4cbe 100644 --- a/lib/echidnabot_obligation.ex +++ b/lib/echidnabot_obligation.ex @@ -30,7 +30,10 @@ defmodule Hypatia.EchidnabotObligation do """ # VeriSimDB / ProofStrategySelection prover names (lowercase snake) mapped - # to echidnabot's ProverKind enum values. Anything else has no ProverKind. + # to echidnabot's ProverKind enum values. HOL Light also accepts + # echidnabot's own slug, `hol-light` (`map_prover_kind` in its + # `src/api/graphql.rs`), so a hint that came from echidnabot is not dropped. + # Anything else has no ProverKind. @prover_kinds %{ "coq" => "COQ", "lean" => "LEAN", @@ -40,6 +43,7 @@ defmodule Hypatia.EchidnabotObligation do "cvc5" => "CVC5", "metamath" => "METAMATH", "hol_light" => "HOL_LIGHT", + "hol-light" => "HOL_LIGHT", "mizar" => "MIZAR", "pvs" => "PVS", "acl2" => "ACL2", diff --git a/test/echidnabot_dispatch_test.exs b/test/echidnabot_dispatch_test.exs index a7edb472..b376c0fb 100644 --- a/test/echidnabot_dispatch_test.exs +++ b/test/echidnabot_dispatch_test.exs @@ -187,6 +187,7 @@ defmodule Hypatia.EchidnabotDispatchTest do test "normalise_prover_hint/1 maps ProverKind names and drops everything else" do assert EchidnabotObligation.normalise_prover_hint("lean") == "LEAN" assert EchidnabotObligation.normalise_prover_hint("hol_light") == "HOL_LIGHT" + assert EchidnabotObligation.normalise_prover_hint("hol-light") == "HOL_LIGHT" assert EchidnabotObligation.normalise_prover_hint("hol4") == "HOL4" assert EchidnabotObligation.normalise_prover_hint("lean4") == nil assert EchidnabotObligation.normalise_prover_hint("idris2") == nil