Introduce --ocamlenv

src/basic/FStarC.Options.fst

@@ -1631,6 +1631,13 @@ let rec specs_with_types warn_unsafe : list (char & string & opt_type & Pprint.d
     "locate_ocaml",
     Const (Bool true),
     text "Print the root of the built OCaml F* library and exit");
+  ( noshort,
+    "ocamlenv",
+    WithSideEffect ((fun _ -> print_error "--ocamlenv must be the first argument, see fstar.exe --help for details\n"; exit 1),
+                     (Const (Bool true))),
+    text "With no arguments: print shell code to set up an environment with the OCaml libraries in scope (similar to 'opam env'). \
+          With arguments: run a command in that environment. \
+          NOTE: this must be the FIRST argument passed to F* and other options are NOT processed.");
   ]
 
 and specs (warn_unsafe:bool) : list (FStarC.Getopt.opt & Pprint.document) =

src/fstar/FStarC.Main.fst

@@ -113,10 +113,36 @@ let load_native_tactics () =
 (* print_in_place options are passed *)
 let fstar_files: ref (option (list string)) = Util.mk_ref None
 
-(****************************************************************************)
-(* Main function                                                            *)
-(****************************************************************************)
-let go _ =
+(* ocamlenv mode: called whenever the *first* argument is exactly 'ocamlenv' *)
+let go_ocamlenv rest_args =
+  let shellescape (s:string) : string =
+    String.list_of_string s |>
+    List.map (function
+      | '\\' -> "\\\\" // backslashes can be escaped by themselves
+      | '\'' -> "'\"'\"'" // single quotes can be escaped by closing and reopening
+      | c -> String.make 1 c
+    ) |>
+    String.concat ""
+  in
+  let ocamldir = Find.locate_ocaml () in
+  let old_ocamlpath = Util.dflt "" (Util.expand_environment_variable "OCAMLPATH") in
+  let ocamlpath_sep = match Platform.system with
+    | Platform.Windows -> ";"
+    | Platform.Posix -> ":"
+  in
+  let new_ocamlpath = ocamldir ^ ocamlpath_sep ^ old_ocamlpath in
+  match rest_args with
+  | [] ->
+    Util.print1 "OCAMLPATH='%s'; export OCAMLPATH;\n" (shellescape new_ocamlpath);
+    exit 0
+
+  | cmd :: args ->
+    (* Update OCAMLPATH and run (exec) the command *)
+    Util.putenv "OCAMLPATH" new_ocamlpath;
+    Util.execvp cmd (cmd :: args)
+
+(* Normal mode with some flags, files, etc *)
+let go_normal () =
   let res, filenames = process_args () in
   if Options.trace_error () then begin
     let h = get_sigint_handler () in
@@ -285,6 +311,17 @@ let go _ =
           Errors.raise_error0 Errors.Error_MissingFileName "No file provided"
         end
 
+(****************************************************************************)
+(* Main function                                                            *)
+(****************************************************************************)
+
+(* choose a main driver function and go *)
+let go () =
+  let args = Util.get_cmd_args () in
+  match args with
+  | _ :: "--ocamlenv" :: rest -> go_ocamlenv rest
+  | _ -> go_normal ()
+
 (* This is pretty awful. Now that we have Lazy_embedding, we can get rid of this table. *)
 let lazy_chooser (k:Syntax.Syntax.lazy_kind) (i:Syntax.Syntax.lazyinfo) : Syntax.Syntax.term
   = match k with

tests/Makefile

@@ -19,6 +19,7 @@ ALL_TEST_DIRS += tactics
 ALL_TEST_DIRS += typeclasses
 ALL_TEST_DIRS += vale
 ALL_TEST_DIRS += hacl
+ALL_TEST_DIRS += simple_hello
 HAS_OCAML := $(shell which ocamlfind 2>/dev/null)
 
 ifneq (,$(HAS_OCAML))

tests/simple_hello/Hello.fst

@@ -0,0 +1,5 @@
+module Hello
+
+open FStar.IO
+
+let _ = print_string "Hello F*!\n"

tests/simple_hello/Makefile

@@ -0,0 +1,13 @@
+# This is probably the simplest makefile to build an F* application, and can be adapted easily.
+# We should not need to include any other internal makefiles.
+# Dune also works fine under the --ocamlenv.
+
+FSTAR ?= ../../bin/fstar.exe
+
+all: Hello.exe
+
+%.ml: %.fst
+	$(FSTAR) --codegen OCaml $< --extract $*
+
+%.exe: %.ml
+	$(FSTAR) --ocamlenv ocamlfind ocamlopt -package fstar.lib -linkpkg $< -o $@