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* 是一门小众语言,但我喜欢它所提供的功能,我希望其他人能够帮助我起步。
以下是最终对我有用的步骤:
使用
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