The Coq mailing list

[Ravi Bajaj <bajaj AT mit.edu>]

@Anthony 

When you write it seems complete are you saying you worked it out by hand 
yourself and then coded it up and found a bug or is the specific logical step 
of the proof iron-clad correct and you're merely unfamiliar with the version 
control documentation for Coq's more recent instantiations?

Ravi

Sent from my iPhone

> On Jan 19, 2018, at 2:27 PM, Gaëtan Gilbert 
> <gaetan.gilbert AT skyskimmer.net>
>  wrote:
> 
> That project seems to have branches for various Coq versions. In the 8.4 
> branch that position in the failing file is not at the end of the proof, 
> suggesting that the most recent version of the development is not 
> compatible with 8.4.
> Try the 8.4 branch or a newer Coq.
> 
> Gaëtan Gilbert
> 
>> On 19/01/2018 19:51, Anthony Bordg wrote:
>> Hi,
>> I would like to build the coq package on projective geometry 
>> <https://github.com/coq-contribs/projective-geometry> to go through the 
>> proofs in the various files with Proof General or coqIDE. But using the 
>> make command I got the following error:
>>  File 
>> "/home/anthony/projective-geometry/Plane/projective_plane_to_Heyting_projective_plane.v",
>>  line 146, characters 0-4:
>> Error: Attempt to save an incomplete proof
>> Makefile.coq:245 : la recette pour la cible « 
>> Plane/projective_plane_to_Heyting_projective_plane.vo » a échouée
>> make[1]: *** [Plane/projective_plane_to_Heyting_projective_plane.vo] 
>> Erreur 1
>> make[1] : on quitte le répertoire « /home/anthony/projective-geometry »
>> Makefile:2 : la recette pour la cible « all » a échouée
>> make: *** [all] Erreur 2
>> However, the aforementioned proof does not seem to be incomplete. I'm 
>> using coq v.8.4pl4 on Ubuntu 16.04 LTS. Any help would be welcome.
>> Regards
>> Anthony
>> -- 
>> *PhD. Anthony Bordg
>> *
>> *Research Associate
>> *
>> *Cambridge University, UK
>> https://sites.google.com/site/anthonybordg/*