По какой-то причине мой файл Coq не компилируется. Я использую CoqIDE в Windows 10. Когда я использую инструмент Compile->Compile buffer, я получаю
С другой стороны, когда я использую инструмент Compile->Make, я получаю
Полный код файла представлен на картинке. Это также включено ниже. Что-то не хватает? Я смотрел высоко и низко в поисках объяснения того, что происходило. Все, что я нашел, это зловещее заявление из Coq GitHub страница:
«Скомпилировать Coq для Windows - далеко не простая задача. Не пытайтесь, если вы не являетесь настоящим гуру Windows. Если вам нужно работать с невыпущенными версиями Coq, или если вы просто хотите облегчить себе жизнь, вы может рассмотреть возможность установки Coq в виртуализированный Linux, как описано ниже ».
Module No1.
(*We first give the axioms of Principia
for the propositional calculus in *1.*)
Axiom MP1_1 : forall P Q : Prop,
(P -> Q)->P -> Q. (*Modus ponens*)
(*I did not bother with *1.11, which is
MP for propositions containing variables.*)
Axiom Taut1_2 : forall P : Prop,
P \/ P-> P. (*Tautology*)
Axiom Add1_3 : forall P Q : Prop,
Q -> Q \/ P. (*Addition*)
Axiom Perm1_4 : forall P Q : Prop,
P \/ Q -> Q \/ P. (*Permutation*)
Axiom Assoc1_5 : forall P Q R : Prop,
P \/ (Q \/ R) -> (P \/ Q) \/ R.
Axiom Sum1_6: forall P Q R : Prop,
(Q -> R) -> (Q \/ R -> P \/ R).
(*These are all the propositional axioms
of Principia Mathematica.*)
End No1.
