coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Helmut Brandl <helmut.brandl AT gmx.net>
To: coq-club AT inria.fr
Subject: [Coq-Club] How to create a makefile for a project using libraries?
Date: Fri, 9 Feb 2018 13:31:23 -0600
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=helmut.brandl AT gmx.net; spf=Pass smtp.mailfrom=helmut.brandl AT gmx.net; spf=None smtp.helo=postmaster AT mout.gmx.net
Ironport-phdr: 9a23:cG9/UBTDydGPssuXnH4uASOfkdpsv+yvbD5Q0YIujvd0So/mwa69ZB2N2/xhgRfzUJnB7Loc0qyK6/mmATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfa5+IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/mHLhcJ/g61Vrg+vqR9hzYDTe4yVKON+fqbBcdMaWWZMXMBcXDFBDIOmaIsPCvIMM+RGoIn5olsOsAe+DhSxCeP10DBIgGL53akn2OkmEQHJwgggH9cTsHTIttn6L70SXvqzzKbVyTXOdPxW2TLy6YTSdBAuv+2MUKt2fMHMykcvDxvIgkuNpYD7JT+ZyPoBvmqB4+Z9V++jkXArpx1prjSx2ssgl5PFip8Jxl3E7yl13Zs5KcemREN7btOpFoZbuTuAOItsWMwiRnlluCYkxb0Cvp62ZC0KyJM6xx7DcfCHfI2I4x35WOaXPzh4mGppeLO5hxms7Uit0vPwWtSq3FpQsCZJjNvBumoQ2xHR8MSLVOdx8l+k2TmV1gDT7u9EIVozlareM5MhwqA/lp4WsUTeAi/6gl75jLWMeUUi5+eo7//qYrrjpp6TLYN0jB/xMrg2lsylHes4KhQOX3Sc+emkyLLj+lT5TKxWgf0yj6nWq4vXJd8bp668Gw9ayJwv6xe5Dze80dQXh2MLLFxfeEHPs4+8MFbXZfv8EP2XglK2kT4tyeqVEKfmB8DtI3zGjaupV6x07UJYgF4zwNRa+o4SAKsIJv73ckD0pJreAwNvYF/8+PruFNgojtBWYmmIGKLMaPqD42/N3fomJqy3XKFQvT/8L/Y/4Pu/33A8iRkbcLX7hMJLOkD9JexvJgCiWVSpms0IQDUFuxp4SuH22gXbDGxjIk2qVqd53QkVTYKrCYCaGtKoh6Gdmii+DttQa3wUUl0=

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