[isabelle-dev] NEWS

[Mark A. Hillebrand]

On Wed, Jul 02, 2008 at 10:31:20AM +0100, Lawrence Paulson wrote:
> It would be interesting to see how big this would be and how long it  
> would take to build. The idea that the Sumo package is too big to  
> download seems ridiculous nowadays. Perhaps the same logic will apply  
> to us.

  In the Verisoft project, where theory development is organized as a
DAG of `modules', we have been using big heaps for a long time now. This
allowed to detect early merge (or Isabelle resource) problems, even if
theory development was separate at the leafs.

  Since `isatool usedir' only works in a linear fashion and it is easy
to get an out-of-date heap due to missing modification checks for
`static' heaps, we have usually avoided that and used `live' heaps
instead (either in a PG session or driven by a Perl script). Live heaps
had the additional advantage to us that only modified theories (and
their dependents) have to be rebuilt and not everything.

  The turn-around time for the Verisoft theories is on the order of a
day, haven't done a full rebuild lately, though.

  Best regards,

  Mark

-- 
Dr. Mark A. Hillebrand
German Research Center for Artificial Intelligence
Saarbruecken, Germany
Building E1 1, Room 4.06
Phone: +49 (0)681 302 57379    Fax: +49 (0)681 302 4290
Email: mah at dfki.de

-------------------------------------------------------------
Deutsches Forschungszentrum fuer Kuenstliche Intelligenz GmbH
Trippstadter Strasse 122, D-67663 Kaiserslautern, Germany

Geschaeftsfuehrung:
Prof. Dr. Dr. h.c. mult. Wolfgang Wahlster (Vorsitzender)
Dr. Walter Olthoff

Vorsitzender des Aufsichtsrats:
Prof. Dr. h.c. Hans A. Aukes

Amtsgericht Kaiserslautern, HRB 2313
-------------------------------------------------------------