ShotTx.IsabelleBridge (ShotTx v0.0.1)

Copy Markdown View Source

Application-level singleton that owns a warm Isabelle connection.

Isabelle's cold start (server + HOL-Main load) is 30–60 s on modest hardware — the single heaviest cost in the ShotTx pipeline. Paying it once per session would dominate proof time, so this bridge holds one long-lived IsabelleClient.Shared GenServer and lets every ShotTx.Prover.ModelAgent.Backend.Nitpick probe borrow it through probe/2 / await/2.

Activation is opt-in via application config:

config :shot_tx, isabelle_backend: :nitpick

When unset (or :none), the bridge starts and stays in :inactive state — no server is spawned, no dependency is loaded, and every probe returns :unknown. That is the default in test and dev.

Concurrency

IsabelleClient.Shared demultiplexes many concurrent callers over one TCP socket, routing async task replies back by task id. Each probe runs in a short-lived Task that blocks on Shared.check_text/5, so N callers get N concurrent Isabelle tasks. Nitpick execution itself is bounded by Isabelle's own thread pool.

Lifecycle

The bridge traps exits. On termination it stops the Shared client, which in turn closes the TCP socket and kills the Isabelle server process — preventing the orphan JVM + polyml processes that would otherwise survive a bridge crash.

Summary

Types

status()

Functions

await(ref, timeout_ms)

Blocks up to timeout_ms for a verdict.

child_spec(init_arg)

Returns a specification to start this module under a supervisor.

probe(theory_body, opts \\ [])

Submits an Isar theory body plus a nitpick invocation. Returns an opaque reference the caller later hands to await/2. When the bridge is :inactive, this delivers :unknown immediately.

start_link(opts \\ [])
status()

Reports the current bridge status.

Types

status()

@type status() :: :inactive | :starting | :ready | :failed

Functions

await(ref, timeout_ms)

@spec await(ShotTx.Prover.ModelAgent.Backend.ref(), pos_integer()) ::
  ShotTx.Prover.ModelAgent.Backend.verdict()

Blocks up to timeout_ms for a verdict.

child_spec(init_arg)

Returns a specification to start this module under a supervisor.

See Supervisor.

probe(theory_body, opts \\ [])

@spec probe(
  String.t(),
  keyword()
) :: {:ok, ShotTx.Prover.ModelAgent.Backend.ref()} | {:error, term()}

Submits an Isar theory body plus a nitpick invocation. Returns an opaque reference the caller later hands to await/2. When the bridge is :inactive, this delivers :unknown immediately.

start_link(opts \\ [])

status()

@spec status() :: status()

Reports the current bridge status.