From 978f7e1b8264f7d686f70af774d7aa0e5c70e0ce Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 14 Oct 2024 17:39:47 -0700 Subject: [PATCH 1/4] nit: reduce dependencies --- ulib/FStar.Tactics.CanonCommMonoidSimple.fst | 2 +- ulib/FStar.Tactics.Parametricity.fst | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/ulib/FStar.Tactics.CanonCommMonoidSimple.fst b/ulib/FStar.Tactics.CanonCommMonoidSimple.fst index 17305a9d45c..e534d902447 100644 --- a/ulib/FStar.Tactics.CanonCommMonoidSimple.fst +++ b/ulib/FStar.Tactics.CanonCommMonoidSimple.fst @@ -22,7 +22,7 @@ open FStar.Tactics.V2.Bare open FStar.Classical open FStar.Tactics.CanonCommSwaps -let term_eq = FStar.Tactics.V2.term_eq_old +let term_eq = FStar.Stubs.Tactics.V2.Builtins.term_eq_old (* A simple expression canonizer for commutative monoids. For a canonizer with more features see FStar.Tactics.CanonCommMonoid.fst. diff --git a/ulib/FStar.Tactics.Parametricity.fst b/ulib/FStar.Tactics.Parametricity.fst index 51c68d5855a..8f5b3463ac9 100644 --- a/ulib/FStar.Tactics.Parametricity.fst +++ b/ulib/FStar.Tactics.Parametricity.fst @@ -319,7 +319,7 @@ let param_inductive (se:sigelt) (fv0 fv1 : fv) : Tac decls = //Tactics.Util.iter (fun bv -> dump ("param bv = " ^ binder_to_string bv)) param_bs; let typ = mk_e_app (param' s typ) [replace_by s false orig; replace_by s true orig] in (* dump ("new typ = " ^ term_to_string typ); *) - let ctors = Tactics.V2.Bare.map (param_ctor nm s) ctors in + let ctors = Tactics.Util.map (param_ctor nm s) ctors in let se = Sg_Inductive {nm=inspect_fv fv1; univs; params=param_bs; typ; ctors} in (* dump ("param_ind : " ^ term_to_string (quote se)); *) [pack_sigelt se] From 2f175019e4368291609ad347e16d22ceae19a6f5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 14 Oct 2024 18:29:29 -0700 Subject: [PATCH 2/4] Tactics.Unseal: move to Stubs --- .../{FStar_Tactics_Unseal.ml => FStarC_Tactics_Unseal.ml} | 0 src/parser/FStarC.Parser.Const.fst | 2 +- ...tar.Tactics.Unseal.fsti => FStar.Stubs.Tactics.Unseal.fsti} | 2 +- ulib/FStar.Stubs.Tactics.V1.Builtins.fsti | 3 +-- ulib/FStar.Stubs.Tactics.V2.Builtins.fsti | 3 +-- 5 files changed, 4 insertions(+), 6 deletions(-) rename ocaml/fstar-lib/{FStar_Tactics_Unseal.ml => FStarC_Tactics_Unseal.ml} (100%) rename ulib/{FStar.Tactics.Unseal.fsti => FStar.Stubs.Tactics.Unseal.fsti} (95%) diff --git a/ocaml/fstar-lib/FStar_Tactics_Unseal.ml b/ocaml/fstar-lib/FStarC_Tactics_Unseal.ml similarity index 100% rename from ocaml/fstar-lib/FStar_Tactics_Unseal.ml rename to ocaml/fstar-lib/FStarC_Tactics_Unseal.ml diff --git a/src/parser/FStarC.Parser.Const.fst b/src/parser/FStarC.Parser.Const.fst index c37ad430fc5..506c4aae997 100644 --- a/src/parser/FStarC.Parser.Const.fst +++ b/src/parser/FStarC.Parser.Const.fst @@ -573,7 +573,7 @@ let fext_on_dom_g_lid = fext_lid "on_dom_g" let sealed_lid = p2l ["FStar"; "Sealed"; "sealed"] let seal_lid = p2l ["FStar"; "Sealed"; "seal"] -let unseal_lid = p2l ["FStar"; "Tactics"; "Unseal"; "unseal"] (* In a separate module due to the mention of TAC *) +let unseal_lid = p2l ["FStar"; "Stubs"; "Tactics"; "Unseal"; "unseal"] (* In a separate module due to the mention of TAC *) let map_seal_lid = p2l ["FStar"; "Sealed"; "map_seal"] let bind_seal_lid = p2l ["FStar"; "Sealed"; "bind_seal"] let tref_lid = p2l ["FStar"; "Stubs"; "Tactics"; "Types"; "tref"] diff --git a/ulib/FStar.Tactics.Unseal.fsti b/ulib/FStar.Stubs.Tactics.Unseal.fsti similarity index 95% rename from ulib/FStar.Tactics.Unseal.fsti rename to ulib/FStar.Stubs.Tactics.Unseal.fsti index b2ee8515f9e..db321b34fe4 100644 --- a/ulib/FStar.Tactics.Unseal.fsti +++ b/ulib/FStar.Stubs.Tactics.Unseal.fsti @@ -16,7 +16,7 @@ (** The [unseal] primitive to observe sealed values. *) -module FStar.Tactics.Unseal +module FStar.Stubs.Tactics.Unseal open FStar.Sealed open FStar.Tactics.Effect diff --git a/ulib/FStar.Stubs.Tactics.V1.Builtins.fsti b/ulib/FStar.Stubs.Tactics.V1.Builtins.fsti index 8a268c6a812..de18e6838f6 100644 --- a/ulib/FStar.Stubs.Tactics.V1.Builtins.fsti +++ b/ulib/FStar.Stubs.Tactics.V1.Builtins.fsti @@ -26,8 +26,7 @@ open FStar.Stubs.Reflection.V1.Data open FStar.Reflection.Const open FStar.Tactics.Effect open FStar.Stubs.Tactics.Types - -include FStar.Tactics.Unseal +include FStar.Stubs.Tactics.Unseal (** [top_env] returns the environment where the tactic started running. * This works even if no goals are present. *) diff --git a/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti b/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti index 2daa44035b9..a2c09a5d71c 100644 --- a/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti +++ b/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti @@ -27,8 +27,7 @@ open FStar.Stubs.Reflection.V2.Builtins open FStar.Tactics.Effect open FStar.Tactics.Effect open FStar.Stubs.Tactics.Types - -include FStar.Tactics.Unseal +include FStar.Stubs.Tactics.Unseal (** Resolve unification variable indirections at the top of the term. *) val compress : term -> Tac term From c683a67b3a52704633340d527643155df3813473 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 14 Oct 2024 21:34:35 -0700 Subject: [PATCH 3/4] snap --- ocaml/fstar-lib/generated/FStarC_Parser_Const.ml | 2 +- .../generated/FStar_InteractiveHelpers_Base.ml | 6 +++--- .../generated/FStar_InteractiveHelpers_ExploreTerm.ml | 2 +- .../generated/FStar_InteractiveHelpers_PostProcess.ml | 2 +- .../fstar-lib/generated/FStar_Reflection_V1_Formula.ml | 2 +- .../fstar-lib/generated/FStar_Reflection_V2_Formula.ml | 2 +- .../fstar-lib/generated/FStar_Tactics_MkProjectors.ml | 6 +++--- ocaml/fstar-lib/generated/FStar_Tactics_NamedView.ml | 2 +- .../fstar-lib/generated/FStar_Tactics_Parametricity.ml | 8 ++++---- .../generated/FStar_Tactics_PatternMatching.ml | 6 +++--- ocaml/fstar-lib/generated/FStar_Tactics_Print.ml | 2 +- ocaml/fstar-lib/generated/FStar_Tactics_V1_Derived.ml | 2 +- ocaml/fstar-lib/generated/FStar_Tactics_V2_Derived.ml | 10 +++++----- 13 files changed, 26 insertions(+), 26 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStarC_Parser_Const.ml b/ocaml/fstar-lib/generated/FStarC_Parser_Const.ml index fccd08dcf26..f9fc87ee90a 100644 --- a/ocaml/fstar-lib/generated/FStarC_Parser_Const.ml +++ b/ocaml/fstar-lib/generated/FStarC_Parser_Const.ml @@ -665,7 +665,7 @@ let (fext_on_dom_g_lid : FStarC_Ident.lident) = fext_lid "on_dom_g" let (sealed_lid : FStarC_Ident.lident) = p2l ["FStar"; "Sealed"; "sealed"] let (seal_lid : FStarC_Ident.lident) = p2l ["FStar"; "Sealed"; "seal"] let (unseal_lid : FStarC_Ident.lident) = - p2l ["FStar"; "Tactics"; "Unseal"; "unseal"] + p2l ["FStar"; "Stubs"; "Tactics"; "Unseal"; "unseal"] let (map_seal_lid : FStarC_Ident.lident) = p2l ["FStar"; "Sealed"; "map_seal"] let (bind_seal_lid : FStarC_Ident.lident) = diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Base.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Base.ml index f95c54133d8..72632ed0e50 100644 --- a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Base.ml +++ b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Base.ml @@ -1541,7 +1541,7 @@ let rec bind_map_get_from_name : (fun b'v -> let uu___1 = let uu___2 = - FStar_Tactics_Unseal.unseal + FStarC_Tactics_Unseal.unseal b'v.FStarC_Reflection_V1_Data.bv_ppname in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal @@ -4838,7 +4838,7 @@ and (deep_apply_subst_in_pattern : (Obj.repr (let uu___ = let uu___1 = - let uu___2 = FStar_Tactics_Unseal.unseal st in + let uu___2 = FStarC_Tactics_Unseal.unseal st in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic @@ -5158,7 +5158,7 @@ let rec (_generate_shadowed_subst : (fun ty -> let uu___6 = - FStar_Tactics_Unseal.unseal + FStarC_Tactics_Unseal.unseal bvv.FStarC_Reflection_V1_Data.bv_ppname in Obj.magic (FStar_Tactics_Effect.tac_bind diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_ExploreTerm.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_ExploreTerm.ml index db662d497d9..da9da5672a4 100644 --- a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_ExploreTerm.ml +++ b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_ExploreTerm.ml @@ -5041,7 +5041,7 @@ and (explore_pattern : (Obj.repr (let uu___2 = let uu___3 = - FStar_Tactics_Unseal.unseal st in + FStarC_Tactics_Unseal.unseal st in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_PostProcess.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_PostProcess.ml index fce637176d6..888dce77f92 100644 --- a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_PostProcess.ml +++ b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_PostProcess.ml @@ -2075,7 +2075,7 @@ let (analyze_effectful_term : = let uu___17 = - FStar_Tactics_Unseal.unseal + FStarC_Tactics_Unseal.unseal bvv0.FStarC_Reflection_V1_Data.bv_ppname in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal diff --git a/ocaml/fstar-lib/generated/FStar_Reflection_V1_Formula.ml b/ocaml/fstar-lib/generated/FStar_Reflection_V1_Formula.ml index 026daa98ed4..aaf2f853e05 100644 --- a/ocaml/fstar-lib/generated/FStar_Reflection_V1_Formula.ml +++ b/ocaml/fstar-lib/generated/FStar_Reflection_V1_Formula.ml @@ -22,7 +22,7 @@ let (bv_to_string : (fun uu___1 -> (fun bvv -> Obj.magic - (FStar_Tactics_Unseal.unseal + (FStarC_Tactics_Unseal.unseal bvv.FStarC_Reflection_V1_Data.bv_ppname)) uu___1) let rec (inspect_unascribe : FStarC_Reflection_Types.term -> diff --git a/ocaml/fstar-lib/generated/FStar_Reflection_V2_Formula.ml b/ocaml/fstar-lib/generated/FStar_Reflection_V2_Formula.ml index 6e8dfdcc7c6..55e3ed5b8e3 100644 --- a/ocaml/fstar-lib/generated/FStar_Reflection_V2_Formula.ml +++ b/ocaml/fstar-lib/generated/FStar_Reflection_V2_Formula.ml @@ -1152,7 +1152,7 @@ let (namedv_to_string : (fun uu___1 -> (fun namedvv -> Obj.magic - (FStar_Tactics_Unseal.unseal + (FStarC_Tactics_Unseal.unseal namedvv.FStarC_Reflection_V2_Data.ppname)) uu___1) let (formula_to_string : formula -> (Prims.string, unit) FStar_Tactics_Effect.tac_repr) = diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_MkProjectors.ml b/ocaml/fstar-lib/generated/FStar_Tactics_MkProjectors.ml index c3685c5ad9e..49e90793ba8 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_MkProjectors.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_MkProjectors.ml @@ -704,7 +704,7 @@ let (mk_proj_decl : debug (fun uu___1 -> let uu___2 = - FStar_Tactics_Unseal.unseal + FStarC_Tactics_Unseal.unseal field.FStar_Tactics_NamedView.ppname in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal @@ -914,7 +914,7 @@ let (mk_proj_decl : = let uu___15 = - FStar_Tactics_Unseal.unseal + FStarC_Tactics_Unseal.unseal field.FStar_Tactics_NamedView.ppname in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal @@ -1492,7 +1492,7 @@ let (mk_proj_decl : = let uu___22 = - FStar_Tactics_Unseal.unseal + FStarC_Tactics_Unseal.unseal field.FStar_Tactics_NamedView.ppname in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_NamedView.ml b/ocaml/fstar-lib/generated/FStar_Tactics_NamedView.ml index 35cecb5a765..246699a6fd8 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_NamedView.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_NamedView.ml @@ -2271,7 +2271,7 @@ let rec (open_pat : | FStarC_Reflection_V2_Data.Pat_Var (ssort, n) -> Obj.magic (Obj.repr - (let uu___ = FStar_Tactics_Unseal.unseal ssort in + (let uu___ = FStarC_Tactics_Unseal.unseal ssort in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Parametricity.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Parametricity.ml index e4273400666..b7449188997 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_Parametricity.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_Parametricity.ml @@ -2107,7 +2107,7 @@ and (param_pat : Obj.magic (Obj.repr (let uu___1 = - let uu___2 = FStar_Tactics_Unseal.unseal sort in + let uu___2 = FStarC_Tactics_Unseal.unseal sort in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic @@ -2363,7 +2363,7 @@ and (push_binder : (fun uu___2 -> (fun typ -> let uu___2 = - FStar_Tactics_Unseal.unseal + FStarC_Tactics_Unseal.unseal b.FStar_Tactics_NamedView.ppname in Obj.magic (FStar_Tactics_Effect.tac_bind @@ -3910,13 +3910,13 @@ let (param_inductive : (Prims.of_int (322)) (Prims.of_int (16)) (Prims.of_int (322)) - (Prims.of_int (59))))) + (Prims.of_int (56))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Parametricity.fst" (Prims.of_int (322)) - (Prims.of_int (62)) + (Prims.of_int (59)) (Prims.of_int (325)) (Prims.of_int (20))))) (Obj.magic diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_PatternMatching.ml b/ocaml/fstar-lib/generated/FStar_Tactics_PatternMatching.ml index 9bc5f96284f..49b6e9e45c1 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_PatternMatching.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_PatternMatching.ml @@ -2266,7 +2266,7 @@ let (name_of_namedv : (Prims.string, unit) FStar_Tactics_Effect.tac_repr) = fun x -> - FStar_Tactics_Unseal.unseal + FStarC_Tactics_Unseal.unseal (FStar_Tactics_NamedView.inspect_namedv x).FStarC_Reflection_V2_Data.ppname let rec (pattern_of_term_ex : FStarC_Reflection_Types.term -> @@ -2747,7 +2747,7 @@ let (cleanup_abspat : let (name_of_named_binder : FStar_Tactics_NamedView.binder -> (Prims.string, unit) FStar_Tactics_Effect.tac_repr) - = fun nb -> FStar_Tactics_Unseal.unseal nb.FStar_Tactics_NamedView.ppname + = fun nb -> FStarC_Tactics_Unseal.unseal nb.FStar_Tactics_NamedView.ppname let (matching_problem_of_abs : FStar_Tactics_NamedView.term -> ((matching_problem * abspat_continuation), unit) @@ -3766,7 +3766,7 @@ let (abspat_arg_of_abspat_argspec : let uu___2 = let uu___3 = let uu___4 = - FStar_Tactics_Unseal.unseal + FStarC_Tactics_Unseal.unseal (argspec.asa_name).FStarC_Reflection_V2_Data.ppname3 in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Print.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Print.ml index 929327587f4..2af1f86a317 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_Print.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_Print.ml @@ -5,7 +5,7 @@ let (namedv_to_string : = fun x -> let uu___ = - FStar_Tactics_Unseal.unseal x.FStarC_Reflection_V2_Data.ppname in + FStarC_Tactics_Unseal.unseal x.FStarC_Reflection_V2_Data.ppname in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V1_Derived.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V1_Derived.ml index 7edb91e2ac1..2b98f67d299 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V1_Derived.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V1_Derived.ml @@ -8,7 +8,7 @@ let (name_of_bv : (Prims.string, unit) FStar_Tactics_Effect.tac_repr) = fun bv -> - FStar_Tactics_Unseal.unseal + FStarC_Tactics_Unseal.unseal (FStarC_Reflection_V1_Builtins.inspect_bv bv).FStarC_Reflection_V1_Data.bv_ppname let (bv_to_string : FStarC_Reflection_Types.bv -> diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Derived.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Derived.ml index 376991dbc5e..e28d77e7458 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Derived.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Derived.ml @@ -11,7 +11,7 @@ let (name_of_bv : (Prims.string, unit) FStar_Tactics_Effect.tac_repr) = fun bv -> - FStar_Tactics_Unseal.unseal + FStarC_Tactics_Unseal.unseal (FStar_Tactics_NamedView.inspect_bv bv).FStarC_Reflection_V2_Data.ppname1 let (bv_to_string : FStar_Tactics_NamedView.bv -> @@ -20,7 +20,7 @@ let (bv_to_string : let (name_of_binder : FStar_Tactics_NamedView.binder -> (Prims.string, unit) FStar_Tactics_Effect.tac_repr) - = fun b -> FStar_Tactics_Unseal.unseal b.FStar_Tactics_NamedView.ppname + = fun b -> FStarC_Tactics_Unseal.unseal b.FStar_Tactics_NamedView.ppname let (binder_to_string : FStar_Tactics_NamedView.binder -> (Prims.string, unit) FStar_Tactics_Effect.tac_repr) @@ -129,13 +129,13 @@ let (binder_to_string : let (binding_to_string : FStar_Tactics_NamedView.binding -> (Prims.string, unit) FStar_Tactics_Effect.tac_repr) - = fun b -> FStar_Tactics_Unseal.unseal b.FStarC_Reflection_V2_Data.ppname3 + = fun b -> FStarC_Tactics_Unseal.unseal b.FStarC_Reflection_V2_Data.ppname3 let (type_of_var : FStar_Tactics_NamedView.namedv -> (FStarC_Reflection_Types.typ, unit) FStar_Tactics_Effect.tac_repr) = fun x -> - FStar_Tactics_Unseal.unseal + FStarC_Tactics_Unseal.unseal (FStar_Tactics_NamedView.inspect_namedv x).FStarC_Reflection_V2_Data.sort let (type_of_binding : FStar_Tactics_NamedView.binding -> FStarC_Reflection_Types.typ) = @@ -5266,7 +5266,7 @@ let (namedv_to_simple_binder : (fun uu___1 -> (fun nv -> let uu___1 = - FStar_Tactics_Unseal.unseal nv.FStarC_Reflection_V2_Data.sort in + FStarC_Tactics_Unseal.unseal nv.FStarC_Reflection_V2_Data.sort in Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal From 3f8b702d9c943a47e16a785bf8b2c01457f03321 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 14 Oct 2024 12:21:10 -0700 Subject: [PATCH 4/4] Introduce tests/dune_hello --- tests/Makefile | 1 + tests/dune_hello/.gitignore | 3 +++ tests/dune_hello/Hello.fst | 5 +++++ tests/dune_hello/Makefile | 15 +++++++++++++++ tests/dune_hello/dune | 11 +++++++++++ tests/dune_hello/dune-project | 7 +++++++ 6 files changed, 42 insertions(+) create mode 100644 tests/dune_hello/.gitignore create mode 100644 tests/dune_hello/Hello.fst create mode 100644 tests/dune_hello/Makefile create mode 100644 tests/dune_hello/dune create mode 100644 tests/dune_hello/dune-project diff --git a/tests/Makefile b/tests/Makefile index 8fad46f21c1..e864166662f 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -20,6 +20,7 @@ ALL_TEST_DIRS += typeclasses ALL_TEST_DIRS += vale ALL_TEST_DIRS += hacl ALL_TEST_DIRS += simple_hello +ALL_TEST_DIRS += dune_hello HAS_OCAML := $(shell which ocamlfind 2>/dev/null) ifneq (,$(HAS_OCAML)) diff --git a/tests/dune_hello/.gitignore b/tests/dune_hello/.gitignore new file mode 100644 index 00000000000..dc72cf78a16 --- /dev/null +++ b/tests/dune_hello/.gitignore @@ -0,0 +1,3 @@ +*.ml +_build +lib diff --git a/tests/dune_hello/Hello.fst b/tests/dune_hello/Hello.fst new file mode 100644 index 00000000000..a9517fd46c5 --- /dev/null +++ b/tests/dune_hello/Hello.fst @@ -0,0 +1,5 @@ +module Hello + +open FStar.IO + +let _ = print_string "Hi!\n" diff --git a/tests/dune_hello/Makefile b/tests/dune_hello/Makefile new file mode 100644 index 00000000000..d37c40926e1 --- /dev/null +++ b/tests/dune_hello/Makefile @@ -0,0 +1,15 @@ +FSTAR_EXE ?= ../../bin/fstar.exe + +.PHONY: all +all: run + +Hello.ml: Hello.fst + $(FSTAR_EXE) --codegen OCaml Hello.fst --extract Hello + +bin/hello.exe: Hello.ml + $(FSTAR_EXE) --ocamlenv dune build @install --profile=release + $(FSTAR_EXE) --ocamlenv dune install --prefix=. + +.PHONY: run +run: bin/hello.exe + ./bin/hello.exe | grep "Hi!" diff --git a/tests/dune_hello/dune b/tests/dune_hello/dune new file mode 100644 index 00000000000..9c5f8d0da84 --- /dev/null +++ b/tests/dune_hello/dune @@ -0,0 +1,11 @@ +(executable + (name hello) + (public_name hello.exe) + (libraries fstar.lib) + (modes native) +) +(env + (_ + (bin_annot false) + (flags (:standard -w -A))) +) diff --git a/tests/dune_hello/dune-project b/tests/dune_hello/dune-project new file mode 100644 index 00000000000..6d145823c5f --- /dev/null +++ b/tests/dune_hello/dune-project @@ -0,0 +1,7 @@ +(lang dune 3.8) +(name hello) + +(package + (name hello) + (synopsis "An example F* application") +)