[isabelle-dev] NEWS

[Brian Huffman]

Quoting Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:

> * Integrated image HOL-Complex with HOL.  Entry points Main.thy and
> Complex_Main.thy remain as they are.

What is the rationale behind merging HOL-Complex with HOL?

The most immediate result that I notice is that it takes twice as long  
to compile the HOL image (which I have to do quite often when working  
on HOLCF).

Another consequence is that nearly the entire distribution now has  
file dependencies on HOL-Complex, so that testing changes to any of  
the HOL-Complex theories requires everything to be rebuilt, not just  
those theories that import Complex_Main.

A minor annoyance is the confusing situation where some (but not all)  
theories in HOL/Library are now part of the HOL image, while others  
are not. Which means that if I want to work on, say,  
Library/Boolean_Algebra.thy, I can load it in ProofGeneral using the  
HOL image just as I did before. But if I want to work on  
Library/Infinite_Set.thy, I must either temporarily change the theory  
name (since Infinite_Set is a finished theory in HOL) or else switch  
to the HOL-Plain image and fiddle around with the search path so that  
the other imports from HOL can be loaded properly.

I would guess that the real reason for the merge is that someone wants  
to be able to load HOL-Complex and some other logic image at the same  
time. Merging HOL-Complex into HOL is at best a temporary hack, and  
not a real solution to the fundamental problem. Before long I will  
probably want to use HOL-Word and HOLCF at the same time; should we  
also merge HOL-Word into HOL to support this?

The real problem is polyml's unfortunate restriction where compiled  
files (i.e. heap images) can only be extended in a linear fashion.  
True separate compilation with run-time linking, or at least a way to  
merge multiple heap images, is sorely needed.

If we could do separate compilation at the level of individual theory  
files, this would seriously improve the experience of both developers  
and users of Isabelle. For developers, file dependencies would be much  
more precise: Changes to a single theory file would only require  
recompilation of those modules that actually depend on it. For users,  
there would be much more flexibility in the combinations of theory  
files they can import. And in ProofGeneral, when you load library  
theories that are not included in the main logic image, you would not  
have to recompile them on the fly every single time you want to use  
them. Also, collections of user-contributed theories (like AFP) would  
be much more reusable.

I apologize for the lengthy rant. But seriously, I hope that some  
other people also recognize the fundamental problem, and are thinking  
about it.

- Brian