Windows中的CoqIDE不会编译

Question

由于某些原因，我的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.

Answer 1

编译Coq程序是为了验证证据。通常，编译的证据永远不会像大多数其他语言那样“运行”，只是检查它是否编译，而且看起来您的代码确实编译了。

您在Github上找到的消息是关于编译Coq二进制文件的，而不是像您正在做的那样的Coq源文件。