Re: [isabelle] Using Isabelle to generate a pdf



>
>
> Message: 1
> Date: Thu, 8 Nov 2007 14:28:18 +0000
> From: Peter Chapman <pc at cs.st-and.ac.uk>
> Subject: [isabelle] Using Isabelle to generate a pdf
> To: isabelle-users at cl.cam.ac.uk
> Message-ID: <67A5CA91-87CB-47FE-903B-2B64749B673F at 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




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