Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Using Isabelle to generate a pdf

view this post on Zulip Email Gateway (Aug 18 2022 at 10:58):

From: Peter Chapman <pc@cs.st-and.ac.uk>
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

view this post on Zulip Email Gateway (Aug 18 2022 at 10:58):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
This seems to indicate that there is no accessible 'pdflatex'. Can you
figure out what happens if you just type 'pdflatex --help' on you shell?

Florian
florian.haftmann.vcf
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 10:58):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
[...]

Do you know where I might be able to find this file, pdflatex?

It seems that your 'pdflatexc' is exactly what Isabelle wants to find as
'pdflatex'; so, it might be sufficient to place a symlink named
'pdflatex', pointing to you 'pdflatexc', in one of the directories
listed in $PATH.

Hope this helps
Florian
florian.haftmann.vcf
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 10:59):

From: Nauman <recluze@gmail.com>

Message: 1
Date: Thu, 8 Nov 2007 14:28:18 +0000
From: Peter Chapman <pc@cs.st-and.ac.uk>
Subject: [isabelle] Using Isabelle to generate a pdf
To: isabelle-users@cl.cam.ac.uk
Message-ID: <67A5CA91-87CB-47FE-903B-2B64749B673F@cs.st-and.ac.uk>
Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed

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*

There's your problem. TeXShop is probably using absolute paths. Isatool
requires pdflatex to be in your $PATH. Try creating a symbolic link to
pdflatex in /usr/bin and it should work.

Document preparation failure in directory '/Users/pc/isabelle/

browser_info/HOL/Nominal/document'
*** No document: "/Users/pc/isabelle/browser_info/HOL/Nominal/
document.pdf"

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

Cheers,
Nauman ...

Blog: http://recluze.wordpress.com
Group: http://securityengineering.wordpress.com
Art gallery: http://recluse.gfxartist.com
Cell: 0321 90 66 275

Last updated: May 03 2024 at 08:18 UTC