Development of the Coq library. (Add LoadPath solution is not good enough.)

3
votes

I am adding some theorems to the library https://github.com/coq-contribs/zfc

But there is a not very good thing. While I developing the code in the CoqIDE I have to add

Add LoadPath "/home/user/0my/GITHUB/".

and to rename all 

Require Import Axioms.

to 

Require Import ZFC.Axioms.

. All files of the library are in

/home/user/0my/GITHUB/ZFC

and the name of the last folder matters.

But when I want to run the "make" command I have to rename everything back.

The file "Make" contains the names of files and the prefix. Deleting the first line didn't solve the problem.

I don't think that it is the best practice of the developing with the CoqIDE, so what shall I do instead?

Edited1:

I have "run_coqide.sh" which consist of

#!/usr/bin/env bash
COQPATH=/home/user/0my/GITHUB/ 
/home/user/opam-coq.8.8.1/4.02.3/bin/coqide

"From ZFC Require Import Sets. " raises error "Cannot find a physical path".

Edited2:

I have find out that this is a working script:

#!/usr/bin/env bash
export COQPATH=/home/user/0my/GITHUB/ 
/home/user/opam-coq.8.8.1/4.02.3/bin/coqide

Is it normal run or a hack?

1
coqcoqide

1 Answers

4
votes

Rename Make to _CoqProject, this is the name currently recognized by CoqIDE where it will look for project configuration (in particular the -R . ZFC option to make the Coq files in the directory visible to CoqIDE). It is also possible to change the name CoqIDE is looking for to Make, but _CoqProject seems to really be the new standard.

Note that the -R . ZFC option, that allows you to import libraries unqualified, corresponds to the command Add Rec LoadPath "/.../ZFC" as ZFC.

I would also suggest to actually switch the whole codebase to explicit qualification ZFC.Axiom, that you've been doing locally by hand, making it less error prone to work with different projects at the same time. I'm not sure why it was necessary to rename things back to run make, my understanding is that it shouldn't be necessary.

See also the Coq reference manual, about the coq_makefile utility.