Coqのソースコードをコンパイル

Coqでいろいろ作ってみたり、証明をしてみたりできたら、そのとき入力したコマンドやタクティックをファイルに保存してみよう。
ファイル名は〜.v というふうにドットvで終わるようにしよう。これでCoqのソースファイルは完成だ！
じゃあ、そのソースファイルをコンパイルしてみよう。Coqでは coqc という命令で、ソースファイルをコンパイルすることができる。ソースファイルは並べて複数個コンパイルすることができる。このとき、エラーが何も出てこなかったらコンパイル成功だ！Coqはその厳密さ故にコンパイルチェックが非常に厳しいので注意しよう。
コンパイルの例

/yoshihiro$ coqc mylemmas.v simplelambda.v

ここで、もし、ソースファイルの中でExtractionを使っていたら、OCamlのコードが出力される。今度はそれをOCamlでコンパイルしてみよう。

/yoshihiro$ ocamlc simplelambda.ml

これはCoqに対して、OCamlがバーチャルマシンになっていると思うことができる。
Javaで例えるならばjavacがcoqcでocamlc(もしくはocamlopt)がjavaなのだ。