coq - Coq 库的开发。（添加 LoadPath 解决方案不够好。）

Question

但是有一个不是很好的事情。当我在 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

这是正常运行还是黑客攻击？

score 4 · Accepted Answer

重命名Make为_CoqProject，这是 CoqIDE 当前识别的名称，它将在其中查找项目配置（特别是-R . ZFC使目录中的 Coq 文件对 CoqIDE 可见的选项）。也可以将 CoqIDE 正在寻找的名称更改为Make，但_CoqProject似乎确实是新标准。

请注意，-R . ZFC允许您导入不合格库的选项对应于 command Add Rec LoadPath "/.../ZFC" as ZFC。

我还建议将整个代码库实际切换为显式限定ZFC.Axiom，您一直在本地手动完成，从而减少同时处理不同项目的错误。我不确定为什么有必要将事物重命名为 run make，我的理解是它不应该是必要的。

1 回答 1