CODEWITHSUNDEEP
windowscompilationcoqcoqide
LDCE
LDCE

Reputation: 11

CoqIDE in Windows will not compile

For some reason, my Coq file will not compile. I am using CoqIDE on Windows 10. When I use the Compile->Compile buffer tool, I get

enter image description here

On the other hand, when I use the Compile->Make tool, I get

enter image description here

The entire code for the file is given in the picture. It is also included below. Is there something it is missing? I looked high and low for some explanation of what was going on. All I found was this ominous statement from the Coq GitHub page:

"It is far from an easy task to compile Coq on Windows. Do not attempt unless you are a real Windows guru. If you need to work with non-released versions of Coq, or if you simply want to make your life easier, you may consider installing Coq into a virtualized Linux, as described below."

    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.

Upvotes: 0

Views: 581

Answers (1)

user138737
user138737

Reputation: 296

Compiling a Coq program is verifying the proof. Often the compiled proof is never "run" like most other languages, it is just checked if it compiles, and it seems like your code does compile.

The message you found on Github is talking about compiling the Coq binaries, not a Coq source file like you are doing.

Upvotes: 1

Related Questions