无法找到库

Question

同一个Linux命令在一个环境中成功,而在另一个环境中失败:

$ coqtop -lv test.v -I Lib

我得到的失败是Debian延伸和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 <     

所以我想弄清楚发生了什么,希望从这篇文章得到答案, 但无济于事.

为了这个问题,我将源代码简化为最简单的:

test.v

Require Import libtest.

LIB/libtest.v

<empty file>

如果这很重要,我已libtest.v在每个环境中重新编译(空)库文件.

$ cd Lib
$ coqc libtest.v
$ cd ..

感谢任何帮助.

Answer 1

实际上,行为-I在8.4到8.5之间变化.在Coq的更改日志中,我们可以找到一条有趣的线.正如在更改日志中暗示的那样,并且根据其他答案的建议,您可以使用-R.