[isabelle-dev] NEWS

[Brian Huffman]

Quoting Makarius <makarius at sketis.net>:

> On Tue, 1 Jul 2008, Brian Huffman wrote:
>
>> 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?
>
> So what are the absolute numbers?  On our local iMacs it is something like
> 2min vs. 4min (without proof terms).  Over the years HOL build time has
> usually been around 10-20min.

On my machine, build time was 3-4 minutes, but is now about 8 or 9.

My main objection really isn't the build time, but what I see as an  
ugly solution to the problem of wanting to be able to load separate  
logic images at the same time.

The merge lets people use any logic image built on HOL together with  
the complex numbers; this is definitely some thing users should be  
able to do, but the current solution is a hack and will not scale. I  
was serious about eventually wanting to use HOL-Word and HOLCF  
together (it would be very useful for reasoning about Haskell programs  
that use word types). But I wouldn't be in favor of grafting HOL-Word  
onto the main HOL image - where would it stop?

If the merge is intended to be a temporary solution, then that is fine  
- as long as someone is looking for a better long-term solution.

- Brian