[SOLVED] Can't compile Hello World in F*

Can't compile Hello World in F*

Both OCaml and F* have been successfully installed. The only thing resembling a Hello World example I was able to find was:

module Hello

open FStar.IO

let main = print_string "Hello F*!\n"

from its GitHub repo.

I verified it with fstar.exe hello.fst --codegen OCaml --extract_module Hello and got back:

Extracted module Hello
hello.fst(5,0-5,38): (Warning 272) Top-level let-bindings must be total; this term may have effects
Verified module: Hello
All verification conditions discharged successfully

I looked up how to specify an IO total effect and tried changing it to let main : unit -> Tot (IO unit) = print_string "Hello F*!\n", but got back (Error 72) Identifier not found: [Tot]. If anyone knows the proper way to declare a total top-level binding, that would be great.

For now, I removed the effect and accepted the warning. I then used ocamlopt -o hello Hello.ml as recommended in the documentation and got back:

File "Hello.ml", line 1, characters 5-10:
1 | open Prims
         ^^^^^
Error: Unbound module Prims

This is what is in Hello.ml:

open Prims
let (main : unit) = FStar_IO.print_string "Hello, F*!\n"

I know F* is a niche language, but I love what it has to offer and I hope others are able to help me get off the ground.

Solution

Here are the steps that ended up working for me:

Install with opam pin add fstar --dev-repo

Adjust source:

module Hello

open FStar.IO
open FStar.All

let main
  : unit  -> ML unit
  = fun _ -> print_string "Hello, F*!\n"

let _ = main ()

Extract with: fstar.exe hello.fst --codegen OCaml --extract_module Hello

Compile with:

OCAMLPATH=~/.opam/default/lib/fstar/ 
ocamlfind opt -package fstar.lib -linkpkg Hello.ml -o Hello