[isabelle-dev] NEWS: Isabelle sessions and build management
makarius at sketis.net
Thu Aug 2 23:20:20 CEST 2012
On Thu, 2 Aug 2012, Makarius wrote:
>>> Note that generated theory sources are not supported by isabelle build
>>> -- it simply does not fit into the concept; this is no longer shell +
>>> make scripting.
>> So, what do we do with the entries that need them?
The other entry is thys/Collections. It *uses* some patching based on two
ruby scripts, but it does not *need* to do so.
We have so many ways to define document antiquotations, or issue logical
specifications under program control in Isabelle/ML. It is the language
that is dedicated to that, better than some external scripting language to
generate the sources.
How should the Prover IDE react, when the user opens such a generated
source? I am not going to provide any provisions for that; this would
open a can of worms of complications.
Right now isabelle build is just a simple command line tool. At the next
stage, it will get a GUI wrapper, and eventually become the first
encounter by new users who have just downloaded Isabelle, potentially with
AFP. Even for users who continue with Proof General later.
There will be a few clicks to say what to build --- HOL, HOLCF,
HOL-Nominal, AFP/Collections, and it will just work. No odd make
BTW, there were other specialities in Collections, Refine_Monadic, and
also Huffman concerning document generation. These were rather
unexciting, and easily performed by regular system functions. This had
also the benefit that the userguide of the first two now actually shows up
on the generated HTML page, and there are no longer any generated document
sources spilled into the user's directory.
More information about the isabelle-dev