I'm a little unclear on how to 'downgrade' my OCaml when it was, in fact,
packaged with the cygwin distribution I downloaded..
On 14 March 2012 11:47, mohamed yousri soliman <[email protected]
> wrote:
> I faced same problem month ago.
> Actually, first option won't work standalone. You have to downgrade your
> Ocamle 3.11. x and camlp5 5.15 or higher.
>
> Dont use camlp5 6.x .
>
> The above version work with the latest HOLlight version checkedout from
> the subversion site
>
>
> On Wed, Mar 14, 2012 at 6:28 AM, "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
>> >
>> >
>> >
>>
>>
>> ------------------------------------------------------------------------------
>>
>> 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
>
>
------------------------------------------------------------------------------
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
