coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] coq-projective-geometry package

From: Anthony Bordg <bordg.anthony AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] coq-projective-geometry package
Date: Fri, 19 Jan 2018 18:51:38 +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-f182.google.com
Ironport-phdr: 9a23:OqUZdRNGKtiXeDegRlMl6mtUPXoX/o7sNwtQ0KIMzox0Iv76rarrMEGX3/hxlliBBdydt6odzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlViDanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr8zRDqi8rxrSAf2hygbKz43/mbXislqg6JaphKquhhzzoHQbY2QMvd1Y6HTcs4ARWdZXshfWS9PDJ6iYYQTFOcOJ/pUopPnqlcSsRezBw+hD/7vxD9SgX/22LU33vgnEQHa3AwgGNQOsXTJp9joM6cSS/26zKbVxjjEdPxW3i3955XHchw7u/6MW65wccrWyUkpFwLIlVqQqYn/MDOU0uQBqXSU7+1lVe+2jWMstg9/oj+qxsg2i4nJgJoYyl/D9SV+z4Y1IcO3RFRnbt6jFZtcry6aN4pqQsMiXmFnozw2xaEBuZ6+eiUB1ZcpxwbHZvCZb4SF5gjvWeWRLDtimn5pZbOyiwyv/UWj1OHxUNS/3kxQoSpfiNbMs2gA1xzN5ciDTftw5kKh1iyO1wDX8+1EOFw0mbbCJ54v37I9lYQfvV7MHi/xn0X2g6uWeVs+9ue07OTnZ63qpp6aN4BqlgHzKroiltC7DOgiMQUDX3KX9fqh2LDi50H1XbZHguMunqncqp/aJMAbpqCjAw9S14Yu8w2wDzC80NsFknkLNkhKeBSbj4jpPFHOJvD5AOywg1SpijhrxvTGMqf9DZXKK3jPiK3hcqpl605A1AozyshS6I5TCrEYOf78RkvxtMHDARIiKAy1w+PnCM1n2Y8EWGKPBLWZMKLIvlOS6OIvObrEWIhAszHkbvMh+vSm2XQ+gBoWebSj9ZoRcnGxWPp8dRa3e33p1/4HDWcNuBt2ZuvwhFLKBTRUfXq9Gas6+jE8DpOOAoLKR4Tri7uEinToVqZKb3xLXwjfWUzjcJ+JDqtdMXPAEopaijUBEIOZZcok3BCquhX9zuM+fOXR8ywc85nk0YosvrGBpVQJ7TVxSv+l/SSVVWgtxzEHQjY32OZ0pkkvkg7eg5g9uORREJlo390MUgo+MsSCnelzCtS3Qx6ZO9nQGAzgTdKhDjU8CNk2xo1Wbg==

Hi,

I would like to build the coq package on 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/

[Coq-Club] coq-projective-geometry package, Anthony Bordg, 01/19/2018
- Re: [Coq-Club] coq-projective-geometry package, Gaëtan Gilbert, 01/19/2018
  - Re: [Coq-Club] coq-projective-geometry package, Ravi Bajaj, 01/19/2018
  - Re: [Coq-Club] coq-projective-geometry package, Anthony Bordg, 01/19/2018