coqide - impossibile caricare i moduli dalla stessa cartella

Question

Non riesco a caricare i moduli che si trovano nella stessa cartella in CoqIde.

che sto cercando di caricare le sorgenti da Software Foundation, sto correndo coqide nella cartella che contiene fonti di SF con coqide o coqide ./, poi dopo l'apertura e l'esecuzione del file, sto ottenendo questo errore:

Error: Cannot find library Poly in loadpath 

in questa linea:

Require Export Poly. 

ed è lo stesso per tutte le altre require comandi.

Quindi come si caricano i programmi da SF in coqide?

Answer 1

È necessario compilare i file .v in file .vo e aggiungere la directory al percorso di caricamento se si desidera richiederli. Per compilarli, eseguire coqc <file-path> nel prompt dei comandi. Per aggiungere la directory dei file al percorso di caricamento in CoqIde, è possibile inserire la riga Add LoadPath "<directory-path>". all'inizio dei file .v.

Answer 2

Mi rendo conto che questo è un thread vecchio, tuttavia non ci sono molte risorse su questo problema. Ho appena trascorso un po 'di tempo a risolverlo, quindi ho pensato che sarebbe stato utile pubblicarlo sul primo argomento che ho avuto da googling. Sto usando Coq 8.4p16 compilato senza alcuna configurazione aggiuntiva su Arch Linux.

Così, il manuale dice che le variabili come $COQPATH, ${XDG_DATA_DIRS}/coq/ e ${XDG_DATA_HOME}/coq/ vengono controllate, tuttavia non ho avuto fortuna con quelle.

Ho anche provato a inserire coqc -I /folder/path il Edit->Preferences->Externals di CoqIde, tuttavia, ancora senza fortuna lì.

Scrivo questi come potrebbero funzionare per qualcuno.

L'unico modo GLOBAL che funziona per me è scrivere un file coqrc con Add LoadPath "<directory-path>". in esso. Su Linux il file deve essere nella cartella home.

Spero che questo salvi qualcuno un po 'di tempo.

Answer 3

Se hai iniziato il tuo file.v con Module file. basta sbarazzarsi di esso (anche sbarazzarsi del End file.) e il problema è risolto.

Answer 4

Per essere in grado di caricare un file sorgente in coqtop, coqc, CoqIDE, o prova generale ci sono diversi modi, uno metodo è il seguente:

Supponiamo di avere scaricato i file di codice per il libro intitolato Programmazione Certificata con tipi dipendenti scritto da Adam Chlipala che sono disponibili here e li estrae in un percorso che chiamiamo CODEHOME. Come potete vedere ci sono la prima linea in tutti i file di origine Require Import Bool Arith List Cpdt.CpdtTactics.

tipo coqc -v Primo di una CLI (Command Line Interface), l'uscita sarebbe qualcosa di simile The Coq Proof Assistant, version 8.4pl4 ...., quindi creare un file chiamato coqrc.8.4pl4, l'estensione del file deve essere in accordo con la versione del coq che si sta utilizzando, nella directory $ HOME/.config/coq se non esiste e scrivere questa riga in esso Add LoadPath "CODEHOME/cpdt/src" as Cpdt . e il gioco è fatto.

Answer 5

Secondo questo: https://github.com/coq/coq/issues/3995#issuecomment-337530500

Usa coqc -R '' '' lavora in CoqIDE, anche se è comunque necessario compilare dipendenze prima. Ma la cosa più frustrante è, usare coqtop -R '' '' causerà l'avvio di CoqIDE, ho dovuto modificare $HOME/AppData/Local/coq/coqiderc (su Windows), cambiarlo di nuovo a cmd_coqtop = "coqtop".