Merge pull request #3581 from mtzguido/ocamlc

Introducing --ocamlc and --ocamlc_plugin

src/basic/FStarC.Compiler.Util.fsti

@@ -394,4 +394,4 @@ val array_length (s:FStar.ImmutableArray.Base.t 'a) : FStarC.BigInt.t
 val array_index (s:FStar.ImmutableArray.Base.t 'a) (i:FStarC.BigInt.t) : 'a
 
 val putenv : string -> string -> unit
-val execvp : string -> list string -> unit
+val execvp : string -> list string -> unit // will return only on error

src/basic/FStarC.Options.fst

@@ -1638,6 +1638,16 @@ let rec specs_with_types warn_unsafe : list (char & string & opt_type & Pprint.d
     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.");
+  ( noshort,
+    "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.");
+  ( noshort,
+    "ocamlc_plugin",
+    WithSideEffect ((fun _ -> print_error "--ocamlc_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 from extracted files.");
   ]
 
 and specs (warn_unsafe:bool) : list (FStarC.Getopt.opt & Pprint.document) =

src/fstar/FStarC.Main.fst

@@ -113,34 +113,6 @@ let load_native_tactics () =
 (* print_in_place options are passed *)
 let fstar_files: ref (option (list string)) = Util.mk_ref None
 
-(* ocamlenv mode: called whenever the *first* argument is exactly '--ocamlenv' *)
-let go_ocamlenv rest_args =
-  if Platform.system = Platform.Windows then (
-    Errors.raise_error0 Errors.Fatal_OptionsNotCompatible [
-      Errors.text "--ocamlenv is not supported on Windows (yet?)"
-    ]
-  );
-  let shellescape (s:string) : string =
-    String.list_of_string s |>
-    List.map (function
-      | '\'' -> "'\"'\"'" // to escape single quotes we need to put them inside a double quote
-      | 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 new_ocamlpath = ocamldir ^ ":" ^ 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)
-
 (* This is used to print a backtrace when F* is interrupted by SIGINT *)
 let set_error_trap () =
   let h = get_sigint_handler () in
@@ -316,7 +288,20 @@ let go_normal () =
 let go () =
   let args = Util.get_cmd_args () in
   match args with
-  | _ :: "--ocamlenv" :: rest -> go_ocamlenv rest
+  | _ :: "--ocamlenv" :: [] ->
+    let new_ocamlpath = OCaml.new_ocamlpath () in
+    Util.print1 "OCAMLPATH='%s'; export OCAMLPATH;\n" (OCaml.shellescape new_ocamlpath);
+    exit 0
+
+  | _ :: "--ocamlenv" :: cmd :: args ->
+    OCaml.exec_in_ocamlenv cmd args
+
+  | _ :: "--ocamlc" :: rest ->
+    OCaml.exec_ocamlc rest
+
+  | _ :: "--ocamlc_plugin" :: rest ->
+    OCaml.exec_ocamlc_plugin rest
+
   | _ -> go_normal ()
 
 (* This is pretty awful. Now that we have Lazy_embedding, we can get rid of this table. *)

src/fstar/FStarC.OCaml.fst

@@ -0,0 +1,58 @@
+(*
+   Copyright 2008-2016 Nikhil Swamy and Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+module FStarC.OCaml
+
+open FStarC
+open FStarC.Compiler
+open FStarC.Compiler.Effect
+
+let shellescape (s:string) : string =
+  String.list_of_string s |>
+  List.map (function
+    | '\'' -> "'\"'\"'" // to escape single quotes we need to put them inside a double quote
+    | c -> String.make 1 c
+  ) |>
+  String.concat ""
+
+let new_ocamlpath () : string =
+  let ocamldir = Find.locate_ocaml () in
+  let old_ocamlpath = Util.dflt "" (Util.expand_environment_variable "OCAMLPATH") in
+  let new_ocamlpath = ocamldir ^ ":" ^ old_ocamlpath in
+  new_ocamlpath
+
+let exec_in_ocamlenv #a (cmd : string) (args : list string) : a =
+  let new_ocamlpath = new_ocamlpath () in
+  if Platform.system = Platform.Windows then (
+    Errors.raise_error0 Errors.Fatal_OptionsNotCompatible [
+      Errors.text "--ocamlenv is not supported on Windows (yet?)"
+    ]
+  );
+  (* Update OCAMLPATH and run (exec) the command *)
+  Util.putenv "OCAMLPATH" new_ocamlpath;
+  Util.execvp cmd (cmd :: args);
+  failwith "execvp failed"
+
+(* OCaml Warning 8: this pattern-matching is not exhaustive.
+This is usually benign as we check for exhaustivenss via SMT. *)
+
+let exec_ocamlc args =
+  exec_in_ocamlenv "ocamlfind"
+    ("opt" :: "-w" :: "-8" :: "-linkpkg" :: "-package" :: "fstar.lib" :: args)
+
+let exec_ocamlc_plugin args =
+  exec_in_ocamlenv "ocamlfind"
+    ("opt" :: "-w" :: "-8" :: "-shared" :: "-package" :: "fstar.lib" ::
+    args)

src/fstar/FStarC.OCaml.fsti

@@ -0,0 +1,38 @@
+(*
+   Copyright 2008-2016 Nikhil Swamy and Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+module FStarC.OCaml
+
+open FStarC.Compiler.Effect
+
+(* Escape a string for use in a shell command, expecting to be wrapped in SINGLE quotes. *)
+val shellescape (s:string) : string
+
+(* Compute a value for OCAMLPATH taken from the current env + extended with our own library.
+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. *)
+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. *)
+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

tests/dune_hello/dune

@@ -4,8 +4,3 @@
  (libraries fstar.lib)
  (modes native)
 )
-(env
-  (_
-    (bin_annot false)
-    (flags (:standard -w -A)))
-)

tests/semiring/Makefile

@@ -23,7 +23,7 @@ $(OUTPUT_DIR)/%.ml:
 
 %.cmxs: %.ml
 	$(call msg, "OCAMLOPT", $<)
-	$(OCAMLOPT) -w -8 -shared -package fstar.lib -o $@ $*.ml
+	$(FSTAR_EXE) --ocamlc_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

@@ -13,4 +13,4 @@ Hello.test: Hello.exe
 	$(FSTAR) --codegen OCaml $< --extract $*
 
 %.exe: %.ml
-	$(FSTAR) --ocamlenv ocamlfind ocamlopt -package fstar.lib -linkpkg $< -o $@
+	$(FSTAR) --ocamlc $< -o $@