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 -------------------------------------------------------------
