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 126.96.36.199; using zlib 188.8.131.52 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"
Description: This is a digitally signed message part.