The Coq mailing list

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

I have the current ssreflect installed and it works fine for me in Coq
8.6 too. On reflection I think that my question is perhaps for the
maintainers of the Feit-Thompson proof. It had not occurred to me that
one might need to maintain a proof!
The issue, I believe, is that when I type "make" in the feit_thompson
directory, it does not use my default installed ssreflect -- for
example one of the things it does is that it runs ocamlc on
src/ssrmatching.mli, which seems to be a 2013 file. Looking at the
current ssreflect source code, my understanding is that a files called
src/ssrmatching.mli is shipped with the version of ssreflect for Coq
8.4 and 8.5 but not 8.6.

So it seems to me that what I need to do is either change things
around a little in the feit_thompson makefile or in feit_thompson/src
so that it is reading a newer ssreflect, or I need to run an older Coq
but preferably one where the bug here

https://coq.inria.fr/bugs/show_bug.cgi?id=3243

is fixed. My impression is that it is fixed in 8.4.6 so I am now going
to downgrade my Coq to 8.4.6 and see if I can compile the proof in
such a way that

make -f Makefile.coq validate

works in the feit_thompson directory.

Kevin

On 14 June 2017 at 10:14, Emilio Jesús Gallego Arias 
<e AT x80.org>
 wrote:
> Dear Kevin,
>
> Kevin Buzzard 
> <kevin.m.buzzard AT gmail.com>
>  writes:
>
>> Just to be clear -- I am using the proof files here
>> https://gforge.inria.fr/projects/coqfinitgroup/
>
> I think the updated files are at https://github.com/math-comp/math-comp,
> they work fine for me in Coq 8.6.
>
> E.