Email Gateway (Aug 19 2022 at 17:14): Email Gateway (Aug 19 2022 at 17:14):From: Bob Fang <bf283@cam.ac.uk>
Hi all,
I want to generate readable PDF file from a theory file and that’s what I
did:
Put the .thy file in a folder and run Isabelle mkroot to get the
following files:
.
├── Whatever.thy
├── ROOT
├── document
│ └── root.tex
├── output
│ ├── document
│ │ ├── FunArray_ex.tex
│ │ ├── comment.sty
│ │ ├── isabelle.sty
│ │ ├── isabellesym.sty
│ │ ├── isabelletags.sty
│ │ ├── pdfsetup.sty
│ │ ├── railsetup.sty
│ │ ├── root.aux
│ │ ├── root.log
│ │ ├── root.out
│ │ ├── root.pdf
│ │ ├── root.tex
│ │ ├── root.toc
│ │ └── session.tex
│ └── document.pdf
└── root.log
Modify the ROOT to something look like this:
session "FuncArray" = "HOL" +
options [document = pdf, document_output = "output"]
theories [document = false]
(* Foo *)
(* Bar *)
theories
Whatever <—————— Note here I added this
(* Baz *)
document_files
"root.tex"
Running Whatever ...
Whatever FAILED
(see also …)
*** LaTeX Warning: There were undefined references.
*** )
*** (see the transcript file for additional information)</usr/local/
texlive/2014/te
*** xmf-dist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/
local/texlive/2014/tex
*** mf-dist/fonts/type1/public/amsfonts/cm/cmbx12.pfb></usr/
local/texlive/2014/texm
*** f-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/
local/texlive/2014/texmf
*** -dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/
local/texlive/2014/texmf-d
*** ist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/
local/texlive/2014/texmf-dis
*** t/fonts/type1/public/amsfonts/cm/cmr17.pfb></usr/local/
texlive/2014/texmf-dist/
*** fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/local/
texlive/2014/texmf-dist/f
*** onts/type1/public/amsfonts/cm/cmsy7.pfb></usr/local/texlive/
2014/texmf-dist/fon
*** ts/type1/public/amsfonts/cm/cmsy8.pfb></usr/local/texlive/
2014/texmf-dist/fonts
*** /type1/public/amsfonts/cm/cmti10.pfb>
*** Output written on root.pdf (4 pages, 123997 bytes).
*** Transcript written on root.log.
*** Document preparation failure in directory 'output/document'
Unfinished session(s): Whatever
0:00:14 elapsed time, 0:00:22 cpu time, factor 1.57
I am on a Mac and I have all the fonts mentioned in the error message, can
you tell me why things go wrong and what should I do?
Thanks.
Best,
Bob
Email Gateway (Aug 19 2022 at 17:14):From: Christian Sternagel <c.sternagel@gmail.com>
The content of "root.log" (as indicated in the error message) might be
instructive.
cheers
chris
Email Gateway (Aug 19 2022 at 17:14):From: Larry Paulson <lp15@cam.ac.uk>
In the last line below, you have commented out the filename, which is the first place to look for clues. It’s true that the file is an exhaustive and fairly unreadable log the entire execution. But there should be a visible error message near the end. Errors from latex always begin with a ! character.
Larry Paulson
Last updated: Apr 23 2024 at 20:15 UTC