Merge pull request #3583 from mtzguido/ocamlc

fstar: rename --ocamlc to --ocamlopt, add --ocamlc for bytecode

src/basic/FStarC.Options.fst

@@ -1642,12 +1642,17 @@ let rec specs_with_types warn_unsafe : list (char & string & opt_type & Pprint.d
     "ocamlc",
     WithSideEffect ((fun _ -> print_error "--ocamlc must be the first argument, see fstar.exe --help for details\n"; exit 1),
                      (Const (Bool true))),
-    text "A helper. This runs 'ocamlopt' in the environment set up by --ocamlenv, for building an F* application executable.");
+    text "A helper. This runs 'ocamlc' in the environment set up by --ocamlenv, for building an F* application bytecode executable.");
   ( noshort,
-    "ocamlc_plugin",
-    WithSideEffect ((fun _ -> print_error "--ocamlc_plugin must be the first argument, see fstar.exe --help for details\n"; exit 1),
+    "ocamlopt",
+    WithSideEffect ((fun _ -> print_error "--ocamlopt must be the first argument, see fstar.exe --help for details\n"; exit 1),
                      (Const (Bool true))),
-    text "A helper. This runs 'ocamlopt' in the environment set up by --ocamlenv, for building an F* plugin from extracted files.");
+    text "A helper. This runs 'ocamlopt' in the environment set up by --ocamlenv, for building an F* application native executable.");
+  ( noshort,
+    "ocamlopt_plugin",
+    WithSideEffect ((fun _ -> print_error "--ocamlopt_plugin must be the first argument, see fstar.exe --help for details\n"; exit 1),
+                     (Const (Bool true))),
+    text "A helper. This runs 'ocamlopt' in the environment set up by --ocamlenv, for building an F* plugin.");
   ]
 
 and specs (warn_unsafe:bool) : list (FStarC.Getopt.opt & Pprint.document) =

src/fstar/FStarC.Main.fst

@@ -299,8 +299,11 @@ let go () =
   | _ :: "--ocamlc" :: rest ->
     OCaml.exec_ocamlc rest
 
-  | _ :: "--ocamlc_plugin" :: rest ->
-    OCaml.exec_ocamlc_plugin rest
+  | _ :: "--ocamlopt" :: rest ->
+    OCaml.exec_ocamlopt rest
+
+  | _ :: "--ocamlopt_plugin" :: rest ->
+    OCaml.exec_ocamlopt_plugin rest
 
   | _ -> go_normal ()
 

src/fstar/FStarC.OCaml.fst

@@ -49,10 +49,14 @@ let exec_in_ocamlenv #a (cmd : string) (args : list string) : a =
 This is usually benign as we check for exhaustivenss via SMT. *)
 
 let exec_ocamlc args =
+  exec_in_ocamlenv "ocamlfind"
+    ("c" :: "-w" :: "-8" :: "-linkpkg" :: "-package" :: "fstar.lib" :: args)
+
+let exec_ocamlopt args =
   exec_in_ocamlenv "ocamlfind"
     ("opt" :: "-w" :: "-8" :: "-linkpkg" :: "-package" :: "fstar.lib" :: args)
 
-let exec_ocamlc_plugin args =
+let exec_ocamlopt_plugin args =
   exec_in_ocamlenv "ocamlfind"
     ("opt" :: "-w" :: "-8" :: "-shared" :: "-package" :: "fstar.lib" ::
     args)

src/fstar/FStarC.OCaml.fsti

@@ -24,15 +24,23 @@ val shellescape (s:string) : string
 This is NOT escaped. *)
 val new_ocamlpath () : string
 
-(* Run a command with the new OCAMLPATH set. The cmd is usually args[0], in Unix convention.
-This calls execvp, so it will not return if successful. Raises a Failure if the execvp fails.
-It also tries to find the command in the PATH, absolute path is not needed. *)
+(* Run a command with the new OCAMLPATH set. This calls execvp, so it
+will not return if successful. Raises a Failure if the execvp fails. It
+also tries to find the command in the PATH, absolute path is not needed.
+*)
 val exec_in_ocamlenv (#a:Type) (cmd : string) (args : list string) : a
 
-(* Run ocamlc passing appropriate flags to generate an executable. Expects
-the source file and further options as arguments. *)
+(* Run ocamlc (i.e. bytecode compiler) passing appropriate flags to
+generate a bytecode executable. Expects the source file and further
+options as arguments. *)
 val exec_ocamlc #a (args : list string) : a
 
-(* Run ocamlc passing appropriate flags to generate an F* plugin, using
-fstar_plugin_lib. Expects the source file and further options as arguments. *)
-val exec_ocamlc_plugin #a (args : list string) : a
+(* Run ocamlopt (i.e. native compiler) passing appropriate flags to
+generate an executable. Expects the source file and further options as
+arguments. *)
+val exec_ocamlopt #a (args : list string) : a
+
+(* Run ocamlc passing appropriate flags to generate an F* plugin,
+using fstar_plugin_lib. Expects the source file and further options as
+arguments. *)
+val exec_ocamlopt_plugin #a (args : list string) : a

tests/dune_hello/Makefile

@@ -13,6 +13,8 @@ bin/hello.exe: Hello.ml
 .PHONY: run
 run: bin/hello.exe
 	./bin/hello.exe | grep "Hi!"
+	# Find a way to install this? dune install skips the bytecode
+	$(FSTAR_EXE) --ocamlenv dune exec ./hello.bc | grep "Hi!"
 
 clean:
 	dune clean

tests/dune_hello/dune

@@ -2,5 +2,8 @@
  (name hello)
  (public_name hello.exe)
  (libraries fstar.lib)
- (modes native)
+ (modes native byte)
 )
+(env
+  (_
+    (flags (:standard -w -A))))

tests/semiring/Makefile

@@ -23,7 +23,7 @@ $(OUTPUT_DIR)/%.ml:
 
 %.cmxs: %.ml
 	$(call msg, "OCAMLOPT", $<)
-	$(FSTAR_EXE) --ocamlc_plugin -o $@ $*.ml
+	$(FSTAR_EXE) --ocamlopt_plugin -o $@ $*.ml
 
 # REMARK: --load will compile $*.ml if $*.cmxs does not exist, but we
 # compile it before and use --load_cmxs

tests/simple_hello/Makefile

@@ -6,14 +6,18 @@ FSTAR ?= ../../bin/fstar.exe
 
 all: Hello.test
 
-Hello.test: Hello.exe
-	./Hello.exe | grep "Hello F\*!"
+Hello.test: Hello.exe Hello.byte
+	./Hello.exe  | grep "Hello F\*!"
+	./Hello.byte | grep "Hello F\*!"
 
 %.ml: %.fst
 	$(FSTAR) --codegen OCaml $< --extract $*
 
 %.exe: %.ml
+	$(FSTAR) --ocamlopt $< -o $@
+
+%.byte: %.ml
 	$(FSTAR) --ocamlc $< -o $@
 
 clean:
-	rm -f *.ml *.exe
+	rm -f *.ml *.exe *.byte