Hi, thanks for your help,
I downloaded the new hol light via svn, and, while there are several ml
files that begin with 'pa_j_3.1x', they all give me this error:
File "pa_j.ml", line 112, characters 71-73:
Error: This expression has type (string * MLast.ctyp) list
but an expression was expected of type
('a * MLast.ctyp) list Ploc.vala
Makefile:33: recipe for target `pa_j.cmo' failed
make: *** [pa_j.cmo] Error 2
On 14 March 2012 06:28, "Mark" <[email protected]> wrote:
> 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
> >
> >
> >
>
------------------------------------------------------------------------------
This SF email is sponsosred by:
Try Windows Azure free for 90 days Click Here
http://p.sf.net/sfu/sfd2d-msazure
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
