[isabelle-dev] NEWS: Isabelle sessions and build management
makarius at sketis.net
Sun Jul 29 21:46:27 CEST 2012
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
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.
More information about the isabelle-dev