Coq: gestire LoadPath in progetto con le sottodirectory

Question

Ho un progetto Coq con le sue librerie organizzati in sottodirectory, qualcosa di simile:

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

Quando compilo i file, mi aspetto di farlo dal directory di lavoro MyProj (via un makefile). Ma voglio anche lavorare sui file usando Proof General/Coqtop, nel qual caso la directory di lavoro è di default la directory in cui il file vive.

Ma ciò significa che il LoadPath è diverso tra i due contesti e pertanto il percorso logico necessario per l'importazione della libreria è diverso. Come si imposta la chiamata coqc, il LoadPath e le dichiarazioni di importazione in modo che funzionino in entrambi i contesti?

Ogni approccio che ho provato, qualcosa va storto. Per esempio, se compilo Aux.v invocando

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

e importarlo in Main.v come

Require Import MyProj.Auxiliary.Aux. 

allora questo funziona quando compilo Main.v con

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

ma non riesce a Coqtop, con Error: Cannot find library MyProj.Auxiliary.Aux in loadpath. D'altra parte, se prima della Require Import aggiungo

Add LoadPath ".." as MyProj. 

allora questo funziona in Coqtop, ma non riesce sotto coqc -R "." "MyProj" Main/Main.v, con

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

MyProj.Auxiliary.Aux e MyProj.MyProj.Auxiliary non biblioteca .

Sto cercando una soluzione che sia solida per una libreria condivisa con i collaboratori (e si spera eventualmente con gli utenti), quindi in particolare non può utilizzare percorsi di file assoluti. Il migliore che ho trovato per ora è quello di aggiungere emacs variabili locali per impostare la LoadPath quando invoca Prova Generale Coqtop:

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

ma questo (a) sembra un po 'hacky, e (b) funziona solo per prova generale , non in Coqide o semplice Coqtop. C'è una soluzione migliore?

Answer 1

So che hai chiesto esplicitamente qualcosa che funziona su piattaforme diverse, ma c'è già una soluzione specifica per Proof-General che è meno hacky di quella che hai. Proof General has a special variable chiamato coq-load-path che è possibile impostare con variabili locali, proprio come hai fatto per coq-prog-args. Il vantaggio è che non devi preoccuparti di altri argomenti che devono essere passati a coqtop (come ad esempio -emacs nell'esempio). Così, il file .dir-locals.el potrebbe avere una linea come questa:

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

Purtroppo, io non sono a conoscenza di tutto ciò che funziona su diverse piattaforme, anche se sono abbastanza sicuro che qualcosa di specifico per CoqIDE deve esistere. In questo caso, potresti creare uno script per mantenere questi file di configurazione aggiornati su piattaforme diverse?

Answer 2

Se si utilizza coq_makefile è possibile installare la libreria nel proprio sistema.

Senza OPAM

Per inizializzare il progetto:

coq_makefile -f _CoqProject -o Makefile 

Condividi la tua libreria con altri progetti:

make install 

Con OPAM

Supponendo di aver installato OPAM, è possibile usa coq-shell per aiutarti a prendersi cura delle dipendenze.

Per impostare il vostro progetto:

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 

Quando si aggiorna la libreria che si dovrebbe fare:

opam upgrade coq:YOURLIBRARY 

Ecco un esempio di un progetto che utilizza il metodo OPAM:

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

Answer 3

Consentitemi di fare un passo alla domanda da suggestin g un processo alternativo, suggerito da Tiago.

Supponendo che l'albero del progetto è simile al seguente:

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

In MyProj, scrivere un file _CoqProject che elenca tutti i tuoi file Coq

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

Quando si apre uno di questi file Coq, Emacs cercare il _CoqProject e fare-the-right-thing (tm).

Come mostrato da Tiago, coq_makefile ti darà anche un Makefile gratuitamente.