coqide - nie można załadować modułów z tego samego folderu

Question

Nie mogę załadować modułów znajdujących się w tym samym folderze w CoqIde.

Próbuję załadować źródeł od fundamentów Software, biegnę coqide w folderze, który zawiera źródła SF coqide lub coqide ./, a następnie po otwarciu i uruchomieniu pliku, dostaję ten błąd:

Error: Cannot find library Poly in loadpath 

w tej linii:

Require Export Poly. 

i to samo na każdych innych require poleceń.

Więc jak ludzie ładują programy z SF do coqide?

Answer 1

Musisz skompilować pliki .v do plików .vo i dodać ich katalog do ścieżki ładowania, jeśli będziesz ich wymagać. Aby je skompilować, uruchom polecenie coqc <file-path> w wierszu polecenia. Aby dodać katalog plików do ścieżki ładowania w CoqIde, możesz wstawić wiersz Add LoadPath "<directory-path>". na początku plików .v.

Answer 2

Zdaję sobie sprawę, że jest to stary wątek, ale nie ma wielu zasobów na ten problem. Po prostu poświęciłem trochę czasu na rozwiązanie tego problemu, więc pomyślałem, że dobrze byłoby opublikować go na pierwszym temacie, który otrzymałem z googlowania. Używam Coq 8.4p16 skompilowanego bez dodatkowej konfiguracji na Arch Linux.

W podręczniku zaznaczono, że zmienne takie jak $COQPATH, ${XDG_DATA_DIRS}/coq/ i ${XDG_DATA_HOME}/coq/ są sprawdzone, jednak nie miałem z nimi szczęścia.

Próbowałem również umieścić coqc -I /folder/path w Edit->Preferences->Externals CoqIde, jednak wciąż nie ma szczęścia.

Piszę te, ponieważ mogą one pracować dla kogoś.

Jedynym sposobem GLOBAL, który działa dla mnie jest pisanie pliku coqrc z Add LoadPath "<directory-path>". w nim. W systemie Linux plik musi znajdować się w folderze domowym.

Mam nadzieję, że to kogoś oszczędza.

Answer 3

Jeśli uruchomiłeś swój file.v z Module file. po prostu się go pozbyć (również pozbyć się End file.) i twój problem został rozwiązany.

Answer 4

Aby móc załadować plik źródłowy w coqtop, coqc, CoqIDE lub Dowód Ogólne istnieje kilka sposobów, jednym ze sposobów jest następująca:

Przypuśćmy pobraniu plików kod na książce zatytułowanej Certyfikowany Programming z zależnymi typami napisane przez Adama Chlipala, które są dostępne here i wyodrębnić je w ścieżce, którą nazywamy KODEKSEM. Jak widać są to pierwsza linia w dowolnych plików źródłowych Require Import Bool Arith List Cpdt.CpdtTactics.

Pierwszy typ coqc -v w CLI (interfejs wiersza poleceń), wyjście byłoby coś The Coq Proof Assistant, version 8.4pl4 ...., a następnie utworzyć plik o nazwie coqrc.8.4pl4, rozszerzenie pliku powinno być zgodne z wersją używanego coq, w katalogu $ HOME/.config/coq, jeśli nie istnieje i wpisać w nim wiersz Add LoadPath "CODEHOME/cpdt/src" as Cpdt . i to wszystko.

Answer 5

Zgodnie z tym: https://github.com/coq/coq/issues/3995#issuecomment-337530500

Zastosowanie coqc -R '' '' pracuje w CoqIDE, choć trzeba jeszcze opracować deps pierwszy. Ale najbardziej frustrujące jest to, że użycie coqtop -R '' '' spowoduje, że CoqIDE się nie uruchomi, musiałem edytować $HOME/AppData/Local/coq/coqiderc (w Windows), zmienić go z powrotem na cmd_coqtop = "coqtop".