# `AtpClient.Isabelle`
[🔗](https://github.com/jcschuster/AtpClient/blob/v0.1.3/lib/atp_client/isabelle.ex#L1)

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, "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)

# `result`

```elixir
@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.

# `close_session`

```elixir
@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`

```elixir
@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`

```elixir
@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 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`

```elixir
@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).

---

*Consult [api-reference.md](api-reference.md) for complete listing*