MacにF*をインストールする.md

前提

• opam 2.0.4

インストール手順

z3のインストール　

brew install z3

F*用の環境をopamで新規作成

opam switch create fstar-dev ocaml-base-compiler.4.07.1
eval $(opam env)

　F*のインストール

opam pin add fstar --dev-repo

The following actions will be performed:
  ∗ install conf-gmp                1               [required by zarith]
  ∗ install conf-m4                 1               [required by ocamlfind]
  ∗ install conf-which              1               [required by biniou]
  ∗ install conf-perl               1               [required by zarith]
  ∗ install dune                    1.10.0
          [required by ppx_deriving, ocaml-migrate-parsetree,
          ppx_deriving_yojson]
  ∗ install ocamlbuild              0.14.0          [required by fstar]
  ∗ install ocamlfind               1.8.0           [required by fstar]
  ∗ install result                  1.4
          [required by ppx_deriving, ocaml-migrate-parsetree,
          ppx_deriving_yojson]
  ∗ install ppx_derivers            1.2.1
          [required by ocaml-migrate-parsetree, ppx_deriving]
  ∗ install jbuilder                transition      [required by stdint]
  ∗ install cppo                    1.6.6
          [required by ppx_deriving, ppx_deriving_yojson]
  ∗ install camlp4                  4.07+1          [required by ulex]
  ∗ install zarith                  1.7             [required by fstar]
  ∗ install ppx_tools               5.1+4.06.0
          [required by ppx_deriving, ppx_deriving_yojson]
  ∗ install pprint                  20180528        [required by fstar]
  ∗ install num                     1.2             [required by batteries]
  ∗ install menhir                  20190626        [required by fstar]
  ∗ install base-bytes              base
          [required by stdint, fileutils, process, ulex]
  ∗ install ocaml-migrate-parsetree 1.3.1           [required by fstar]
  ∗ install easy-format             1.3.1           [required by yojson]
  ∗ install batteries               2.9.0           [required by fstar]
  ∗ install ulex                    1.2             [required by fstar]
  ∗ install stdint                  0.5.1           [required by fstar]
  ∗ install process                 0.2.1           [required by fstar]
  ∗ install fileutils               0.5.3           [required by fstar]
  ∗ install ppxfind                 1.3
          [required by ppx_deriving, ppx_deriving_yojson]
  ∗ install biniou                  1.2.0           [required by yojson]
  ∗ install ppx_deriving            4.3             [required by fstar]
  ∗ install yojson                  1.7.0           [required by fstar]
  ∗ install ppx_deriving_yojson     3.4             [required by fstar]
  ∗ install fstar                   0.9.7.0-alpha1*
===== ∗ 31 =====
Do you want to continue? [Y/n] Y

opam install fstar

試してみる

fstar.exe --version

F* 0.9.7.0-alpha1
platform=Darwin_x86_64
compiler=OCaml 4.07.1
date=<not set>
commit=86777fca088e7769ccf473fb44406633fc28a913

fstar.exe Fact.fst

/home/yoshihiro_imai/.opam/fstar/lib/fstar/prims.fst(0,0-0,0): (Warning 241) Unable to load /home/yoshihiro_imai/.opam/fstar/lib/fstar/prims.fst.checked since checked file /home/yoshihiro_imai/.opam/fstar/lib/fstar/prims.fst.checked does not exist; will recheck /home/yoshihiro_imai/.opam/fstar/lib/fstar/prims.fst (suppressing this warning for further modules)
(Warning 282) Expected Z3 version "Z3 version 4.8.5", got "Z3 version 4.4.1
"
Please download the version of Z3 corresponding to your platform from:
https://github.com/FStarLang/binaries/tree/master/z3-tested
and add the bin/ subdirectory into your PATH

Verified module: Fact (1549 milliseconds)
All verification conditions discharged successfully

トラブルシューティング

opam install fstar で install --D のエラーになってしまう場合はおそらくGNU installがないことが原因。

エラーメッセージ

yoshihiro_imai:~ $ opam install fstar

<><> Synchronising pinned packages ><><><><><><><><><><><><><><><><><><><><>  🐫 
[fstar.0.9.7.0-alpha1] no changes from git://github.com/FStarLang/FStar

The following actions will be performed:
  ∗ install fstar 0.9.7.0-alpha1*

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><>  🐫 
[ERROR] The installation of fstar failed at "make PREFIX=/Users/yoshihiro_imai/.opam/fstar -C src/ocaml-output install".

#=== ERROR while installing fstar.0.9.7.0-alpha1 ==============================#
# context     2.0.3 | macos/x86_64 | ocaml-base-compiler.4.07.1 | pinned(git://github.com/FStarLang/FStar#62881814)
# path        ~/.opam/fstar/.opam-switch/build/fstar.0.9.7.0-alpha1
# command     ~/.opam/opam-init/hooks/sandbox.sh install make PREFIX=/Users/yoshihiro_imai/.opam/fstar -C src/ocaml-output install
# exit-code   2
# env-file    ~/.opam/log/fstar-86716-e4db2f.env
# output-file ~/.opam/log/fstar-86716-e4db2f.out
### output ###
# [...]
# # We deliberately leave out date, so that rebuilds are no-ops
# echo 'FStar_Options._commit:= "628818147b19898eb1000aad11f242d726d09814";;' >> FStar_Version.ml
# cd ../../ && ocamlbuild -cflag -g -I src/ocaml-output -I src/basic/ml -I src/parser/ml -I src/fstar/ml -I src/extraction/ml -I src/prettyprint/ml -I src/tactics/ml -I src/tests/ml -I ulib/ml -j 24 -build-dir src/ocaml-output/_build -use-ocamlfind main.native src/ocaml-output/FStar_Syntax_Syntax.inferred.mli
# # No parallelism done
# install -m 755 -D _build/src/fstar/ml/main.native /Users/yoshihiro_imai/.opam/fstar/bin/fstar.exe
# install: illegal option -- D
# usage: install [-bCcpSsv] [-B suffix] [-f flags] [-g group] [-m mode]
#                [-o owner] file1 file2
#        install [-bCcpSsv] [-B suffix] [-f flags] [-g group] [-m mode]
#                [-o owner] file1 ... fileN directory
#        install -d [-v] [-g group] [-m mode] [-o owner] directory ...
# make: *** [install] Error 64



<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><>  🐫 
┌─ The following actions failed
│ ∗ install fstar 0.9.7.0-alpha1
└─ 
╶─ No changes have been performed

解決法

brew install coreutils