RustBeltのビルド (Windows)

概要: Coqと高階分離論理を用いたRustの検証プロジェクトであるRustBeltの論文とCoqの証明ファイルが公開されたので、とりあえずビルドしてみた。

RustBeltはopamを使うと簡単にビルドできるようだが、ここではWindowsでビルドしてみた。

環境

• 64bit Windows
• MSYS2

gitとmakeのインストール

$ pacman -S make git

Coqのインストール

CoqのWebサイト から coq-installer-8.6-x86_64.exe をダウンロードし、実行する。今回はデフォルトのディレクトリ C:\Coq にインストールした。

/c/Coq/bin ã‚’PATHに追加する。例えば .zshrc に

export PATH="${PATH}:/c/Coq/bin"

と書く。

ssreflect/mathcompのインストール

依存関係: Coq, make

ssreflect/mathcompのWebサイト から ssreflect-mathcomp-installer-1.6.1-win64.exe をダウンロードし、実行する。Coqのインストールディレクトリと同じディレクトリ C:\Coq を指定する。ssreflectは %COQDIR%\lib\user-contrib\mathcomp にインストールされる。

coq-std++のビルドとインストール

依存関係: Coq, git, make

$ git clone -b ee6200b4d74bfd06034f3cc36d1afdc309427e5c https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git
$ cd coq-stdpp
$ make && make install

Irisのビルドとインストール

依存関係: Coq, ssreflect/mathcomp, git, make, coq-std++

$ git clone -b 398bae9d092b6568cf8d504ca98d8810979eea33 https://gitlab.mpi-sws.org/FP/iris-coq.git
$ cd iris-coq
$ make && make install

RustBeltのビルド

依存関係: Coq, ssreflect/mathcomp, git, make, coq-std++, iris

RustBeltのWebサイトの “RustBelt: Securing the Foundations of the Rust Programming Language.” という論文のappendixをダウンロードする。 appendix.zip を解凍する。

$ cd appendix/lambdaRust
$ make && make install

以上