The Coq mailing list

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

Dear Coq users,

I get errors compiling ssreflect 1.5 with Ocaml 4.01.0. Unfortunately the 
ssreflect INSTALL file doesn't mention an recommended Ocaml version.

As it look I am not the only one getting these errors, see e.g.:

http://www.lix.polytechnique.fr/coq/pylons/logs/view/ReleasedSsreflect/3069174337681179041

I get the same errors about deprecated syntax, which are trivial to fix. In 
addition I get this error:

File "src/ssreflect.ml4", line 843, characters 21-22:
Parse error: [fun_def_cont] expected (in [fun_def])
Error while running external preprocessor

which at least for me is not trivial to fix. Did someone compile ssreflect 
1.5 with Ocaml 4.01.0?

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?



Best regards,

Michael