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
以上