Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] How to create a makefile for a project using libraries?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to create a makefile for a project using libraries?


Chronological Thread 
  • From: Pierre Courtieu <pierre.courtieu AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] How to create a makefile for a project using libraries?
  • Date: Sat, 10 Feb 2018 12:15:40 +0000
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f49.google.com
  • Ironport-phdr: 9a23:mOrYqRYaVnASgUjlpe/mcAX/LSx+4OfEezUN459isYplN5qZoMq7bnLW6fgltlLVR4KTs6sC17KP9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCagbb9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjE2/mHYiMx+gqxYrhy8uRJw35XZb5uJOPdkZK7RYc8WSGhHU81MVyJBGIS8b44XAuQbPOZXsZP9p0EQohCjGwSsA/7vyiVUhn/3w6I6zvkqHAbe3AwhAd0Oqm7Uo8vvOKgOVuC10bPIzSnCb/xIxDfw84fIchU7rvGNWbJ8a9beyU4qFw7ciFibtILrPzSQ1usXsmib6fJtVeOpi249qgF+uCKjxsk2ioTPm4kbyUjE+D1nzIopIdC0Uk12bN6+HJdOqi2XNJF6T8wmTmxupS000KcJuYShcygP0JknxwDQa/iAc4WQ5xLsTueRITNhiHJiebKzmw++8Uavx+D4TMW031FKri1KktnIqH8BzQDc6s+CSvdl/0eh3yiA1xzL5+1aPUw5kbDXJp0hz7IqiJYfrEfOEjX5lUjylKOWc18r+ums6+TpeLXmoZqcOpdsigH/LKsugNa/DvoiPgcSWGib5P681KHi/ULnXbVHlfI2kqzDv5DbIcQXvLK2AwhQ0oo78RawEy+m0MgEnXkANF9KZBWHj5HwN17SJPD4EOywjk+3kDZrwvDGJqfuDo/MLnjFirfhfKxy51RSyAopnphj4MdfDahEK/buUGfwssbZB1k3KV+a2eHiXe1825kEVCqkBbKDLKLfrBfc/uMiOfOBIoQSpSzhKvU4z/HrhH4931QaeP/6jtMsdHmkE6E+cA2ian32j4JZSDZYjk8FVOXvzWa6f3tWbne2Ubg742hiWo2jBIbHAIuqhe7YhXvpLthtfmlDT2u0PzLwbYzdAqUDbSuTJolqlTlWDeH8Gb9k7gmnsUrB85QiLufQ/XdF55fq1dww4OyL0B9upHp7CMOS12zLRGZxzDsF

Indeed if you make install you have to use subdirectories. Otherwise the same (install) directory would correspond to different logical names. You can use files where they are compiled instead of installing them and then “.” works but you need to add -R options to tell coq where to find the library.

Documentation is not very clear about that indeed.

P

Le sam. 10 févr. 2018 à 04:38, Helmut Brandl <helmut.luis.brandl AT gmail.com> a écrit :
Hello list.

I have experimented a lot. It seems to me that all examples in the reference manual and in Chlipala's cpdt are broken. It is **not** correct to put '-R . Lib' into _CoqProject. You have to use a subdirectory instead of '.'.

After this minor but obviously very significant change my example works fine.

Is there any plan to update the reference manual. The actual behaviour of coq is very confusing if you just follow the manual. Or did I overlooked something?

Regards
Helmut

On Feb 9, 2018 19:14, "Helmut Brandl" <helmut.luis.brandl AT gmail.com> wrote:


On Feb 9, 2018 16:19, "Pierre Courtieu" <pierre.courtieu AT gmail.com> wrote:
Or you can just use -R options in _coqProject files?
P. 

Hi Pierre.

I have tried already the following:

Added "-R . Mylib" to the _CoqProject file of the library. Then issued 'make install' after successful compilation.

In the project using the common library I tried in the sourcefile 'Require Import Mylib.Name'.

Compiling the project I get '.../Mylib/Name.vo contains library Name and not Mylib.Name'.

Using only 'Require Import Name' does not work, because the compiler does not find it.

Regards
Helmut



Le ven. 9 févr. 2018 à 23:17, Théo Zimmermann <theo.zimmi AT gmail.com> a écrit :
Hi,

You probably want to use the $COQPATH environment variable instead. See https://coq.inria.fr/refman/commands.html#EnvVariables and https://coq.inria.fr/refman/gallina-ext.html#loadpath.

Regards,
Théo

Le ven. 9 févr. 2018 à 20:32, Helmut Brandl <helmut.brandl AT gmx.net> a écrit :
Hello coq-clubbers.

I have the following problem with the creation of a makefile:

- I have a coq library with several common function (i.e. a collection of *.v files). The libraries can be processed find with a proper _CoqProject file which as basically the list of source files. The program ‘coq_makefile’ generates a makefile whose usage by gnu make creates the corresponding *.vo files.

- I have two independent coq projects which want to use the library. The coq compiler needs some instructions on how to find the library objects. However for obvious reasons I don’t want to put ‘Add LoadPath’ statements into my source files.

Is there a generic way to solve this problem? Maybe the solution is so simple that I just don’t see it by reading the manual. Thanks for any hint.

Regards
Helmut




Archive powered by MHonArc 2.6.18.

Top of Page