Search code examples
command-linecoq

Human readable Coq output from command line

I'm invoking Coq from command line on this simple input file:

$ cat AddingZero.v
Theorem plus_O_n : (forall n, O + n = n).
Proof.
  intros n.
  simpl.
  exact (eq_refl n).
Qed.

Here's how I do it:

$ coqc ./AddingZero.v ; echo $?
0

When I see the 0 output I know things went OK, so I try to examine the output of Coq by doing:

$ vim ./AddingZero.vo

But I get some binary gibberish with that. What am I doing wrong? thanks!

Solution

  • .vo are compiled .v file. They are not for human consumption.

    The typical way to interact with a Coq file is to open it in a text editor with support for Coq (e.g. coqide, emacs with proofgeneral) and to step through the proof.

    Alternatively, you can use a tool like proviola to generate an html+js file which will show the statements, the proofs and all the intermediate states the prover is in after each proof step.