1

我需要在 GitHub 中使用与 Coq 标准库不同的库。但我不知道如何手动设置它以便我可以在 CoqIDE 中使用它。

我需要在 CoqIDE中使用这个库。我已将文件夹下载并保存到我的计算机，但是当我打开 CoqIDE 并编写“需要导入 StringEq”（其中 StringEq 是库中的 Coq 文件的名称）时，我收到错误消息“无法找到库 StringEq”。

有什么方法可以手动设置这个库，以便我可以将它与 CoqIDE 一起使用？（库的 GitHub 页面上的 READme 文件没有说明。）

4

1 回答 1

2

官方的用法似乎是将 kami 添加到$COQPATH环境变量中。

在 Linux 上，将此行添加到您的 shell 使用的初始化.bashrc或.zshrc任何初始化，然后重新启动您的 shell：

export COQPATH=/path/to/kami:$COQPATH
# That path must be so that `/path/to/kami/Kami/Lib/StringEq.v` is the path to `StringEq` for example

下面是我正在使用的另一种方式。
这似乎不是预期的用途。也许我只是拒绝改变我的方式，但我也更喜欢明确我的依赖关系，而且我不确定COQPATH环境变量是否可以很容易地在不同的项目中拥有同一个库的不同版本。

添加一个_CoqProject告诉 CoqIDE 在哪里可以找到 kami。

这是一个示例布局：

kami/           # The Kami repository
myproject/      # Your workspace
  _CoqProject
  theories/
    MyProject.v

其中myproject/_CoqProject包含：

-Q ../kami/Kami Kami
# and possibly other options

无论哪种方式，请记住构建 Kami：

cd kami/
make
于 2019-08-19T01:09:01.280 回答