[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