1 ddc03123 2020-03-28 op [F*](https://fstar-lang.org) is a *general purpose functional
2 ddc03123 2020-03-28 op programming language with effects aimed at program verification.*
3 ddc03123 2020-03-28 op Recently I've been playing a bit with it, it's nice, and here's a
4 ddc03123 2020-03-28 op quick guide on how to compile it on OpenBSD.
8 ddc03123 2020-03-28 op *Edit*: This "guide" is partially incomplete. Doing some re-install
9 ddc03123 2020-03-28 op after this guide was published, I noticed that not everything is as I
10 ddc03123 2020-03-28 op wrote it here. Things change, I suppose. Some problems have been
11 ddc03123 2020-03-28 op fixed, but not everything. In particular `ocamlfind` will complain
12 ddc03123 2020-03-28 op (probably multiple times) during the build that it cannot find the
13 ddc03123 2020-03-28 op `XXX` package, and a simple `opam install XXX` will amend.
17 ddc03123 2020-03-28 op We'll need both `git` and GNU `make` from ports, and also ocaml (to
18 ddc03123 2020-03-28 op build F* and run F* programs), opam (the ocaml package manager),
19 ddc03123 2020-03-28 op ocaml-camlp4 and python 3 (to build `z3`, a theorem prover).
21 ddc03123 2020-03-28 op $ pkg_add git gmake ocaml ocaml-camlp4 opam python
23 ddc03123 2020-03-28 op *Note* I've installed camlp4 from the ports instead of through opam
24 ddc03123 2020-03-28 op because I was getting an error. I don't have much experience with
25 ddc03123 2020-03-28 op ocaml, but I've read *somewhere* that installing through the package
26 ddc03123 2020-03-28 op manager solved those problems.
28 ddc03123 2020-03-28 op ## Building z3
30 ddc03123 2020-03-28 op z3 is the engine that powers the verification system of F*
31 ddc03123 2020-03-28 op (AFAIK). It's not available through ports, so we'll need to build from
32 ddc03123 2020-03-28 op source. Even though is a project that came from Microsoft, it seems to
33 ddc03123 2020-03-28 op run on OpenBSD just fine. Building it is also straightforward:
35 ddc03123 2020-03-28 op $ git clone https://github.com/Z3Prover/z3
37 ddc03123 2020-03-28 op $ CXX=clang++ python3 script/mk_make.py
40 ddc03123 2020-03-28 op $ cp z3 $SOMEWHERE_IN_PATH # (maybe?)
42 ddc03123 2020-03-28 op *Note* by default `script/mk_make.py` will try to use base g++ and the
43 ddc03123 2020-03-28 op build will fail. The version of g++ is too ancient and doesn't support
46 ddc03123 2020-03-28 op ## Building F*
48 ddc03123 2020-03-28 op First of all, we need some ocaml dependencies, so make sure to
49 ddc03123 2020-03-28 op initialize opam (see `opam init`) and add the suggested stuff to your
50 ddc03123 2020-03-28 op shell init file.
52 ddc03123 2020-03-28 op $ opam install ocamlfind batteries stdint zarith ppx_deriving ppx_deriving_yojson ocaml-migrate-parsetree process
54 ddc03123 2020-03-28 op We can now build the F* compiler from the ocaml output present in the
55 ddc03123 2020-03-28 op repo. You can also build the ocaml output by yourself, but I've skip
58 ddc03123 2020-03-28 op $ gmake -j9 -C src/ocaml-output
60 ddc03123 2020-03-28 op The last step is to build the library. While the docs describes this
61 ddc03123 2020-03-28 op as an optional step, I wasn't able to compile F* programs without it.
63 ddc03123 2020-03-28 op $ gmake -j9 -C ulib/ml
65 ddc03123 2020-03-28 op This was all. Let's try the hello world now!
67 ddc03123 2020-03-28 op $ gmake -C examples/hello hello
69 ddc03123 2020-03-28 op It should take a decent amount of time to compile, output a *lot* of
70 ddc03123 2020-03-28 op text and, finally, at the end, a beautiful "Hello World".
72 ddc03123 2020-03-28 op Congrats, now you have a working F* installation!
