我在库中添加了一些定理
https://github.com/coq-contribs/zfc
但是有一件不是很好的事情。
在CoqIDE中开发代码时，我必须添加
Add LoadPath "/home/user/0my/GITHUB/".
并重命名所有
Require Import Axioms.
至
Require Import ZFC.Axioms.
。库中的所有文件都在
/home/user/0my/GITHUB/ZFC
和最后一个文件夹的名称很重要。
但是，当我想运行“ make”命令时，我必须将所有内容重命名。
文件“ Make”包含文件名和前缀。删除第一行并不能解决问题。
我认为这不是使用CoqIDE进行开发的最佳实践，那么我应该怎么做呢？
编辑1：
我有“ run_coqide.sh”，其中包括
#!/usr/bin/env bash
COQPATH=/home/user/0my/GITHUB/
/home/user/opam-coq.8.8.1/4.02.3/bin/coqide
“来自ZFC要求导入集。”引发错误“找不到物理路径”。
编辑2：
我发现这是一个有效的脚本：
#!/usr/bin/env bash
export COQPATH=/home/user/0my/GITHUB/
/home/user/opam-coq.8.8.1/4.02.3/bin/coqide
是正常运行还是黑客入侵？
最佳答案
将Make重命名为_CoqProject，这是CoqIDE当前识别的名称，它将在其中查找项目配置（尤其是-R . ZFC选项，以使该目录中的Coq文件对CoqIDE可见）。
也可以将CoqIDE寻找的名称更改为Make，但是_CoqProject似乎确实是新标准。
请注意，允许您导入不合格库的-R . ZFC选项对应于命令Add Rec LoadPath "/.../ZFC" as ZFC。
我还建议您将整个代码库实际切换为显式的限定ZFC.Axiom，因为您一直在本地进行手工操作，这样可以减少在同一时间处理不同项目的错误。我不确定为什么需要将其重命名以运行make，我的理解是这不是必须的。
另请参阅Coq参考手册about the coq_makefile utility。