2014-09-01から1ヶ月間の記事一覧

チャットでも証明が書きたい

チャット上で証明が書けたら面白そうだなと思ったので、ProveEverywhere のサーバを使う hubot スクリプトを書きました。 こんなかんじ。 導入方法 (hubot 自体の導入方法については他の記事に任せます) 適当なサーバに Coq 8.4 以上をインストールします。 …

なつやすみのにっき

夏休みです。 Coq Summer School 8月の終わりに NII Shonan School on Coq に行ってきました。 一週間みっちりCoq漬けでした。楽しかった。でも英語ができればもっと……。 夏ゼミ Coq合宿が終わった3日後から2泊3日の研究室合宿がありました。千葉の館山に行…

homebrew で MathComp を入れる

追記 2015/11/11 今だったら公式の opam リポジトリから入れたほうが簡単にマルチコアを使えて速いし安心だと思います。 opam repo add coq-released https://coq.inria.fr/opam/released # opam に Coq 関連のライブラリを追加 opam install -j4 coq.8.4.6 …