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-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev