On Sun, 29 Jul 2012, Brian Huffman wrote:
On Sun, Jul 29, 2012 at 7:11 PM, Makarius <makar...@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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
