coqide - kann keine Module aus demselben Ordner laden

Question

Ich kann keine Module laden, die sich in CoqIde in demselben Ordner befinden.

Ich versuche Quellen von Software Foundations zu laden, ich bin mit coqide in Ordner, SF Quellen mit coqide oder coqide ./ enthält, dann nach dem Öffnen der Datei und ausgeführt wird, erhalte ich diese Fehlermeldung:

Error: Cannot find library Poly in loadpath 

in dieser Zeile:

Require Export Poly. 

und es für alle anderen require Befehle gleiche.

Also, wie Sie Leute laden Programme von SF in Coqide?

Answer 1

Sie müssen die .v-Dateien in .vo-Dateien kompilieren und ihr Verzeichnis zu Ihrem Ladepfad hinzufügen, wenn Sie sie benötigen. Führen Sie coqc <file-path> in der Eingabeaufforderung aus, um sie zu kompilieren. Um das Verzeichnis der Dateien zu Ihrem Ladepfad in CoqIde hinzuzufügen, können Sie am Anfang der .v-Dateien die Zeile Add LoadPath "<directory-path>". einfügen.

Answer 2

Ich weiß, dies ist ein alter Thread, aber es gibt nicht viele Ressourcen für dieses Problem. Ich habe gerade etwas Zeit damit verbracht, es zu lösen, also dachte ich, es wäre gut, es beim ersten Thema, das ich vom Googlen bekommen habe, zu posten. Ich verwende Coq 8.4p16 kompiliert ohne zusätzliche Konfiguration auf Arch Linux.

Also, das Handbuch sagt Variablen wie $COQPATH, ${XDG_DATA_DIRS}/coq/ und ${XDG_DATA_HOME}/coq/ sind überprüft, aber ich hatte kein Glück mit denen.

Ich habe auch versucht, coqc -I /folder/path die Edit->Preferences->Externals von CoqIde, aber immer noch kein Glück dort.

Ich schreibe diese, wie sie für jemanden arbeiten können.

Der einzige GLOBALE Weg, der für mich funktioniert, ist das Schreiben einer Coqrc-Datei mit Add LoadPath "<directory-path>". darin. Unter Linux muss sich die Datei im Home-Ordner befinden.

Hoffe das spart jemand Zeit.

Answer 3

Wenn Sie Ihre file.v mit Module file. gestartet haben nur loswerden (Auch loswerden End file.) und Ihr Problem ist gelöst.

Answer 4

eine Quelldatei in coqtop, coqc, CoqIDE oder Proof General gibt es mehr Möglichkeiten, um in der Lage zu laden, wird ein Verfahren wie folgt:

Sie Code-Dateien für das Certified Programmierung betitelten Buch heruntergeladen haben Angenommen mit abhängigen Typen geschrieben von Adam Chlipala, die here verfügbar sind und extrahieren sie in einem Pfad, den wir CODEHOME nennen. Wie Sie diese erste Zeile gibt es in allen Quelldateien sehen Require Import Bool Arith List Cpdt.CpdtTactics.

erste Typen coqc -v in einer CLI (Command Line Interface), würde die Ausgabe so etwas wie The Coq Proof Assistant, version 8.4pl4 .... sein, dann eine Datei coqrc.8.4pl4 namens erstellen, sollte die Dateierweiterung im Einklang mit der Version der Coq, die Sie verwenden, in $ HOME/.config/coq-Verzeichnis, wenn es nicht existiert und schreiben Sie diese Zeile in Add LoadPath "CODEHOME/cpdt/src" as Cpdt . und das ist es.

Answer 5

dies nach: https://github.com/coq/coq/issues/3995#issuecomment-337530500

Verwenden coqc -R '' '' in CoqIDE funktioniert, obwohl Sie noch deps müssen zuerst kompilieren. Aber das frustrierendste ist, verwenden coqtop -R '' '' wird dazu führen, dass CoqIDE nicht gestartet werden konnte, musste ich $HOME/AppData/Local/coq/coqiderc bearbeiten (unter Windows), ändern Sie es zurück zu cmd_coqtop = "coqtop".