Hi Marco, Thanks a lot. Now it works perfectly. As you said, the source of the problem was indeed explained at the very end of the README file. All the Best! |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
________________________________ From: Marco Maggesi [mailto:[email protected]] Sent: Tue 30/12/2008 05:20 To: Alfio Ricardo de B Martini Cc: [email protected] Subject: Re: [Hol-info] Help on HOL Light (possible problems with the installation) 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
