Hi Alfio,
you should be able to fix your problem by using a customized OCaml
toplevel
with the num library preloaded.
Try this:
cd hol_light
ocamlmktop -o ocamlnum nums.cma
./ocamlnum
#use "hol.ml";;
This is explained at the very end in the README of the HOL Light
distribution.
Hope it helps,
Marco
On Dec 30, 2008, at 3:29 AM, Alfio Ricardo de B Martini wrote:
Hi People,
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?
Many thanks!
-------------------------------------------------------------------------------------------------------------------------------------
bash-3.2$ cd hol_light
bash-3.2$ ocaml
Objective Caml version 3.08.2
# #use "hol.ml";;
[...]
File "/home/hol_light/sys.ml", line 31, characters 0-34:
Warning: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
false
- : bool -> bool = <fun>
Cannot load required shared library dllnums.
Reason: dynamic loading not supported on this platform.
Reference to undefined global `Num'
Error in included file /home/hol_light/sys.ml
- : unit = ()
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
