coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] import

From: Erik Martin-Dorel <e.mdorel AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] import
Date: Tue, 22 Sep 2020 10:50:45 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=e.mdorel AT gmail.com; spf=Pass smtp.mailfrom=e.mdorel AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f47.google.com
Ironport-phdr: 9a23:ou816xVVfw0U/EWiRs/ddiOjG+vV8LGtZVwlr6E/grcLSJyIuqrYbRaPt8tkgFKBZ4jH8fUM07OQ7/m/HzVcqs7Q+DBaKdoQDkFD0Z1X1yUbQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2agMu4zf299IPOaAtUmjW9falyLBKrpgnNq8Uam4RvJrszxxfTv3dFdOtayX9sKFmOmxrw+tq88IRs/ihNuv8t7dJMXbn/c68lUbFWETMqPnwv6sb2rxfDVwyP5nUdUmUSjBVFBhXO4Q/5UJnsrCb0r/Jx1yaGM8L4S7A0Qimi4LxwSBD0kicHNiU2/3/Rh8dtka9UuhOhpxh4w47JfIGYMed1c63Bcd8GQ2dKQ8BcXDFDDIyhdYsCF+UOPehaoInnp1UAoxiwCxSyCuzz0TJHnGP60Lcg3ug9DQ3L3gotFM8OvnTOq9X1Mb8fX++vzKnJzjXIcvRY1i3n6IjUcxAhp+iAU7x3ccrL10YvEx7Og1KOpoD/OjOay+MNs3KF4OpkTu+vhGsnpBtwojir3Msjlo7JhocMx13C6C52z5o7K8eiR05nfd6rDoFQtyeCOoV5Xs4vQ39ktSI6x7MIpZO2eCsHxYgnyhPBZPGKcYmF7wz+WeuRITl0mn1rdK+xihi870StyPPxWMao3FtKriRIlMTHuH4K1xzW8MeHS/1981+g2TaJzQDT6/tLLVo6larBM5Ihzb8wloYTsUTeBSD6gln5jKiTdkgi5+Om6Pznb634qpOAM4J4kALzP6Q0lsChHeg1MRICUmeZ9Om6ybbt51f2QK9Qgf0ziqTZsI7VJcAcpqOhBg9ayIcj6xKmAzi4zdsUgGALLFxKdR+FlYTpNFbOIPf3Dfe7nVugiitkx/fDPrH5A5XNKGbMkKv5cLpj90JRzBA/wNNf6p5OFL0NPPH+VlX+udHaFhM5Nha7w+fjCNVzzIMeXmePD7eHP6/ItF+H++UvI/OSa48Rozv9JP0l6OTvjX89g1MSYa6p3Z4PZHCiAvtmO1mZYWbrgtoZDWgKuRM+QPX2h12GTD5cfG2/X7k85zE+EIKpF53PRoGrgLyb3Se0BIdaZm5cCgPELXC9fIKdHvwIdSi6I8l7kzVCW6LycYI50QCSs1r30btkaO/d4DEZs9fv08J448Xekwp38S1zCYKayW7eYXtzmzYlXT41lIV2u1B8zBKv1rJ1h7QMGJpW6/RTXwMSOpvVzug8ANf3DFGSNuyVQUqrF431SQo6Scg8lodXPhRNXu66hxWG5BKERr8Yk7vRWc4x+6PYmnX9foNzlymA264mgF0rBMBIMD/+3/8tx03oH4fM1n6hueOvfKUY0jTK8T7an2WLtUBcFgV3VPecBCxNVg7ttd38o3j6Yfq2E71+a1lOzMeDLu1Bbdi71Vg=

Dear Patricia,

Le mar. 22 sept. 2020 à 10:40, Théo Zimmermann <theo AT irif.fr> a écrit :

But usually, users working on a Coq project will avoid calling coqc
manually every time. Soon, you will be better off using one of the
solutions proposed here:
https://coq.inria.fr/refman/practical-tools/utilities.html#building-a-coq-project

In particular, using coq_makefile should be preferred to writing one's
own Makefile.

Indeed; and just to give another pointer − if you still want to automate the coq_makefile call itself by relying on a dedicated but concise Makefile,

you could reuse that Makefile for example: https://github.com/coq-community/coqoban/blob/master/Makefile

My 2 cents,

Erik MD

[Coq-Club] import, Patricia Peratto, 09/19/2020
- Re: [Coq-Club] import, Pierre Courtieu, 09/22/2020
  - Re: [Coq-Club] import, Théo Zimmermann, 09/22/2020
    - Re: [Coq-Club] import, Erik Martin-Dorel, 09/22/2020
- <Possible follow-up(s)>
- [Coq-Club] import, Patricia Peratto, 09/21/2020