Re: [isabelle-dev] NEWS: Isabelle server
Just for the record: Makarius' reply resolved the issue for me (see also below). On 05/09/2018 11:57 PM, Makarius wrote: > On 26/03/18 13:48, Christian Sternagel wrote: >> >> Thanks, I forgot about that option. >> >> With "isabelle latex" in the specified directory the error boils down to: >> >> ./root.tex:31: Package pdftex.def Error: File >> `isabelle-eps-converted-to.pdf' n >> ot found. >> >> See the pdftex.def package documentation for explanation. >> Type H for immediate help. >> ... >> >> Should isabelle-eps-converted-to.pdf exist on my system? > > I guess that the "epstopdf" tool is missing: there should be some Fedora > package for it. That is correct. Thanks for pointing it out, it was not clear to me from the error message. > > Anyway, in Isabelle/2a5ae592eafb the latex errors are again spilled into > user output -- this is required for hard errors of missing executables > and style files. > > With that I have managed to do "isabelle build -o document=pdf -g doc" > or "isabelle build_doc -a" sucessfully on Fedora 28: after cumbersome > saturation of the texlive installation, where almost every style file > has its own package. This kind of saturation is indeed cumbersome, but at least its possible as long as you know which packages are missing ;) cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle server
On 26/03/18 13:48, Christian Sternagel wrote: > > Thanks, I forgot about that option. > > With "isabelle latex" in the specified directory the error boils down to: > > ./root.tex:31: Package pdftex.def Error: File > `isabelle-eps-converted-to.pdf' n > ot found. > > See the pdftex.def package documentation for explanation. > Type H for immediate help. > ... > > Should isabelle-eps-converted-to.pdf exist on my system? I guess that the "epstopdf" tool is missing: there should be some Fedora package for it. Anyway, in Isabelle/2a5ae592eafb the latex errors are again spilled into user output -- this is required for hard errors of missing executables and style files. With that I have managed to do "isabelle build -o document=pdf -g doc" or "isabelle build_doc -a" sucessfully on Fedora 28: after cumbersome saturation of the texlive installation, where almost every style file has its own package. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle server
Dear Makarius, Thanks, I forgot about that option. With "isabelle latex" in the specified directory the error boils down to: ./root.tex:31: Package pdftex.def Error: File `isabelle-eps-converted-to.pdf' n ot found. See the pdftex.def package documentation for explanation. Type H for immediate help. ... Should isabelle-eps-converted-to.pdf exist on my system? cheers chris On 03/26/2018 01:26 PM, Makarius wrote: > On 26/03/18 09:33, Christian Sternagel wrote: >> >> I don't see a significant difference in output between my original >> >> isabelle build_doc system > >> *** Failed to build document in >> "/tmp/isabelle-griff/document_output1585848392449927242/system" >> >> and the suggested >> >> isabelle build -c -b System -o document=pdf -o document_output=output >> >> *** Failed to build document in >> "/home/griff/repos/tools/isabelle/src/Doc/System/output/system" >> >> I am still unclear on why "isabelle document" fails in both cases. > > The difference is the output directory. In the latter situation, you can > go there and inspect root.log or run pdflatex root manually. > > > Makarius > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle server
On 26/03/18 09:33, Christian Sternagel wrote: > > I don't see a significant difference in output between my original > > isabelle build_doc system > *** Failed to build document in > "/tmp/isabelle-griff/document_output1585848392449927242/system" > > and the suggested > > isabelle build -c -b System -o document=pdf -o document_output=output > > *** Failed to build document in > "/home/griff/repos/tools/isabelle/src/Doc/System/output/system" > > I am still unclear on why "isabelle document" fails in both cases. The difference is the output directory. In the latter situation, you can go there and inspect root.log or run pdflatex root manually. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle server
Dear Makarius, I don't see a significant difference in output between my original isabelle build_doc system where I get ... isabelle document -d /tmp/isabelle-griff/document_output1585848392449927242/system -o pdf -n system *** Failed to build document in "/tmp/isabelle-griff/document_output1585848392449927242/system" and the suggested isabelle build -c -b System -o document=pdf -o document_output=output where I get ... isabelle document -d output/system -o pdf -n system *** Failed to build document in "/home/griff/repos/tools/isabelle/src/Doc/System/output/system" I am still unclear on why "isabelle document" fails in both cases. cheers chris PS: Anyway, I can get the manual from the URL you provided. Thanks! On 03/23/2018 11:51 AM, Makarius wrote: > On 23/03/18 10:29, Christian Sternagel wrote: >> >> 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): > > You can build all docs with detailed results like this: > > isabelle build -c -g doc -o document=pdf -o document_output=output > > > For the purpose of the updated system manual, you can now download the > nightly snapshot: https://isabelle.sketis.net/devel/release_snapshot > > > Makarius > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle server
On 23/03/18 10:29, Christian Sternagel wrote: > > 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): You can build all docs with detailed results like this: isabelle build -c -g doc -o document=pdf -o document_output=output For the purpose of the updated system manual, you can now download the nightly snapshot: https://isabelle.sketis.net/devel/release_snapshot Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle server
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
Re: [isabelle-dev] NEWS: Isabelle server
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
