The runtime's Isabelle server and its logic sessions.
The server is started on the first check and each logic session ("HOL", …)
on the first check that names it. Both live as long as this process: a
watchdog kills the server when this process or the whole VM exits. If the
connection dies, this process exits and its supervisor restarts it, so the
next check starts afresh.
The last result per theory file is cached and returned while the source and logic session are unchanged.
Summary
Functions
Returns a specification to start this module under a supervisor.
Writes and checks theory in the logic session logic.
Functions
Returns a specification to start this module under a supervisor.
See Supervisor.
Writes and checks theory in the logic session logic.
Returns the raw use_theories result, or the failed task's result when
Isabelle rejects the theory header.