[MLton-devel] Twelf Performance -- more numbers

Frank Pfenning Frank Pfenning <fp@cs.cmu.edu>
Sat, 21 Dec 2002 15:23:56 -0500


I carried out two more experiments that test different
aspects of Twelf.  These paint a different picture.

  TALT Snapshot 02-12-10 (Karl Crary)
  Twelf Standard Regression Suite

I have also added the memory leak example, single run
(which is most application relevant) as the last column.

Here are the numbers:

                TALT   Regress  Leak
SML/NJ 110.0.3  87.050 105.210  24.460
SML/NJ 110.40   53.270  50.540  13.771    
Poly/ML 4.1.3  136.570 122.840  34.320
MLton 20020923  57.460  60.050   6.500

All of these were used "out of the box" with default
settings.  By the way, my machine has a 1GHz processor
(Pentium III Coppermine) - thanks for everyone who
sent me the right incantations.

For those familiar with Twelf, the primary aspects
tested by these suites are

TALT - meta-theorem verfication [coverage checking]
Regress - operational semantics [logic programming search]
Leak - type reconstruction      [checking proof terms]

  - Frank


-------------------------------------------------------
This SF.NET email is sponsored by: Order your Holiday Geek Presents Now!
Green Lasers, Hip Geek T-Shirts, Remote Control Tanks, Caffeinated Soap,
MP3 Players,  XBox Games,  Flying Saucers,  WebCams,  Smart Putty.
T H I N K G E E K . C O M       http://www.thinkgeek.com/sf/
_______________________________________________
MLton-devel mailing list
MLton-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/mlton-devel