The Coq mailing list

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

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