HolyHammer breaks at every update of Ocaml.

[barakeel]

I propose to port the holyHammer translation to SML using ideas and code from Metis and Holyhammer. This will remove the depenency on Ocaml. I plan to do finish this port in June.

[barakeel]

I have finished a first port of holyhammer translation to SML. You can call holyHammer.hh_new to test it and you won't require OCaml. For those familiar with HOL4 conversions and interested in optimizing/debugging it, the translation occurs in hhTranslate.sml and hhTptp.sml.

Next step is to compare the performance of this new translation with the old one and gradually optimize it:

• adding unfolding of ?!, COND, etc
• sharing equations and definitions.
• adding more checks and proofs if not too time-consuming.

[barakeel]

Here is an example that the new translation can solve but not the old one: load "holyHammer"; open holyHammer; val cj = MAP f [1;2] = REVERSE (MAP f [2;1]); holyhammer cj; hh_new cj;

[barakeel]

Ok, the newly developped translation is actually unsound, that is why it could find this theorem. I guess proving every step of the translation will be necessary after all.

[mn200]

Please fix your recent commits to remove Unicode from your sources. The regression tests are failing.

You should run build -t to check that everything is OK before pushing to GitHub.

[barakeel]

Ok I ran build -t and I got this error.

Performing self-test... Cannot find file selftest.ui error in load selftest : Fail "Cannot find file selftest.ui" Uncaught exception: Fail "Cannot find file selftest.ui" Selftest failed in directory /home/tgauthier/HOL/src/monad

[mn200]

You need to build cleanAll first

[barakeel]

Here are the results for the comparison between the new and the old translation out of 1881 theorems from the theories ["list", "measure", "sorting", "probability", "finite_map", "arithmetic", "real", "complex"]

Old (through HOL Light): 959 proven in 5 seconds 919 reconstructed in 1 seconds New (only SML): 973 proven in 5 seconds 923 reconstructed in 1 seconds

The remaining task before removing OCaml code is to: 1) Optimize the translation it seems that in some cases the SML translation is much slower than the compiled OCaml. Find these cases if they exist. 2) Do a soundess check by trying to prove false from the dependencies of each of those problems. 3) Port the THF printer and the monomorphization conversion. 4) Make sure that it is correct with the original by calling Satallax on the problems.

[barakeel]

HolyHammer now works without installing OCaml therefore I am closing this issue.