merging in master; setting Ext options context_pruning default to true

FStarLang · Feb 1, 2025 · c146a66 · c146a66
2 parents e8af8b2 + 8a81ab2
commit c146a66
Showing 62 changed files with 63 additions and 37 deletions.
diff --git 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

diff --git 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

diff --git 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_add (psmap_empty ()) "context_pruning" "true"))
+
+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
@@ -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
@@ -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
@@ -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
@@ -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/ml/bare/FStarC_BaseTypes.ml → src/ml/FStarC_BaseTypes.ml b/src/ml/bare/FStarC_BaseTypes.ml → src/ml/FStarC_BaseTypes.ml
diff --git a/src/ml/bare/FStarC_BigInt.ml → src/ml/FStarC_BigInt.ml b/src/ml/bare/FStarC_BigInt.ml → src/ml/FStarC_BigInt.ml
diff --git a/src/ml/bare/FStarC_Bytes.ml → src/ml/FStarC_Bytes.ml b/src/ml/bare/FStarC_Bytes.ml → src/ml/FStarC_Bytes.ml
diff --git a/src/ml/bare/FStarC_Dyn.ml → src/ml/FStarC_Dyn.ml b/src/ml/bare/FStarC_Dyn.ml → src/ml/FStarC_Dyn.ml
diff --git a/src/ml/bare/FStarC_Effect.ml → src/ml/FStarC_Effect.ml b/src/ml/bare/FStarC_Effect.ml → src/ml/FStarC_Effect.ml
diff --git a/src/ml/bare/FStarC_Extraction_ML_PrintML.ml → src/ml/FStarC_Extraction_ML_PrintML.ml b/src/ml/bare/FStarC_Extraction_ML_PrintML.ml → src/ml/FStarC_Extraction_ML_PrintML.ml
diff --git a/src/ml/bare/FStarC_Getopt.ml → src/ml/FStarC_Getopt.ml b/src/ml/bare/FStarC_Getopt.ml → src/ml/FStarC_Getopt.ml
diff --git a/src/ml/bare/FStarC_Hash.ml → src/ml/FStarC_Hash.ml b/src/ml/bare/FStarC_Hash.ml → src/ml/FStarC_Hash.ml
diff --git a/src/ml/bare/FStarC_Hints.ml → src/ml/FStarC_Hints.ml b/src/ml/bare/FStarC_Hints.ml → src/ml/FStarC_Hints.ml
diff --git a/src/ml/bare/FStarC_Json.ml → src/ml/FStarC_Json.ml b/src/ml/bare/FStarC_Json.ml → src/ml/FStarC_Json.ml
diff --git a/src/ml/bare/FStarC_List.ml → src/ml/FStarC_List.ml b/src/ml/bare/FStarC_List.ml → src/ml/FStarC_List.ml
diff --git a/src/ml/bare/FStarC_Parser_LexFStar.ml → src/ml/FStarC_Parser_LexFStar.ml b/src/ml/bare/FStarC_Parser_LexFStar.ml → src/ml/FStarC_Parser_LexFStar.ml
diff --git a/src/ml/bare/FStarC_Parser_Parse.mly → src/ml/FStarC_Parser_Parse.mly b/src/ml/bare/FStarC_Parser_Parse.mly → src/ml/FStarC_Parser_Parse.mly
diff --git a/src/ml/bare/FStarC_Parser_ParseIt.ml → src/ml/FStarC_Parser_ParseIt.ml b/src/ml/bare/FStarC_Parser_ParseIt.ml → src/ml/FStarC_Parser_ParseIt.ml
diff --git a/src/ml/bare/FStarC_Parser_Utf8.ml → src/ml/FStarC_Parser_Utf8.ml b/src/ml/bare/FStarC_Parser_Utf8.ml → src/ml/FStarC_Parser_Utf8.ml
diff --git a/src/ml/bare/FStarC_Parser_Util.ml → src/ml/FStarC_Parser_Util.ml b/src/ml/bare/FStarC_Parser_Util.ml → src/ml/FStarC_Parser_Util.ml
diff --git a/src/ml/bare/FStarC_Platform.ml → src/ml/FStarC_Platform.ml b/src/ml/bare/FStarC_Platform.ml → src/ml/FStarC_Platform.ml
diff --git a/src/ml/bare/FStarC_Plugins_Base.ml → src/ml/FStarC_Plugins_Base.ml b/src/ml/bare/FStarC_Plugins_Base.ml → src/ml/FStarC_Plugins_Base.ml
diff --git a/src/ml/bare/FStarC_Pprint.ml → src/ml/FStarC_Pprint.ml b/src/ml/bare/FStarC_Pprint.ml → src/ml/FStarC_Pprint.ml
diff --git a/src/ml/bare/FStarC_Range.ml → src/ml/FStarC_Range.ml b/src/ml/bare/FStarC_Range.ml → src/ml/FStarC_Range.ml
diff --git a/src/ml/bare/FStarC_Reflection_Types.ml → src/ml/FStarC_Reflection_Types.ml b/src/ml/bare/FStarC_Reflection_Types.ml → src/ml/FStarC_Reflection_Types.ml
diff --git a/src/ml/bare/FStarC_Sedlexing.ml → src/ml/FStarC_Sedlexing.ml b/src/ml/bare/FStarC_Sedlexing.ml → src/ml/FStarC_Sedlexing.ml
diff --git a/src/ml/bare/FStarC_String.ml → src/ml/FStarC_String.ml b/src/ml/bare/FStarC_String.ml → src/ml/FStarC_String.ml
diff --git a/src/ml/bare/FStarC_StringBuffer.ml → src/ml/FStarC_StringBuffer.ml b/src/ml/bare/FStarC_StringBuffer.ml → src/ml/FStarC_StringBuffer.ml
diff --git a/src/ml/bare/FStarC_Syntax_TermHashTable.ml → src/ml/FStarC_Syntax_TermHashTable.ml b/src/ml/bare/FStarC_Syntax_TermHashTable.ml → src/ml/FStarC_Syntax_TermHashTable.ml
diff --git a/src/ml/bare/FStarC_Tactics_Native.ml → src/ml/FStarC_Tactics_Native.ml b/src/ml/bare/FStarC_Tactics_Native.ml → src/ml/FStarC_Tactics_Native.ml
diff --git a/src/ml/bare/FStarC_Unionfind.ml → src/ml/FStarC_Unionfind.ml b/src/ml/bare/FStarC_Unionfind.ml → src/ml/FStarC_Unionfind.ml
diff --git a/src/ml/bare/FStarC_Util.ml → src/ml/FStarC_Util.ml b/src/ml/bare/FStarC_Util.ml → src/ml/FStarC_Util.ml
diff --git 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
@@ -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
@@ -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" <> "false"
+    ; 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
@@ -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)
@@ -322,7 +322,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" <> "false"
+= if Options.Ext.enabled "context_pruning"
   then give_delay_assumptions resetting ds s
   else give_now resetting ds s
 
@@ -465,7 +465,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 *)
@@ -484,7 +484,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" <> "false"
+    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/smtencoding/FStarC.SMTEncoding.Z3.fst b/src/smtencoding/FStarC.SMTEncoding.Z3.fst
@@ -176,7 +176,12 @@ let check_z3version (p:proc) : unit =
     );
     _already_warned_solver_mismatch := true
   );
-  let ver_found : string = BU.trim_string (getinfo "version") in
+  (* 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 (
     let open FStarC.Errors in

diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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/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
+../../../src/ml/FStarC_Parser_Parse.mly
diff --git a/stage1/dune/fstar-guts/bare b/stage1/dune/fstar-guts/bare
diff --git a/stage1/dune/fstar-guts/ml b/stage1/dune/fstar-guts/ml
@@ -0,0 +1 @@
+../../../src/ml/
diff --git a/stage1/dune/fstar-plugins/full b/stage1/dune/fstar-plugins/full
diff --git a/stage1/dune/libplugin/full b/stage1/dune/libplugin/full
diff --git 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
+../../../src/ml/FStarC_Parser_Parse.mly
diff --git a/stage2/dune/fstar-guts/bare b/stage2/dune/fstar-guts/bare
diff --git a/stage2/dune/fstar-guts/ml b/stage2/dune/fstar-guts/ml
@@ -0,0 +1 @@
+../../../src/ml/
diff --git a/stage2/dune/fstar-plugins/full b/stage2/dune/fstar-plugins/full
diff --git a/stage2/dune/libplugin/full b/stage2/dune/libplugin/full
diff --git 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;
   }
 

diff --git 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/src/ml/full/FStarC_Tactics_Unseal.ml → ulib/ml/plugin/FStarC_Tactics_Unseal.ml b/src/ml/full/FStarC_Tactics_Unseal.ml → ulib/ml/plugin/FStarC_Tactics_Unseal.ml
diff --git a/src/ml/full/FStarC_Tactics_V1_Builtins.ml → ulib/ml/plugin/FStarC_Tactics_V1_Builtins.ml b/src/ml/full/FStarC_Tactics_V1_Builtins.ml → ulib/ml/plugin/FStarC_Tactics_V1_Builtins.ml
diff --git a/src/ml/full/FStarC_Tactics_V2_Builtins.ml → ulib/ml/plugin/FStarC_Tactics_V2_Builtins.ml b/src/ml/full/FStarC_Tactics_V2_Builtins.ml → 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
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		../../../src/ml/bare/FStarC_Parser_Parse.mly
		../../../src/ml/FStarC_Parser_Parse.mly