From f92185e9dbd7304028abbfbf27bc5f30eb5c4dbc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 17 Oct 2024 14:16:38 -0700 Subject: [PATCH 1/4] src: refactor --ocamlenv logic into own module --- src/basic/FStarC.Compiler.Util.fsti | 2 +- src/fstar/FStarC.Main.fst | 37 +++++------------------ src/fstar/FStarC.OCaml.fst | 46 +++++++++++++++++++++++++++++ src/fstar/FStarC.OCaml.fsti | 30 +++++++++++++++++++ 4 files changed, 85 insertions(+), 30 deletions(-) create mode 100644 src/fstar/FStarC.OCaml.fst create mode 100644 src/fstar/FStarC.OCaml.fsti diff --git a/src/basic/FStarC.Compiler.Util.fsti b/src/basic/FStarC.Compiler.Util.fsti index 62da14e5102..880adc8a5b0 100644 --- a/src/basic/FStarC.Compiler.Util.fsti +++ b/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 diff --git a/src/fstar/FStarC.Main.fst b/src/fstar/FStarC.Main.fst index 1ae7ad8c1b4..0ccb69c7813 100644 --- a/src/fstar/FStarC.Main.fst +++ b/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,14 @@ 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 + | _ -> go_normal () (* This is pretty awful. Now that we have Lazy_embedding, we can get rid of this table. *) diff --git a/src/fstar/FStarC.OCaml.fst b/src/fstar/FStarC.OCaml.fst new file mode 100644 index 00000000000..0ce3ef7405a --- /dev/null +++ b/src/fstar/FStarC.OCaml.fst @@ -0,0 +1,46 @@ +(* + 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" diff --git a/src/fstar/FStarC.OCaml.fsti b/src/fstar/FStarC.OCaml.fsti new file mode 100644 index 00000000000..cc64e0b8520 --- /dev/null +++ b/src/fstar/FStarC.OCaml.fsti @@ -0,0 +1,30 @@ +(* + 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 From 87961a27d81bf5776a6701cc4c79758ec7388ddc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 17 Oct 2024 14:33:53 -0700 Subject: [PATCH 2/4] Introduce --ocamlc and --ocaml_plugin --- src/basic/FStarC.Options.fst | 10 ++++++++++ src/fstar/FStarC.Main.fst | 6 ++++++ src/fstar/FStarC.OCaml.fst | 12 ++++++++++++ src/fstar/FStarC.OCaml.fsti | 8 ++++++++ 4 files changed, 36 insertions(+) diff --git a/src/basic/FStarC.Options.fst b/src/basic/FStarC.Options.fst index 86a46785360..a0b32cf9f60 100644 --- a/src/basic/FStarC.Options.fst +++ b/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) = diff --git a/src/fstar/FStarC.Main.fst b/src/fstar/FStarC.Main.fst index 0ccb69c7813..5f2691d4717 100644 --- a/src/fstar/FStarC.Main.fst +++ b/src/fstar/FStarC.Main.fst @@ -296,6 +296,12 @@ let go () = | _ :: "--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. *) diff --git a/src/fstar/FStarC.OCaml.fst b/src/fstar/FStarC.OCaml.fst index 0ce3ef7405a..610661a332a 100644 --- a/src/fstar/FStarC.OCaml.fst +++ b/src/fstar/FStarC.OCaml.fst @@ -44,3 +44,15 @@ let exec_in_ocamlenv #a (cmd : string) (args : list string) : a = 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) diff --git a/src/fstar/FStarC.OCaml.fsti b/src/fstar/FStarC.OCaml.fsti index cc64e0b8520..1719ce5bec3 100644 --- a/src/fstar/FStarC.OCaml.fsti +++ b/src/fstar/FStarC.OCaml.fsti @@ -28,3 +28,11 @@ val new_ocamlpath () : string 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 From a56c1d7eb7bf1885488a806f0191a98180241b79 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 17 Oct 2024 14:34:14 -0700 Subject: [PATCH 3/4] tests: use new options --- tests/dune_hello/dune | 5 ----- tests/semiring/Makefile | 2 +- tests/simple_hello/Makefile | 2 +- 3 files changed, 2 insertions(+), 7 deletions(-) diff --git a/tests/dune_hello/dune b/tests/dune_hello/dune index 9c5f8d0da84..86f94bf3049 100644 --- a/tests/dune_hello/dune +++ b/tests/dune_hello/dune @@ -4,8 +4,3 @@ (libraries fstar.lib) (modes native) ) -(env - (_ - (bin_annot false) - (flags (:standard -w -A))) -) diff --git a/tests/semiring/Makefile b/tests/semiring/Makefile index 7e6b0f392fb..a67094ab53e 100644 --- a/tests/semiring/Makefile +++ b/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 diff --git a/tests/simple_hello/Makefile b/tests/simple_hello/Makefile index d4cbb66c1b3..384b2942d0d 100644 --- a/tests/simple_hello/Makefile +++ b/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 $@ From beb06996a19f8a7d26a5ee538fcb4b415e3bf1ec Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 17 Oct 2024 14:56:27 -0700 Subject: [PATCH 4/4] snap --- ocaml/fstar-lib/generated/FStarC_Main.ml | 50 ++++---------------- ocaml/fstar-lib/generated/FStarC_OCaml.ml | 48 +++++++++++++++++++ ocaml/fstar-lib/generated/FStarC_Options.ml | 52 ++++++++++++++++++++- 3 files changed, 109 insertions(+), 41 deletions(-) create mode 100644 ocaml/fstar-lib/generated/FStarC_OCaml.ml diff --git a/ocaml/fstar-lib/generated/FStarC_Main.ml b/ocaml/fstar-lib/generated/FStarC_Main.ml index a8146727a44..94101c318e9 100644 --- a/ocaml/fstar-lib/generated/FStarC_Main.ml +++ b/ocaml/fstar-lib/generated/FStarC_Main.ml @@ -131,45 +131,6 @@ let (fstar_files : Prims.string Prims.list FStar_Pervasives_Native.option FStarC_Compiler_Effect.ref) = FStarC_Compiler_Util.mk_ref FStar_Pervasives_Native.None -let (go_ocamlenv : Prims.string Prims.list -> unit) = - fun rest_args -> - if FStarC_Platform.system = FStarC_Platform.Windows - then - (let uu___1 = - let uu___2 = - FStarC_Errors_Msg.text - "--ocamlenv is not supported on Windows (yet?)" in - [uu___2] in - FStarC_Errors.raise_error0 - FStarC_Errors_Codes.Fatal_OptionsNotCompatible () - (Obj.magic FStarC_Errors_Msg.is_error_message_list_doc) - (Obj.magic uu___1)) - else (); - (let shellescape s = - let uu___1 = - let uu___2 = FStarC_Compiler_String.list_of_string s in - FStarC_Compiler_List.map - (fun uu___3 -> - match uu___3 with - | 39 -> "'\"'\"'" - | c -> FStarC_Compiler_String.make Prims.int_one c) uu___2 in - FStarC_Compiler_String.concat "" uu___1 in - let ocamldir = FStarC_Find.locate_ocaml () in - let old_ocamlpath = - let uu___1 = - FStarC_Compiler_Util.expand_environment_variable "OCAMLPATH" in - FStarC_Compiler_Util.dflt "" uu___1 in - let new_ocamlpath = - Prims.strcat ocamldir (Prims.strcat ":" old_ocamlpath) in - match rest_args with - | [] -> - ((let uu___2 = shellescape new_ocamlpath in - FStarC_Compiler_Util.print1 "OCAMLPATH='%s'; export OCAMLPATH;\n" - uu___2); - FStarC_Compiler_Effect.exit Prims.int_zero) - | cmd::args -> - (FStarC_Compiler_Util.putenv "OCAMLPATH" new_ocamlpath; - FStarC_Compiler_Util.execvp cmd (cmd :: args))) let (set_error_trap : unit -> unit) = fun uu___ -> let h = FStarC_Compiler_Util.get_sigint_handler () in @@ -442,7 +403,16 @@ let (go : unit -> unit) = fun uu___ -> let args = FStarC_Compiler_Util.get_cmd_args () in match args with - | uu___1::"--ocamlenv"::rest -> go_ocamlenv rest + | uu___1::"--ocamlenv"::[] -> + let new_ocamlpath = FStarC_OCaml.new_ocamlpath () in + ((let uu___3 = FStarC_OCaml.shellescape new_ocamlpath in + FStarC_Compiler_Util.print1 "OCAMLPATH='%s'; export OCAMLPATH;\n" + uu___3); + FStarC_Compiler_Effect.exit Prims.int_zero) + | uu___1::"--ocamlenv"::cmd::args1 -> + FStarC_OCaml.exec_in_ocamlenv cmd args1 + | uu___1::"--ocamlc"::rest -> FStarC_OCaml.exec_ocamlc rest + | uu___1::"--ocamlc_plugin"::rest -> FStarC_OCaml.exec_ocamlc_plugin rest | uu___1 -> go_normal () let (lazy_chooser : FStarC_Syntax_Syntax.lazy_kind -> diff --git a/ocaml/fstar-lib/generated/FStarC_OCaml.ml b/ocaml/fstar-lib/generated/FStarC_OCaml.ml new file mode 100644 index 00000000000..b167f842a35 --- /dev/null +++ b/ocaml/fstar-lib/generated/FStarC_OCaml.ml @@ -0,0 +1,48 @@ +open Prims +let (shellescape : Prims.string -> Prims.string) = + fun s -> + let uu___ = + let uu___1 = FStarC_Compiler_String.list_of_string s in + FStarC_Compiler_List.map + (fun uu___2 -> + match uu___2 with + | 39 -> "'\"'\"'" + | c -> FStarC_Compiler_String.make Prims.int_one c) uu___1 in + FStarC_Compiler_String.concat "" uu___ +let (new_ocamlpath : unit -> Prims.string) = + fun uu___ -> + let ocamldir = FStarC_Find.locate_ocaml () in + let old_ocamlpath = + let uu___1 = + FStarC_Compiler_Util.expand_environment_variable "OCAMLPATH" in + FStarC_Compiler_Util.dflt "" uu___1 in + let new_ocamlpath1 = + Prims.strcat ocamldir (Prims.strcat ":" old_ocamlpath) in + new_ocamlpath1 +let exec_in_ocamlenv : 'a . Prims.string -> Prims.string Prims.list -> 'a = + fun cmd -> + fun args -> + let new_ocamlpath1 = new_ocamlpath () in + if FStarC_Platform.system = FStarC_Platform.Windows + then + (let uu___1 = + let uu___2 = + FStarC_Errors_Msg.text + "--ocamlenv is not supported on Windows (yet?)" in + [uu___2] in + FStarC_Errors.raise_error0 + FStarC_Errors_Codes.Fatal_OptionsNotCompatible () + (Obj.magic FStarC_Errors_Msg.is_error_message_list_doc) + (Obj.magic uu___1)) + else (); + FStarC_Compiler_Util.putenv "OCAMLPATH" new_ocamlpath1; + FStarC_Compiler_Util.execvp cmd (cmd :: args); + failwith "execvp failed" +let exec_ocamlc : 'a . Prims.string Prims.list -> 'a = + fun args -> + exec_in_ocamlenv "ocamlfind" ("opt" :: "-w" :: "-8" :: "-linkpkg" :: + "-package" :: "fstar.lib" :: args) +let exec_ocamlc_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 diff --git a/ocaml/fstar-lib/generated/FStarC_Options.ml b/ocaml/fstar-lib/generated/FStarC_Options.ml index e067383b3ec..a6273f19aa9 100644 --- a/ocaml/fstar-lib/generated/FStarC_Options.ml +++ b/ocaml/fstar-lib/generated/FStarC_Options.ml @@ -3529,7 +3529,57 @@ let rec (specs_with_types : (Bool true)))), uu___280) in - [uu___279] in + let uu___280 + = + let uu___281 + = + let uu___282 + = + text + "A helper. This runs 'ocamlopt' in the environment set up by --ocamlenv, for building an F* application executable." in + (FStarC_Getopt.noshort, + "ocamlc", + (WithSideEffect + ((fun + uu___283 + -> + FStarC_Compiler_Util.print_error + "--ocamlc must be the first argument, see fstar.exe --help for details\n"; + FStarC_Compiler_Effect.exit + Prims.int_one), + (Const + (Bool + true)))), + uu___282) in + let uu___282 + = + let uu___283 + = + let uu___284 + = + text + "A helper. This runs 'ocamlopt' in the environment set up by --ocamlenv, for building an F* plugin from extracted files." in + (FStarC_Getopt.noshort, + "ocamlc_plugin", + (WithSideEffect + ((fun + uu___285 + -> + FStarC_Compiler_Util.print_error + "--ocamlc_plugin must be the first argument, see fstar.exe --help for details\n"; + FStarC_Compiler_Effect.exit + Prims.int_one), + (Const + (Bool + true)))), + uu___284) in + [uu___283] in + uu___281 + :: + uu___282 in + uu___279 + :: + uu___280 in uu___277 :: uu___278 in