[isabelle-dev] HOL vs. HOL-Complex

[Florian Haftmann]

Hi Brian,

first of all, I want to emphasize that the merging of HOL-Complex with
HOL is not necessarily the final state.  We are still experimenting and
collecting feedback,

> What is the rationale behind merging HOL-Complex with HOL?
> 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.

This is not correct insofar that the merge was not suggested by a
particular user request.  The structure of the Distribution itself
motivated to remove the distinction between HOL and HOL-Complex since a
bunch of theories based on the HOL image would load particular
HOL-Complex theories (esp. real numbers) on-the-fly, making the
distinction between both somehow erratic.

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

This is a misunderstanding: Parity.thy etc. are needed by HOL-Complex,
and for this reason they belong to the (greater) HOL image.  Of course
it would be desirable to reflect this also in the location of the
theories, but you cannot move files in CVS easily.

> 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).
> ... switch
> to the HOL-Plain image and fiddle around with the search path so that
> the other imports from HOL can be loaded properly.

This was actually the idea how development in HOL (or HOLCF) theories
could take place.  Anyway any fiddling with the search path should not
be necessary.  I will have a look at this again.

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

This is true, but should only be relevant for running whole regression
sessions after minor changes - do I miss something!?

> Merging HOL-Complex into HOL is at best a temporary hack, and  
> not a real solution to the fundamental problem.
> I apologize for the lengthy rant. But seriously, I hope that some  
> other people also recognize the fundamental problem, and are thinking  
> about it.

Indeed, this observation is true.  Makarius already has sketched how the
road could go on here.

Hope this helps,

Cheers
Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 252 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20080702/0665137e/attachment.sig>