Lỗi tải đường dẫn CoqIDE cho ssreflect

Question

Tôi là người mới sử dụng Coq và do đó cải thiện sự hiểu biết của tôi về kiểm tra bằng chứng Tôi đang cố gắng sử dụng thư viện Ssreflect.

Tôi đã cài đặt Ssreflect v 1.5 trên Mac OS v 10.10.3 (Yosemite) chạy ở Thiết bị đầu cuối.

Tuy nhiên khi tôi đã cố gắng để tải thư viện vào CoqIDE 8.4p15 sử dụng:

Require Import ssreflect. 

tôi nhận được lỗi:

Cannot find library ssreflect in loadpath 

Tôi đã cố gắng sử dụng:

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

nơi SSRCOQ_LIB hiện được đặt nhưng tôi gặp lỗi:

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

Biết ơn vì bất kỳ trợ giúp nào trong việc tải thư viện ssreflect từ trong CoqIDE.

Answer 1

Cảm ơn mọi người về số Coq-Club Forum đã giúp giải quyết vấn đề này và đặc biệt Pierre Boutillier đã xác định nguyên nhân của sự cố và cung cấp giải pháp.

Vấn đề là tôi đã có 2 bản sao của coqtop và 2 bản sao của thư viện tiêu chuẩn:

• Một trong/opt/local/bin/coqtop (đó là thư mục nơi bản sao của tôi được cài đặt bạn có thể ở một thư mục khác) và được sử dụng để biên dịch ssreflect (I MacPorts đã sử dụng để cài đặt coq).
• Một trong /Ứng dụng/CoqIDE_8.4pl5.app/Resources/bin/coqtop được tải bởi CoqIDE khi nhấp đúp vào ứng dụng (tôi đã tải xuống từ trang web Cog).

Do đó khi tôi ở trong CoqIDE, nó đang gọi một phiên bản khác của coqtop so với phiên bản tôi đã sử dụng để biên dịch và cài đặt thư viện Ssreflect.

Giải pháp là như sau:

• Double click vào CoqIDE
• mở các ưu đãi trong menu CoqIDE
• Set Externals -> coqtop (hoặc nó có thể là AUTO) để "/ opt/local/bin/coqtop "(hoặc bất cứ nơi nào phiên bản của bạn được cài đặt) Áp dụng OK Đóng.
• Thoát và khởi động lại CoqIDE.

tôi nạp thành công thư viện Ssreflect cả sử dụng coqtop trong Terminal và CoqIDE sử dụng:

Require Import ssreflect.