Update(2022/11/09)
この記事はやや古くなっています。
ubuntuにおいて、2022/11/09に以下のリポジトリの手順で動くことを確かめました。
https://github.com/yuchiki/fstar-install-battle
前置き
F* とは、マイクロソフトとInriaが開発している強い型システムを備えたF#ライクな依存型言語です。
F*という言語の特徴については弊記事F*(F Star)の複雑な型システムの何が嬉しいのか?をご覧ください。
インストール手順は公式のrepositoryのインストール手順 に従います。
$HOME/fstar というレポジトリが生成されますが、これにはライブラリが含まれています。削除すると実行ファイルがコンパイルできなくなります。
linux
cd $HOME
wget https://github.com/FStarLang/FStar/releases/download/V0.9.7.0-alpha1/fstar_0.9.7.0-alpha1_Linux_x86_64.tar.gz -O - | tar -xz
sudo cp fstar/bin/fstar.exe /usr/local/bin/fstar.exe
sudo cp fstar/bin/z3 /usr/local/bin/z3
Mac
cd $HOME
wget https://github.com/FStarLang/FStar/releases/download/V0.9.7.0-alpha1/fstar_0.9.7.0-alpha1_Darwin_x86_64.tar.gz -O - | tar -xz
sudo cp fstar/bin/fstar.exe /usr/local/bin/fstar.exe
sudo cp fstar/bin/z3 /usr/local/bin/z3
動作確認
動作確認用のレポジトリを用意しました。
git clone git@github.com:yuchiki/fstar_sample_repository.git
cd fstar_sample_repository
静的検査が通ることは以下で確かめられます。
make check
ocamloptなどがインストールされており、ocamlファイルをコンパイルできる環境が整っていれば、以下でコードを実行することができます。
make execute