diff --git a/ocaml/fstar-lib/generated/FStarC_OCaml.ml b/ocaml/fstar-lib/generated/FStarC_OCaml.ml index b780e413aec..007f1e660eb 100644 --- a/ocaml/fstar-lib/generated/FStarC_OCaml.ml +++ b/ocaml/fstar-lib/generated/FStarC_OCaml.ml @@ -38,15 +38,22 @@ let exec_in_ocamlenv : 'a . Prims.string -> Prims.string Prims.list -> 'a = FStarC_Compiler_Util.putenv "OCAMLPATH" new_ocamlpath1; FStarC_Compiler_Util.execvp cmd (cmd :: args); failwith "execvp failed" +let (app_lib : Prims.string) = "fstar.lib" +let (plugin_lib : Prims.string) = "fstar.lib" +let (wstr : Prims.string) = "-8" +let (common_args : Prims.string Prims.list) = ["-w"; wstr; "-thread"] let exec_ocamlc : 'a . Prims.string Prims.list -> 'a = fun args -> - exec_in_ocamlenv "ocamlfind" ("c" :: "-w" :: "-8" :: "-linkpkg" :: - "-package" :: "fstar.lib" :: args) + exec_in_ocamlenv "ocamlfind" + (FStar_List_Tot_Base.op_At ("c" :: common_args) ("-linkpkg" :: + "-package" :: app_lib :: args)) let exec_ocamlopt : 'a . Prims.string Prims.list -> 'a = fun args -> - exec_in_ocamlenv "ocamlfind" ("opt" :: "-w" :: "-8" :: "-linkpkg" :: - "-package" :: "fstar.lib" :: args) + exec_in_ocamlenv "ocamlfind" + (FStar_List_Tot_Base.op_At ("opt" :: common_args) ("-linkpkg" :: + "-package" :: app_lib :: args)) let exec_ocamlopt_plugin : 'a . Prims.string Prims.list -> 'a = fun args -> - exec_in_ocamlenv "ocamlfind" ("opt" :: "-w" :: "-8" :: "-shared" :: - "-package" :: "fstar.lib" :: args) \ No newline at end of file + exec_in_ocamlenv "ocamlfind" + (FStar_List_Tot_Base.op_At ("opt" :: common_args) ("-shared" :: + "-package" :: plugin_lib :: args)) \ No newline at end of file diff --git a/src/fstar/FStarC.OCaml.fst b/src/fstar/FStarC.OCaml.fst index e40a621293d..53c59f8d690 100644 --- a/src/fstar/FStarC.OCaml.fst +++ b/src/fstar/FStarC.OCaml.fst @@ -16,6 +16,7 @@ module FStarC.OCaml open FStarC +open FStar.List.Tot.Base open FStarC.Compiler open FStarC.Compiler.Effect @@ -45,18 +46,26 @@ let exec_in_ocamlenv #a (cmd : string) (args : list string) : a = Util.execvp cmd (cmd :: args); failwith "execvp failed" +let app_lib = "fstar.lib" +let plugin_lib = "fstar.lib" + (* OCaml Warning 8: this pattern-matching is not exhaustive. This is usually benign as we check for exhaustivenss via SMT. *) +let wstr = "-8" + +let common_args = + "-w" :: wstr :: + "-thread" :: + [] let exec_ocamlc args = exec_in_ocamlenv "ocamlfind" - ("c" :: "-w" :: "-8" :: "-linkpkg" :: "-package" :: "fstar.lib" :: args) + ("c" :: common_args @ "-linkpkg" :: "-package" :: app_lib :: args) let exec_ocamlopt args = exec_in_ocamlenv "ocamlfind" - ("opt" :: "-w" :: "-8" :: "-linkpkg" :: "-package" :: "fstar.lib" :: args) + ("opt" :: common_args @ "-linkpkg" :: "-package" :: app_lib :: args) let exec_ocamlopt_plugin args = exec_in_ocamlenv "ocamlfind" - ("opt" :: "-w" :: "-8" :: "-shared" :: "-package" :: "fstar.lib" :: - args) + ("opt" :: common_args @ "-shared" :: "-package" :: plugin_lib :: args)