You are not the first to have had trouble! The first thing is that you are trying to install HOL Light. When people say "HOL" they mean HOL4, which is another HOL theorem prover.
The problem you get is due to there being significant changes between OCaml 3.11.X and 3.12.X, and the version of HOL Light you have (presumably the snapshot from 10th Jan 2010?), does not cater for OCaml 3.12.X. Versions of HOL Light since the 10th Jan 2010 snapshot are only available as a Subversion snapshot. There are 3 possible solutions: 1. Download the latest HOL Light Subversion shapshot (see the HOL Light webpage). For this you need to install Subversion. 2. Tweak the version of HOL Light you have to work with OCaml 3.12.X. This doesn't take long, and I can tell you how if needed. 3. Install an older version of OCaml. I've had problems installing OCaml 3.11.X (and OCaml 3.12.0) on 64-bit Linux, so perhaps OCaml 3.10.2 is the safest choice. I recommend solution 1. Another thing to remember is that you must do a "make clean" before reattempting a "make" in the same HOL Light directory. And another thing is that you need the right version of Camlp5 (do "camlp5 -v" to find out). Note that there was a similar posting a few months ago: http://sourceforge.net/mailarchive/message.php?msg_id=28674314 Hope this helps, Mark. on 14/3/12 9:23 AM, Adam Golding <[email protected]> wrote: > My Situation: > Windows 7 64-bit Ultimate > Cygwin (with the Cygwin version of OCaml 3.12.1) > > Since there is no pa_j_3.12.ml file I copied pa_j_3.11.ml to pa_j.ml > > I get the following error when trying to 'make' HOL: > > $ ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" -I +camlp5 > pa_j.ml > File "pa_j.ml", line 1689, characters 37-56: > While expanding quotation "class_expr": > Parse error: ']' or [expr] expected after '[' (in [expr]) > File "pa_j.ml", line 1, characters 0-1: > Error: Preprocessor error > > Not having the first clue about OCaml, I don't know how to proceed from > here.. > > Many Thanks :-) > Adam Golding > > > > ---------------------------------------- > > ---------------------------------------------------------------------------- > -- > Virtualization & Cloud Management Using Capacity Planning > Cloud computing makes use of virtualization - but cloud computing > also focuses on allowing computing to be delivered as a service. > http://www.accelacomm.com/jaw/sfnl/114/51521223/ > > > ---------------------------------------- > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info > > > ------------------------------------------------------------------------------ Virtualization & Cloud Management Using Capacity Planning Cloud computing makes use of virtualization - but cloud computing also focuses on allowing computing to be delivered as a service. http://www.accelacomm.com/jaw/sfnl/114/51521223/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
