Hi Alfio,
| I am new member to the list (since a few minutes ago) and I am
| struggling to install correctly the HOL Light system (in a cygwin
| environment). Actually the installation and building is pretty
| straightforward (as described in the tutorial), but when I load the
| HOL system from the ocaml top level, there are a number of errors
| during the loading of the several files. As a consequence, I am only
| able to use the pure ML language (the top level). I attach part of the
| messages printed in the cygwin bash shell below. Can you help me on
| this?
I think the key problem is this line, and the others are all
consequential:
Cannot load required shared library dllnums.
Cygwin doesn't support the dynamic loading feature of OCaml. So
instead, you need to build a new OCaml toplevel with the Num
library pre-loaded. Fortunately this is relatively easy using
"ocamlmktop". For example, the following
ocamlmktop -o ocamlnum nums.cma
will create a new toplevel "ocamlnum" (or maybe it will be
"ocamlnum.exe" in Cygwin). You can then fire up this "ocamlnum"
instead of the plain "ocaml", and HOL Light should load into
that without problems, I hope.
John.
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
