Re: [isabelle] datatype definition performance



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.