AtpClient.Isabelle (AtpClient v0.1.4)

Copy Markdown View Source

Client for Isabelle servers, built on top of IsabelleClientMini 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)
# => {: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)
{:ok, result2} = AtpClient.Isabelle.prove_theory(session, theory2)
: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. Any 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, opts \\ [])

Writes theory_text to <local_dir>/<theory_name>.thy, asks the Isabelle server to process it in the given session, and blocks until results are in.

query(theory_text, opts \\ [])

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

Types

result()

@type result() ::
  {:ok, AtpClient.ResultNormalization.atp_result()}
  | {:ok, keyword()}
  | {: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 Isabelle status list, depending on the :raw option;
  • {:error, {:isabelle_failed, payload, status}} when the server reports a terminal failed: message (e.g. a theory file that Isabelle could not load);
  • {:error, {:timeout, status}} when polling did not observe a :finished or :failed message before the deadline, with status being the accumulated poll output so far;
  • other {:error, reason} for connection and I/O issues.

Functions

close_session(session)

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

Stops the session and closes the socket. Any 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 emit a :finished message (default 120_000).

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

@spec prove_theory(AtpClient.Isabelle.Session.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 results are in.

By default the result is interpreted by AtpClient.ResultNormalization.interpret_isabelle_status/1. Pass raw: true to get back the full status keyword list returned by IsabelleClientMini.poll_status/1.

Options

  • :raw — return the raw status list (default false);
  • :use_theories_timeout_ms — overall deadline for polling (default from config, 120_000);
  • :poll_interval_ms — how long to wait between polls (default from config, 500).

query(theory_text, opts \\ [])

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

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