[isabelle] Document preparation



I'm trying to get Isabelle 2008's document preparation to work. I can't even 
get the dry run to work, as described in section 4.2.1 of the tutorial. I've 
attached the output when I run those commands, as well as the output of 
pdflatex -version. I've also attached the log mentioned in the output of 
isatool make. Can anyone make sense of it? It mentions that it can't find 
comment.sty; where should I expect to find this?

Tim
<><
tim at jemimah:~$ isatool mkdir HOL MySession 
Preparing session "MySession" ...          
creating ./IsaMakefile                     
creating ./MySession/ROOT.ML               
creating ./MySession/document              
creating ./MySession/document/root.tex     

Notes:

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

  * ./IsaMakefile contains compilation options and file dependencies

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

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

tim at jemimah:~$ isatool make
Running HOL-MySession ...  
Browser info at /home/tim/isabelle/browser_info/HOL/MySession
HOL-MySession FAILED                                         
(see also /home/tim/isabelle/heaps/Isabelle2008/polyml-5.2_x86-linux/log/HOL-MySession)

Enter file name: 
! Emergency stop.
<read *>         
                 
l.198 \let       
          \fmtname\isafmtname^^M
!  ==> Fatal error occurred, no output PDF file produced!
Transcript written on root.log.                          
Document preparation failure in directory '/home/tim/isabelle/browser_info/HOL/MySession/document'
*** No document: "/home/tim/isabelle/browser_info/HOL/MySession/document.pdf"                     

make: *** [/home/tim/isabelle/heaps/Isabelle2008/polyml-5.2_x86-linux/log/HOL-MySession.gz] Error 1
tim at jemimah:~$ pdflatex -version
pdfTeX using libpoppler 3.141592-1.40.3-2.2 (Web2C 7.5.6)
kpathsea version 3.5.6                                   
Copyright 2007 Peter Breitenlohner (eTeX)/Han The Thanh (pdfTeX).
Kpathsea is copyright 2007 Karl Berry and Olaf Weber.
There is NO warranty.  Redistribution of this software is
covered by the terms of both the pdfTeX using libpoppler copyright and
the Lesser GNU General Public License.
For more information about these matters, see the file
named COPYING and the pdfTeX using libpoppler source.
Primary author of pdfTeX using libpoppler: Peter Breitenlohner (eTeX)/Han The Thanh (pdfTeX).
Kpathsea written by Karl Berry, Olaf Weber, and others.

Compiled with libpng 1.2.27; using libpng 1.2.27
Compiled with zlib 1.2.3.3; using zlib 1.2.3.3
Compiled with libpoppler version 3.00

> val it = () : unit
val commit = fn : unit -> bool

### Browser info: cannot access session index of "/home/tim/isabelle/browser_info/HOL"
"$ISATOOL" document -c -o 'pdf' -n 'document' -t '' '/home/tim/isabelle/browser_info/HOL/MySession/document' 2>&1
This is pdfTeXk, Version 3.141592-1.40.3 (Web2C 7.5.6)
 %&-line parsing enabled.
entering extended mode
LaTeX2e <2005/12/01>
Babel <v3.8h> and hyphenation patterns for english, usenglishmax, dumylang, noh
yphenation, loaded.

(./root.tex (/usr/share/texmf-texlive/tex/latex/base/article.cls
Document Class: article 2005/09/16 v1.4f Standard LaTeX document class
(/usr/share/texmf-texlive/tex/latex/base/size11.clo)) (./isabelle.sty

! LaTeX Error: File `comment.sty' not found.

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

Enter file name: 
! Emergency stop.
<read *> 
         
l.198 \let
          \fmtname\isafmtname^^M
!  ==> Fatal error occurred, no output PDF file produced!
Transcript written on root.log.
Document preparation failure in directory '/home/tim/isabelle/browser_info/HOL/MySession/document'
*** No document: "/home/tim/isabelle/browser_info/HOL/MySession/document.pdf"

Attachment: signature.asc
Description: This is a digitally signed message part.



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