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