FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.7k stars 234 forks source link

Introduce --ocamlenv #3565

Closed mtzguido closed 1 month ago

mtzguido commented 1 month ago

This options allows to easily extend a shell with an OCAMLPATH suitable for building F* OCaml programs, and also to simply run a build command easily by prepending fstar.exe --ocamlenv to it.

Example below.

module Hello
open FStar.IO
let _ = print_string "Hello F*!\n"
$ fstar.exe --ocamlenv
OCAMLPATH='/home/guido/r/fstar/master/lib:'; export OCAMLPATH;
$ fstar.exe --ocamlenv ocamlfind ocamlopt -linkpkg -package fstar.lib Hello.ml
findlib: [WARNING] Interface ratio.cmi occurs in several directories: /home/guido/.opam/4.14.1/lib/num, home/guido/.opam/4.14.1/lib/ocaml
findlib: [WARNING] Interface num.cmi occurs in several directories: /home/guido/.opam/4.14.1/lib/num, home/guido/.opam/4.14.1/lib/ocaml
findlib: [WARNING] Interface topdirs.cmi occurs in several directories: /home/guido/.opam/4.14.1/lib/ocaml/compiler-libs, home/guido/.opam/4.14.1/lib/ocaml
findlib: [WARNING] Interface big_int.cmi occurs in several directories: /home/guido/.opam/4.14.1/lib/num, home/guido/.opam/4.14.1/lib/ocaml
findlib: [WARNING] Interface nat.cmi occurs in several directories: /home/guido/.opam/4.14.1/lib/num, home/guido/.opam/4.14.1/lib/ocaml
findlib: [WARNING] Interface arith_status.cmi occurs in several directories: /home/guido/.opam/4.14.1/lib/num, home/guido/.opam/4.14.1/lib/ocaml
ocamlfind: [WARNING] Package `threads': Linking problems may arise because of the missing -thread or -vmthread switch
$ ./a.out
Hello F*!

Obviously the command required is not as simple as it could be, but this is already an improvement since it provides a standard way of locating the needed OCAMLPATHs.