找不到图书馆
Unable to locate library
相同的 Linux 命令在一个环境中成功，而在另一个环境中失败：
$ coqtop -lv test.v -I Lib
我遇到的失败是在 Debian stretch 和 Coq v8.5 下
$ uname -a
Linux front 4.8.0-1-amd64 #1 SMP Debian 4.8.7-1 (2016-11-13) x86_64 GNU/Linux
$ coqtop -v
The Coq Proof Assistant, version 8.5 (June 2016)
compiled on Jun 9 2016 12:4:46 with OCaml 4.02.3
我收到的错误消息是：
Welcome to Coq 8.5 (June 2016)
Require Import libtest.
Error during initialization:
File "/home/user/dev/coq/test.v", line 1, characters 15-22:
Error: Unable to locate library libtest.
同源同命令执行成功的环境是：
$ uname -a
Linux back 3.16.0-4-amd64 #1 SMP Debian 3.16.36-1+deb8u2 (2016-10-19)x86_64 GNU/...
$ coqtop
The Coq Proof Assistant, version 8.4pl4 (July 2014)
compiled on Jul 27 2014 13:34:24 with OCaml 4.01.0
成功结果如下：
Welcome to Coq 8.4pl4 (July 2014)
Require Import libtest.
Coq <
所以我想弄清楚这是怎么回事，希望得到答案
this post 但无济于事。
为了这个问题，我把源代码精简到最简单的：
test.v
Require Import libtest.
Lib/libtest.v
<empty file>
如果这很重要，我已经在每个环境中重新编译了（空）库文件 libtest.v。
$ cd Lib
$ coqc libtest.v
$ cd ..
非常感谢任何帮助。
以下适用于我（我使用的是 Coq 8.5pl3）。
让我们编译我们的库，把它放在 Lib 命名空间中：
$ pwd
<...>/libtest-question
$ cd Lib
$ coqc -R . "Lib" libtest.v
$ cd ..
然后我们修改我们的test.v:
$ cat test.v
Require Import Lib.libtest.
并用
加载它
$ coqtop -R Lib Lib -l test.v
-Q 开关也可以，有关详细信息，请参阅参考手册的 §14.3.3。
确实，-I 的行为在 8.4 和 8.5 之间发生了变化。在 Coq 的 changelog 中，我们可以找到 an interesting line. As hinted in the changelog and as advised by the ，你可以使用 -R 代替。
相同的 Linux 命令在一个环境中成功，而在另一个环境中失败：
$ coqtop -lv test.v -I Lib
我遇到的失败是在 Debian stretch 和 Coq v8.5 下
$ uname -a
Linux front 4.8.0-1-amd64 #1 SMP Debian 4.8.7-1 (2016-11-13) x86_64 GNU/Linux
$ coqtop -v
The Coq Proof Assistant, version 8.5 (June 2016)
compiled on Jun 9 2016 12:4:46 with OCaml 4.02.3
我收到的错误消息是：
Welcome to Coq 8.5 (June 2016)
Require Import libtest.
Error during initialization:
File "/home/user/dev/coq/test.v", line 1, characters 15-22:
Error: Unable to locate library libtest.
同源同命令执行成功的环境是：
$ uname -a
Linux back 3.16.0-4-amd64 #1 SMP Debian 3.16.36-1+deb8u2 (2016-10-19)x86_64 GNU/...
$ coqtop
The Coq Proof Assistant, version 8.4pl4 (July 2014)
compiled on Jul 27 2014 13:34:24 with OCaml 4.01.0
成功结果如下：
Welcome to Coq 8.4pl4 (July 2014)
Require Import libtest.
Coq <
所以我想弄清楚这是怎么回事，希望得到答案 this post 但无济于事。
为了这个问题，我把源代码精简到最简单的：
test.v
Require Import libtest.
Lib/libtest.v
<empty file>
如果这很重要，我已经在每个环境中重新编译了（空）库文件 libtest.v。
$ cd Lib
$ coqc libtest.v
$ cd ..
非常感谢任何帮助。
以下适用于我（我使用的是 Coq 8.5pl3）。
让我们编译我们的库，把它放在 Lib 命名空间中：
$ pwd
<...>/libtest-question
$ cd Lib
$ coqc -R . "Lib" libtest.v
$ cd ..
然后我们修改我们的test.v:
$ cat test.v
Require Import Lib.libtest.
并用
加载它$ coqtop -R Lib Lib -l test.v
-Q 开关也可以，有关详细信息，请参阅参考手册的 §14.3.3。
确实，-I 的行为在 8.4 和 8.5 之间发生了变化。在 Coq 的 changelog 中，我们可以找到 an interesting line. As hinted in the changelog and as advised by the -R 代替。