由于某种原因，我的 Coq 文件无法编译。我在 Windows 10 上使用 CoqIDE。当我使用该Compile->Compile buffer工具时，我得到
另一方面，当我使用该Compile->Make工具时，我得到
文件的完整代码在图片中给出。它也包括在下面。它缺少什么吗？我四处张望，想知道发生了什么。我发现的只是 Coq GitHub页面上的这个不祥的陈述：
“在 Windows 上编译 Coq 绝非易事。除非你是真正的 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.