The Coq mailing list

[Kevin Buzzard <kevin.m.buzzard AT gmail.com>]

Just to be clear -- I am using the proof files here

https://gforge.inria.fr/projects/coqfinitgroup/

and my impression is that the version of ssreflect there will not
compile on the latest version of Coq. Ideally I would be using the
latest version of everything but I am having trouble persuading
the feit thompson files to use the latest ssreflect.


On 14 June 2017 at 08:29, Kevin Buzzard 
<kevin.m.buzzard AT gmail.com>
 wrote:
> I am on Ubuntu 14.04. I wanted to take a look at the Coq Feit Thompson
> proof. I started with the Ubuntu 14.04 repository of coq (8.4pl5 or
> so) and did get as far as compiling the proof with make, but then I
> ran into this:
>
> https://mathoverflow.net/a/164998/43076
>
> I felt like this issue shouldn't be ignored, so I decided to start
> again and install everything from opam (now giving me Coq 8.6). But
> when I do this, "make" in the feit thompson directory gives me
>
> make[1]: Entering directory `/home/buzzard/Encfs/Coq/feit_thompson'
> CAMLC -c src/ssrmatching.mli
> File "src/ssrmatching.mli", line 76, characters 14-34:
> Error: Unbound type constructor glob_constr_and_expr
> make[1]: *** [src/ssrmatching.cmi] Error 2
> make[1]: Leaving directory `/home/buzzard/Encfs/Coq/feit_thompson'
> make: *** [all] Error 2
>
> My understanding of this error is that it's a problem with an early
> version of ssreflect not compiling with the later version of coq. I
> have installed coq-mathcomp-ssreflect using pam, but now I have to
> persuade the Feit-Thompson code to use this more modern version of
> ssreflect and I can't see how to change the ssreflect option in the
> makefile.
>
> **
>
> What I am trying to do is to get and IDE up and running where I can
> analyse the feit thompson proof files and step through them etc. I'm
> finding this tough. Can anyone give me any pointers?
>
> Kevin Buzzard