wercker を使って Coq コードを CI する

wercker の Coq box をけっこう前に作っていたのでその紹介です。

wercker は Travis CI のような CI as a Service と呼ばれる類の Web サービスです。基本無料です。
wercker では任意のアプリケーションをインストールした環境 (box といいます) を自分で作ることができて、その環境を使って CI をすることができます。

使い方

1. GitHub または Bitbucket にリポジトリ (Private でも可) を作り、wercker にそのリポジトリを登録します。

2. Make というファイルを作り、下のように Coq ファイルの名前を書いていきます。

   • ファイル名は Make でなくてもいいのですが、Coq演習第7回 に「Makeという名前にすることが多い」と書いているとおり ssreflect やその他いろいろなライブラリで Make という名前を使っていたので、ここでも Make というファイル名にしています。
   • Make ファイルには本当はもっといろいろ書けるのですが、ここでは簡単のためファイル名を書くだけにしています。詳細については Coq Reference を参照してください。プラグインかつライブラリである ssreflect の Make ファイルも参考になると思います。

Make

A.v
B.v
C.v

3.リポジトリのトップに下のような wercker.yml というファイルを作ります。

wercker.yml

box: amutake/coq@0.0.2
build:
  steps:
    - script:
        name: build
        code: |
          coq_makefile -f Make -o Makefile
          make

こんなかんじに書くと、リポジトリにプッシュする度に wercker で自動的にビルドスクリプトが走ってコードをコンパイルしてみてくれます。Coq ではコンパイルが通る = 証明が正しいということ (Admitted とか使ってズルをしてたら別ですけど) なので、Coq の場合は GitHub や Bitbucket にプッシュすると自動でその証明が正しいかどうか確かめてくれるということになります。

こうしておくと、間違っておかしい証明をプッシュしたときにもすぐに気がつけますし、Coq の証明に Pull Request が来たときにも、その証明が正しいかどうかをチェックして結果を表示してくれたりするので嬉しいです。

また、実際に試してみてはいないのですが、頑張れば OCaml とかに抽出してビルドしてデプロイまでの一連の流れをすべて Wercker にやってもらう、みたいなこともできそうです。

ssreflect/mathcomp の box もあります。

たぶん便利なので使ってみてください。