KinoAtpClient.IsabelleRuntime (KinoAtpClient v0.2.0)

Copy Markdown View Source

Lazy singleton that auto-manages a local Isabelle server + HOL session for the Smart Cell's Isabelle backend, mirroring the workflow demonstrated in the isabelle_elixir livebooks: spawn a local server, open one session, load the bundled TPTP.thy, and re-use both across calls.

Compared with AtpClient.Isabelle.query_tptp/2, this:

  • needs zero configuration when the isabelle executable is on PATH (or ISABELLE_TOOL is set) — no :password, no :local_dir, no :isabelle_dir;
  • persists the server + session for the lifetime of the BEAM node, so the ~30 s HOL start-up only happens on the first solve click;
  • writes theory files into the session's own tmp_dir rather than a configured shared directory, so the BEAM and the Isabelle server always agree on where the theory lives.

The runtime is started as a permanent child of the package's application supervision tree but stays idle until the first query_tptp/2 call — no Isabelle process is spawned just by loading the package.

Summary

Functions

available?()

Returns :ok if a local Isabelle executable is reachable on this machine.

child_spec(init_arg)

Returns a specification to start this module under a supervisor.

query_tptp(problem, opts \\ [])

Checks a TPTP/THF problem against the auto-managed local Isabelle session and returns the per-lemma classification.

reset()

Stops the running session (if any) and tears down the local server.

start_link(opts \\ [])

Starts the runtime supervisor child. Does not spawn Isabelle yet.

Functions

available?()

@spec available?() :: :ok | {:error, term()}

Returns :ok if a local Isabelle executable is reachable on this machine.

Probes ISABELLE_TOOL and then PATH; does not spawn anything.

child_spec(init_arg)

Returns a specification to start this module under a supervisor.

See Supervisor.

query_tptp(problem, opts \\ [])

@spec query_tptp(
  String.t(),
  keyword()
) :: {:ok, [AtpClient.ResultNormalization.lemma_result()]} | {:error, term()}

Checks a TPTP/THF problem against the auto-managed local Isabelle session and returns the per-lemma classification.

opts:

  • :proof_method — Isabelle tactic appended after each generated lemma (default "by auto").

Returns {:ok, [%{line:, name:, result:}]} on success or {:error, reason} if Isabelle is unavailable, the TPTP fragment failed to parse, or the server reported a task failure.

reset()

Stops the running session (if any) and tears down the local server.

Useful for tests; not strictly necessary in production since the runtime is terminated when the application shuts down.

start_link(opts \\ [])

Starts the runtime supervisor child. Does not spawn Isabelle yet.