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?

From: Théo Zimmermann <theo.zimmi AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] How to create a makefile for a project using libraries?
Date: Fri, 09 Feb 2018 22:16:20 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua0-f174.google.com
Ironport-phdr: 9a23:li209hHfytbB7lRq9g5E551GYnF86YWxBRYc798ds5kLTJ78o86wAkXT6L1XgUPTWs2DsrQY07OQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmCexbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KODE38G7VisJ+gqFVrg+/qRNj2IPbep2ZOeBkc6/BYd8XR2xMVdtRWSxbBYO8apMCAfQBPeFCqInyv1gBrRq7BQmpGuzv0DpIiWXw3a08zu8sFh3G3Aw+ENIJqnjVrdT1NKIXUeC016TIwjDDYOlX2Tf58oTHbhchofSVUL92bMHfx04vFwbfgVWRr4zoJzKV1uIXs2ia9eVsT+yvi3QhpgpsoTav3t8hhpfVio8R0FzJ9iV0zJwrKdGlSkN3e8OoHZlfuiycKoB4WNktQ3tytyY/0rAGuYC0fCwNyJk/wh7Qcf2Hc4yR7hL+TumdPS50hHx4dL+9iBu+60egyur7Vsm71FZFsDBJncXLtnAIzxDT686HReVh/kq5xzqDywTe5vtHLE00j6bXNYMtz7wqmpYOs0nOETf6mEDsg6+XckUk9PKo6+PiYrj+up+cN5F7igbkPqUvm8y/BOE4MgkVUmiU/OSzzrzj/UnjTLpWif02l7HVsIrGKsQDuq65HwhV354/5Ba4FjeqycgXnX0aLF1eYx+HlIjoO1TWIP/iF/u/glKskC1qx//cJLHhDI/NfTD/l+Lqeq844EpBwiIyy8pe7tRaEOIvOvX2D3PxNdvvPB48NgGuxu/hDp0pyoMTXiSdA6qcMYvdtFaJ4qQkJOzaN9xdgyr0N/Vwv62mtnQ+g1JIJfD4j6tSU2ixG7FdG2vcZHPthtkbFmJT51gxSeXrjBuJVjsBPi/uDZJ53SkyDcedNamGXpqk2eXT0yKyH5kQbWdDWAjVTCXYMr6cUvJJUxq8Z89sljteC+qkQo4lkAyn7Er0kuU7aOXT/SIcuNTo090nv+A=

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

[Coq-Club] How to create a makefile for a project using libraries?, Helmut Brandl, 02/09/2018
- Re: [Coq-Club] How to create a makefile for a project using libraries?, Théo Zimmermann, 02/09/2018
  - Re: [Coq-Club] How to create a makefile for a project using libraries?, Pierre Courtieu, 02/09/2018
    - Re: [Coq-Club] How to create a makefile for a project using libraries?, Helmut Brandl, 02/10/2018
      - Re: [Coq-Club] How to create a makefile for a project using libraries?, Helmut Brandl, 02/10/2018
        
        Re: [Coq-Club] How to create a makefile for a project using libraries?, Pierre Courtieu, 02/10/2018
        
        Re: [Coq-Club] How to create a makefile for a project using libraries?, Théo Zimmermann, 02/10/2018
        
        Re: [Coq-Club] How to create a makefile for a project using libraries?, Helmut Brandl, 02/11/2018
        
        Re: [Coq-Club] How to create a makefile for a project using libraries?, Théo Zimmermann, 02/11/2018
        Re: [Coq-Club] How to create a makefile for a project using libraries?, Helmut Brandl, 02/12/2018
        
        Re: [Coq-Club] How to create a makefile for a project using libraries?, Helmut Brandl, 02/14/2018