如何在GitHub中手动设置库以便在CoqIDE中使用？

Question

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

我需要在CoqIDE中使用这个library。我已经将该文件夹下载并保存到我的计算机上，但是当我打开CoqIDE并写入"Require“(其中StringEq是库中的StringEq文件的名称)时，我收到错误信息"Unable to locate library StringEq”。

有没有办法手动设置这个库，这样我就可以在CoqIDE中使用它了？(库的GitHub页面上的READme文件中没有任何说明。)

Answer 1

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

在Linux上，将下面这一行添加到.bashrc或.zshrc或您的shell使用的任何初始化中，然后重新启动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

下面是我使用的另一种方式。

It doesn't seem like intended usage。也许我只是抗拒改变我的方式，但我也更喜欢明确地说明我的依赖关系，而且我不确定COQPATH环境变量是否会使在不同项目中拥有同一个库的不同版本变得同样容易。

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

下面是一个布局示例：

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