Errore Coqide: libreria compilata Basics.vo fa presupposti incoerenti sulla libreria

Question

sto usando CoqIDE_8.4pl5 su mac os X. Questo messaggio di errore compare quando CoqIDE inoltra a questo comando: Richiedi Nozioni di base sull'importazione.

Errore: Compilato biblioteca Basics.vo formula ipotesi inconsistenti oltre biblioteca Coq.Init.Notations

Non ho avuto questo problema sul mio vecchio MacBook Air quando stavo usando CoqIDE_8.4pl5, ma quando sono arrivato un nuovo MacBook Pro, e l'ho scaricato di nuovo dallo stesso sito web. Ma questa volta su questo macbook pro, ho usato brew cask install coq per installarlo ... ma sembrava non funzionare, così l'ho scaricato dal sito web e ho impostato il mio percorso coqide allo stesso percorso che era nel mio vecchio macbook air .. e quando provo ad inoltrare i miei compiti, ottengo questo problema. C'è un modo per risolvere questo problema? o devo rimuovere coq e copiato e reinstallarlo?

Answer 1

Questo è in genere un caso di Coq che dice che la versione compilata di Basics.v (Basics.vo) è stata compilata con una versione di Coq diversa da quella attualmente in uso.

Per motivi di sicurezza, ogni versione di Coq richiede solo i file compilati con la stessa versione.

La correzione consiste in genere nell'eliminare il file Basics.vo compromettente e riprodurre il passaggio di compilazione che lo ha creato.

Se l'errore si ripresenta, è possibile che il sistema abbia due versioni di Coq installate, una delle quali viene raggiunta dallo script dell'edificio, mentre l'altra viene utilizzata da CoqIDE.