*To*: Peter Sewell <Peter.Sewell at cl.cam.ac.uk>*Subject*: Re: [isabelle] datatype definition performance*From*: Stefan Berghofer <berghofe at in.tum.de>*Date*: Wed, 08 Feb 2006 11:10:25 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <E1F6SqF-0007ls-00@mta1.cl.cam.ac.uk>*Organization*: Technische Universität München*References*: <E1F6SqF-0007ls-00@mta1.cl.cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.7.12) Gecko/20050920

Peter Sewell wrote:

I have what I thought would be a straightforward definition of a datatype of abstract syntax, a mutually-recursive definition of 5 datatypes, with around 33 constructors in total. Running it under "Isabelle2005: October 2005" (which seems to be the default lab install here) on a 3.2GHz P4 takes just under 9 minutes (painful), whereas using the April 2004 version takes less than 9 seconds. Any suggestions would be very welcome - I'm a very naive user at this point, so might well be doing something stupid.

Dear Peter, I am not aware of any recent changes to the datatype package that could have had an influence on its performance. However, there are a number of flags that can influence the performance of the datatype package, in particular "proofs" and "quick_and_dirty". The "proofs" reference variable controls the amount of detail to be recorded in proof objects (0 = only calls to oracles, 1 = only dependencies on axioms and other theorems, 2 = full proof objects, i.e. proofs as \lambda-terms). In ProofGeneral, "proofs" is usually set to 1. Note that setting "proofs" to 2 can lead to a considerable slowdown. The "quick_and_dirty" flag instructs most definitional packages not to prove characteristic theorems, but merely state them as axioms. This speeds up processing of theories quite a bit, which is a good thing when using Isabelle interactively. For this reason, "quick_and_dirty" is usually set to true in ProofGeneral, whereas it is set to false in batch mode. In order to examine the values of these flags in interactive mode, you can either have a look at the items "Full Proofs" and "Quick And Dirty" in the "Isabelle -> Settings" menu of ProofGeneral, or issue the commands ML proofs ML quick_and_dirty which is a bit more reliable. To find out about the values of the flags in batch mode, issue the command isatool getenv -h in a shell and examine the values of the ISABELLE_USEDIR_OPTIONS environment variable. If it contains the "-p 2" option, then full proof objects are switched on permanently in batch mode. Also check the ROOT.ML file that loads your theories for commands like "set quick_and_dirty". If you think that Isabelle 2004 and Isabelle 2005 behave differently, although you have set the above flags to the same values, please send me your datatype definition, so that I can have a closer look at the problem. Greetings, Stefan -- Dr. Stefan Berghofer E-Mail: berghofe at in.tum.de Institut fuer Informatik Phone: +49 89 289 17328 Technische Universitaet Muenchen Fax: +49 89 289 17307 Boltzmannstr. 3 Room: 01.11.059 85748 Garching, GERMANY http://www.in.tum.de/~berghofe

**References**:**[isabelle] datatype definition performance***From:*Peter Sewell

- Previous by Date: [isabelle] Axclass info
- Next by Date: Re: [isabelle] datatype definition performance
- Previous by Thread: [isabelle] datatype definition performance
- Next by Thread: Re: [isabelle] datatype definition performance
- Cl-isabelle-users February 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list