Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] coq-projective-geometry package

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] coq-projective-geometry package


Chronological Thread 
  • From: Anthony Bordg <bordg.anthony AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] coq-projective-geometry package
  • Date: Fri, 19 Jan 2018 21:35:09 +0000
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=bordg.anthony AT gmail.com; spf=Pass smtp.mailfrom=bordg.anthony AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f179.google.com
  • Ironport-phdr: 9a23:RaL4cBUKiiXnlZlQAeQBK6TaFtbV8LGtZVwlr6E/grcLSJyIuqrYbBaCt8tkgFKBZ4jH8fUM07OQ7/i5HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba9vIBmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KhsVRHolTwHNyYn/27Llsx+gqVboBe7qBx+xY7ffYWZOfV6c6/Ye94RWGhPUdtLVyFZAIy8YYsBAeQCM+hFsYfyu0ADogGiCQS2Hu7j1iNEi33w0KYn0+ohCwbG3Ak4Et8StnTUsNX1NKAUUeG10aLF0DLDb+lL1jfy9YPFdQsuofaWXb1tfsrd01MgFwXZjlWQrozlOTOU2/8Cs2ie9eVgVOavh3Q7pAF2pzii38EhgZTHiIISz1DL7yR5wIAtKN23T057ZtGkEJ9OuC2AK4R2RcYiT3lnuCY71r0GuYO7czMQxJs7wB7fbvqKeJWL7BL7TOudPyt0iXZ/dL+8hxu+61asxvD9W8WuzVpHrC5In9/RvX4XzRPT8NKISv5l80ehxzmP0wfT5/lBIU8ulKrbL4ctwqcslpYPqEjDEDL6lUfygaOMeUUk/e+o6+vjYrr4vJOTK4h0igTmPqQvnMywH/g4PxAQU2SH/emwzr7u8E3jTLlUk/E7k7PVvI3YKMkfvqK5BhVa0ocn6xaxFTem19EYkGEcI1JCYhKIkofpN0vUL/D+Efe/g1OskDFrxv3dMb3hB4/CLnnHkLv7Ybl97EtcxBIpzd9D/5JUFq0BIPXrV0Dts9zYFwY1PBCww+b6E9pwzZgeWGKKAq+BKqzeq16I5uQ1I+mNfoAZojj9K+J2r8Lp2HQ+gBoWebSjlc8cb2n9FfB7KW2YZ2Dti5EPCzFZkBA5SbnDjkGCVjhCL1y1Ra4zrmUxD5iqAsHKQJyth7qQ9Ci+F5xSIGtBDwbfQj/Ta4yYVqJUO2qpKch7n2lYBOHwGb9k7gmnsUrB85QiK+PV/iMCspe6jYp64uTSkVc58jkmVp3BgVHIdHl9myYzfxFzxLp2+BUvxVKK0Kw+iPtdR4QKuqF5FzwiPJuZ9NRUTtD/XgWbIIWMQVeiB8y6WXQ/F41ghdAJZEl5FpOpiRWRhyc=
@Gaëtan: I tried to build the version 8.4 of the package and I got the following error

File "/home/anthony/projective-geometry-8.4/Plane/P14_pseudo_midpoint.v", line 35, characters 0-14:
In nested Ltac calls to "not_eq" and "(A <> B)" (with B:=lMN, A:=lPQ), last
term evaluation failed.
Error: The variable lPQ was not found in the current environment.
Makefile:191 : la recette pour la cible « Plane/P14_pseudo_midpoint.vo » a échouée
make: *** [Plane/P14_pseudo_midpoint.vo] Erreur 1


2018-01-19 19:26 GMT+00:00 Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>:
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/*



--
PhD. Anthony Bordg
Research Associate
Cambridge University, UK
https://sites.google.com/site/anthonybordg/

Archive powered by MHonArc 2.6.18.

Top of Page