The Coq mailing list

[Helmut Brandl <helmut.luis.brandl AT gmail.com>]

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