Verify coq theorems in build script?

Question

I'm using coq to study the meta theory of a programming language.

Composing and verifying theorems interactively in the IDE is all well and good, but I need to automate (re)verification. I see the man pages, but I don't see this use case spelled out anywhere.

How can I incorporate coq verification into a build script?

Answer 1

If we have this metatheory/hello_world.v:

$ cat metatheory/hello_world.v
Theorem hello_world : forall a b:Prop, a /\ b -> b /\ a.
intros a b H.
split.
destruct H as [H1 H2].
exact H1. (* A bug: We actually need H2 here. *)
intuition.

Then we can see the error (with failing exit code) with:

$ coqtop -batch -silent -l metatheory/hello_world.v
Error while reading metatheory/hello_world.v:
File "/vagrant/metatheory/hello_world.v", line 5, characters 6-8:
Error: In environment
a : Prop
b : Prop
H1 : a
H2 : b
The term "H1" has type "a" while it is expected to have type
"b".

If we fix the problem:

$ coqtop -batch -silent -l metatheory/hello_world.v

..with a successful exit code.