[INFO] HOL Light Native

Open htzh opened this issue 4 years ago • 1 comments

I have adapted HOL Light to compile natively. Now one is no longer restricted to a particular version of OCaml!

However it is just a start. For details see the holnat project.

Any feedback welcome in this thread or over at the new repo.

Aug 19 '21 22:08 htzh

After implementing a caching mechanism (through simple pure OCaml) all the modules listed in hol.ml can be loaded in slightly over 1s on an M1 MacBook Air. This is significantly faster than uncached, not to mention bytecode versions :-)

Aug 26 '21 03:08 htzh