無法找到庫

Question

相同的Linux命令在一個環境中成功，而失敗的另一個：

$ coqtop -lv test.v -I Lib 

我得到的失敗是Debian下拉伸和勒柯克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. 

環境下的相同命令有關的s AME源成功是：

$ 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 .. 

任何幫助感激不盡。

Answer 1

確實，-I的行爲在8.4和8.5之間變化。在Coq的更新日誌中，我們可以找到an interesting line。正如變更日誌中暗示的那樣，並且根據other answer的建議，您可以改爲使用-R。

Answer 2

以下這些適用於我（我正在使用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瞭解更多詳情。