The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Enrico,

I am on Ubuntu 12.04 LTS, but I don't have root rights, which makes package 
installtion complicated. Compile everything from sources seems to be easier. 
Also I prefer to know exactly what I have.

I am currently trying the latest 3.X Ocaml version instead of 4.01.0. I guess 
this might fix the issues.

The problems I encountered so far with compiling ssreflect are:

- GEXTEND needs to be changed to EXTEND

- Ocaml 4 seems to have a stricter sytnax and semantics for tuples. I hade to 
change a few cases like "a,b" into "(a,b)" and functions which are declared 
to take 2 arguments into functions which take a 2 tuple. Especially the 
latter looks rather bizare to me, more like a bug in Ocaml 3.X that this did 
compile at all, but I must admit I never wrote a single line of Ocaml and I 
can only guess the meaning from my Coq knowledge.

- Currently I am pondering about the line " let ssrmmod = Gram.Entry.create 
"ssrmmod" " in ssreflect.ml4. It gives me some sort of unbound variable error 
(I am right noe rebuilding everythign with Ocaml 3.X so I can't tell the 
exact error right now).

In case everything (Ocaml, Coq, CompCert, VST) builds fine with Ocaml 3.X 
work, I think I am fine with it, but I am happy to check fixes for the Ocaml 
4.X builds.

Best regards,

Michael

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Enrico Tassi
Sent: Wednesday, January 14, 2015 3:30 PM
To: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] Errors compiling ssreflect 1.5 using Ocaml 4.01.0 - 
Question on ssreflect INSTALL file

On Wed, Jan 14, 2015 at 10:32:16AM +0000, Soegtrop, Michael wrote:
> In case it makes a difference: I use the Coq 8.4pl5 (compiled from 
> sources using the same Ocaml).
> 
> The ssreflect INSTALL file mentions that "Coq version 8.4 compiled 
> with CamlP5" is required. I am not sure I understand the dependency on 
> CamlP5. I compiled Coq 8.4pl5 from sources ant it works fine (e.g.
> CompCert and VST builds run through fine). I also compiled and 
> installed CamlP5 before building ssreflect, but I am not sure I 
> understand what is meant by "Coq compiled with CamlP5". Should I 
> compile Coq in some different non standard way in order to be able to 
> compile ssreflect 1.5?

I can help you but first I need to know on which platform are you are working.
Is it win, osx, or liunx (which distro)?  Maybe there is an easy way top get 
ssr 1.5 for your platform...

Best,
--
Enrico Tassi