Konfigurieren von Proof General für Coq in Emacs

2465
P basak

Ich habe Coq in meinem System über das Standardinstallationsprogramm installiert. Dann fügte ich meinen bestehenden Emacs Beweise hinzu. Aber das Problem ist, wenn ich versuche, einen Befehl in Emacs auszuführen, finde ich Folgendes von Emacs:

Suche nach Programm, keine solche Datei oder Verzeichnis coqtop

Ich glaube, es gibt einige Konfigurationsfehler.

Freue mich auf deine Gedanken.

4
Was Sie beschreiben, klingt wie eine grundlegende Situation, in der als Erstes geprüft werden muss, ob sich die Bibliothek in Ihrem Ladepfad befindet und ob diese Bibliothek am Ende mit einer Bereitstellungsanweisung versehen ist und ob in Ihrer Benutzerkonfigurationsdatei eine Anforderung enthalten ist. Normalerweise ordnen Sie dem Ladepfad ein Verzeichnis zu und platzieren die Bibliothek dort. In der Benutzerkonfiguration hat file eine Anweisung `(required '....)`. Solange sich die Bibliothek im Ladepfad befindet und eine Anweisung wie '(Bereitstellen' ...) 'vorhanden ist, reicht dies normalerweise aus, um Ladeprobleme zu lösen. lawlist vor 9 Jahren 0

2 Antworten auf die Frage

1
P basak

Ich habe gerade herausgefunden, dass ich den Pfad zum Coactop zum Emacs-Pfad hinzufügen muss. oder Sie können das in Ihrem Systempfad haben. In diesem Fall müssen Sie Emacs von der Shell aufrufen.

Hallo, ich bekomme die gleiche Fehlermeldung, obwohl ich Coq mit Homebrew auf einem Mac installiert habe. Könnten Sie möglicherweise näher erläutern, wie Sie den Pfad zum Emacs-Pfad hinzufügen können? Michael Bächtold vor 9 Jahren 1
Es wurde behoben, indem Folgendes zu .emacs hinzugefügt wurde: (benutzerdefinierte-set-variables '(coq-prog-name "PATH / TO / coqtop")' (proof-three-window-enable t)) Michael Bächtold vor 9 Jahren 1
Ich habe eigentlich nur Emacs von der Shell aus aufgerufen und erbt in diesem Fall die PATH-Variable der Bash. P basak vor 9 Jahren 0
1
dinosaur

Anders als beim OP, aber ein ähnliches Problem: Die Fehlermeldung Searching for program: no such file or directory, coqtopkann auch auftreten, wenn Sie coq nicht installiert haben. Dann coqtopfehlt der Befehl in Ihrem System.

Um zu diagnostizieren, rennen Sie which coqtop. Wenn das Ergebnis leer ist, ist es nicht installiert oder befindet sich nicht in Ihrem Pfad.

Auf dem Mac löste ich dieses Problem, indem coq mit der Installation von Homebrew mitbrew install coq

In der Frage heißt es * Ich habe Coq installiert *, dies ist also nicht das Problem. Toby Speight vor 7 Jahren 0
Wie gesagt, das unterscheidet sich vom Fall der OP. Diese Frage wird jedoch in den Suchergebnissen für `` `Suchen nach Programm, keine solche Datei oder Verzeichnis coqtop``` angezeigt. In vielen dieser Fälle ist diese Antwort hilfreich. dinosaur vor 7 Jahren 1

Verwandte Probleme