The Coq mailing list

[Laurent Th�ry <Laurent.Thery AT sophia.inria.fr>]

Edsko de Vries wrote:
> Hi,
>
> I am trying to compile ssreflect. I have Coq installed through macports. At first I tried to install ssreflect with 8.2pl1 but that didn't work, as ocaml had since been upgraded to 3.12.0, which is not compatible with 8.2pl1. Although version 8.2pl2 is not yet available in macports, I modified the portfile to refer to 8.2pl2 (and disabled one patch which seems to have already been included in 8.2pl2) to upgrade Coq -- that seemed to go fine. Compilation of ssrcoq, following the instructions, then also worked fine (that is, compilation didn't give any errors). 
>
> However, when I try to generate a version of coqide, things break:
>
> [edsko@devriese2
>  ~/csw/src/ssreflect-1.2/src]
> # coqmktop -ide -opt ssreflect.cmx -o ../bin/ssrcoqide
> File "/var/folders/kg/kgA4gpp3Gnu+Kv5tWCp9yE+++TI/-Tmp-/coqmaindd09f5.ml", 
> line 2, characters 17-29:
> Error: Unbound module Coqide
>
> I'm not sure what exactly the error means and how I could try to fix it.. Any 
> suggestions?
>
>
>   
There is a mailing list dedicated to ssreflect: 
ssreflect AT msr-inria.inria.fr.

Two possible sources for this problem:
The coq you have just compiled has not generated the coqide (check if in 
the bin directory of your coq
there is a coqide).

You are using a wrong version of coqmktop (make sure it calls the 
version you have just installed)

--
Laurent