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