7

私は Coq 初心者なので、プルーフ チェックの理解を深めるために、Ssreflect ライブラリを使用しようとしています。

ターミナルで動作する Mac OS v 10.10.3 ( Yosemite ) に Ssreflect v 1.5 をインストールしました。

ただし、次を使用してライブラリを CoqIDE 8.4p15 にロードしようとしたとき:

Require Import ssreflect.

エラーが発生します：

Cannot find library ssreflect in loadpath

私は使用してみました：

Add LoadPath "/opt/local/lib/coq/user-contrib/Ssreflect/".

SSRCOQ_LIB は現在設定されていますが、次のエラーが表示されます。

The file /opt/local/lib/coq/user-contrib/Ssreflect/ssreflect.vo contains library Ssreflect.ssreflect and not library ssreflect

CoqIDE 内から ssreflect ライブラリをロードする際の助けに感謝します。

4

1 に答える 1

8

この問題を解決してくれたCoq-Club フォーラムの人々、特に問題の原因を突き止めて解決策を提供してくれた Pierre Boutilier に感謝します。

問題は、coqtop の 2 つのコピーと標準ライブラリの 2 つのコピーがあったことです。

  • /opt/local/bin/coqtop (これは、私のコピーがインストールされているフォルダーで、別のフォルダーにある可能性があります) にあり、ssreflect のコンパイルに使用されます (MacPorts を使用して coq をインストールしました)。
  • /Applications/CoqIDE_8.4pl5.app/Resources/bin/coqtop にあるもので、アプリをダブルクリックすると CoqIDE によって読み込まれます (Cog Web サイトからダウンロードしました)。

したがって、私が CoqIDE を使用していたとき、Ssreflect ライブラリのコンパイルとインストールに使用したものとは異なるバージョンの coqtop を呼び出していました。

解決策は次のとおりです。

  • CoqIDEをダブルクリック
  • CoqIDE メニューで設定を開きます
  • Externals -> coqtop (または AUTO の場合もあります) を "/opt/local/bin/coqtop" (またはバージョンがインストールされている場所) に設定します。 OK を適用して閉じます。
  • CoqIDE を終了して再起動します。

ターミナルでcoqtopを使用し、次を使用してCoqIDEを使用して、Ssreflectライブラリを正常にロードしました。

Require Import ssreflect.
于 2015-06-12T18:49:49.287 に答える