[opentheory-users] the Unwanted namespace

[Joe Hurd]

Hi Ramana,

I fixed a performance bug in the proof rewriting, and your example
goes through pretty quickly now (see below). The fix is both pushed
and released in the latest version of the opentheory tool.

Cheers,

Joe

________________________________________________________________

dimholt:~/dev/opentheory$ gzcat ~/Desktop/ll.art.gz | time
bin/mlton/opentheory info --inference article:-
WARNING: 38 objects left on the stack by -
WARNING: 473,658 objects left in the dictionary by -
Primitive inferences:
eqMp ............ 150,377
deductAntisym ... 129,584
subst ............ 76,065
appThm ........... 20,748
assume ........... 18,086
refl .............. 9,363
betaConv .......... 7,461
absThm ............ 4,564
axiom ............... 193
defineConst .......... 25
defineTypeOp .......... 1
Total ........... 416,467
       24.40 real
       15.30 user
         9.07 sys

dimholt:~/dev/opentheory$ time bin/mlton/opentheory info --inference
foo.art Primitive inferences:
eqMp ............. 68,100
subst ............ 56,228
deductAntisym .... 51,689
appThm ........... 17,378
betaConv .......... 6,866
refl .............. 6,325
absThm ............ 4,267
assume ............ 1,608
axiom ............... 190
defineConst .......... 26
defineTypeOp .......... 1
Total ........... 212,678

real	0m5.289s
user	0m5.027s
sys	0m0.256s