Re: [isabelle] Generate PDF from .thy File?



The content of "root.log" (as indicated in the error message) might be instructive.

cheers

chris

On 02/16/2015 12:31 AM, Bob Fang wrote:
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.