Help us understand the problem. What is going on with this article?

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

More than 5 years have passed since last update.

werckerCoq 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 もあります。

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

Why not register and get more from Qiita?
  1. We will deliver articles that match you
    By following users and tags, you can catch up information on technical fields that you are interested in as a whole
  2. you can read useful information later efficiently
    By "stocking" the articles you like, you can search right away
Comments
No comments
Sign up for free and join this conversation.
If you already have a Qiita account
Why do not you register as a user and use Qiita more conveniently?
You need to log in to use this function. Qiita can be used more conveniently after logging in.
You seem to be reading articles frequently this month. Qiita can be used more conveniently after logging in.
  1. We will deliver articles that match you
    By following users and tags, you can catch up information on technical fields that you are interested in as a whole
  2. you can read useful information later efficiently
    By "stocking" the articles you like, you can search right away
ユーザーは見つかりませんでした