AtpClient.Isabelle (AtpClient v0.2.0)

Copy Markdown View Source

Client for Isabelle servers, built on top of IsabelleClient from the :isabelle_elixir package.

The Isabelle server cannot accept theory text over the wire — theories have to live as .thy files on a filesystem that both the BEAM node running AtpClient and the Isabelle server can see. This module handles the file bookkeeping for you: you pass the theory body as a string, and it is written into a configured shared directory before use_theories is invoked.

Configuration

config :atp_client, :isabelle,
  host: "isabelle.example.org",
  port: 9999,
  password: System.get_env("ISABELLE_PASSWORD"),
  # Where AtpClient writes .thy files (as seen by this BEAM node):
  local_dir: "/shared/problems",
  # Where those same files appear on the Isabelle side (may differ in
  # containerised setups; defaults to `local_dir` when unset):
  isabelle_dir: "/shared/problems",
  session: "HOL"

Paths: local_dir vs. isabelle_dir

The Isabelle server wants a filesystem path it can resolve in its own view of the world. When the BEAM and the Isabelle server see the same directory under the same path, only local_dir is needed — this module expands it to an absolute path and passes it to Isabelle as master_dir.

When the two views differ, you must set isabelle_dir explicitly. The two common cases:

  • Containers: BEAM writes to /shared/problems inside its container; the Isabelle server container has the same volume mounted at /data/problems. Set local_dir: "/shared/problems" and isabelle_dir: "/data/problems".
  • Windows + Cygwin: BEAM on Windows sees C:/Users/you/thy; Isabelle started from a Cygwin shell sees the same directory as /cygdrive/c/Users/you/thy. Set both accordingly.

Paths given via isabelle_dir are passed through verbatim — the library does not try to translate Windows paths to POSIX or vice-versa.

Example

theory = ~S"""
theory Example imports Main begin
lemma "P \<or> \<not> P" by auto
end
"""

{:ok, result} = AtpClient.Isabelle.query(theory, "Example")
# => {:ok, :thm}

For fine-grained workflows, open a session once and reuse it:

{:ok, session} = AtpClient.Isabelle.open_session()
{:ok, result1} = AtpClient.Isabelle.prove_theory(session, theory1, "T1")
{:ok, result2} = AtpClient.Isabelle.prove_theory(session, theory2, "T2")
:ok = AtpClient.Isabelle.close_session(session)

Summary

Types

result()

The result of a call to prove_theory/4 or query/3

Functions

close_session(session)

Stops the session and closes the socket. Errors from the server-side session_stop are swallowed, since the socket is torn down regardless.

open_session(opts \\ [])

Connects to the Isabelle server, starts a session (typically HOL or Main), and returns a Session handle. The caller is responsible for eventually passing the handle to close_session/1.

prove_theory(session, theory_text, theory_name, opts \\ [])

Writes theory_text to <local_dir>/<theory_name>.thy, asks the Isabelle server to process it in the given session, and blocks until the task finishes or fails.

query(theory_text, theory_name, opts \\ [])

Convenience wrapper: opens a session, calls prove_theory/4, and unconditionally closes the session afterwards (even on error).

Types

result()

@type result() ::
  {:ok, AtpClient.ResultNormalization.atp_result()}
  | {:ok, map()}
  | {:error, term()}

The result of a call to prove_theory/4 or query/3:

  • {:ok, result} where result is either the normalized ATP result or the raw use_theories payload (a map with "nodes", "errors", "ok", …), depending on the :raw option;
  • {:error, {:isabelle_failed, payload, notes}} when the server reports a FAILED message for the task (e.g. a theory file that Isabelle could not load). notes is the list of intermediate NOTE payloads accumulated by IsabelleClient.Task before the failure;
  • {:error, {:isabelle_failed, payload, hints}} — same shape, but with hints carrying diagnostic suggestions and the local_dir / isabelle_dir actually used. Currently emitted when the server reports "Cannot load theory file";
  • other {:error, reason} for connection, session-start, and I/O issues.

Functions

close_session(session)

@spec close_session(AtpClient.Isabelle.Session.t()) :: :ok

Stops the session and closes the socket. Errors from the server-side session_stop are swallowed, since the socket is torn down regardless.

open_session(opts \\ [])

@spec open_session(keyword()) ::
  {:ok, AtpClient.Isabelle.Session.t()} | {:error, term()}

Connects to the Isabelle server, starts a session (typically HOL or Main), and returns a Session handle. The caller is responsible for eventually passing the handle to close_session/1.

Options

  • :host, :port, :password — override config;
  • :session — name of the Isabelle session to start (default from config, typically "HOL");
  • :session_start_timeout_ms — how long to wait for the initial session_start to complete (default 120_000).

prove_theory(session, theory_text, theory_name, opts \\ [])

@spec prove_theory(AtpClient.Isabelle.Session.t(), String.t(), String.t(), keyword()) ::
  result()

Writes theory_text to <local_dir>/<theory_name>.thy, asks the Isabelle server to process it in the given session, and blocks until the task finishes or fails.

By default the result is interpreted by AtpClient.ResultNormalization.interpret_isabelle_result/1. Pass raw: true to get back the full use_theories payload (a map with "nodes", "ok", "errors", …) returned by the Isabelle server.

Options

  • :raw — return the raw payload map (default false);
  • :use_theories_timeout_ms — overall deadline for the task (default from config, 120_000).

query(theory_text, theory_name, opts \\ [])

@spec query(String.t(), String.t(), keyword()) :: result()

Convenience wrapper: opens a session, calls prove_theory/4, and unconditionally closes the session afterwards (even on error).