依存型言語 F*のインストール+実行可能コード生成までの手順(2022年)

概要

F*の処理系をインストールし、動作確認までした。

• 環境: Ubuntu 22.04 (VSCode devcontainer 機能で入れたもの)
• 静的検査が通ることを確認済み
• OCamlコードを出力して、実行できることを確認済み

F* って？

F*(F Star)とは、Microsoftが解決した依存型プログラミング言語である。詳しくは以前私が書いたF*(F Star)の複雑な型システムの何が嬉しいのか？ という記事を参照されたい。

手順

以下のリポジトリにまとめた。

https://github.com/yuchiki/fstar-install-battle

注意したところ・気を使ったところ

公式手順が masterブランチの最新版の fstarを入れさせようとしてくる

公式手順には以下のように記載がある。

$ opam pin add fstar --dev-repo

しかし私が手順を実行した時点ではmasterブランチの最新版ではそもそもビルド＋インストールが成功しなかった。
そこで最新のタグを指定してインストールするように変更した

$ opam pin add fstar https://github.com/FStarLang/FStar.git  --with-version "2022.11.07"

実行可能なファイルを生成することが難しい

fstar.exe --codegen OCaml コマンドは、コード自体に対応するOCamlコードに加えて、コードが依存するライブラリに相当するOCamlコードも生成する。しかしこのコマンドでは、コード中に明示されていない場合暗黙的に開かれる Prims という依存ライブラリが生成されず、実行可能ファイルの生成に失敗する。
実行可能ファイル生成時に --package fstarlib -linkpkg オプションを指定することで Prims ライブラリを結合できるが、この場合自動生成されてしまった依存ライブラリと衝突し、実行可能ファイルの生成に失敗する。

今回の手順では、コード生成するライブラリを --extract "Main" オプションで Main に限定し、そのうえで --package fstarlib -linkpkg オプションを追加することで実行可能ファイルを生成することができた。

感想

• 結構動作確認に至るまででハマりどころが多かった。
• 走りやすいインストール＋実行までの手順を書いたので、日本語圏でF*を触ってみる人が増えると嬉しい。