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?
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.