Błąd ścieżki ładowania CoqIDE dla ssreflect

Question

Jestem nowicjuszem Coq i dlatego chcę lepiej zrozumieć sprawdzanie dowodów Próbuję użyć biblioteki Ssreflect.

Zainstalowałem Ssreflect v 1.5 na Mac OS v 10.10.3 (Yosemite), który działa w Terminalu.

Jednak gdy próbowałem załadować biblioteki w CoqIDE 8.4p15 używając:

Require Import ssreflect. 

pojawia się błąd:

Cannot find library ssreflect in loadpath 

Próbowałem, używając:

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

gdzie SSRCOQ_LIB jest aktualnie ustawiony, ale pojawia się błąd:

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

Wdzięczny za pomoc w załadowaniu biblioteki ssreflect z poziomu CoqIDE.

Answer 1

Wielkie dzięki dla osób z Coq-Club Forum, którzy pomogli w rozwiązaniu tego problemu, a zwłaszcza Pierre Boutillier, który wskazał przyczynę problemu i dostarczył rozwiązanie.

Problemem było to, że miałem 2 kopie coqtop i 2 kopie standardowych bibliotek:

• jeden w/opt/local/bin/coqtop (co jest folder, w którym mój egzemplarz jest zainstalowany twój może w inny folder) i użyte do kompilacji ssreflect (I użyte MacPorts do zainstalowania coq).
• Jeden w /Aplikacje/CoqIDE_8.4pl5.app/Resources/bin/coqtop ładowany przez CoqIDE po dwukrotnym kliknięciu na aplikację (pobrałem ją ze strony internetowej Cog).

Dlatego też, gdy byłem w CoqIDE, wywoływano inną wersję coqopu niż tę, której używałem do kompilowania i instalowania biblioteki Ssreflect.

Rozwiązanie jest następujące:

• Podwójne kliknięcie na CoqIDE
• otworzyć preferencje w menu CoqIDE
• Set zewnętrznymi -> coqtop (lub może to być auto) na „/ opt/local/bin/coqtop "(lub gdziekolwiek twoja wersja jest zainstalowana) Zastosuj OK Zamknij.
• Zamknij i ponownie uruchom CoqIDE.

pomyślnie załadował bibliotekę Ssreflect zarówno przy użyciu coqtop w terminalu i CoqIDE używając:

Require Import ssreflect.