brianh at cs.pdx.edu
Tue Jul 1 17:40:30 CEST 2008
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
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
More information about the isabelle-dev