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";;
val hol_version : string = "2.20"
val hol_dir : string ref = {contents = "/home/hol_light"}
val temp_path : string ref = {contents = "/tmp"}
- : unit = ()
val use_file : string -> unit = <fun>
val load_path : string list ref = {contents = ["."; "/home/hol_light"]}
val loaded_files : '_a list ref = {contents = []}
val file_on_path : string list -> string -> string = <fun>
val load_on_path : string list -> string -> unit = <fun>
val loads : string -> unit = <fun>
val loadt : string -> unit = <fun>
val needs : string -> unit = <fun>
- : unit = ()
- : unit = ()
val quotexpander : string -> string = <fun>
- : unit = ()
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 = ()
.
.
.
Error in included file /home/hol_light/iter.ml
- : unit = ()
File "/home/hol_light/cart.ml", line 23737, characters 15-29:
Unbound value new_definition
Error in included file /home/hol_light/cart.ml
- : unit = ()
File "/home/hol_light/define.ml", line 23970, characters 19-43:
Unbound value new_recursive_definition
Error in included file /home/hol_light/define.ml
- : unit = ()
File "/home/hol_light/help.ml", line 24636, characters 18-27:
Unbound value mergesort
Error in included file /home/hol_light/help.ml
- : unit = ()
Camlp4 Parsing version 3.08.2
# `x+1`;;
Unbound value parse_term
|Prof. Alfio Martini
|http://www.inf.pucrs.br/~alfio
|PUCRS - Pontificia Universidade Catolica do Rio Grande do Sul
|Faculty of Informatics -- Av. Ipiranga 6681
|Predio 32 -- 90619 - 900
|Porto Alegre - RS - Brasil
|Tel: +55 (051) 3320-8707
|Fax: +55 (051) 3320-3758
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
