fix(config): require HYPATIA_VERISIM_URL / HYPATIA_ECHIDNABOT_URL, no localhost defaults

CHANGELOG.adoc

@@ -120,6 +120,32 @@ extended to thread the four new check functions into its return
 
 === Changed
 
+==== No built-in VeriSimDB / echidnabot URLs (2026-10-08)
+
+hypatia no longer falls back to `http://localhost:8080` (verisim-api) or
+`http://localhost:9001` (echidnabot) when the service URL is unset. The new
+`Hypatia.ServiceUrl` reads `HYPATIA_VERISIM_URL` and `HYPATIA_ECHIDNABOT_URL`.
+A variable that is unset, empty or whitespace-only means the feature is off:
+callers return `{:error, :not_configured}` (or their existing empty value)
+without a network call, and nothing fails at boot.
+
+* `ProofStrategySelection`, `StrategyDrift`, `VCL.ProofResolver`,
+  `ProofObligation` prover hints and `LearningScheduler` re-queues all go
+  through `ServiceUrl`.
+* `Neural.ProverRecommender` used to read `VERISIM_URL` (echidna's variable)
+  at **compile time**. It now reads `HYPATIA_VERISIM_URL` at runtime, like
+  every other caller.
+* `FleetDispatcher` reads `HYPATIA_<BOT>_URL` and `HYPATIA_FLEET_URL`
+  through `ServiceUrl.from_env/1`, so a blank value counts as unset
+  there too. Before, a blank per-bot URL was POSTed to as `"  /graphql"` and
+  the dispatch failed instead of falling back to the fleet coordinator or
+  the manifest.
+* With `HYPATIA_ECHIDNABOT_URL` unset, a strategy shift logs the dropped
+  re-queue candidates at info and returns `:ok`. Before this change the
+  same candidates were lost against the unreachable default.
+
+Covered by `test/service_url_test.exs`.
+
 ==== docs/ second-pass bucketing (2026-05-25, post-#315)
 
 Five flat files at `docs/` root moved into proper subdirs. PR #315

docs/wiki-pages/Operations.md

@@ -56,7 +56,8 @@ The supervision tree starts Bandit on port 9090 (9099 under `MIX_ENV=test`):
 |---|---|
 | `HYPATIA_DISPATCH_PAT` | GitHub PAT with `repo` scope for cross-repo dispatch |
 | `HYPATIA_HTTP_PORT` | Override the Bandit listen port (default 9090) |
-| `HYPATIA_VERISIM_URL` | verisim-api endpoint, when deployed |
+| `HYPATIA_VERISIM_URL` | verisim-api base URL. No default: unset or blank turns off prover hints, strategy-shift detection and recommender retraining |
+| `HYPATIA_ECHIDNABOT_URL` | echidnabot base URL (`/graphql` is appended). No default: unset or blank means strategy-shift re-queues are logged and dropped |
 | `HYPATIA_FLEET_PATH` | Path to the gitbot-fleet checkout |
 | `HYPATIA_ALERT_WEBHOOK_URL` | Webhook for watcher alerts |
 | `HYPATIA_ALERT_LOG_FILE` | File sink for watcher alerts |

lib/fleet_dispatcher.ex

@@ -14,6 +14,7 @@ defmodule Hypatia.FleetDispatcher do
   alias Hypatia.Rules.ProofObligation
   alias Hypatia.Rules.DependabotAlerts
   alias Hypatia.EchidnabotObligation
+  alias Hypatia.ServiceUrl
 
   require Logger
 
@@ -840,24 +841,27 @@ defmodule Hypatia.FleetDispatcher 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.
+  # - Both variables are read through `Hypatia.ServiceUrl.from_env/1`, so an
+  #   empty or whitespace-only value counts as unset, as it does for every
+  #   other service URL.
   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
-      nil ->
-        case System.get_env("HYPATIA_FLEET_URL") do
-          nil ->
+    case ServiceUrl.from_env(per_bot_env) do
+      {:error, :not_configured} ->
+        case ServiceUrl.from_env("HYPATIA_FLEET_URL") do
+          {:error, :not_configured} ->
             {nil, :none, nil}
 
-          fleet_url when is_nil(variables) ->
+          {:ok, fleet_url} when is_nil(variables) ->
             {fleet_url <> "/dispatch/" <> bot_name, "via fleet coordinator", query}
 
-          fleet_url ->
+          {:ok, fleet_url} ->
             {fleet_url <> "/dispatch/" <> bot_name, "via fleet coordinator",
              graphql_envelope(query, variables)}
         end
 
-      bot_url ->
+      {:ok, bot_url} ->
         {bot_url <> "/graphql", "via per-bot URL #{per_bot_env}",
          graphql_envelope(query, variables)}
     end

lib/learning_scheduler.ex

@@ -21,6 +21,7 @@ defmodule Hypatia.LearningScheduler do
 
   alias Hypatia.ConfidenceAnnealing
   alias Hypatia.EchidnabotObligation
+  alias Hypatia.ServiceUrl
 
   # 5 minutes
   @poll_interval_ms 5 * 60 * 1_000
@@ -259,16 +260,15 @@ defmodule Hypatia.LearningScheduler do
 
   # Fetches proof_attempts from VeriSimDB and re-fits ProverRecommender's
   # per-class RBF networks. Returns true if training succeeded, false if
-  # VeriSimDB was unreachable or returned too few samples.
+  # VeriSimDB was unconfigured (HYPATIA_VERISIM_URL unset), unreachable or
+  # returned too few samples.
   #
   # Minimum sample threshold (50) prevents overfitting on early sparse data.
   # The existing in-memory models continue serving recommendations until
   # a successful retrain replaces them.
   defp retrain_prover_recommender do
-    base_url = System.get_env("HYPATIA_VERISIM_URL") || "http://localhost:8080"
-
     try do
-      case Hypatia.Neural.ProverRecommender.train_from_verisim(base_url: base_url) do
+      case Hypatia.Neural.ProverRecommender.train_from_verisim() do
         {:ok, models} ->
           sample_size = Map.get(models, :sample_size, 0)
 
@@ -369,12 +369,11 @@ defmodule Hypatia.LearningScheduler do
   # Runs StrategyDrift.check_all_shifts/1 on each tick. For each shift
   # event, enqueues the candidate failed-attempt IDs via echidnabot's
   # submitProofObligation mutation with the new top prover as hint.
-  # Logs but does not block on re-queueing errors.
+  # Logs but does not block on re-queueing errors. With HYPATIA_VERISIM_URL
+  # unset no class can shift, so this returns [] without a network call.
   defp detect_and_requeue_strategy_shifts do
-    base_url = System.get_env("HYPATIA_VERISIM_URL") || "http://localhost:8080"
-
     try do
-      events = Hypatia.Rules.StrategyDrift.check_all_shifts(base_url: base_url)
+      events = Hypatia.Rules.StrategyDrift.check_all_shifts()
 
       Enum.each(events, fn {:shift, class, old_top, new_top, candidates} ->
         Logger.info(
@@ -402,8 +401,10 @@ defmodule Hypatia.LearningScheduler do
   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.FleetDispatcher` gives it, and `/graphql` is appended. It has no
+  default: when it is unset or blank, nothing is sent, the dropped candidates
+  are logged, and the call returns `:ok` (see `Hypatia.ServiceUrl`).
+  `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.
@@ -412,10 +413,23 @@ defmodule Hypatia.LearningScheduler do
   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()
+    case ServiceUrl.echidnabot() do
+      {:ok, base_url} ->
+        send_requeues(EchidnabotObligation.graphql_url(base_url), class, new_top, candidates)
+
+      {:error, :not_configured} ->
+        Logger.info(
+          "LearningScheduler: HYPATIA_ECHIDNABOT_URL unset -- not re-queueing " <>
+            "#{length(candidates)} attempts for class=#{class}"
+        )
+
+        :ok
+    end
+  end
 
+  # Send at most 20 re-queues to echidnabot's GraphQL endpoint
+  # `echidnabot_url` and log how many it accepted.
+  defp send_requeues(echidnabot_url, class, new_top, candidates) do
     success_count =
       candidates
       # rate-limit: max 20 re-queues per tick

lib/neural/prover_recommender.ex

@@ -31,8 +31,8 @@ defmodule Hypatia.Neural.ProverRecommender do
 
   require Logger
   alias Hypatia.Neural.RadialNeuralNetwork
+  alias Hypatia.ServiceUrl
 
-  @verisim_base_url System.get_env("VERISIM_URL") || "http://127.0.0.1:8080"
   @default_limit 500
 
   # Persistent-term key for the live model snapshot.
@@ -68,11 +68,22 @@ defmodule Hypatia.Neural.ProverRecommender do
   Train one RBF network per obligation_class from the most recent N
   proof_attempts. Returns a map `%{class => rbf}` indexed by obligation
   class, plus a global fallback model trained on all rows.
+
+  The verisim-api URL is `:base_url`, else `HYPATIA_VERISIM_URL`. With
+  neither set this returns `{:error, :not_configured}` without a network
+  call (see `Hypatia.ServiceUrl`).
   """
   def train_from_verisim(opts \\ []) do
     limit = Keyword.get(opts, :limit, @default_limit)
-    base_url = Keyword.get(opts, :base_url, @verisim_base_url)
 
+    with {:ok, base_url} <- ServiceUrl.verisim(opts) do
+      train_from(base_url, limit)
+    end
+  end
+
+  # Fetch up to `limit` attempts from the verisim-api at `base_url` and
+  # train the global and per-class networks on them.
+  defp train_from(base_url, limit) do
     case fetch_attempts(limit, base_url) do
       {:ok, attempts} ->
         {vectors, targets, classes} = prepare_training_data(attempts)
@@ -123,28 +134,26 @@ defmodule Hypatia.Neural.ProverRecommender do
   # Fetch recent proof attempts from the row-level VeriSim API, falling back
   # to aggregate strategy data when that endpoint is unavailable.
   defp fetch_attempts(limit, base_url) do
-    resolved_url = base_url || @verisim_base_url
-    url = "#{resolved_url}/api/v1/proof_attempts?limit=#{limit}"
+    url = "#{base_url}/api/v1/proof_attempts?limit=#{limit}"
     # verisim-api /proof_attempts GET doesn't exist yet -- fall back to ClickHouse
     # strategy endpoint aggregates when the row-level endpoint is absent.
     case http_get(url) do
       {:ok, body} -> Jason.decode(body)
-      {:error, _} -> fetch_attempts_via_clickhouse(limit, resolved_url)
+      {:error, _} -> fetch_attempts_via_clickhouse(limit, base_url)
     end
   end
 
   # Convert aggregate ClickHouse-backed strategy recommendations into the
   # synthetic attempt rows expected by the recommender's training pipeline.
   defp fetch_attempts_via_clickhouse(limit, base_url) do
-    resolved_url = base_url || @verisim_base_url
     # ClickHouse HTTP: reach it by probing each active class's strategy endpoint
     # and folding the recommendations back into synthetic attempt rows.
     classes = ~w(safety linearity termination equiv correctness confluence
                  totality invariant refinement model-check other)
 
     attempts =
       Enum.flat_map(classes, fn class ->
-        url = "#{resolved_url}/api/v1/proof_attempts/strategy?class=#{class}&limit=20"
+        url = "#{base_url}/api/v1/proof_attempts/strategy?class=#{class}&limit=20"
 
         case http_get(url) do
           {:ok, body} ->

lib/rules/proof_obligation.ex

@@ -296,14 +296,11 @@ defmodule Hypatia.Rules.ProofObligation do
   end
 
   # Look up the historically best prover for an obligation class.
-  # Returns nil if VeriSimDB is unreachable or has no data for this class.
+  # Returns nil if VeriSimDB is unconfigured, unreachable or has no data for
+  # this class. `:verisim_url` overrides HYPATIA_VERISIM_URL; there is no
+  # built-in default (see Hypatia.ServiceUrl).
   defp prover_hint_for(obligation_class, opts) do
-    base_url =
-      Keyword.get(
-        opts,
-        :verisim_url,
-        System.get_env("HYPATIA_VERISIM_URL") || "http://localhost:8080"
-      )
+    base_url = Keyword.get(opts, :verisim_url)
 
     case ProofStrategySelection.recommend(obligation_class, base_url: base_url) do
       {:ok, [%{"prover" => p} | _]} -> p

lib/rules/proof_strategy_selection.ex

@@ -25,19 +25,18 @@ defmodule Hypatia.Rules.ProofStrategySelection do
                       → fleet_dispatcher routes with prover hint
                       → echidnabot runs recommended prover first
 
-  Graceful degradation: if VeriSimDB is unreachable, `recommend/2`
-  returns `{:error, reason}`. The caller should fall back to the
-  configured default prover rather than failing the dispatch.
+  Graceful degradation: if VeriSimDB is unconfigured or unreachable,
+  `recommend/2` returns `{:error, reason}`. The caller should fall back to
+  the configured default prover rather than failing the dispatch.
 
   Rule IDs: PS001-PS010
   """
 
   require Logger
+  alias Hypatia.ServiceUrl
 
   @default_limit 5
   @default_timeout_ms 5_000
-  @verisim_url_env "HYPATIA_VERISIM_URL"
-  @default_verisim_url "http://localhost:8080"
 
   # Tier-1 provers for novelty gating: when an obligation_class has no
   # historical data, route to a Tier-1 prover from the same family rather
@@ -75,17 +74,26 @@ defmodule Hypatia.Rules.ProofStrategySelection do
   Options:
     - `:limit` (default 5) -- maximum recommendations to return
     - `:timeout` (default 5000ms) -- HTTP request timeout
-    - `:base_url` -- override VeriSimDB URL (else HYPATIA_VERISIM_URL env or default)
+    - `:base_url` -- override VeriSimDB URL (else `HYPATIA_VERISIM_URL`; there
+      is no built-in default, see `Hypatia.ServiceUrl`)
 
-  Returns `{:error, :not_configured}` if VeriSimDB URL is missing,
+  Returns `{:error, :not_configured}`, without a network call, when neither
+  `:base_url` nor `HYPATIA_VERISIM_URL` holds a URL,
   `{:error, {:http_status, code}}` on non-2xx response,
   `{:error, {:transport, reason}}` on network failure,
   `{:error, {:decode, reason}}` on malformed JSON.
   """
   def recommend(obligation_class, opts \\ []) when is_binary(obligation_class) do
+    with {:ok, base_url} <- ServiceUrl.verisim(opts) do
+      fetch_recommendations(obligation_class, base_url, opts)
+    end
+  end
+
+  # GET the strategy endpoint under `base_url` and decode its
+  # recommendations, mapping each failure to the shape `recommend/2` documents.
+  defp fetch_recommendations(obligation_class, base_url, opts) do
     limit = Keyword.get(opts, :limit, @default_limit)
     timeout_ms = Keyword.get(opts, :timeout, @default_timeout_ms)
-    base_url = resolve_base_url(opts)
 
     path =
       "/api/v1/proof_attempts/strategy?class=" <>
@@ -186,8 +194,15 @@ defmodule Hypatia.Rules.ProofStrategySelection do
   defp cert_rank(_), do: 0
 
   defp fetch_certs(obligation_class, opts) do
+    with {:ok, base_url} <- ServiceUrl.verisim(opts) do
+      fetch_certs_from(obligation_class, base_url, opts)
+    end
+  end
+
+  # GET the certificates endpoint under `base_url` and index the PROVEN
+  # rows by prover; any failure becomes `{:error, {:certs_unavailable, _}}`.
+  defp fetch_certs_from(obligation_class, base_url, opts) do
     timeout_ms = Keyword.get(opts, :timeout, @default_timeout_ms)
-    base_url = resolve_base_url(opts)
 
     url =
       base_url <>
@@ -369,13 +384,6 @@ defmodule Hypatia.Rules.ProofStrategySelection do
 
   # ─── internals ──────────────────────────────────────────────────────
 
-  defp resolve_base_url(opts) do
-    case Keyword.get(opts, :base_url) do
-      nil -> System.get_env(@verisim_url_env) || @default_verisim_url
-      url -> url
-    end
-  end
-
   defp http_get(url, timeout_ms) do
     request = {String.to_charlist(url), [{~c"accept", ~c"application/json"}]}
 

lib/rules/strategy_drift.ex

@@ -45,9 +45,9 @@ defmodule Hypatia.Rules.StrategyDrift do
 
   require Logger
   alias Hypatia.Rules.ProofStrategySelection
+  alias Hypatia.ServiceUrl
 
   @table :hypatia_strategy_drift
-  @default_base_url "http://localhost:8080"
 
   # ── Public API ─────────────────────────────────────────────────────────
 
@@ -72,14 +72,16 @@ defmodule Hypatia.Rules.StrategyDrift do
       first observation)
     * `{:shift, class, old_top, new_top, failed_attempt_ids}` -- top prover
       changed; failed_attempt_ids are candidates for re-queueing
-    * `{:error, reason}` -- couldn't reach strategy endpoint
+    * `{:error, reason}` -- couldn't reach strategy endpoint, or
+      `{:error, :not_configured}` when neither `:base_url` nor
+      `HYPATIA_VERISIM_URL` holds a URL (no network call is made)
 
   Pass `:hypatia_strategy_drift` or set up the ETS table via `init_table/0`
   before calling.
   """
   def check_shift(class, opts \\ []) when is_binary(class) do
     init_table()
-    base_url = Keyword.get(opts, :base_url, @default_base_url)
+    base_url = Keyword.get(opts, :base_url)
 
     case ProofStrategySelection.recommend_with_novelty(class, base_url: base_url) do
       {:ok, []} ->
@@ -156,10 +158,20 @@ defmodule Hypatia.Rules.StrategyDrift do
 
   # ── Internals ───────────────────────────────────────────────────────────
 
+  # The attempt ids that failed with `prover` on `class`, or [] when
+  # VeriSimDB is unconfigured, unreachable or returns an unexpected shape.
   defp fetch_failed_attempts(class, prover, opts) do
+    case ServiceUrl.verisim(opts) do
+      {:ok, base_url} -> fetch_failed_attempts_from(base_url, class, prover, opts)
+      {:error, :not_configured} -> []
+    end
+  end
+
+  # Query the verisim-api under `base_url` for the failed attempt ids of
+  # (`class`, `prover`).
+  defp fetch_failed_attempts_from(base_url, class, prover, opts) do
     # ClickHouse query: attempt_ids where outcome='failure' for (class, prover).
     # We query verisim-api's raw SQL endpoint -- if it doesn't exist we return [].
-    base_url = Keyword.get(opts, :base_url, @default_base_url)
     timeout_ms = Keyword.get(opts, :timeout, 5_000)
 
     # Use the /certificates endpoint with evidence_limit to pull failed rows.