IsabelleClient.Shared (isabelle_elixir v0.3.0)
View SourceGenServer-backed Isabelle client.
The process owns command ordering and routes Isabelle async task messages by task id, so multiple callers can wait on concurrent Isabelle tasks safely.
Summary
Functions
Builds an Isabelle session image and waits for the task result.
Checks an existing .thy file.
Writes and checks a theory.
Returns a specification to start this module under a supervisor.
Stops the client process and closes its socket.
Runs a synchronous Isabelle command through the client process.
Alias for start_link/1.
Round-trips a JSON value through Isabelle's echo command.
Returns the server command names supported by Isabelle.
Purges theories from a session.
Asks the Isabelle server process to shut down.
Starts a GenServer-backed Isabelle client.
Starts an Isabelle session and stores it in the client process.
Stops the active Isabelle session.
Stops an explicit Isabelle session id or %IsabelleClient.Session{}.
Checks theories and waits for the task result.
Functions
Builds an Isabelle session image and waits for the task result.
Options:
:on_event- called with%{type: type, task: id, body: body}for:started,:note,:finished, and:failedtask events
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. Accepts
the same async task options as build_session/4.
Writes and checks a theory.
If text is not a complete theory, it is written as a theory importing
Main with the provided text starting on line 2 of the file. By default this
uses the active client session. Isabelle offsets are whole-file symbol offsets,
so the generated header contributes to reported offsets. Pass "session_id"
or :session_id in the options to use another server session explicitly.
Returns a specification to start this module under a supervisor.
See Supervisor.
Stops the client process and closes its socket.
Runs a synchronous Isabelle command through the client process.
Alias for start_link/1.
Round-trips a JSON value through Isabelle's echo command.
Returns the server command names supported by Isabelle.
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.
Asks the Isabelle server process to shut down.
Starts a GenServer-backed Isabelle client.
Pass :password, :host, and :port to connect to an existing Isabelle
server. Without :password, a local server is started. Pass :session to
start an initial session.
Starts an Isabelle session and stores it in the client process.
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.
Accepts the same async task options as build_session/4.
Stops the active Isabelle session.
Returns {:ok, task} or {:error, task} and removes the stopped session from
the local client stack. Accepts the same async task options as
build_session/4.
Stops an explicit Isabelle session id or %IsabelleClient.Session{}.
Stopping a non-active session removes it from the local stack without changing the active session.
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.
Accepts the same async task options as build_session/4.