[isabelle-dev] isabelle build

[Christian Urban]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: ROOT
Type: application/octet-stream
Size: 785 bytes
Desc: ROOT
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120806/9557f8ec/attachment-0004.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Base.thy
Type: application/octet-stream
Size: 831 bytes
Desc: Base.thy
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120806/9557f8ec/attachment-0005.obj>