LoginSignup
1

More than 1 year has passed since last update.

F*(f star) の処理系をインストールする

Last updated at Posted at 2021-01-02

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

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
1