[isabelle-dev] isabelle build

Makarius makarius at sketis.net
Wed Aug 8 20:50:21 CEST 2012


Here are some further refinements leading up to Isabelle/3a6c03b15916.

   * The "Session Modelling Language" (S.M.L.) has been simplified to
     accomodate applications better, instead of the received layout of the
     Isabelle distribution.

     Session names are always verbatim (without implicit concatenation) and
     the default directory is "." (not the session base name).

     Examples from the distribution:

       session HOL = Pure + theories Complex_Main

       session "HOL-Nominal" in Nominal = HOL + theories Nominal

       session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
         theories Nominal_Examples
         theories [quick_and_dirty] VC_Condition

     Examples from AFP:

       session "Depth-First-Search" (AFP) = HOL +
         theories DFS

       session BDD (AFP) = Simpl +
         theories
           EvalProof
           NormalizeTotalProof
         files
           "document/root.bib"
           "document/root.tex"

   * "isabelle build -D DIR" includes a directory and selects all its
      session defined there.

   * "isabelle mkroot" has been refined a bit. I still need to figure out
     how to avoid "document_dump" in most practical situations. (It is not
     enabled there now.)


 	Makarius



More information about the isabelle-dev mailing list