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

[Makarius]

On Sun, 29 Jul 2012, Brian Huffman wrote:

> On Sun, Jul 29, 2012 at 7:11 PM, Makarius <makarius at sketis.net> wrote:
>> The question is if HOL-Plain and HOL-Main still have any purpose.  Full HOL
>> now takes < 2min on a reasonably fast machine with 4 cores.
>
> Images like HOL-Plain or HOL-Main are often useful when I am doing
> development on libraries within the HOL image. Building these images
> saves me a lot of time, because otherwise I would have to load the
> same set of files repeatedly in Proof General, which can take several
> minutes on my (old, not-reasonably-fast, 2-core) machine.

OK.  There is no immediate need to change the status-quo of HOL-Plain and 
HOL-Main.

BTW, the new build tool does not hardwire the "build heap" aspect of a 
session.  That is a matter of the command line invocation.  This saves 
quite some time and disk space for images that were never used.  If users 
do want one, they can say "-b" on the spot.


> Of course, if we can make it easy enough to build custom images, then 
> there is no practical reason to have HOL-Plain or HOL-Main set up by 
> default in the distribution.

I did not think of this option yet.  It might be actually simple to set 
that up locally.


 	Makarius