読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

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

Coq入門 Extraction

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なのだ。