How do I verify the Coq proof of Feit-Thompson? I probably don't have the appropriate background to even ask this question.  I know next to nothing about formal or computer-aided proof, and very little even about group theory.  And this question is more "tech support" than math.
But: after reading that Georges Gonthier and collaborators had formalized a proof of the Feit-Thompson theorem in Coq, I thought it would be fun to try to verify it on my own computer.
So I installed Coq (8.4pl2), OCaml, etc, on my Ubuntu box, and then went here and downloaded feit_thompson.tar.gz (v2.0).  I unpacked it and ran make.  It ran various invocations of coqc for about two hours, and then finished with no error reported.  A bunch of .vo files were produced, including one for theories/stripped_odd_order_theorem.v, which even the casual observer can see contains what appears to be a statement of the Feit-Thompson theorem.
Is that it?  Does that mean that Coq agrees with the correctness of the proof?  Or are there more steps?
I was particularly curious because I saw that Makefile.coq has a validate target (which isn't run by just doing make).  So I ran make -f Makefile.coq validate.  This started a coqchk command which ran for about five minutes and then failed with:
 User error: Signature components for label fun_of_fin do not match
 make: *** [validate] Error 1

Was I not supposed to do that?  Or did I just find a flaw in their proof? :-)
Again, I freely admit that I do not really know what I'm doing.  In particular, it's not clear to me whether compilation of a Coq file actually verifies the theorems and proofs within it, or merely prepares it for later validation.  If an expert answers "Go away until you understand Coq" I'll meekly accept it.  But it does seem like it might be helpful for even a newbie to be able to understand how to properly run Coq on a proof created by someone else, and I couldn't find documentation that clearly explained it.
 A: The error you get is a real one, but is not in the proof of the odd order theorem.  It is in Coq.  Let me be more clear: a bug in the kernel of Coq
was making the .vo files (the files coqchk checks) incomplete.  Some universe
constraints coming from module sub typing were forgotten.  coqchk correctly spots it, and actually revealed the bug I fixed a while ago.  A patchlevel release of Coq including the fix is already on its way.
The bugreport:
https://coq.inria.fr/bugs/show_bug.cgi?id=3243
The commit that fixed the bug:
https://github.com/coq/coq/commit/a07deb4eac1d5f886159784ef5d8d006892be547
A: Following Enrico Tassi's answer, I compiled the current snapshot of Coq 8.4pl4 from https://github.com/coq/coq.  With it, I was able to successfully compile and validate the proof.
 Modules were successfully checked

What an impressive piece of work!
A: To convince yourself that the proof is indeed valid, you need to do at least two things:


*

*read and understand the definitions as well as the theorem statement thus knowing for a fact that the proof is indeed a proof of the right theorem;

*check the development using a proofchecker you trust.
Now, that second part can be a bit tricky: coqc is quite a big piece of code allowing the use of plugins, the definition of custom tactics, etc. That's why a standalone checker coqchk exists: it can only deal with compiled files (i.e. raw proof terms) and therefore is much simpler thus making it easier to review its code.
It is bothering that coqchk fails on this development. It would be worth mentioning either on coq's bug tracker or on the ML.
