[isabelle-dev] NEWS: Isabelle server

Makarius makarius at sketis.net
Thu Mar 22 17:30:15 CET 2018


On 19/03/18 19:35, Makarius wrote:
> *** System ***
> 
> * The command-line tools "isabelle server" and "isabelle client" provide
> access to the Isabelle Server: it supports responsive session management
> and concurrent use of theories, based on Isabelle/PIDE infrastructure.
> See also the "system" manual.
> 
> 
> This refers to Isabelle/465f43a9f780. The chapter in the "system" manual
> provides general explanations, but lacks the description of specific
> server commands: these may be derived from
> src/Pure/Tools/server_commands.scala right now.

I have made further refinements in Isabelle/0b70405b3969. The chapter in
the "system" manual now has almost 20 pages of explanations, including
various examples, see
http://isabelle.in.tum.de/repos/isabelle/file/0b70405b3969/src/Doc/System/Server.thy
or better its LaTeX rendering (e.g. via "isabelle build_doc system &&
isabelle doc system").

The server should already be usable, but the following fine points are
still missing:

  * command "purge_theories" to get rid of results from "use_theories"

  * command "session_status" to provide continuous node_status
information, similar to the Theories dockable in Isabelle/jEdit


> It is only the start of a serious server, many more ideas are still in
> the pipeline, e.g. forwarding over an SSH tunnel that may
> disconnect/reconnect spontaneously.

The SSH tunnel will require more work. It practically needs a way to
send theory files from the client OS context to the server OS context.
(All tools for that are there in Isabelle/Scala, but need to be fit
together in the proper way.)


	Makarius



More information about the isabelle-dev mailing list