[isabelle] Using Isabelle to generate a pdf



Hi

I'm trying to create a pdf file from within Isabelle, as described in the tutorial section 4.2 (Document Preparation). I have ran

isatool mkdir HOL Nominal

[dyn-195-171:~] pc% ../../usr/local/bin/isatool mkdir HOL Nominal
Preparing session "Nominal" ...
creating ./IsaMakefile
keeping ./Nominal/ROOT.ML
keeping ./Nominal/document

Notes:

* 'isatool make' processes the session (including document preparation)

  * ./IsaMakefile contains compilation options and file dependencies

* ./Nominal/document/root.tex contains the LaTeX master document setup

  * ./Nominal/ROOT.ML needs to contain ML code to load all theories

which creates the appropriate folder and some other stuff, as specified in the notes. Then, when I run the second part

isatool make

I get the following error messages

[dyn-195-171:~] pc% ../../usr/local/bin/isatool make
Running HOL-Nominal ...
Browser info at /Users/pc/isabelle/browser_info/HOL/Nominal
HOL-Nominal FAILED
(see also /Users/pc/isabelle/heaps/Isabelle_12-Oct-2007/ polyml-5.0_ppc-darwin/log/HOL-Nominal)


### Browser info: cannot access session index of "/Users/pc/isabelle/ browser_info/HOL" "$ISATOOL" document -c -o 'pdf' -n 'document' -t '' '/Users/pc/ isabelle/browser_info/HOL/Nominal/document' 2>&1 /usr/local/Isabelle1/lib/Tools/latex: line 79: pdflatex: command not found Document preparation failure in directory '/Users/pc/isabelle/ browser_info/HOL/Nominal/document' *** No document: "/Users/pc/isabelle/browser_info/HOL/Nominal/ document.pdf"

make: *** [/Users/pc/isabelle/heaps/Isabelle_12-Oct-2007/ polyml-5.0_ppc-darwin/log/HOL-Nominal.gz] Error 1

The tutorial says that "any failure at this stage usually indicates technical problems of the LaTeX installation". I use TeXshop, so everything was installed automatically. Does anyone know what the problem is?

Thanks

Peter








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.