On Monday, August 6, 2012 at 12:09:54 (+0200), Makarius wrote: > Did everybody try the isabelle build tool? Are there any problems left, > apart from retraining fingers after 16 years of usedir/make/makeall?
I just did. Building of heaps worked nicely. But two questions:
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.
2) Transferring the IsaMakefile and ROOT.ML file of the Isabelle
Cookbook to the new ROOT (see below) has thrown up the following
problem:
...
*** Theory loader: failed to load "Simple_Inductive_Package" (unresolved
"Base")
*** Inconsistent declaration of outer syntax keyword "ML"
*** At command "theory" (line 1 of
"/Users/cu/isabelle-cookbook/ProgTutorial/Base.thy")
The Base.thy (see below) file redefines several "core" Isabelle
keywords, which was OK with the old ways (if one knew what one is doing).
Is this now seriously prevented?
Thanks for any insight,
Christian
ROOT
Description: ROOT
Base.thy
Description: Base.thy
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
