見つけることができませんライブラリ

Question

それは別のに失敗しながら、同じLinuxコマンドは、1つの環境で成功する：

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

雨の源は成功です：

$ 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を変更してみましょう：-Qスイッチがあまりにもうまくいく

$ cat test.v 
Require Import Lib.libtest. 

をして

$ coqtop -R Lib Lib -l test.v 

でそれを読み込みます詳細については、リファレンスマニュアルの§14.3.3を参照してください。