Email Gateway (Aug 18 2022 at 11:31): Email Gateway (Aug 18 2022 at 11:31):From: Peter Chapman <pc@cs.st-and.ac.uk>
Hi
I'm getting Isabelle to build and produce a pdf. It works, after a
fashion, and I get a document produced that is called root.pdf.
However, I cannot get the references to print out at all. I have
followed the instructions in the Isabelle manual and have placed all
of the files in the correct places, but still it does not print them
out. I also get the error message
Running HOL-Nominal-CraigND ...
Browser info at /Users/pc/isabelle/browser_info/HOL/HOL-Nominal/CraigND
HOL-Nominal-CraigND FAILED
(see also /Users/pc/isabelle/heaps/Isabelle2007/polyml-5.1_x86-darwin/
log/HOL-No
minal-CraigND)
exmf-dist/fonts/type1/bluesky/cm/cmr9.pfb></usr/local/texlive/2007/
texmf-dist/f
onts/type1/bluesky/cm/cmsy10.pfb></usr/local/texlive/2007/texmf-dist/
fonts/type
1/bluesky/cm/cmsy5.pfb></usr/local/texlive/2007/texmf-dist/fonts/type1/
bluesky/
cm/cmsy7.pfb></usr/local/texlive/2007/texmf-dist/fonts/type1/bluesky/
cm/cmsy8.p
fb></usr/local/texlive/2007/texmf-dist/fonts/type1/bluesky/cm/
cmsy9.pfb></usr/l
ocal/texlive/2007/texmf-dist/fonts/type1/bluesky/cm/cmti10.pfb>
Output written on root.pdf (15 pages, 162580 bytes).
Transcript written on root.log.
Document preparation failure in directory '/Users/pc/isabelle/
browser_info/HOL/H
OL-Nominal/CraigND/document'
*** No document: "/Users/pc/isabelle/browser_info/HOL/HOL-Nominal/
CraigND/docume
nt.pdf"
make: *** [/Users/pc/isabelle/heaps/Isabelle2007/polyml-5.1_x86-darwin/
log/HOL-N
ominal-CraigND.gz] Error 1
In the log file (root.log) it tells me that there were lots of
undefined citations. Usually in LaTeX you have to run things a couple
of times to get references to work properly, and once as a BibTeX
build. Is there any way to do this using Isabelle? Does anyone know
how to make my references appear properly?
Thanks
Peter
Email Gateway (Aug 18 2022 at 11:31):From: Makarius <makarius@sketis.net>
The Isabelle document tool takes care of running the proper number of
times to get references right. How exactly did you invoke the document
preparation session?
Makarius
Last updated: Nov 21 2024 at 12:39 UTC