私は、Ubuntu 17.04にCoq 8.6を新しくインストールしました。 makeを使ってプロジェクトをコンパイルしようとすると、最初のエラーメッセージが出るまでうまく動作します。そして、このように、私は、エラーを見つけて修正するためにCoqIDEを使用しようと、私は新しいエラーメッセージが出ます：LinuxのCoqIDE設定
「ファイルfoo.voは、ライブラリTop.fooとライブラリではないのfooが含まれている」
私の推測CoqIDEの設定に何か問題がありますが、それが何であるか分かりません。何かヒント？
ありがとうございます。 Marcus。
は、私はあなたが今、「あなたは、引数ここ
-Q . Top
与えるTop名前空間に現在のディレクトリ.内のファイルをマップするには、ファイルfoo.vo
のディレクトリにされて立っていることを推測します完全な "例です。
mkdir test; cd test
echo 'Definition a:=1.' > foo.v
coqc -Q . Top foo.v # this puts the foo module into Top as Top.foo.
coqtop -Q . Top
Coq < Require Import Top.foo. Print a.
a = 1
: nat
それが失敗したコンパイルされたに名前空間に.voをマッピングすることなく、coqtopを使用して：
coqtop
Coq < Require foo.
> Require foo.
> ^^^^^^^^^^^^
Error: The file /.../test/foo.vo contains library Top.foo
and not library foo
ありがとうございました。 _CoqProjectという名前のファイルを、スクリプトに-Rを付けたフォルダに追加しました。トップ、今はすべて正常に動作します。それにもかかわらず、私はWindowsでこれを行う必要はなかったので、これはLinuxに特有のものだと思います。 – Marcus
あなたfoo.vはあなたのCoqIDEが使用するもの以外のフラグやパスでコンパイルされました。ファイルを再コンパイルするか、コンパイル時に使用したのと同じフラグをCoqIDEに使用させてください。関連するフラグは-R、-I、-Qフラグですと思います。場合によっては、これらのフラグ（パスを名前空間にどのようにマップするかを指定する）は '_CoqProject'ファイルで設定し、エディタに自動的に読み込むことができます。 – larsr