定理証明支援系 matita のdockerイメージを作った
Matitaという定理証明系のdockerイメージを作りました。
MatitaはBologna(ボローニャ)大学で作られた、OCaml(+lablgtk)製の、依存型に基づく定理証明器です。
Leanの論文から参照されていたので知りました。
定理証明器の研究用途に作成されたようなので実用するものでは無さそうですが*1、検証器の実装に興味がある人には面白そうです。
最新版にはパッケージが無いようですし、ビルドも面倒なのでdockerイメージを作りました。 > eldesh/matita
使い方
$ docker pull eldesh/matita:0.99.3
IDEとして使用するため環境変数DISPLAYを指定して起動します。
# /usr/local/matita/matitacというのがCLIを提供するようですがよく分かりません*2。
$ docker run -it --rm -e DISPLAY=192.168.1.2:0 eldesh/matita:0.99.3
使い方を知るには/usr/local/matita/lib/tutorialにチュートリアルがあるのでこれを読むと良さそうです。
SMLUnitのインストールを通してSML/NJ向けのライブラリのインストール方法を解説する
SML/NJにはCM(CompilationManager)というビルドツールが付いてきます。
以前は基本的な使い方を書きました>CompileManager(SML用make)の使い方。今回の記事ではSMLUnitというユニットテストライブラリを例にCMで管理するライブラリのインストール方法を説明します。
SMLUnitのインストール
SMLUnitというSML向けのユニットテストライブラリがあります*1。
このライブラリをSML/NJから使う際は以下のようにインストールします*2。
# 新 $ LOCAL_LIB=~/.smlnj/lib $ mkdir -p $LOCAL_LIB $ echo 'CM.stabilize true "smlunitlib.cm";' | sml $ echo "smlunitlib.cm $LOCAL_LIB/smlunitlib.cm" >> ~/.smlnj-pathconfig $ mkdir -p $LOCAL_LIB/smlunitlib.cm $ cp -R .cm $LOCAL_LIB/smlunitlib.cm/.cm
上記のインストール方法は私がここ数日で見直したモノで、以前は以下の手順でした。
# 旧 $ SMLNJ_ROOT=<SML/NJをインストールした場所> $ echo 'CM.stabilize true "smlunitlib.cm";' | sml $ echo "smlunitlib.cm smlunitlib.cm" >> $SMLNJ_ROOT/lib/pathconfig $ mkdir -p $SMLNJ_ROOT/lib/smlunitlib.cm $ cp -R src/main/.cm $SMLNJ_ROOT/lib/smlunitlib.cm/.cm
pathconfigファイルの詳細は後述しますが、ライブラリの配置場所を指定しています。
以前と違って新しい方法では処理系がインストールされたディレクトリやそれ以下のファイル($SMLNJ_ROOT/lib/pathconfig)を書き換える必要がありません。
見ての通りCMはビルド時に$HOME/.smlnj-pathconfigも読みに行くのです。非常に行儀が良くなりましたね。
Dockerイメージから使う
上記のような方法を採ると、ホスト側にライブラリをインストールしておき、それをDockerイメージから読み込むこともより簡単に出来ます。
例としてSMLUnitを上の方法でインストールした上で、それをDockerイメージから利用する方法を以下に示します。
$ ls ~/.smlnj/lib/ smlunitlib.cm $ docker run -it --rm -v $HOME:$HOME -e HOME=$HOME eldesh/smlnj:110.82 - CM.make "$/smlunitlib.cm"; (* ... snip ... *) - open SMLUnit; (* ... signatureだばー ... *)
出来ました。
しかし $HOME を差し替えているのが微妙に気持ち悪いですね?
実は CM_LOCAL_PATHCONFIG という環境変数で直接 pathconfig ファイルを指定することも出来ます!
$ docker run -it --rm -v $HOME:$HOME -e CM_LOCAL_PATHCONFIG=$HOME/.smlnj-pathconfig eldesh/smlnj:110.82 - CM.make "$/smlunitlib.cm"; (* ... snip ... *) - open SMLUnit; (* ... signatureだばー ... *)
やりました。
以上で真っ当にライブラリをインストール;利用出来る環境になりました。
CMの詳細な動作
CMはライブラリを探す際以下のように動作します。
- CM_PATHCONFIG が定義されていたらそれを読む
- CM_PATHCONFIG が定義されてなければ $SML_ROOT/lib/pathconfig を読む
- CM_LOCAL_PATHCONFIG が定義されていたらそれを読む
- CM_LOCAL_PATHCONFIG が定義されていなければ $HOME/.smlnj-pathconfig を読む
pathconfig ファイルはライブラリの名前とその場所を指定する設定ファイルで、構文と意味は以下の通りです。
- 行毎にファイル先頭から処理される
- 二つのトークンから成る行は '<ライブラリ名> <ライブラリパス>' と解釈され、エントリが追加される
- 一つのトークンのみから成る行は '<ライブラリ名>' と解釈され、その名前のエントリは削除される
- '-'(マイナス)のみの行はそれ以前の内容を全てリセットする
- 空行は無視される
#以上の内容は CM公式マニュアル §3.4 Anchor configurationに書いてあります。
まとめ
まとめると、SML/NJ向けのライブラリをインストールする際は以下のような手順で行うと良さそうです。
$ LOCAL_LIB=~/.smlnj/lib $ mkdir -p $LOCAL_LIB $ echo 'CM.stabilize true <インストールしたいライブラリのCMファイル>;' | sml $ echo "<インストールするライブラリ名> <インストール先>" >> ~/.smlnj-pathconfig $ mkdir -p <インストール先> $ cp -R .cm <インストール先>/.cm
*1:SML#には処理系本体に同梱されているのでそちらを使いましょう
*2:SMLUnit/readme.md Setup>SML/NJ参照
MLtonのdockerイメージを作りました
SMLの最適化コンパイラであるMLtonのDockerイメージを作りました。
MLtonは開発は行われているのですが、長らくリリースが出ていないため使いづらい状態です。あとなぜか私の手元だとビルドに失敗したりします*1。
そこで現状の開発ヘッドをビルドしたイメージを作りました。
- latest タグでgithubのmaster
- 20130715 タグが現状最新のリリース
に対応します。
使い方
一応使い方書きますと:
$ docker pull eldesh/mlton:latest
このように取得できます。
で、(例えば)以下のように実行します。
$ ls main.sml main.mlb $ docker run --rm -v `pwd`:`pwd` --workdir=`pwd` eldesh/mlton:latest -output main main.mlb $ ./main
*1:このイメージビルド時にはてきとーなパッチ当ててます
VeriFastのDockerイメージを作りました
C言語/Java検証器であるVeriFastのDockerイメージを公開しました。
> https://hub.docker.com/r/eldesh/verifast/
現時点(2017/8/24)での開発ヘッドをビルドしてあります*1。リリース版は公式サイトでバイナリが配布されているのでそちらを使いましょう。
このイメージはgitのコミットハッシュをタグにしてあり、latestタグは無いので明示的にこれを指定してDockerイメージを取得する必要があります。
つまり以下のようにすると
$ docker pull eldesh/verifast:93c7917
取得できます。
使い方
デフォルトではvfideというVeriFastのGUIフロントエンドが起動するので、以下のように環境変数 DISPLAY の設定が必要です。
// 例: ディスプレイ 192.168.1.2:0 を使う $ docker run -e DISPLAY=192.168.1.2:0 eldesh/verifast:93c7917
当然ながらverifastコマンドもインストールされているので、明示すれば使うことが出来ます。
// ボリューム some-vol にあるコードを検査
$ docker run -v some-vol:/src eldesh/verifast:93c7917 verifast /src/hoge.c
ついでにZ3サポートも付いています。
// SMTソルバとしてZ3を使う $ docker run -v some-vol:/src eldesh/verifast:93c7917 verifast -prover z3v4.5 /src/hoge.c
SML#3.3.0のDockerイメージを作った
Dockerの練習として SML#3.3.0 の入ったDockerイメージを作ってみました。> https://hub.docker.com/r/eldesh/smlsharp/
$ docker pull eldesh/smlsharp:3.3.0
とやれば使えるはず。ベースイメージは centos:centos7.3.1611 です。
LLVMのサイズが強敵でした。
使用例
$ sudo docker pull eldesh/smlsharp:3.3.0 Trying to pull repository docker.io/eldesh/smlsharp ... 3.3.0: Pulling from docker.io/eldesh/smlsharp 45a2e645736c: Already exists 85c1b05ddc2b: Pull complete 5112e2b943c9: Pull complete Digest: sha256:801b4d8f650ff25be594ecacab6029e6afc3992c3d4cebe8edc0454a1dde9ed3 $ sudo docker run -it --rm --name SMLSharp eldesh/smlsharp:3.3.0 SML# 3.3.0 (2017-06-20 18:17:19 JST) for x86_64-pc-linux-gnu with LLVM 3.7.1 # val puts = _import "puts" : string -> int; val puts = fn : string -> int # puts "Hello, SML#"; Hello, SML# val it = 12 : int
デフォルトで rlwrap 越しに起動するので
Dockerイメージのアップロードが謎の失敗
VMware Player上のCentOSからDockerHubへのDockerイメージのアップロードが謎の理由で失敗する。
当然 docker login 済み。
以下のようになる。
smlsharp-3.3.0$ sudo docker push eldesh/smlsharp:3.3.0 The push refers to a repository [docker.io/eldesh/smlsharp] 5216ccdd4424: Pushing [==================================================>] 549.2 MB bdc4c3dd2305: Layer already exists 34e7b85d83e4: Layer already exists unauthorized: authentication required
なぜ最後に認証情報を確認するんだろう…?
ともかくログは以下のようになっていた。
smlsharp-3.3.0$ cat /var/log/messages . . Aug 7 18:12:14 localhost kernel: XFS (dm-4): Unmounting Filesystem Aug 7 18:12:20 localhost dockerd-current: time="2017-08-07T18:12:20.802131012+09:00" level=error msg="Upload failed: unauthorized: authentication required" Aug 7 18:12:20 localhost dockerd-current: time="2017-08-07T18:12:20.804147067+09:00" level=error msg="Attempting next endpoint for push after error: unauthorized: authentication required" Aug 7 18:14:50 localhost dockerd-current: time="2017-08-07T18:14:50.518246440+09:00" level=info msg="{Action=auth, Username=eldesh, LoginUID=1000, PID=35534}" . .
VMの時刻が大幅に間違っているのを直したら正常に動作するようになった。
smlsharp-3.3.0$ date -s 2017/08/08 01:17:00 smlsharp-3.3.0$ docker push eldesh/smlsharp:3.3.0 The push refers to a repository [docker.io/eldesh/smlsharp] 5216ccdd4424: Pushed bdc4c3dd2305: Layer already exists 34e7b85d83e4: Layer already exists 3.3.0: digest: sha256:c5df978cac256fe7d605398051fd12705337c05fed10e1e2b5f8a1a39ef12775 size: 950 smlsharp-3.3.0$
時々この手のエラー踏むよね…。
ちなみに~/.docker/config.json を設定しろというissueが挙がってけど今回は無関係だった*1。
環境
*1:関係無いけどまさかパスワードを生で送ってるわけじゃないよね…?
ML勉強会#2 と ProofSummit2017 に参加した
ProofSummit2017とML勉強会#2に参加してきました。
とりあえず二日連続はつらいものがあった。
個々の感想
- SML#の話は良かった。言語や処理系の機能が列挙されていると個人的に楽しい。そういう意味ではATSも楽しいんだけど、機能(のアップデート)が少なかったし、楽しさの半分は岡部さん自身が面白いことに由来している気もする。
- autorewriteの話のストーリーが良かった。既存の部品を使って問題がうまく解決されている(と思う)。
- tanakaさんのCoqの話は楽しいような気がした。でもtrusted baseが小さいという主張はなんかだまされた感がある。(C側の実装をVeriFastで検証しませう?)
- パワーの溢れる若者が機械学習で自動証明の話をしていた。まだちょっと無理がある印象。証明戦略の選択をする話とかはまずSMTソルバとかでやってみてうまくいくことを確認してからでもいいんじゃないかという気がした。まぁ研究は野心的なことをやるべきなのかも知れないけど。そういえば発表中に出て来たものはほとんど対象がHOLだったし、自動化し易いのかな。
全体の感想
- 発表にはストーリーがある(かつ明確な)方が良い。どこが主張で、今どの辺について喋ってるのか分からないとつらい。どの辺が重要なのか判定不能なので一瞬でも聞き逃すとリカバリ不能になる(というかする気がなくなる_(:3」∠)_。例えばコード生成について話してるけど、それ以降で高階型推論についての考察が始まるのか、シンタックスについてのコダワリが語られるのか、生成系の証明が始まるのかで注視するとこが違ってくる。聞きながらググるべき事の選定にも効いてくる(かも知れない)。
- 特にそれが有名で無い場合は、紹介or提案or実装している言語or処理系or論理体系の大雑把な能力の説明があった方が良い。命題論理か述語論理か、一階か高階か、コンパイラかインタプリタか、型推論は完全性を持つのかなどなど。
- あと発表と無関係だけどJavaScriptへの殺意が高まった