Re: [isabelle] datatype definition performance



Peter Sewell wrote:
(still, 9 minutes to really prove those theorems seems quite a while -
for curiosity, is it known how this should scale with the numbers of
mutually-recursive types and of constructors?)

Appendix B (page 88) of my diploma thesis, which is available at

  http://www4.in.tum.de/~berghofe/papers/dipl.pdf

contains a table with runtimes for various datatype definitions
and a comparison with John Harrison's datatype package for HOL Light
(unfortunately, the thesis is in German). For example, processing
a datatype with 62 constructors (representing the SML grammar) took
2759.88 seconds, whereas a datatype with 124 constructors (representing
the Verilog grammar) took 17516.06 seconds (measured on a Sun Ultra-2
workstation a long time ago).

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.