Coq: zarządzanie LoadPath w projekcie z podkatalogów

Question

Mam projektu Coq z jego bibliotek organizowanych do podkatalogów, coś jak:

…/MyProj/Auxiliary/Aux.v 
…/MyProj/Main/Main.v (imports Auxiliary/Aux.v) 

Kiedy skompilować pliki, spodziewam się, aby to zrobić z katalogu roboczego MyProj (przez plik Makefile). Ale chcę także pracować nad plikami przy użyciu Proof General/Coqtop, w którym to przypadku katalog roboczy jest domyślnie katalogiem, w którym plik się znajduje.

Ale to oznacza, że ​​ścieżka ładowania różni się między tymi dwoma kontekstami, więc logiczna ścieżka potrzebna do importu biblioteki jest inna. Jak skonfigurować wywołanie coqc, ścieżkę LoadPath i deklaracje importu, aby działały w obu kontekstach?

Każde podejście, które próbowałem, coś poszło nie tak. Na przykład, jeśli mogę skompilować Aux.v powołując

coqc -R "." "MyProj" Auxiliary/Aux.v 

i zaimportować go w Main.v jak

Require Import MyProj.Auxiliary.Aux. 

wtedy działa, kiedy skompilować Main.v z

coqc -R "." "MyProj" Main/Main.v 

ale nie w Coqtop, z Error: Cannot find library MyProj.Auxiliary.Aux in loadpath. Z drugiej strony, jeśli przed Require Import dodam

Add LoadPath ".." as MyProj. 

wtedy działa w Coqtop, ale nie pod coqc -R "." "MyProj" Main/Main.v z

Error: The file […]/MyProj/Auxiliary/Aux.vo contains library 

MyProj.Auxiliary.Aux i MyProj.MyProj.Auxiliary nie biblioteka .Aux

Szukam rozwiązania odpornego na bibliotekę, która jest udostępniana współpracownikom (i miejmy nadzieję, że ostatecznie z użytkownikami), więc w szczególności nie może korzystać z bezwzględnych ścieżek plików. Najlepszym znalazłem teraz jest dodanie Emacs zmiennych lokalnych ustawić LoadPath się, gdy przywołuje Dowód Ogólne Coqtop:

((coq-mode . ((coq-prog-args . ("-R" ".." "MyProj" "-emacs"))))) 

ale to (a) wydaje się nieco hacky, oraz (b) działa tylko na dowód generalnego , nie w Coqide lub zwykłym Coqtop. Czy istnieje lepsze rozwiązanie?

Answer 1

Wiem, że wyraźnie prosiłeś o coś, co działa na różnych platformach, ale istnieje już rozwiązanie specyficzne dla Proof-General, które jest mniej hakerowskie niż to, które masz. Dowódca generalny has a special variable o nazwie coq-load-path, który można ustawić za pomocą zmiennych lokalnych, podobnie jak w przypadku coq-prog-args. Zaletą jest to, że nie musisz się martwić o żadne inne argumenty, które należy przekazać do coqtop (np. -emacs w twoim przykładzie). Zatem plik .dir-locals.el może mieć linię:

((coq-mode . ((coq-load-path . ((".." "MyProj")))))) 

Niestety, nie jestem świadomy wszystkiego, co działa na różnych platformach, chociaż jestem pewien, że coś specyficzne dla CoqIDE musi istnieć. Jeśli tak jest, może mógłbyś skonfigurować skrypt, aby zachować te pliki konfiguracyjne na różnych platformach?

Answer 2

Jeśli używasz coq_makefile, możesz zainstalować bibliotekę w swoim systemie.

Bez OPAM

Aby zainicjować projekt:

coq_makefile -f _CoqProject -o Makefile 

udostępnić bibliotekę z innymi projektami:

make install 

Z OPAM

Zakładając zainstalowaniu OPAM, można użyj coq-shell, aby pomóc ci zająć się zależnościami.

Aby skonfigurować Twój projekt:

coq_shell_url="https://raw.githubusercontent.com/gares/opam-coq-shell/master/src/opam-coq" 
curl -s "${coq_shell_url}" | bash /dev/stdin init 8.4 # Install Coq and its dependencies 
eval `opam config env --switch=coq-shell-8.4`   # Setup the environment 
coq_makefile -f _CoqProject -o Makefile    # Generates the makefile 
opam pin add coq:YOURLIBRARY .      # Add your library to OPAM 

Po zaktualizowaniu biblioteki należy zrobić:

opam upgrade coq:YOURLIBRARY 

Oto przykład projektu, który wykorzystuje metodę OPAM:

https://bitbucket.org/cogumbreiro/aniceto-coq/src

Answer 3

Pozwól mi zadać pytanie krok po kroku g alternatywny proces, o którym wspomniał Tiago.

Zakładając, że drzewo swój projekt wygląda tak:

MyProj/Auxiliary/Aux.v 
MyProj/Main/Main.v 

W MyProj, zapisz plik _CoqProject listę wszystkich plikami Coq

-R . ProjectName 
Auxiliary/Aux.v 
Main/Main.v 

Po otwarciu jednego z tych plików Coq, Emacs poszukaj projektu _CoqProject i rzeczy do zrobienia (tm).

Jak pokazuje Tiago, coq_makefile dostarczy również plik Makefile za darmo.