From c52f271268bfc161cb0d30a837a12441326f2460 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 17 Oct 2024 18:04:19 -0700 Subject: [PATCH 1/3] fstar: rename --ocamlc to --ocamlopt, add --ocamlc for bytecode --- src/basic/FStarC.Options.fst | 13 +++++++++---- src/fstar/FStarC.Main.fst | 7 +++++-- src/fstar/FStarC.OCaml.fst | 6 +++++- src/fstar/FStarC.OCaml.fsti | 24 ++++++++++++++++-------- tests/semiring/Makefile | 2 +- 5 files changed, 36 insertions(+), 16 deletions(-) diff --git a/src/basic/FStarC.Options.fst b/src/basic/FStarC.Options.fst index a0b32cf9f60..71649bfc83d 100644 --- a/src/basic/FStarC.Options.fst +++ b/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) = diff --git a/src/fstar/FStarC.Main.fst b/src/fstar/FStarC.Main.fst index 5f2691d4717..f3f0d8f3c15 100644 --- a/src/fstar/FStarC.Main.fst +++ b/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 () diff --git a/src/fstar/FStarC.OCaml.fst b/src/fstar/FStarC.OCaml.fst index 610661a332a..e40a621293d 100644 --- a/src/fstar/FStarC.OCaml.fst +++ b/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) diff --git a/src/fstar/FStarC.OCaml.fsti b/src/fstar/FStarC.OCaml.fsti index 1719ce5bec3..9b095824b3a 100644 --- a/src/fstar/FStarC.OCaml.fsti +++ b/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 diff --git a/tests/semiring/Makefile b/tests/semiring/Makefile index a67094ab53e..6a4dfb7cff8 100644 --- a/tests/semiring/Makefile +++ b/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 From 443289c2ba3c37fb17fc23d3641c24371e7bc4e2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 17 Oct 2024 18:07:06 -0700 Subject: [PATCH 2/3] simple_hello/dune_hello: test bytecode too --- tests/dune_hello/Makefile | 2 ++ tests/dune_hello/dune | 5 ++++- tests/simple_hello/Makefile | 10 +++++++--- 3 files changed, 13 insertions(+), 4 deletions(-) diff --git a/tests/dune_hello/Makefile b/tests/dune_hello/Makefile index 84107aea18d..99e2277ff37 100644 --- a/tests/dune_hello/Makefile +++ b/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 diff --git a/tests/dune_hello/dune b/tests/dune_hello/dune index 86f94bf3049..e1bb73c8a6b 100644 --- a/tests/dune_hello/dune +++ b/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)))) diff --git a/tests/simple_hello/Makefile b/tests/simple_hello/Makefile index 14bfea61f9b..728af2a84e2 100644 --- a/tests/simple_hello/Makefile +++ b/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 From 0ac83562eae8083333ea83299089763072d68684 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 17 Oct 2024 18:09:23 -0700 Subject: [PATCH 3/3] snap --- ocaml/fstar-lib/generated/FStarC_Main.ml | 4 ++- ocaml/fstar-lib/generated/FStarC_OCaml.ml | 6 +++- ocaml/fstar-lib/generated/FStarC_Options.ml | 35 ++++++++++++++++++--- 3 files changed, 38 insertions(+), 7 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStarC_Main.ml b/ocaml/fstar-lib/generated/FStarC_Main.ml index 94101c318e9..24bdc28d43e 100644 --- a/ocaml/fstar-lib/generated/FStarC_Main.ml +++ b/ocaml/fstar-lib/generated/FStarC_Main.ml @@ -412,7 +412,9 @@ let (go : unit -> unit) = | 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::"--ocamlopt"::rest -> FStarC_OCaml.exec_ocamlopt rest + | uu___1::"--ocamlopt_plugin"::rest -> + FStarC_OCaml.exec_ocamlopt_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 index b167f842a35..b780e413aec 100644 --- a/ocaml/fstar-lib/generated/FStarC_OCaml.ml +++ b/ocaml/fstar-lib/generated/FStarC_OCaml.ml @@ -39,10 +39,14 @@ let exec_in_ocamlenv : 'a . Prims.string -> Prims.string Prims.list -> 'a = 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" ("c" :: "-w" :: "-8" :: "-linkpkg" :: + "-package" :: "fstar.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) -let exec_ocamlc_plugin : 'a . Prims.string Prims.list -> 'a = +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 diff --git a/ocaml/fstar-lib/generated/FStarC_Options.ml b/ocaml/fstar-lib/generated/FStarC_Options.ml index a6273f19aa9..dd03a623717 100644 --- a/ocaml/fstar-lib/generated/FStarC_Options.ml +++ b/ocaml/fstar-lib/generated/FStarC_Options.ml @@ -3536,7 +3536,7 @@ let rec (specs_with_types : let uu___282 = text - "A helper. This runs 'ocamlopt' in the environment set up by --ocamlenv, for building an F* application executable." in + "A helper. This runs 'ocamlc' in the environment set up by --ocamlenv, for building an F* application bytecode executable." in (FStarC_Getopt.noshort, "ocamlc", (WithSideEffect @@ -3558,22 +3558,47 @@ let rec (specs_with_types : 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 + "A helper. This runs 'ocamlopt' in the environment set up by --ocamlenv, for building an F* application native executable." in (FStarC_Getopt.noshort, - "ocamlc_plugin", + "ocamlopt", (WithSideEffect ((fun uu___285 -> FStarC_Compiler_Util.print_error - "--ocamlc_plugin must be the first argument, see fstar.exe --help for details\n"; + "--ocamlopt 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 + let uu___284 + = + let uu___285 + = + let uu___286 + = + text + "A helper. This runs 'ocamlopt' in the environment set up by --ocamlenv, for building an F* plugin." in + (FStarC_Getopt.noshort, + "ocamlopt_plugin", + (WithSideEffect + ((fun + uu___287 + -> + FStarC_Compiler_Util.print_error + "--ocamlopt_plugin must be the first argument, see fstar.exe --help for details\n"; + FStarC_Compiler_Effect.exit + Prims.int_one), + (Const + (Bool + true)))), + uu___286) in + [uu___285] in + uu___283 + :: + uu___284 in uu___281 :: uu___282 in