Matitaという定理証明系のdockerイメージを作りました。 MatitaはBologna(ボローニャ)大学で作られた、OCaml(+lablgtk)製の、依存型に基づく定理証明器です。 Leanの論文から参照されていたので知りました。 定理証明器の研究用途に作成されたようなので実用…

SML/NJにはCM(CompilationManager)というビルドツールが付いてきます。 以前は基本的な使い方を書きました>CompileManager(SML用make)の使い方。今回の記事ではSMLUnitというユニットテストライブラリを例にCMで管理するライブラリのインストール方法を説明…

SMLの最適化コンパイラであるMLtonのDockerイメージを作りました。MLtonは開発は行われているのですが、長らくリリースが出ていないため使いづらい状態です。あとなぜか私の手元だとビルドに失敗したりします*1。 そこで現状の開発ヘッドをビルドしたイメー…