CODEWITHSUNDEEP
coqcoqide
Barry Jay
Barry Jay

Reputation: 73

why does `make` using _CoqProject in coqide differ from `coqc` on the commandline?

I have two short files: cc_test is given by Lemma cc: 4 = 4. Proof. auto. Qed. and libtest is given by Require Import cc_test. Check cc.

When I execute coqc -R . ClosureLib -top ClosureLib cc_test in directory "/home/barry/svn/Coq/Closure_Calculus" and coqc -R "/home/barry/svn/Coq/Closure_Calculus" ClosureLib libtest in its directory, I get the expected output cc: 4 = 4

However, when the arguments to coqc above (from -R to the end) are placed in _CoqProject files, and I call Make makefile and then Make from the coqide menu, cc_test is okay but libtest yields output File "./libtest.v", line 1, characters 15-22: Error: Unable to locate library cc_test.

How should I modify the project files to make this work?

Comment: the coq reference manual (Chapter 15) does not mention any differences between these approaches. Also, the argument "-top ClosureLib" seems to be necessary in the commandline approach, but does not appear to matter using make as, in other experiments, I frequently get error messages saying that it found Top.foo but not ClosureLib.foo.

Upvotes: 3

Views: 1721

Answers (1)

eponier
eponier

Reputation: 3122

First, I do not think -top ClosureLib is useful here. The documentation describes -top as

Not valid for coqc as the toplevel module name is inferred from the name of the output file

As for your main question, I must admit my solution is to install the dependencies using

coq_makefile -f _CoqProject -o Makefile
make
make install

make install puts the libraries in user-contrib, a place where they will be loaded automatically. You can then use Require directly.

EDIT:

Thanks to @Zimm48, I understood how to use $COQPATH to accomplish the same task without having to install the dependencies first. But the name of the folder will be used as the logical prefix, so you must use the same identifier in the -R or -Q argument and for the name of the directory.

I would suggest to use the following architecture:

  • in directory /home/barry/svn/Coq/ClosureLib (note that I renamed the directory, so that its name is identical to the identifier passed to -R), _CoqProject contains

    -R . ClosureLib
cc_test.v

    You compile cc_test.v as follows:

    coq_makefile -f _CoqProject -o Makefile
make

  • in the directory containing libtest.v, _CoqProject contains

    -R . MyLib
libtest.v

    You can compile libtest.v as follows:

    coq_makefile -f _CoqProject -o Makefile
COQPATH=/home/barry/svn/Coq make

Upvotes: 2

Related Questions