IsabelleClient (isabelle_elixir v0.3.0)
View SourceDefault stateful Isabelle client.
Use %IsabelleClient{} for scripts and LiveBooks that benefit from a session
stack in a struct. The active session is the top of client.sessions. It is
not meant to be shared by multiple concurrent processes; use
IsabelleClient.Shared for that. Use IsabelleClient.Raw for protocol-level
socket control.
Summary
Functions
Returns the active session from the top of the client's session stack.
Builds an Isabelle session image and waits for the async task result.
Checks an existing .thy file.
Writes and checks a theory.
Closes the client's TCP socket.
Runs a synchronous Isabelle command, normalizing Elixir keyword arguments to JSON keys.
Connects to an Isabelle server and returns a stateful client struct.
Returns diagnostic messages from a task, result map, or task notes.
Round-trips a JSON value through Isabelle's echo command.
Returns error messages from a task or result map, with optional position filters.
Returns typed exports from all theory nodes in a use_theories result.
Extracts the session_id from a session struct, session-start task, or result map.
Removes a session from the local client stack without contacting Isabelle.
Returns the server command names supported by Isabelle.
Returns user-facing message strings from a task, result map, or task notes.
Finds a typed theory node by node_name or theory_name.
Returns typed theory nodes from a use_theories result.
Purges theories from a session.
Decodes a session_build result or task into a %IsabelleClient.Result.SessionBuildResult{}.
Returns the client's session stack, newest session first.
Asks the connected Isabelle server process to shut down.
Starts a local resident Isabelle server.
Starts an Isabelle session and pushes it onto client.sessions.
Returns typed top-level error messages from a use_theories result.
Checks theories and waits for the task result.
Decodes a use_theories result or task into a %IsabelleClient.Result.UseTheoriesResult{}.
Returns warning messages from a task or result map, with optional position filters.
Types
@type t() :: %IsabelleClient{ server_name: String.t() | nil, sessions: [IsabelleClient.Session.t()], socket: port() }
Stateful client with one socket and a local stack of Isabelle sessions.
Functions
Returns the active session from the top of the client's session stack.
Builds an Isabelle session image and waits for the async task result.
args is forwarded to Isabelle's session_build command after key
normalization. Typical keys are :session, :dirs, :options,
:include_sessions, :preferences, and :verbose.
Checks an existing .thy file.
By default this uses the active client session. Pass "session_id" or
:session_id in the arguments to use another server session explicitly.
master_dir and theories are derived from path unless supplied.
Writes and checks a theory.
If text is not a complete theory, it is written as:
theory <name> imports Main begin
<text>
endUse opts[:imports] to replace Main. The provided text starts on line 2 of
the written file, so Isabelle diagnostics line up as text_line + 1. By
default this uses the active client session. Isabelle offsets remain
whole-file symbol offsets: with default Main, the snippet starts after
27 + String.length(theory) symbols from the generated header and newline.
Pass "session_id" or :session_id in the options to use another server
session explicitly.
Closes the client's TCP socket.
Runs a synchronous Isabelle command, normalizing Elixir keyword arguments to JSON keys.
Connects to an Isabelle server and returns a stateful client struct.
Pass a %IsabelleClient.Server.Info{} returned by start_server/1, or pass
the server password with explicit :host and :port options for an already
running local or remote server.
Returns diagnostic messages from a task, result map, or task notes.
Round-trips a JSON value through Isabelle's echo command.
Returns error messages from a task or result map, with optional position filters.
Returns typed exports from all theory nodes in a use_theories result.
Extracts the session_id from a session struct, session-start task, or result map.
Removes a session from the local client stack without contacting Isabelle.
Use this when a session was stopped elsewhere, or when Isabelle reports
No session ... for an id still remembered by this client.
Returns the server command names supported by Isabelle.
Returns user-facing message strings from a task, result map, or task notes.
Finds a typed theory node by node_name or theory_name.
Returns typed theory nodes from a use_theories result.
Purges theories from a session.
By default this uses the active client session. Pass "session_id" or
:session_id in the arguments to purge theories from another server session.
This is a synchronous Isabelle command.
Decodes a session_build result or task into a %IsabelleClient.Result.SessionBuildResult{}.
Returns the client's session stack, newest session first.
Asks the connected Isabelle server process to shut down.
Starts a local resident Isabelle server.
Options:
:server_name- resident server name, defaults to a unique name:server_port- resident server port, defaults to0
Starts an Isabelle session and pushes it onto client.sessions.
The argument list or map is forwarded to Isabelle's session_start command,
which accepts session_build arguments (:session, :preferences,
:options, :dirs, :include_sessions, :verbose) plus :print_mode.
Pass :label to store a local label in the resulting session struct. Labels
are not sent to Isabelle. Returns {:ok, client, task}.
Stops a session.
With the default arguments, this stops the active session and pops it from
the client's session stack. Pass a %IsabelleClient.Session{} or session id
to stop another server session explicitly.
Returns typed top-level error messages from a use_theories result.
Checks theories and waits for the task result.
By default this uses the active client session. Pass "session_id" or
:session_id in the arguments to use another server session explicitly.
Isabelle use_theories arguments are forwarded after key normalization:
:session_id, :theories, :master_dir, :pretty_margin,
:unicode_symbols, :export_pattern, :check_delay, :check_limit,
:watchdog_timeout, and :nodes_status_delay.
Returns {:ok, task} for a finished Isabelle task, or {:error, task} when
Isabelle reports task failure.
Decodes a use_theories result or task into a %IsabelleClient.Result.UseTheoriesResult{}.
Returns warning messages from a task or result map, with optional position filters.