なぜcoqideで_CoqProjectを使って `make 'するのがコマンドラインで` coqc`と違うのですか？

Question

私は2つの短いファイルを持っている：cc_testが Lemma cc: 4 = 4. Proof. auto. Qed. によって与えられ、libtestは私が実行 Require Import cc_test. Check cc.

で与えられる ディレクトリ内coqc -R . ClosureLib -top ClosureLib cc_test "/ホーム/バリー/ SVN /コック/ Closure_Calculus" と coqc -R "/home/barry/svn/Coq/Closure_Calculus" ClosureLib libtestそのディレクトリ内 、（-Rから最後まで）上記coqcする引数は_CoqProjectファイルに配置されているとき、私は、しかし、期待される出力 cc: 4 = 4

を取得S、と私はcoqideメニューからMake makefile、その後Makeを呼び出し、cc_testは大丈夫ですが、libtest利回り出力 File "./libtest.v", line 1, characters 15-22: Error: Unable to locate library cc_test.

は、どのように私はこの仕事をするために、プロジェクトファイルを変更する必要がありますか？

コメント：coqリファレンスマニュアル（第15章）では、これらのアプローチの違いについては言及していません。また、引数 "-top ClosureLib" はコマンドラインのアプローチでは必要なようですが、makeを使用しているようには見えません。他の実験では、Top.fooが見つかったがClosureLib.foo 。

Answer 1

まず、-top ClosureLibはここでは役に立たないと思います。 documentationは、トップレベルのモジュール名はあなたの主な質問については、出力ファイル

の 名前から推測されるように、私は私の解決策を認めなければならないcoqcため-topない

として有効を説明しインストールすることです

coq_makefile -f _CoqProject -o Makefile 
make 
make install 

make installを使用して依存関係は、user-contribに、彼らは自動的に読み込まれます場所をライブラリを置きます。その後、Requireを直接使用することができます。

EDIT：@ Zimm48に

おかげで、私は最初の依存関係をインストールすることなく、同じタスクを実行するために$COQPATHの使用方法を理解していました。しかし、フォルダの名前は論理プレフィックスとして使用されるので、-Rまたは-Q引数と同じ識別子とディレクトリ名を使用する必要があります。

私は次のようなアーキテクチャを使用することをお勧め：_CoqProjectは

が含まれている、ディレクトリ /home/barry/svn/Coq/ClosureLibで

• を（その名前が-Rに渡された識別子と同じになるように、私はディレクトリの名前を変更していることに注意してください）

  -R . ClosureLib 
  cc_test.v 
  

  cc_testをコンパイルします。V次のように次のようにlibtest.vを含むディレクトリ内

  coq_makefile -f _CoqProject -o Makefile 
  make 
  

• を、_CoqProjectが

  -R . MyLib 
  libtest.v 
  

  が含まれているあなたはlibtest.vをコンパイルすることができます。

  coq_makefile -f _CoqProject -o Makefile 
  COQPATH=/home/barry/svn/Coq make