From d575a6a842dd8da923286afb5eff1ad66e8fe4ed Mon Sep 17 00:00:00 2001 From: Johannes Blaser Date: Wed, 29 Jan 2025 15:58:31 +0100 Subject: [PATCH 1/8] Reverted removal of Z3 version check fix which breaks when Z3 binaries output additional information after the version number when calling z3 --version --- src/smtencoding/FStarC.SMTEncoding.Z3.fst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smtencoding/FStarC.SMTEncoding.Z3.fst b/src/smtencoding/FStarC.SMTEncoding.Z3.fst index a20469feddb..4969be078c4 100644 --- a/src/smtencoding/FStarC.SMTEncoding.Z3.fst +++ b/src/smtencoding/FStarC.SMTEncoding.Z3.fst @@ -176,7 +176,7 @@ let check_z3version (p:proc) : unit = ); _already_warned_solver_mismatch := true ); - let ver_found : string = BU.trim_string (getinfo "version") in + let ver_found : string = BU.trim_string (List.hd (BU.split (getinfo "version") "-")) in let ver_conf : string = BU.trim_string (Options.z3_version ()) in if ver_conf <> ver_found && not (!_already_warned_version_mismatch) then ( let open FStarC.Errors in From 91b8c024887634b88bb1625bd1bcf49e53a8dcac Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 29 Jan 2025 17:51:53 -0800 Subject: [PATCH 2/8] Makefile: macos compatibility --- Makefile | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Makefile b/Makefile index 9be23b6b9ae..f7b7c61b0ec 100644 --- a/Makefile +++ b/Makefile @@ -310,11 +310,11 @@ endif setlink-%: if [ -e out ] && ! [ -h out ]; then echo "ERROR: out/ exists and is not a symbolic link, please remove it"; false; fi - ln -Trsf stage$*/out out + rm -f out && ln -sf $(CURDIR)/stage$*/out out # For compatibility with the previous layout mkdir -p bin - ln -Trsf out/bin/fstar.exe bin/fstar.exe - ln -Trsf .scripts/get_fstar_z3.sh bin/get_fstar_z3.sh + ln -sf $(CURDIR)/out/bin/fstar.exe bin/fstar.exe + ln -sf $(CURDIR)/.scripts/get_fstar_z3.sh bin/get_fstar_z3.sh stage1: .install-stage1.touch 1: stage1 From dde3d94ec632bed11bdaf74e3871a3cfbce04254 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 30 Jan 2025 08:56:27 -0800 Subject: [PATCH 3/8] Z3: add a comment about version checking --- src/smtencoding/FStarC.SMTEncoding.Z3.fst | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/smtencoding/FStarC.SMTEncoding.Z3.fst b/src/smtencoding/FStarC.SMTEncoding.Z3.fst index 4969be078c4..9652190e69b 100644 --- a/src/smtencoding/FStarC.SMTEncoding.Z3.fst +++ b/src/smtencoding/FStarC.SMTEncoding.Z3.fst @@ -176,6 +176,11 @@ let check_z3version (p:proc) : unit = ); _already_warned_solver_mismatch := true ); + (* Note: Z3 can either output a "clean" version like 4.13.4 or something like + "4.13.4 - build hashcode 6d3cfb63daa9afdd7d6d6b4d2f2fb84bd7324571" depending + on how it was built. Hence we split by "-" and take the first component to + ignore the hashcode. See https://github.com/FStarLang/FStar/pull/3700 for + more details. *) let ver_found : string = BU.trim_string (List.hd (BU.split (getinfo "version") "-")) in let ver_conf : string = BU.trim_string (Options.z3_version ()) in if ver_conf <> ver_found && not (!_already_warned_version_mismatch) then ( From 13a2b8901a8cc92b4b108eacdefeb592694077f8 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Thu, 30 Jan 2025 14:54:53 +0000 Subject: [PATCH 4/8] allow use_hints even when context_pruning is set --- src/smtencoding/FStarC.SMTEncoding.Solver.fst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smtencoding/FStarC.SMTEncoding.Solver.fst b/src/smtencoding/FStarC.SMTEncoding.Solver.fst index 91b6337a299..c6cd200a8b0 100644 --- a/src/smtencoding/FStarC.SMTEncoding.Solver.fst +++ b/src/smtencoding/FStarC.SMTEncoding.Solver.fst @@ -65,7 +65,7 @@ let replaying_hints: ref (option hints) = BU.mk_ref None (****************************************************************************) (* Hint databases (public) *) (****************************************************************************) -let use_hints () = Options.use_hints () && Options.Ext.get "context_pruning" = "" +let use_hints () = Options.use_hints () let initialize_hints_db src_filename format_filename : unit = if Options.record_hints() then recorded_hints := Some []; let norm_src_filename = BU.normalize_file_path src_filename in From cfa0715592bfe16b16fc240c93ae6eab11d4dcfc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 30 Jan 2025 14:31:14 -0800 Subject: [PATCH 5/8] build: simplify, coallescing src/ml/full into ulib/ml/plugin, move src/ml/bare -> src/ml This separation did not make sense, files in both src/ml/full and ulib/ml/plugin are there for the support of plugins only, and not needed for the bare compiler. So we can coallesce these directories into ulib/ml/plugin, and place all compiler ML files in just src/ml. --- src/ml/{bare => }/FStarC_BaseTypes.ml | 0 src/ml/{bare => }/FStarC_BigInt.ml | 0 src/ml/{bare => }/FStarC_Bytes.ml | 0 src/ml/{bare => }/FStarC_Dyn.ml | 0 src/ml/{bare => }/FStarC_Effect.ml | 0 src/ml/{bare => }/FStarC_Extraction_ML_PrintML.ml | 0 src/ml/{bare => }/FStarC_Getopt.ml | 0 src/ml/{bare => }/FStarC_Hash.ml | 0 src/ml/{bare => }/FStarC_Hints.ml | 0 src/ml/{bare => }/FStarC_Json.ml | 0 src/ml/{bare => }/FStarC_List.ml | 0 src/ml/{bare => }/FStarC_Parser_LexFStar.ml | 0 src/ml/{bare => }/FStarC_Parser_Parse.mly | 0 src/ml/{bare => }/FStarC_Parser_ParseIt.ml | 0 src/ml/{bare => }/FStarC_Parser_Utf8.ml | 0 src/ml/{bare => }/FStarC_Parser_Util.ml | 0 src/ml/{bare => }/FStarC_Platform.ml | 0 src/ml/{bare => }/FStarC_Plugins_Base.ml | 0 src/ml/{bare => }/FStarC_Pprint.ml | 0 src/ml/{bare => }/FStarC_Range.ml | 0 src/ml/{bare => }/FStarC_Reflection_Types.ml | 0 src/ml/{bare => }/FStarC_Sedlexing.ml | 0 src/ml/{bare => }/FStarC_String.ml | 0 src/ml/{bare => }/FStarC_StringBuffer.ml | 0 src/ml/{bare => }/FStarC_Syntax_TermHashTable.ml | 0 src/ml/{bare => }/FStarC_Tactics_Native.ml | 0 src/ml/{bare => }/FStarC_Unionfind.ml | 0 src/ml/{bare => }/FStarC_Util.ml | 0 stage1/dune/fstar-guts/FStarC_Parser_Parse.mly | 2 +- stage1/dune/fstar-guts/bare | 1 - stage1/dune/fstar-guts/ml | 1 + stage1/dune/fstar-plugins/full | 1 - stage1/dune/libplugin/full | 1 - stage2/dune/fstar-guts/FStarC_Parser_Parse.mly | 2 +- stage2/dune/fstar-guts/bare | 1 - stage2/dune/fstar-guts/ml | 1 + stage2/dune/fstar-plugins/full | 1 - stage2/dune/libplugin/full | 1 - {src/ml/full => ulib/ml/plugin}/FStarC_Tactics_Unseal.ml | 0 {src/ml/full => ulib/ml/plugin}/FStarC_Tactics_V1_Builtins.ml | 0 {src/ml/full => ulib/ml/plugin}/FStarC_Tactics_V2_Builtins.ml | 0 41 files changed, 4 insertions(+), 8 deletions(-) rename src/ml/{bare => }/FStarC_BaseTypes.ml (100%) rename src/ml/{bare => }/FStarC_BigInt.ml (100%) rename src/ml/{bare => }/FStarC_Bytes.ml (100%) rename src/ml/{bare => }/FStarC_Dyn.ml (100%) rename src/ml/{bare => }/FStarC_Effect.ml (100%) rename src/ml/{bare => }/FStarC_Extraction_ML_PrintML.ml (100%) rename src/ml/{bare => }/FStarC_Getopt.ml (100%) rename src/ml/{bare => }/FStarC_Hash.ml (100%) rename src/ml/{bare => }/FStarC_Hints.ml (100%) rename src/ml/{bare => }/FStarC_Json.ml (100%) rename src/ml/{bare => }/FStarC_List.ml (100%) rename src/ml/{bare => }/FStarC_Parser_LexFStar.ml (100%) rename src/ml/{bare => }/FStarC_Parser_Parse.mly (100%) rename src/ml/{bare => }/FStarC_Parser_ParseIt.ml (100%) rename src/ml/{bare => }/FStarC_Parser_Utf8.ml (100%) rename src/ml/{bare => }/FStarC_Parser_Util.ml (100%) rename src/ml/{bare => }/FStarC_Platform.ml (100%) rename src/ml/{bare => }/FStarC_Plugins_Base.ml (100%) rename src/ml/{bare => }/FStarC_Pprint.ml (100%) rename src/ml/{bare => }/FStarC_Range.ml (100%) rename src/ml/{bare => }/FStarC_Reflection_Types.ml (100%) rename src/ml/{bare => }/FStarC_Sedlexing.ml (100%) rename src/ml/{bare => }/FStarC_String.ml (100%) rename src/ml/{bare => }/FStarC_StringBuffer.ml (100%) rename src/ml/{bare => }/FStarC_Syntax_TermHashTable.ml (100%) rename src/ml/{bare => }/FStarC_Tactics_Native.ml (100%) rename src/ml/{bare => }/FStarC_Unionfind.ml (100%) rename src/ml/{bare => }/FStarC_Util.ml (100%) delete mode 120000 stage1/dune/fstar-guts/bare create mode 120000 stage1/dune/fstar-guts/ml delete mode 120000 stage1/dune/fstar-plugins/full delete mode 120000 stage1/dune/libplugin/full delete mode 120000 stage2/dune/fstar-guts/bare create mode 120000 stage2/dune/fstar-guts/ml delete mode 120000 stage2/dune/fstar-plugins/full delete mode 120000 stage2/dune/libplugin/full rename {src/ml/full => ulib/ml/plugin}/FStarC_Tactics_Unseal.ml (100%) rename {src/ml/full => ulib/ml/plugin}/FStarC_Tactics_V1_Builtins.ml (100%) rename {src/ml/full => ulib/ml/plugin}/FStarC_Tactics_V2_Builtins.ml (100%) diff --git a/src/ml/bare/FStarC_BaseTypes.ml b/src/ml/FStarC_BaseTypes.ml similarity index 100% rename from src/ml/bare/FStarC_BaseTypes.ml rename to src/ml/FStarC_BaseTypes.ml diff --git a/src/ml/bare/FStarC_BigInt.ml b/src/ml/FStarC_BigInt.ml similarity index 100% rename from src/ml/bare/FStarC_BigInt.ml rename to src/ml/FStarC_BigInt.ml diff --git a/src/ml/bare/FStarC_Bytes.ml b/src/ml/FStarC_Bytes.ml similarity index 100% rename from src/ml/bare/FStarC_Bytes.ml rename to src/ml/FStarC_Bytes.ml diff --git a/src/ml/bare/FStarC_Dyn.ml b/src/ml/FStarC_Dyn.ml similarity index 100% rename from src/ml/bare/FStarC_Dyn.ml rename to src/ml/FStarC_Dyn.ml diff --git a/src/ml/bare/FStarC_Effect.ml b/src/ml/FStarC_Effect.ml similarity index 100% rename from src/ml/bare/FStarC_Effect.ml rename to src/ml/FStarC_Effect.ml diff --git a/src/ml/bare/FStarC_Extraction_ML_PrintML.ml b/src/ml/FStarC_Extraction_ML_PrintML.ml similarity index 100% rename from src/ml/bare/FStarC_Extraction_ML_PrintML.ml rename to src/ml/FStarC_Extraction_ML_PrintML.ml diff --git a/src/ml/bare/FStarC_Getopt.ml b/src/ml/FStarC_Getopt.ml similarity index 100% rename from src/ml/bare/FStarC_Getopt.ml rename to src/ml/FStarC_Getopt.ml diff --git a/src/ml/bare/FStarC_Hash.ml b/src/ml/FStarC_Hash.ml similarity index 100% rename from src/ml/bare/FStarC_Hash.ml rename to src/ml/FStarC_Hash.ml diff --git a/src/ml/bare/FStarC_Hints.ml b/src/ml/FStarC_Hints.ml similarity index 100% rename from src/ml/bare/FStarC_Hints.ml rename to src/ml/FStarC_Hints.ml diff --git a/src/ml/bare/FStarC_Json.ml b/src/ml/FStarC_Json.ml similarity index 100% rename from src/ml/bare/FStarC_Json.ml rename to src/ml/FStarC_Json.ml diff --git a/src/ml/bare/FStarC_List.ml b/src/ml/FStarC_List.ml similarity index 100% rename from src/ml/bare/FStarC_List.ml rename to src/ml/FStarC_List.ml diff --git a/src/ml/bare/FStarC_Parser_LexFStar.ml b/src/ml/FStarC_Parser_LexFStar.ml similarity index 100% rename from src/ml/bare/FStarC_Parser_LexFStar.ml rename to src/ml/FStarC_Parser_LexFStar.ml diff --git a/src/ml/bare/FStarC_Parser_Parse.mly b/src/ml/FStarC_Parser_Parse.mly similarity index 100% rename from src/ml/bare/FStarC_Parser_Parse.mly rename to src/ml/FStarC_Parser_Parse.mly diff --git a/src/ml/bare/FStarC_Parser_ParseIt.ml b/src/ml/FStarC_Parser_ParseIt.ml similarity index 100% rename from src/ml/bare/FStarC_Parser_ParseIt.ml rename to src/ml/FStarC_Parser_ParseIt.ml diff --git a/src/ml/bare/FStarC_Parser_Utf8.ml b/src/ml/FStarC_Parser_Utf8.ml similarity index 100% rename from src/ml/bare/FStarC_Parser_Utf8.ml rename to src/ml/FStarC_Parser_Utf8.ml diff --git a/src/ml/bare/FStarC_Parser_Util.ml b/src/ml/FStarC_Parser_Util.ml similarity index 100% rename from src/ml/bare/FStarC_Parser_Util.ml rename to src/ml/FStarC_Parser_Util.ml diff --git a/src/ml/bare/FStarC_Platform.ml b/src/ml/FStarC_Platform.ml similarity index 100% rename from src/ml/bare/FStarC_Platform.ml rename to src/ml/FStarC_Platform.ml diff --git a/src/ml/bare/FStarC_Plugins_Base.ml b/src/ml/FStarC_Plugins_Base.ml similarity index 100% rename from src/ml/bare/FStarC_Plugins_Base.ml rename to src/ml/FStarC_Plugins_Base.ml diff --git a/src/ml/bare/FStarC_Pprint.ml b/src/ml/FStarC_Pprint.ml similarity index 100% rename from src/ml/bare/FStarC_Pprint.ml rename to src/ml/FStarC_Pprint.ml diff --git a/src/ml/bare/FStarC_Range.ml b/src/ml/FStarC_Range.ml similarity index 100% rename from src/ml/bare/FStarC_Range.ml rename to src/ml/FStarC_Range.ml diff --git a/src/ml/bare/FStarC_Reflection_Types.ml b/src/ml/FStarC_Reflection_Types.ml similarity index 100% rename from src/ml/bare/FStarC_Reflection_Types.ml rename to src/ml/FStarC_Reflection_Types.ml diff --git a/src/ml/bare/FStarC_Sedlexing.ml b/src/ml/FStarC_Sedlexing.ml similarity index 100% rename from src/ml/bare/FStarC_Sedlexing.ml rename to src/ml/FStarC_Sedlexing.ml diff --git a/src/ml/bare/FStarC_String.ml b/src/ml/FStarC_String.ml similarity index 100% rename from src/ml/bare/FStarC_String.ml rename to src/ml/FStarC_String.ml diff --git a/src/ml/bare/FStarC_StringBuffer.ml b/src/ml/FStarC_StringBuffer.ml similarity index 100% rename from src/ml/bare/FStarC_StringBuffer.ml rename to src/ml/FStarC_StringBuffer.ml diff --git a/src/ml/bare/FStarC_Syntax_TermHashTable.ml b/src/ml/FStarC_Syntax_TermHashTable.ml similarity index 100% rename from src/ml/bare/FStarC_Syntax_TermHashTable.ml rename to src/ml/FStarC_Syntax_TermHashTable.ml diff --git a/src/ml/bare/FStarC_Tactics_Native.ml b/src/ml/FStarC_Tactics_Native.ml similarity index 100% rename from src/ml/bare/FStarC_Tactics_Native.ml rename to src/ml/FStarC_Tactics_Native.ml diff --git a/src/ml/bare/FStarC_Unionfind.ml b/src/ml/FStarC_Unionfind.ml similarity index 100% rename from src/ml/bare/FStarC_Unionfind.ml rename to src/ml/FStarC_Unionfind.ml diff --git a/src/ml/bare/FStarC_Util.ml b/src/ml/FStarC_Util.ml similarity index 100% rename from src/ml/bare/FStarC_Util.ml rename to src/ml/FStarC_Util.ml diff --git a/stage1/dune/fstar-guts/FStarC_Parser_Parse.mly b/stage1/dune/fstar-guts/FStarC_Parser_Parse.mly index 53c2cb3f29e..4952a1b17c0 120000 --- a/stage1/dune/fstar-guts/FStarC_Parser_Parse.mly +++ b/stage1/dune/fstar-guts/FStarC_Parser_Parse.mly @@ -1 +1 @@ -../../../src/ml/bare/FStarC_Parser_Parse.mly \ No newline at end of file +../../../src/ml/FStarC_Parser_Parse.mly \ No newline at end of file diff --git a/stage1/dune/fstar-guts/bare b/stage1/dune/fstar-guts/bare deleted file mode 120000 index 1f9e8d416f1..00000000000 --- a/stage1/dune/fstar-guts/bare +++ /dev/null @@ -1 +0,0 @@ -../../../src/ml/bare/ \ No newline at end of file diff --git a/stage1/dune/fstar-guts/ml b/stage1/dune/fstar-guts/ml new file mode 120000 index 00000000000..56ee79ada53 --- /dev/null +++ b/stage1/dune/fstar-guts/ml @@ -0,0 +1 @@ +../../../src/ml/ \ No newline at end of file diff --git a/stage1/dune/fstar-plugins/full b/stage1/dune/fstar-plugins/full deleted file mode 120000 index fbfc3b1c40c..00000000000 --- a/stage1/dune/fstar-plugins/full +++ /dev/null @@ -1 +0,0 @@ -../../../src/ml/full/ \ No newline at end of file diff --git a/stage1/dune/libplugin/full b/stage1/dune/libplugin/full deleted file mode 120000 index fbfc3b1c40c..00000000000 --- a/stage1/dune/libplugin/full +++ /dev/null @@ -1 +0,0 @@ -../../../src/ml/full/ \ No newline at end of file diff --git a/stage2/dune/fstar-guts/FStarC_Parser_Parse.mly b/stage2/dune/fstar-guts/FStarC_Parser_Parse.mly index 53c2cb3f29e..4952a1b17c0 120000 --- a/stage2/dune/fstar-guts/FStarC_Parser_Parse.mly +++ b/stage2/dune/fstar-guts/FStarC_Parser_Parse.mly @@ -1 +1 @@ -../../../src/ml/bare/FStarC_Parser_Parse.mly \ No newline at end of file +../../../src/ml/FStarC_Parser_Parse.mly \ No newline at end of file diff --git a/stage2/dune/fstar-guts/bare b/stage2/dune/fstar-guts/bare deleted file mode 120000 index 1f9e8d416f1..00000000000 --- a/stage2/dune/fstar-guts/bare +++ /dev/null @@ -1 +0,0 @@ -../../../src/ml/bare/ \ No newline at end of file diff --git a/stage2/dune/fstar-guts/ml b/stage2/dune/fstar-guts/ml new file mode 120000 index 00000000000..56ee79ada53 --- /dev/null +++ b/stage2/dune/fstar-guts/ml @@ -0,0 +1 @@ +../../../src/ml/ \ No newline at end of file diff --git a/stage2/dune/fstar-plugins/full b/stage2/dune/fstar-plugins/full deleted file mode 120000 index fbfc3b1c40c..00000000000 --- a/stage2/dune/fstar-plugins/full +++ /dev/null @@ -1 +0,0 @@ -../../../src/ml/full/ \ No newline at end of file diff --git a/stage2/dune/libplugin/full b/stage2/dune/libplugin/full deleted file mode 120000 index fbfc3b1c40c..00000000000 --- a/stage2/dune/libplugin/full +++ /dev/null @@ -1 +0,0 @@ -../../../src/ml/full/ \ No newline at end of file diff --git a/src/ml/full/FStarC_Tactics_Unseal.ml b/ulib/ml/plugin/FStarC_Tactics_Unseal.ml similarity index 100% rename from src/ml/full/FStarC_Tactics_Unseal.ml rename to ulib/ml/plugin/FStarC_Tactics_Unseal.ml diff --git a/src/ml/full/FStarC_Tactics_V1_Builtins.ml b/ulib/ml/plugin/FStarC_Tactics_V1_Builtins.ml similarity index 100% rename from src/ml/full/FStarC_Tactics_V1_Builtins.ml rename to ulib/ml/plugin/FStarC_Tactics_V1_Builtins.ml diff --git a/src/ml/full/FStarC_Tactics_V2_Builtins.ml b/ulib/ml/plugin/FStarC_Tactics_V2_Builtins.ml similarity index 100% rename from src/ml/full/FStarC_Tactics_V2_Builtins.ml rename to ulib/ml/plugin/FStarC_Tactics_V2_Builtins.ml From d62b0aa5e532dbef25a2d7320bbd58dc283afee3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 30 Jan 2025 15:00:56 -0800 Subject: [PATCH 6/8] lib.mk: include most FStar.Class modules Only skip FStar.Class.Embeddable which depends on terms, and can only go into the plugin lib. --- mk/lib.mk | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mk/lib.mk b/mk/lib.mk index 3e602dc8360..4d1b2884067 100644 --- a/mk/lib.mk +++ b/mk/lib.mk @@ -43,7 +43,7 @@ EXTRACT_NS += -FStar.TaggedUnion EXTRACT_NS += -FStar.Bytes EXTRACT_NS += -FStar.Util EXTRACT_NS += -FStar.InteractiveHelpers -EXTRACT_NS += -FStar.Class +EXTRACT_NS += -FStar.Class.Embeddable EXTRACT_NS += -FStar.Vector.Base EXTRACT_NS += -FStar.Vector.Properties EXTRACT_NS += -FStar.Vector From 0d417ec3a605a9ee415c4f20fd3463e7727ca847 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 30 Jan 2025 14:12:12 -0800 Subject: [PATCH 7/8] Options.Ext: refactor, and allow turning off boolean extensions by setting to 0/off/false instead of just empty --- src/basic/FStarC.Options.Ext.fst | 13 +++++++++++-- src/basic/FStarC.Options.Ext.fsti | 5 +++++ src/basic/FStarC.Plugins.fst | 2 +- src/basic/FStarC.Range.Type.fst | 2 +- src/extraction/FStarC.Extraction.ML.UEnv.fst | 2 +- src/smtencoding/FStarC.SMTEncoding.Encode.fst | 10 +++++----- src/smtencoding/FStarC.SMTEncoding.Pruning.fst | 4 ++-- src/smtencoding/FStarC.SMTEncoding.Solver.fst | 4 ++-- src/smtencoding/FStarC.SMTEncoding.SolverState.fst | 8 ++++---- src/syntax/FStarC.Syntax.Resugar.fst | 2 +- src/tactics/FStarC.Tactics.CtrlRewrite.fst | 2 +- src/tactics/FStarC.Tactics.V2.Basic.fst | 4 ++++ src/tactics/FStarC.Tactics.V2.Basic.fsti | 1 + src/tactics/FStarC.Tactics.V2.Primops.fst | 1 + src/typechecker/FStarC.TypeChecker.Cfg.fst | 2 +- src/typechecker/FStarC.TypeChecker.Rel.fst | 4 ++-- ulib/FStar.Stubs.Tactics.V2.Builtins.fsti | 4 ++++ ulib/ml/plugin/FStarC_Tactics_V2_Builtins.ml | 1 + 18 files changed, 48 insertions(+), 23 deletions(-) diff --git a/src/basic/FStarC.Options.Ext.fst b/src/basic/FStarC.Options.Ext.fst index 4c8ddc59582..d9c64464567 100644 --- a/src/basic/FStarC.Options.Ext.fst +++ b/src/basic/FStarC.Options.Ext.fst @@ -23,7 +23,11 @@ module BU = FStarC.Util type ext_state = | E : map : BU.psmap string -> ext_state -let cur_state = BU.mk_ref (E (BU.psmap_empty ())) +(* If we ever want to set any defaults, this is the place to do it. *) +let init : ext_state = + E (BU.psmap_empty ()) + +let cur_state = BU.mk_ref init (* Set a key-value pair in the map *) let set (k:key) (v:value) : unit = @@ -38,6 +42,11 @@ let get (k:key) : value = in r +let enabled (k:key) : bool = + let v = get k in + let v = String.lowercase v in + v <> "" && not (v = "off" || v = "false" || v = "0") + (* Find a home *) let is_prefix (s1 s2 : string) : ML bool = let open FStarC.String in @@ -67,4 +76,4 @@ let restore (s:ext_state) : unit = () let reset () : unit = - cur_state := E (BU.psmap_empty ()) + cur_state := init diff --git a/src/basic/FStarC.Options.Ext.fsti b/src/basic/FStarC.Options.Ext.fsti index 26aa1ab012c..a0cbae57e1a 100644 --- a/src/basic/FStarC.Options.Ext.fsti +++ b/src/basic/FStarC.Options.Ext.fsti @@ -29,6 +29,11 @@ val set (k:key) (v:value) : unit (* Get the value from the map, or return "" if not there *) val get (k:key) : value +(* For boolean-like options, return true if enabled. We consider an +extension enabled when set to a non-empty string what is NOT "off", +"false", or "0" (and this comparison is case-insensitive). *) +val enabled (k:key) : bool + (* Get a list of all KV pairs that "begin" with k, considered as a namespace. *) val getns (ns:string) : list (key & value) diff --git a/src/basic/FStarC.Plugins.fst b/src/basic/FStarC.Plugins.fst index e5ebae7151b..d21c88f5bc8 100644 --- a/src/basic/FStarC.Plugins.fst +++ b/src/basic/FStarC.Plugins.fst @@ -126,7 +126,7 @@ let compile_modules dir ms = if it could find a plugin with the proper name. This will fail hard if loading the plugin fails. *) let autoload_plugin (ext:string) : bool = - if Options.Ext.get "noautoload" <> "" then false else ( + if Options.Ext.enabled "noautoload" then false else ( if Debug.any () then BU.print1 "Trying to find a plugin for extension %s\n" ext; match Find.find_file (ext ^ ".cmxs") with diff --git a/src/basic/FStarC.Range.Type.fst b/src/basic/FStarC.Range.Type.fst index 4b13ade7863..21883db463b 100644 --- a/src/basic/FStarC.Range.Type.fst +++ b/src/basic/FStarC.Range.Type.fst @@ -93,7 +93,7 @@ let mk_rng file_name start_pos end_pos = { let mk_range f b e = let r = mk_rng f b e in range_of_rng r r let string_of_file_name f = - if Options.Ext.get "fstar:no_absolute_paths" = "1" then + if Options.Ext.enabled "fstar:no_absolute_paths" then BU.basename f else if Options.ide () then try diff --git a/src/extraction/FStarC.Extraction.ML.UEnv.fst b/src/extraction/FStarC.Extraction.ML.UEnv.fst index 64e10d4ee89..44651801cc1 100644 --- a/src/extraction/FStarC.Extraction.ML.UEnv.fst +++ b/src/extraction/FStarC.Extraction.ML.UEnv.fst @@ -254,7 +254,7 @@ let is_fv_type g fv = let no_fstar_stubs_ns (ns : list mlsymbol) : list mlsymbol = match ns with - | "FStar"::"Stubs"::rest when plug_no_lib () && Options.Ext.get "__guts" <> "" -> "FStarC"::rest + | "FStar"::"Stubs"::rest when plug_no_lib () && Options.Ext.enabled "__guts" -> "FStarC"::rest (* These 3 modules are special, and are not in the guts. They live in src/ml/full and are visible at the ambient namespace when building the plugin lib. *) diff --git a/src/smtencoding/FStarC.SMTEncoding.Encode.fst b/src/smtencoding/FStarC.SMTEncoding.Encode.fst index 6a414bc8185..d3df2f34161 100644 --- a/src/smtencoding/FStarC.SMTEncoding.Encode.fst +++ b/src/smtencoding/FStarC.SMTEncoding.Encode.fst @@ -824,7 +824,7 @@ let encode_top_level_let : let app_is_prop = Term.mk_subtype_of_unit app in if should_encode_logical then ( - if is_sub_singleton && Options.Ext.get "retain_old_prop_typing" = "" + if is_sub_singleton && not (Options.Ext.enabled "retain_old_prop_typing") then ( Util.mkAssume(mkForall (S.range_of_lbname lbn) ([[app_is_prop]], vars, mkImp(mk_and_l binder_guards, mk_Valid <| app_is_prop)), @@ -1064,7 +1064,7 @@ let encode_sig_inductive (env:env_t) (se:sigelt) let is_l = mk_data_tester env l xx in let inversion_case, decls' = if injective_type_params - || Options.Ext.get "compat:injectivity" <> "" + || Options.Ext.enabled "compat:injectivity" then ( let _, data_t = Env.lookup_datacon env.tcenv l in let args, res = U.arrow_formals data_t in @@ -1183,7 +1183,7 @@ let encode_datacon (env:env_t) (se:sigelt) let s_fuel_tm = mkApp("SFuel", [fuel_tm]) in let vars, guards, env', binder_decls, names = encode_binders (Some fuel_tm) formals env in let injective_type_params = - injective_type_params || Options.Ext.get "compat:injectivity" <> "" + injective_type_params || Options.Ext.enabled "compat:injectivity" in let fields = names |> @@ -1345,11 +1345,11 @@ let encode_datacon (env:env_t) (se:sigelt) | Tm_fvar fv -> if BU.for_some (S.fv_eq_lid fv) mutuals then Some (bs, c) - else if Options.Ext.get "compat:2954" <> "" + else if Options.Ext.enabled "compat:2954" then (warn_compat(); Some (bs, c)) //compatibility mode else None | _ -> - if Options.Ext.get "compat:2954" <> "" + if Options.Ext.enabled "compat:2954" then (warn_compat(); Some (bs, c)) //compatibility mode else None ) diff --git a/src/smtencoding/FStarC.SMTEncoding.Pruning.fst b/src/smtencoding/FStarC.SMTEncoding.Pruning.fst index 48c87fc48bf..4451cdccf29 100644 --- a/src/smtencoding/FStarC.SMTEncoding.Pruning.fst +++ b/src/smtencoding/FStarC.SMTEncoding.Pruning.fst @@ -47,7 +47,7 @@ type pruning_state = { } let debug (f: unit -> unit) : unit = - if Options.Ext.get "debug_context_pruning" <> "" + if Options.Ext.enabled "debug_context_pruning" then f() let print_pruning_state (p:pruning_state) @@ -461,7 +461,7 @@ let prune (p:pruning_state) (roots:list decl) | Some a -> [a]) (reached_names@p.ambients) in - // if Options.Ext.get "debug_context_pruning" <> "" + // if Options.Ext.enabled "debug_context_pruning" // then ( // BU.print1 "Retained %s assumptions\n" (show (List.length reached_assumptions)) // ); diff --git a/src/smtencoding/FStarC.SMTEncoding.Solver.fst b/src/smtencoding/FStarC.SMTEncoding.Solver.fst index c6cd200a8b0..3673d0892e7 100644 --- a/src/smtencoding/FStarC.SMTEncoding.Solver.fst +++ b/src/smtencoding/FStarC.SMTEncoding.Solver.fst @@ -605,7 +605,7 @@ let query_info settings z3result = let msg = if used_hint settings then Pprint.doc_of_string "Hint-replay failed" :: msg else msg in FStarC.Errors.log_issue range FStarC.Errors.Warning_HitReplayFailed msg) end - else if Options.Ext.get "profile_context" <> "" + else if Options.Ext.enabled "profile_context" then match z3result.z3result_status with | UNSAT core -> process_unsat_core core | _ -> () @@ -1221,7 +1221,7 @@ let get_cfg env : solver_cfg = ; valid_intro = Options.smtencoding_valid_intro () ; valid_elim = Options.smtencoding_valid_elim () ; z3version = Options.z3_version () - ; context_pruning = Options.Ext.get "context_pruning" <> "" + ; context_pruning = Options.Ext.enabled "context_pruning" } let save_cfg env = diff --git a/src/smtencoding/FStarC.SMTEncoding.SolverState.fst b/src/smtencoding/FStarC.SMTEncoding.SolverState.fst index 31b38d51e10..eebd5dd11da 100644 --- a/src/smtencoding/FStarC.SMTEncoding.SolverState.fst +++ b/src/smtencoding/FStarC.SMTEncoding.SolverState.fst @@ -80,7 +80,7 @@ let solver_state_to_string (s:solver_state) = instance showable_solver_state : showable solver_state = { show = solver_state_to_string } let debug (msg:string) (s0 s1:solver_state) = - if Options.Ext.get "debug_solver_state" <> "" + if Options.Ext.enabled "debug_solver_state" then ( BU.print3 "Debug (%s):{\n\t before=%s\n\t after=%s\n}" msg (solver_state_to_string s0) @@ -317,7 +317,7 @@ let give_now (resetting:bool) (ds:list decl) (s:solver_state) let give_aux resetting (ds:list decl) (s:solver_state) : solver_state -= if Options.Ext.get "context_pruning" <> "" += if Options.Ext.enabled "context_pruning" then give_delay_assumptions resetting ds s else give_now resetting ds s @@ -460,7 +460,7 @@ let filter_with_unsat_core queryid (core:U.unsat_core) (s:solver_state) U.filter core all_decls let would_have_pruned (s:solver_state) = - if Options.Ext.get "context_pruning_sim" = "" + if not (Options.Ext.enabled "context_pruning_sim") then None else (*find the first level with pruning roots, and prune the context with respect to them *) @@ -479,7 +479,7 @@ let would_have_pruned (s:solver_state) = let flush (s:solver_state) : list decl & solver_state = let s = - if Options.Ext.get "context_pruning" <> "" + if Options.Ext.enabled "context_pruning" then ( (*find the first level with pruning roots, and prune the context with respect to them *) let rec aux levels = diff --git a/src/syntax/FStarC.Syntax.Resugar.fst b/src/syntax/FStarC.Syntax.Resugar.fst index de239bfc176..a97ec986883 100644 --- a/src/syntax/FStarC.Syntax.Resugar.fst +++ b/src/syntax/FStarC.Syntax.Resugar.fst @@ -530,7 +530,7 @@ let rec resugar_term' (env: DsEnv.env) (t : S.term) : A.term = mk (A.App (acc, aa, qq))) h else if not (Options.print_implicits ()) - && Options.Ext.get "show_hide_reveal" = "" + && not (Options.Ext.enabled "show_hide_reveal") && is_hide_or_reveal e && List.length args = 1 //args already filtered then ( diff --git a/src/tactics/FStarC.Tactics.CtrlRewrite.fst b/src/tactics/FStarC.Tactics.CtrlRewrite.fst index 2929f24f764..7b895b67215 100644 --- a/src/tactics/FStarC.Tactics.CtrlRewrite.fst +++ b/src/tactics/FStarC.Tactics.CtrlRewrite.fst @@ -109,7 +109,7 @@ let __do_rewrite (* unrefine typ as is done for the type arg of eq2 *) let typ = - if Options.Ext.get "__unrefine" <> "" then + if Options.Ext.enabled "__unrefine" then let typ_norm = N.unfold_whnf' [Env.DontUnfoldAttr [Parser.Const.do_not_unrefine_attr]] env typ in if Tm_refine? (SS.compress typ_norm).n then (* It is indeed a refinement, normalize again to remove them. *) diff --git a/src/tactics/FStarC.Tactics.V2.Basic.fst b/src/tactics/FStarC.Tactics.V2.Basic.fst index 01909d49aff..b3a1f2fe3f8 100644 --- a/src/tactics/FStarC.Tactics.V2.Basic.fst +++ b/src/tactics/FStarC.Tactics.V2.Basic.fst @@ -2223,6 +2223,10 @@ let ext_getv (k:string) : tac string = return () ;! return (Options.Ext.get k) +let ext_enabled (k:string) : tac bool + = return () ;! + return (Options.Ext.enabled k) + let ext_getns (ns:string) : tac (list (string & string)) = return () ;! return (Options.Ext.getns ns) diff --git a/src/tactics/FStarC.Tactics.V2.Basic.fsti b/src/tactics/FStarC.Tactics.V2.Basic.fsti index fa02b229630..474d268d08a 100644 --- a/src/tactics/FStarC.Tactics.V2.Basic.fsti +++ b/src/tactics/FStarC.Tactics.V2.Basic.fsti @@ -122,6 +122,7 @@ val free_uvars : term -> tac (list Z.t) val all_ext_options : unit -> tac (list (string & string)) val ext_getv : string -> tac string +val ext_enabled : string -> tac bool val ext_getns : string -> tac (list (string & string)) val alloc : 'a -> tac (tref 'a) diff --git a/src/tactics/FStarC.Tactics.V2.Primops.fst b/src/tactics/FStarC.Tactics.V2.Primops.fst index 49d2f64e234..e37b1406e91 100644 --- a/src/tactics/FStarC.Tactics.V2.Primops.fst +++ b/src/tactics/FStarC.Tactics.V2.Primops.fst @@ -224,6 +224,7 @@ let ops = [ mk_tac_step_1 0 "free_uvars" free_uvars free_uvars; mk_tac_step_1 0 "all_ext_options" all_ext_options all_ext_options; mk_tac_step_1 0 "ext_getv" ext_getv ext_getv; + mk_tac_step_1 0 "ext_enabled" ext_enabled ext_enabled; mk_tac_step_1 0 "ext_getns" ext_getns ext_getns; mk_tac_step_2 1 "alloc" diff --git a/src/typechecker/FStarC.TypeChecker.Cfg.fst b/src/typechecker/FStarC.TypeChecker.Cfg.fst index f2b7593dfa3..08c9df18cf4 100644 --- a/src/typechecker/FStarC.TypeChecker.Cfg.fst +++ b/src/typechecker/FStarC.TypeChecker.Cfg.fst @@ -430,7 +430,7 @@ let config' psteps s e = memoize_lazy = true; normalize_pure_lets = (not steps.pure_subterms_within_computations) || Options.normalize_pure_terms_for_extraction(); reifying = false; - compat_memo_ignore_cfg = Options.Ext.get "compat:normalizer_memo_ignore_cfg" <> ""; + compat_memo_ignore_cfg = Options.Ext.enabled "compat:normalizer_memo_ignore_cfg"; } let config s e = config' [] s e diff --git a/src/typechecker/FStarC.TypeChecker.Rel.fst b/src/typechecker/FStarC.TypeChecker.Rel.fst index b51bb586032..0b14f2373fa 100644 --- a/src/typechecker/FStarC.TypeChecker.Rel.fst +++ b/src/typechecker/FStarC.TypeChecker.Rel.fst @@ -2210,7 +2210,7 @@ let rec solve (probs :worklist) : solution = | _ -> false in let maybe_expand (tp:tprob) : tprob = - if Options.Ext.get "__unrefine" <> "" && tp.relation = SUB && is_expand_uvar tp.rhs + if Options.Ext.enabled "__unrefine" && tp.relation = SUB && is_expand_uvar tp.rhs then let lhs = tp.lhs in let lhs_norm = N.unfold_whnf' [Env.DontUnfoldAttr [PC.do_not_unrefine_attr]] (p_env probs hd) lhs in @@ -5642,7 +5642,7 @@ let resolve_implicits' env is_tac is_gen (implicits:Env.implicits) BU.print1 "Deferring implicit due to open ctx/typ %s\n" (show ctx_u); until_fixpoint ((hd, Implicit_unresolved)::out, changed, defer_open_metas) tl ) else if is_open && not (meta_tac_allowed_for_open_problem tac) - && Options.Ext.get "compat:open_metas" = "" then ( // i.e. compat option unset + && not (Options.Ext.enabled "compat:open_metas") then ( // i.e. compat option unset (* If the tactic is not explicitly whitelisted to run with open problems, then defer. *) until_fixpoint ((hd, Implicit_unresolved)::out, changed, defer_open_metas) tl diff --git a/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti b/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti index 9e145dc2e67..c883d904e5c 100644 --- a/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti +++ b/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti @@ -478,6 +478,10 @@ val all_ext_options : unit -> Tac (list (string & string)) is returned if the key was unset. *) val ext_getv (k:string) : Tac string +(* Returns true iff the extension flag is enabled. I.e. it's a non-empty +string that is not 0/off/false. *) +val ext_enabled (k:string) : Tac bool + (* Return all k/v pairs in the state which are within the given namespace. *) val ext_getns (ns:string) : Tac (list (string & string)) diff --git a/ulib/ml/plugin/FStarC_Tactics_V2_Builtins.ml b/ulib/ml/plugin/FStarC_Tactics_V2_Builtins.ml index 7d1bf2ef51f..f47e475f23a 100644 --- a/ulib/ml/plugin/FStarC_Tactics_V2_Builtins.ml +++ b/ulib/ml/plugin/FStarC_Tactics_V2_Builtins.ml @@ -136,6 +136,7 @@ let t_smt_sync = from_tac_1 "B.t_smt_sync" B.t_smt_sync let free_uvars = from_tac_1 "B.free_uvars" B.free_uvars let all_ext_options = from_tac_1 "B.all_ext_options" B.all_ext_options let ext_getv = from_tac_1 "B.ext_getv" B.ext_getv +let ext_enabled = from_tac_1 "B.ext_enabled" B.ext_enabled let ext_getns = from_tac_1 "B.ext_getns" B.ext_getns let alloc x = from_tac_1 "B.alloc" B.alloc x From e7396acf8b51e3f0d3abc4b995783072b81d18b0 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Fri, 31 Jan 2025 00:13:52 +0000 Subject: [PATCH 8/8] remove unnecessary straggling admit (thanks to Brian Milnes for pointing out!) --- ulib/FStar.FunctionalQueue.fst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ulib/FStar.FunctionalQueue.fst b/ulib/FStar.FunctionalQueue.fst index f4af0d78298..5caf7291c5b 100644 --- a/ulib/FStar.FunctionalQueue.fst +++ b/ulib/FStar.FunctionalQueue.fst @@ -144,7 +144,7 @@ let lemma_snoc_list_seq (#a:Type) (x:a) (q:queue a) seq_of_list l `Seq.append` seq_of_list [x]; == { assert (Seq.equal (seq_of_list [x]) (Seq.create 1 x)) } seq_of_list l `Seq.append` Seq.create 1 x; - == { admit() } + == { } Seq.snoc (seq_of_list l) x; }