[isabelle-dev] NEWS

[Gerwin Klein]

My $0,02: I was wondering about the merge as well. For my taste, there is 
almost too much in HOL already as it is.

It's not such a big problem, though. You can always build your own custom 
images with exactly the part you need (not that it's a nice user-interface 
paradigm, and you need to replicate parts of Makefiles, but it's not a 
show-stopper either).

We could copy xemacs and have a separate HOL-sumo with just everything in there..

Somewhat related: we were thinking about an Isabelle search engine, based on 
the current theorem search, but with web interface (for the distribution, but 
also for AFP and other larger projects). It would basically need such an image 
with everything in it to be able to find things in different sessions. It 
would also need a significant performance improvement in the theorem search 
(it currently scales linearly in the number of theorems and we're starting to 
have problems with response time > 20sec).

Cheers,
Gerwin

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