Need help generating LaTeX document from Isabelle proof

[stefjoosten]

@sjcjoosten, I have prepared a document according to the instructions in the Isabelle manual. I have checked it in on AmpersandTarski/documentation@ac4ae27c84244cf8411d1f337e1af1d301c23492. However, I cannot manage to get a text produced from it. Somehow I fail to make Isabelle generate the sessions.tex file.

Could you give a hand? I wonder where I go wrong.

Here is what I did:

C:>Isabelle2016-1.exe mkroot -d "Joosten APF 2017"

C:>Isabelle2016-1.exe build -D "Joosten APF 2017"

C:>cd "Joosten APF 2017\document"

C:>pdflatex root
This is pdfTeX, Version 3.14159265-2.6-1.40.17 (MiKTeX 2.9 64-bit)
entering extended mode
(root.tex
LaTeX2e <2016/03/31> patch level 3
Babel <3.9r> and hyphenation patterns for 75 language(s) loaded.
("D:\Program Files\MiKTeX 2.9\tex\latex\base\article.cls"
Document Class: article 2014/09/29 v1.4h Standard LaTeX document class
("D:\Program Files\MiKTeX 2.9\tex\latex\base\size11.clo")) (isabelle.sty
(comm
           ... (LaTeX log made shorter by Stef)
LaTeX Warning: Citation `vdWoude2011' on page 1 undefined on input line 40.

LaTeX Warning: Citation `Nipkow2002' on page 1 undefined on input line 44.

! LaTeX Error: File `session.tex' not found.

Type X to quit or <RETURN> to proceed,
or enter new name. (Default extension: tex)

Enter file name:

[sjcjoosten]

C:>Isabelle2016-1.exe build -D "Joosten APF 2017" should work now (creates a directory called 'output' that contains the document). If it does not, please try the following and paste the output: C:>Isabelle2016-1.exe build -D "Joosten APF 2017" -v PS: I had to ask my colleagues for help here: I had no idea that I needed to set an output directory and could only find something about this in the manual after being told the fix.

[stefjoosten]

It still doesn't work on my end. Whatever I try, nothing works. I feel very helpless. Can we skype about this?

I have moved the stuff (including your changes) to a new repo. You will find it in AmpersandTarski/Publications@9e380adca240930c0adcb5b3079a2ac4d2d4700b

[sjcjoosten]

Let's also use the ticket tracker of the Publications repo then, and please let me know the output of

Isabelle2016-1.exe build -D "Joosten APF 2017" -v

[WolframKahl]

Isabelle2016-1.exe build -D "Joosten APF 2017" -v

And in doubt, use file names not containing spaces or special characters.