[isabelle] Generate PDF from .thy File?



Hi all,

I want to generate readable PDF file from a theory file and thatâs what I
did:

1. 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

2. 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"
3. Run ``Isabelle build -D .â and I got this error:

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



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