[isabelle-dev] building isabelle

[Makarius]

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 
Proof General.


> 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.


 	Makarius