[isabelle-dev] NEWS: Isabelle sessions and build management

[Makarius]

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 
scripting anymore.


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.


 	Makarius