[isabelle-dev] building isabelle
makarius at sketis.net
Fri Mar 13 11:44:33 CET 2009
On Thu, 12 Mar 2009, Chris Capel wrote:
> If I want to test changes I make to Isar or other parts of the Isabelle
> core, is possible to do this without also rebuilding my HOL image? (Or
> is rebuilding the image faster than the first build?) Is it sufficient
> to simply rebuild Pure?
No, you always have to rebuild the whole path that leads to a desired
point in the tree of logic images. When experimenting with Pure or other
basic things, it is usually sufficient to build HOL-Plain instead of the
full HOL image -- this takes only 1-2 min.
You can also build Pure only and then load parts of HOL interactively into
> I couldn't find any documentation on developing isabelle that talked
> about building.
Some bits of information about this are in INSTALL, src/Pure/README, and
the Isabelle System manual. The very notion of "dumped-world" images is
taken for granted, although these days few people might remember that this
was quite commonplace in the past (notably in the Lisp community). Our
SML platforms are in the same tradition: no separate loading of modules,
but persistent heap images.
More information about the isabelle-dev