[isabelle-dev] NEWS: Isabelle server

[Christian Sternagel]

Dear Makarius,

I am on 67927:0b70405b3969 and

  ./bin/isabelle build_doc system

doesn't work for me. I get the error:

  Build started for documentation "system"
  Cleaning System ...
  Running System ...
  System FAILED
  ...
  isabelle document -d
/tmp/isabelle-griff/document_output14698640433302927/system -o pdf -n system
  *** Failed to build document in
"/tmp/isabelle-griff/document_output14698640433302927/system"
  Unfinished session(s): System

Is there a way to get a more detailed report on why the last step,
"isabelle document ...",  failed?

Btw: I also get (sometimes more specific) errors for building other
documentation.

Okay, turns out that I was missing the LaTeX packages

  nomencl, regexpatch, subfigure, supertabular

on my system (Fedora 27). After installing those I still get some errors
(all with similar error message):

  Running Tutorial ...
  Tutorial FAILED
  ...
  isabelle document -d
/tmp/isabelle-griff/document_output1759007754075439311/tutorial -o pdf
-n tutorial
  *** Failed to build document in
"/tmp/isabelle-griff/document_output1759007754075439311/tutorial"
  Isar_Ref FAILED
  ...
  Codegen FAILED
  ...
  Prog_Prove FAILED
  ...
  Implementation FAILED
  ...
  Classes FAILED
  ...
  Eisbach FAILED
  ...
  Intro FAILED
  ...
  JEdit FAILED
  ...
  Logics FAILED
  ...
  Logics_ZF FAILED
  ...
  Nitpick FAILED
  ...
  Sledgehammer FAILED
  ...
  System FAILED
  ...
  Typeclass_Hierarchy FAILED

cheers

chris

On 03/22/2018 05:30 PM, Makarius wrote:
> 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>