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

Brian Huffman huffman at in.tum.de
Sun Jul 29 21:02:35 CEST 2012


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.

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.

- Brian



More information about the isabelle-dev mailing list