[isabelle-dev] isabelle build
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
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 [quick_and_dirty] VC_Condition
Examples from AFP:
session "Depth-First-Search" (AFP) = HOL +
session BDD (AFP) = Simpl +
* "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.)
More information about the isabelle-dev