The Coq mailing list

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

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