[isabelle-dev] NEWS

[Tobias Nipkow]

Brian,

Thank you for your critical feedback - I had wondered about compilation 
times myself. We will discuss the merger issue again internally.

Tobias

Brian Huffman schrieb:
> 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
> 
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev