[isabelle-dev] isabelle build

Makarius makarius at sketis.net
Mon Aug 6 17:09:21 CEST 2012


On Mon, 6 Aug 2012, Christian Urban wrote:

> 1) I transferred two "old" IsaMakefile/ROOT.ML files to a
>  "new" ROOT like:
>
>     session Nominal2! in "Nominal" = HOL +
>     options [document = false]
>     theories
>       "Nominal2"
>       "Atoms"
>       "Eqvt"
>
>     session Esop! in "ESOP-Paper" = Nominal2 +
>     theories [document = false]
>       "~~/src/HOL/Library/LaTeXsugar"
>     theories
>       "Paper"
>     files "document/root.bib" "document/root.tex"
>
>  Now calling
>
>    isabelle build -v -d . Esop
>
>  I expected that a pdf-file for the paper is created.
>  But I could not see anything. Also
>
>    isabelle build -v -d . -o document=pdf Esop
>
>  did not produce anything. Is there some magic I missed
>  to generate the pdf-files? Is there some control where
>  the pdf is generated and how it is called? My IsaMakefiles
>  often contain commands like
>
>    cp ESOP-Paper/document.pdf esop-paper.pdf
>
>  for copying any pdf-file in a more convenient place and
>  under a more intelligible name.

There must have been more options in your IsaMakefile, because the default 
document preparation happens somewhere in $ISABELLE_BROWSER_INFO, and the 
generated sources are deleted in the end.

In Isabelle/doc-src/ROOT there are some examples with document_dump and 
document_dump_mode that are leading into the direction to make typical 
configurations for papers based on regular sessions.

I have my own traditional idioms here, but did not try to express them in 
the new way yet.  It will practially require some ./build script to wrap 
up the whole process as used to be done by several IsaMakefile command 
lines, but shell scripting is no longer built into the build tool.

Anyway, do you happen to have an old-style document/IsaMakefile as well?
It needs to be turned into document/build (as mentioned in NEWS and the 
system manual).


 	Makarius



More information about the isabelle-dev mailing list