coqchk.opt – Online in der Cloud

PROGRAMM:

NAME/FUNKTION

coqchk – Der Coq Proof Checker-Verifizierer für kompilierte Bibliotheken

ZUSAMMENFASSUNG

coqchk [ Optionen ] Module

BESCHREIBUNG

coqchk ist der eigenständige Prüfer für kompilierte Bibliotheken (von coqc erstellte .vo-Dateien) für
der Coq-Proof-Assistent. Weitere Informationen finden Sie im Referenzhandbuch. Es kehrt mit zurück
Exit-Code 0, wenn alle angeforderten Aufgaben erfolgreich waren. Ein Rückkehrcode ungleich Null bedeutet dies
Etwas ist schief gelaufen: Eine Bibliothek wurde nicht gefunden, der Inhalt ist beschädigt, Typprüfung
Ausfall usw.

Module ist eine Liste der zu prüfenden Module. Auf Module kann mit einem kurzen oder verwiesen werden
qualifizierter Name.

OPTIONAL

-I ist, --enthalten dir
Verzeichnis hinzufügen dir im Include-Pfad

-R dir coqdir
physikalische rekursiv abbilden dir zu logisch coqdir

-Leise
macht coqchk weniger ausführlich.

-zugeben Modulen
Markiert das angegebene Modul und alle seine Abhängigkeiten als vertrauenswürdig und wird dies nicht tun
erneut überprüft, es sei denn, dies wird ausdrücklich von anderen Optionen verlangt.

-norec Modulen
Gibt an, dass das angegebene Modul überprüft werden soll, ohne dass eine Überprüfung erforderlich ist
Abhängigkeiten.

-M, --Erinnerung
Zeigt eine Zusammenfassung des vom Prüfer verwendeten Speichers an.

-Ö, --output-context
Zeigt eine Zusammenfassung der überprüften logischen Inhalte an: Annahmen und
Verwendung von Unvorhersehbarkeit.

-Imprädikativ-Set
Ermöglicht dem Prüfer, Bibliotheken zu akzeptieren, die mit diesem Flag kompiliert wurden.

-v COQCHK-Version drucken und beenden.

-coqlib dir
überschreibt den Standardspeicherort der Standardbibliothek.

-wo Drucken Sie den Speicherort der Standardbibliothek von coqchk und beenden Sie ihn.

-H, --help
Liste der Optionen drucken

Verwenden Sie coqchk.opt online über die Dienste von onworks.net