[opentheory-users] opentheory tool implementing eqMp incorrectly

[Joe Hurd]

Hi Ramana,

> I find it mildly disturbing that constants aren't determined solely by
> their names.

At least the opentheory tool raises an error if the assumptions or
theorems of a theory contain two versions of a constant with the same
name.

> I've updated my article at http://cam.xrchz.net/cl.art.gz
> Try reading it, if you want, and tell me what should be improved...
> I got some warnings from the opentheory tool.

These errors are harmless, but compressing the article also cleans it
up (see below).

> Also the tool is really slow! (I compiled with mosml though and maybe
> should try mlton.)

Your article provided an excellent case study for speed testing.

gzcat ~/Desktop/cl.art.gz | bin/mlton/opentheory info --inference article:-
WARNING: 20 objects left on the stack by -
WARNING: 92,617 objects left in the dictionary by -
Primitive inferences:
eqMp ............ 29,353
deductAntisym ... 22,621
subst ........... 15,979
appThm ........... 8,852
refl ............. 4,600
assume ........... 3,873
absThm ........... 2,233
betaConv ......... 2,184
axiom ............... 68
defineConst ......... 16
defineTypeOp ......... 1
Total ........... 89,780

Timing on the development version of the opentheory tool with debugging on:

Moscow ML: 492.82s
MLton:      14.17s
Poly/ML:    10.02s

Timing on the development version without debugging (i.e., commenting
out the line MLPP_OPTS += -r 'OpenTheoryDebug' in Makefile.dev) - this
is the same as the production version:

Moscow ML: 197.07s
MLton:      12.13s
Poly/ML:     7.23s

How about compressing the article using the command:

gzcat ~/Desktop/cl.art.gz | time bin/polyml/opentheory info --article
-o cl.art article:- && gzip cl.art

This results in an article with a smaller number of both bytes and inferences:

ls -l ~/Desktop/cl.art.gz cl.art.gz
-rw-r--r--@ 1 joe  staff  627875 Sep 15 15:17 /Users/joe/Desktop/cl.art.gz
-rw-r--r--  1 joe  staff  302685 Sep 15 16:15 cl.art.gz

gzcat cl.art.gz | bin/mlton/opentheory info --inference article:-
Primitive inferences:
eqMp ............ 14,071
subst ........... 11,368
deductAntisym .... 9,528
appThm ........... 7,125
refl ............. 2,455
absThm ........... 2,106
betaConv ......... 1,750
assume ............. 362
axiom ............... 68
defineConst ......... 14
defineTypeOp ......... 1
Total ........... 48,848

And re-running the production version of the opentheory tool on the
compressed article sees a corresponding speed-up:

Moscow ML: 95.50s
MLton:      3.27s
Poly/ML:    3.01s

> A next step for me would be to upload my (locally installed) package
> somewhere - the infrastructure is in place for that I presume..?

Yes indeed - the gilith repo is open for business

http://opentheory.gilith.com/

Make a theory file for your article, and use the opentheory tool to
first install it locally and then upload it to the gilith repo.

Cheers,

Joe