Coqide-Fehler: Kompilierte Bibliothek Basics.vo macht inkonsistente Annahmen über Bibliothek

Question

Ich verwende CoqIDE_8.4pl5 auf Mac OS X. Diese Fehlermeldung erscheint, wenn CoqIDE an diesen Befehl weiterleitet: Require Import Basics.

Fehler: Zusammengestellt Bibliothek Basics.vo macht inkonsistent Annahmen über Bibliothek Coq.Init.Notations

Ich habe nicht dieses Problem auf meinem alten Macbook Air, wenn ich CoqIDE_8.4pl5 wurde mit, aber wenn ich bekam ein neues MacBook Pro, und ich habe es erneut von der gleichen Website heruntergeladen. Aber diesmal auf diesem MacBook Pro, ich benutzte brew cask install coq, um es installiert zu bekommen ... aber es schien nicht zu funktionieren, also habe ich es von der Website heruntergeladen und legte meinen coqide Pfad auf den gleichen Weg wie in meinem alten Macbook Air .. und wenn ich versuche, meine Aufgaben weiterzuleiten, bekomme ich dieses Problem. Gibt es trotzdem etwas zu beheben? Oder muss ich Coq entfernen und kopiert und neu installieren?

Answer 1

Dies ist normalerweise ein Fall von Coq, der Ihnen mitteilt, dass die kompilierte Version von Basics.v (Basics.vo) mit einer anderen Version von Coq kompiliert wurde als die, die Sie gerade verwenden.

Aus Sicherheitsgründen möchte jede Coq-Version nur Dateien verwenden, die mit derselben Version kompiliert wurden.

Die Korrektur besteht normalerweise darin, die belastende Datei Basics.vo zu löschen und den Kompilierungsschritt, der sie erstellt hat, zu reproduzieren.

Wenn der Fehler erneut auftritt, kann es sein, dass auf Ihrem System zwei Versionen von Coq installiert sind, von denen eine von Ihrem Gebäudeskript erreicht wird, während die andere von CoqIDE verwendet wird.