无法在F*中编译Hello World

Question

OCaml 和 F* 均已成功安装。我能找到的唯一类似于 Hello World 示例的是：

module Hello

open FStar.IO

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

来自其 GitHub 存储库。

我用

fstar.exe hello.fst --codegen OCaml --extract_module Hello

验证并返回：

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

我查找了如何指定 IO 总效果并尝试将其更改为

let main : unit -> Tot (IO unit) = print_string "Hello F*!\n"

，但又回来了

(Error 72) Identifier not found: [Tot]

。如果有人知道声明总顶级绑定的正确方法，那就太好了。

目前，我删除了该效果并接受了警告。然后我按照文档中的建议使用

ocamlopt -o hello Hello.ml

并返回：

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

这就是

Hello.ml

中的内容：

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

我知道 F* 是一门小众语言，但我喜欢它所提供的功能，我希望其他人能够帮助我起步。

Answer 1

以下是最终对我有用的步骤：

使用

opam pin add fstar --dev-repo

安装

调整来源：

module Hello

open FStar.IO
open FStar.All

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

let _ = main ()

提取：

fstar.exe hello.fst --codegen OCaml --extract_module Hello

编译：

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