Updating debug flags in tests/examples

FStarLang · Apr 29, 2024 · 54cf68b · 54cf68b
1 parent 77a0682
commit 54cf68b
Show file tree

Hide file tree

Showing 30 changed files with 37 additions and 41 deletions.
diff --git a/.completion/fish/fstar.exe.fish b/.completion/fish/fstar.exe.fish
@@ -12,8 +12,7 @@ complete -c fstar.exe -l print_cache_version --description "Print the version fo
 complete -c fstar.exe -l cmi --description "Inline across module interfaces during extraction (aka. cross-module inlining)"
 complete -c fstar.exe -l codegen -r --description "Generate code for further compilation to executable code, or build a compiler plugin"
 complete -c fstar.exe -l codegen-lib --description "namespace  External runtime library (i.e. M.N.x extracts to M.N.X instead of M_N.x)"
-complete -c fstar.exe -l debug --description "module_name  Print lots of debugging information while checking module"
-complete -c fstar.exe -l debug_level -r --description "Control the verbosity of debugging info"
+complete -c fstar.exe -l debug -r --description "Control the verbosity of debugging info"
 complete -c fstar.exe -l defensive -r --description "Enable several internal sanity checks, useful to track bugs and report issues."
 complete -c fstar.exe -l dep -r --description "Output the transitive closure of the full dependency graph in three formats:"
 complete -c fstar.exe -l detail_errors --description "Emit a detailed error report by asking the SMT solver many queries; will take longer"

diff --git a/examples/dm4free/README.md b/examples/dm4free/README.md
@@ -23,7 +23,7 @@ To see more debug output related to the DMFF elaboration and star
 transformations:
 
 ```
-fstar.exe --trace_error --debug_level ED --debug FStar.DM4F.IntST FStar.DM4F.IntST.fst --prn --print_implicits --print_universes --print_bound_var_types
+fstar.exe --trace_error --debug ED FStar.DM4F.IntST.fst --prn --print_implicits --print_universes --print_bound_var_types
 ```
 
 Current status:

diff --git a/examples/dm4free/old/StExn.Handle.fst b/examples/dm4free/old/StExn.Handle.fst
@@ -197,7 +197,6 @@ val handle: #a:Type0 -> #wp:wp a -> $f:(unit -> StateExn a wp)
 (*                           match x with  *)
 (*                           | None -> False *)
 (*                           | Some z -> (ens h0 None h1 /\ z=def) \/ ens h0 x h1) *)
-(* #set-options "--debug StExn.Handle --debug_level HACK!"			   *)
 (* let handle2 #a #req #ens f def = *)
 (*   StateExn.reflect (fun h0 -> *)
 (*      match reify (f ()) h0 with *)

diff --git a/examples/dm4free/old/intST.fst b/examples/dm4free/old/intST.fst
@@ -105,7 +105,7 @@ let put_unfolded (n: int): (n0: int -> PURE (unit * int) (fun post -> post ((),
 let put_cps_type = n:int -> Tot (repr unit (fun n0 post -> post ((), n)))
 let put_cps_type_unfolded = n:int -> Tot (n0: int -> PURE (unit * int) (fun post -> post ((), n)))
 
-(* #reset-options "--debug NatST --debug_level SMTEncoding" *)
+(* #reset-options "--debug SMTEncoding" *)
 
 reifiable reflectable new_effect {
   STATE : a:Type -> wp:wp a -> Effect

diff --git a/examples/native_tactics/Imp.Fun.Driver.fst b/examples/native_tactics/Imp.Fun.Driver.fst
@@ -47,6 +47,6 @@ let normal #a (e:a) =
 
 let norm_assert (p:Type) : Lemma (requires (normal p)) (ensures True) = ()
 
-#set-options "--debug Imp.Fun.Driver --debug_level print_normalized_terms --admit_smt_queries true"
+#set-options "--debug print_normalized_terms --admit_smt_queries true"
 // let _ = norm_assert (forall (x:int) rm. R.sel (eval' (Seq [Const x (reg 0)]) rm) 0 == x) // eval' (Seq [Const x (reg 0)]) rm == rm)
 let _ = norm_assert (forall x y. equiv_norm (long_zero x) (long_zero y))
diff --git a/examples/native_tactics/Imp.Fun.DriverNBE.fst b/examples/native_tactics/Imp.Fun.DriverNBE.fst
@@ -48,6 +48,6 @@ let normal #a (e:a) =
 
 let norm_assert (p:Type) : Lemma (requires (normal p)) (ensures True) = ()
 
-#set-options "--debug Imp.Fun.DriverNBE --debug_level print_normalized_terms --admit_smt_queries true"
+#set-options "--debug print_normalized_terms --admit_smt_queries true"
 // let _ = norm_assert (forall (x:int) rm. R.sel (eval' (Seq [Const x (reg 0)]) rm) 0 == x) // eval' (Seq [Const x (reg 0)]) rm == rm)
 let _ = norm_assert (forall x y. equiv_norm (long_zero x) (long_zero y))
diff --git a/examples/native_tactics/Imp.Fun.fst b/examples/native_tactics/Imp.Fun.fst
@@ -14,7 +14,7 @@
    limitations under the License.
 *)
 module Imp.Fun
-//#set-options "--debug Imp --debug_level SMTQuery"
+//#set-options "--debug SMTQuery"
 open FStar.Mul
 module R = Registers.Fun
 
@@ -167,7 +167,7 @@ let normal #a (e:a) =
 
 let norm_assert (p:Type) : Lemma (requires (normal p)) (ensures True) = ()
 
-#set-options "--debug Registers.Imp --debug_level print_normalized_terms --admit_smt_queries true"
+#set-options "--debug print_normalized_terms --admit_smt_queries true"
 // let _ = norm_assert (forall (x:int) rm. R.sel (eval' (Seq [Const x (reg 0)]) rm) 0 == x) // eval' (Seq [Const x (reg 0)]) rm == rm)
 let _ = norm_assert (forall x y. equiv_norm (long_zero x) (long_zero y))
 // let _ = norm_assert (forall x y. equiv_norm (long_zero x) (long_zero y))

diff --git a/examples/native_tactics/Imp.List.Driver.fst b/examples/native_tactics/Imp.List.Driver.fst
@@ -47,6 +47,6 @@ let normal #a (e:a) =
 
 let norm_assert (p:Type) : Lemma (requires (normal p)) (ensures True) = ()
 
-#set-options "--debug Imp.List.Driver --debug_level print_normalized_terms --admit_smt_queries true"
+#set-options "--debug print_normalized_terms --admit_smt_queries true"
 // let _ = norm_assert (forall (x:int) rm. R.sel (eval' (Seq [Const x (reg 0)]) rm) 0 == x) // eval' (Seq [Const x (reg 0)]) rm == rm)
 let _ = norm_assert (forall x y. equiv_norm (long_zero x) (long_zero y))
diff --git a/examples/native_tactics/Imp.List.DriverNBE.fst b/examples/native_tactics/Imp.List.DriverNBE.fst
@@ -48,5 +48,5 @@ let normal #a (e:a) =
 
 let norm_assert (p:Type) : Lemma (requires (normal p)) (ensures True) = ()
 
-#set-options "--debug Imp.List.DriverNBE --debug_level print_normalized_terms --admit_smt_queries true"
+#set-options "--debug print_normalized_terms --admit_smt_queries true"
 let _ = norm_assert (forall x y. equiv_norm (long_zero x) (long_zero y))
diff --git a/examples/native_tactics/Imp.List.fst b/examples/native_tactics/Imp.List.fst
@@ -14,7 +14,7 @@
    limitations under the License.
 *)
 module Imp.List
-//#set-options "--debug Imp --debug_level SMTQuery"
+//#set-options "--debug SMTQuery"
 open FStar.Mul
 module R = Registers.List
 

diff --git a/examples/native_tactics/Makefile b/examples/native_tactics/Makefile
@@ -54,7 +54,7 @@ all: $(addsuffix .sep.test, $(TAC_MODULES)) $(addsuffix .test, $(ALL))
 	touch $@
 
 %.sep.test: %.fst %.ml
-	$(FSTAR) $*.Test.fst --load $* --debug $* --debug_level tactics
+	$(FSTAR) $*.Test.fst --load $*
 	touch $@
 
 %.ml: %.fst

diff --git a/examples/native_tactics/Registers.Imp.fst b/examples/native_tactics/Registers.Imp.fst
@@ -14,7 +14,7 @@
    limitations under the License.
 *)
 module Registers.Imp
-//#set-options "--debug Imp --debug_level SMTQuery"
+//#set-options "--debug SMTQuery"
 open FStar.Mul
 module R = Registers.List
 
@@ -167,7 +167,7 @@ let normal #a (e:a) =
 
 let norm_assert (p:Type) : Lemma (requires (normal p)) (ensures True) = ()
 
-#set-options "--debug Registers.Imp --debug_level print_normalized_terms --admit_smt_queries true"
+#set-options "--debug print_normalized_terms --admit_smt_queries true"
 // let _ = norm_assert (forall (x:int) rm. R.sel (eval' (Seq [Const x (reg 0)]) rm) 0 == x) // eval' (Seq [Const x (reg 0)]) rm == rm)
 let _ = norm_assert (forall x y. equiv_norm (long_zero x) (long_zero y))
 // let _ = norm_assert (forall x y. equiv_norm (long_zero x) (long_zero y))

diff --git a/examples/tactics/Imp.fst b/examples/tactics/Imp.fst
@@ -15,7 +15,7 @@
 *)
 module Imp
 
-//#set-options "--debug Imp --debug_level SMTQuery"
+//#set-options "--debug SMTQuery"
 
 open FStar.Mul
 open FStar.Tactics.V2

diff --git a/examples/tactics/micro-benchmarks/rewriteEqualityImplications.fst b/examples/tactics/micro-benchmarks/rewriteEqualityImplications.fst
@@ -14,7 +14,7 @@
    limitations under the License.
 *)
 (* Here's the incantation I use to check this file: *)
-(* $ fstar rewriteEqualityImplications.fst --debug RewriteEqualityImplications --debug_level Low | grep "\(Got goal\)\|Checking top-level decl let" *)
+(* $ fstar rewriteEqualityImplications.fst --debug Low | grep "\(Got goal\)\|Checking top-level decl let" *)
 (* Notice the "Got goal" output, in particular---that's the result of preprocessing the VC for each top-level term. *)
 (* Each term results in 0 or more queries that get sent to Z3 *)
 module RewriteEqualityImplications

diff --git a/tests/bug-reports/Bug2478.fst b/tests/bug-reports/Bug2478.fst
@@ -28,7 +28,7 @@ let key0 (bytes:Type0) (#pf: bytes_like bytes) = bytes
 // assume
 // val ps_key0: #bytes:Type0 -> (#pf: bytes_like bytes ) -> test_type bytes (key0 bytes #pf)
 
-// //#push-options "--debug Bug2478 --debug_level Rel,RelCheck,Tac --lax"
+// //#push-options "--debug Rel,RelCheck,Tac --lax"
 // let ps_pair3_0 (bytes:Type0) (#pf: bytes_like bytes ): (test_type bytes (x0:bytes & (x1:bytes & bytes))) =
 //     ps_key0 #_ #_;;
 //     ps_key0 ;;
@@ -39,7 +39,7 @@ let key (bytes:Type0) {|bytes_like bytes|} = bytes
 
 assume val ps_key: #bytes:Type0 -> {|bytes_like bytes|} -> test_type bytes (key bytes)
 
-// #push-options "--debug Bug2478 --debug_level Rel,RelCheck,Tac --lax"
+// #push-options "--debug Rel,RelCheck,Tac --lax"
 let ps_pair3 (bytes:Type0) {| pf: bytes_like bytes|}: (test_type bytes (x0:bytes & (x1:bytes & bytes))) =
     ps_key #_ #_;;
     ps_key;;

diff --git a/tests/bug-reports/Bug3185.fst b/tests/bug-reports/Bug3185.fst
@@ -3,7 +3,7 @@ module Bug3185
 module FT = FStar.Tactics.V2
 
 #push-options "--print_bound_var_types --print_full_names"
-// #push-options "--debug_level NBE --debug Test_NbeIllTyped"
+// #push-options "--debug NBE"
 
 let test_normalise (): unit =
   assert (forall (i: int). op_LessThanOrEqual == op_LessThanOrEqual)

diff --git a/tests/bug-reports/Bug575.fst b/tests/bug-reports/Bug575.fst
@@ -26,7 +26,7 @@ noeq type multi (r:relation) : int -> Type0 =
 
 // Because the dependent pattern matching here goes wrong
 //    Probably because the abbreviation isn't unfolded at the right time
-//#set-options "--debug Bug575 --debug_level Rel --debug_level RelCheck"
+//#set-options "--debug Rel,RelCheck"
 let is_Multi_step (r:relation) (x:int) (projectee : multi r x) =
   match projectee with
   | Multi_step y ry  -> true

diff --git a/tests/bug-reports/UnificationCrash.fst b/tests/bug-reports/UnificationCrash.fst
@@ -16,5 +16,5 @@
 module UnificationCrash
 type tree (a:Type0) = | Tree : a -> tree a
 assume val tree_merge : #a:Type -> cmp:(a -> a -> bool) -> h1:tree a -> tree a
-(* #set-options "--debug Crash --debug_level Rel --debug_level RelCheck --debug_level Extreme --debug_level Gen" *)
+(* #set-options "--debug Rel,RelCheck,Extreme,Gen" *)
 let tree_insert cmp h = tree_merge cmp h
diff --git a/tests/error-messages/QuickTestNBE.fst b/tests/error-messages/QuickTestNBE.fst
@@ -127,7 +127,7 @@ let va_qcode_Test2 : (quickCode unit) =
   )
 
 #push-options "--print_expected_failures"
-//#push-options "--debug QuickTestNBE --debug_level SMTQuery --ugly --print_implicits"
+//#push-options "--debug SMTQuery --ugly --print_implicits"
 [@@expect_failure [19]]
 let va_lemma_Test2 (va_s0:vale_state) =
   wp_sound_code_norm

diff --git a/tests/micro-benchmarks/CoreEqualityGuard.fst b/tests/micro-benchmarks/CoreEqualityGuard.fst
@@ -11,14 +11,14 @@ val r_b (x:a) (y z:b x) : Type0
 
 let dsnd #a (#b: a -> Type) (x: dtuple2 a b) : b (dfst x) = dsnd x
 
-// #push-options "--debug CoreEqualityGuard --debug_level SMTQuery,Rel"
+// #push-options "--debug SMTQuery,Rel"
 // let test (t1 t2 : dtuple2 a b)
 //          (p: squash (dfst t1 == dfst t2))
 //   : b (dfst t1)
 //   = dsnd t2
 
 
-#push-options "--debug CoreEqualityGuard --debug_level Core"
+#push-options "--debug Core"
 
 let test (t1 t2 : dtuple2 a b)
          (p: (dfst t1 == dfst t2 /\

diff --git a/tests/micro-benchmarks/CoreGeneralization.fst b/tests/micro-benchmarks/CoreGeneralization.fst
@@ -2,6 +2,6 @@ module CoreGeneralization
 
 let test (x:int) (#a:Type) (y:a) = y
 
-#push-options "--debug CoreGeneralization --debug_level TwoPhases,Gen"
+#push-options "--debug TwoPhases,Gen"
 let gen x = test x
 
diff --git a/tests/micro-benchmarks/CoreUnivs.fst b/tests/micro-benchmarks/CoreUnivs.fst
@@ -4,6 +4,6 @@ val embedding (a:Type u#a) : Type u#a
 
 val e_div_arrow (#a:Type u#a) (#b:Type u#b) (f:a -> Dv b) : embedding u#a (a -> Dv b)
 
-(* #push-options "--debug CoreUnivs --debug_level Extreme,Rel,ExplainRel,Core" *)
+(* #push-options "--debug Extreme,Rel,ExplainRel,Core" *)
 let e_div_arrow (#a:Type u#a) (#b:Type u#b) (f:a -> Dv b) = admit()
 
diff --git a/tests/micro-benchmarks/Test.NBE.fst b/tests/micro-benchmarks/Test.NBE.fst
@@ -47,4 +47,4 @@ let test3 =
   assert (norm [primops; delta; zeta; nbe] (List.append [1;2;3;4;5;6;7] [8;9])
           = [1;2;3;4;5;6;7;8;9])
 
-#set-options "--debug_level NBE --debug Test.NBE --max_fuel 0"
+// #set-options "--debug NBE --max_fuel 0"
diff --git a/tests/micro-benchmarks/Test.QuickCode.fst b/tests/micro-benchmarks/Test.QuickCode.fst
@@ -35,7 +35,7 @@ let sel (r:reg_file) (x:int) = r x
 let upd (r:reg_file) (x:int) (v:int) = fun y -> if x=y then v else sel r y
 
 
-//#set-options "--debug_level print_normalized_terms --debug_level NBE"
+//#set-options "--debug print_normalized_terms,NBE"
 
 // let test = 
 //   assert (norm_simple (if 0 = 0 then true else false) == true)
@@ -50,8 +50,8 @@ let upd (r:reg_file) (x:int) (v:int) = fun y -> if x=y then v else sel r y
 ////////////////////////////////////////////////////////////////////////////////
 //#reset-options "--z3rlimit 10 --lax"
 
-#set-options "--debug_level NBE"
-//#set-options "--debug_level print_normalized_terms --debug_level NBE"
+#set-options "--debug NBE"
+//#set-options "--debug print_normalized_terms,NBE"
 
 noeq type state = {
   ok: bool;
@@ -95,8 +95,8 @@ let wp_compute_ghash_incremental (x:int) (s0:state) (k:(state -> Type0)) : Type0
   let sM = up_xmm 6 x (up_xmm 5 x (up_xmm 4 x sM)) in
   (k sM)
 
-//#reset-options "--z3rlimit 10 --debug_level NBE --debug_level SMTQuery"
-#reset-options "--z3rlimit 10 --admit_smt_queries true --debug_level SMTQuery"
+//#reset-options "--z3rlimit 10 --debug NBE --debug SMTQuery"
+#reset-options "--z3rlimit 10 --admit_smt_queries true --debug SMTQuery"
 
 let lemma_gcm_core (s0:state) (x:int) : Lemma True =
   let k s =

diff --git a/tests/typeclasses/Bug3130.fst b/tests/typeclasses/Bug3130.fst
@@ -22,7 +22,7 @@ assume val truc:
 
 open FStar.Tactics.Typeclasses
 
-#set-options "--debug_level Low"
+#set-options "--debug Low"
 
 noeq
 type machin (a:Type) (d : typeclass2 bytes #solve a) (content:a) = {

diff --git a/tests/vale/X64.Vale.StrongPost_i.fsti b/tests/vale/X64.Vale.StrongPost_i.fsti
@@ -224,7 +224,7 @@ let va_lemma_weakest_pre_norm_wp (inss:list ins) (s0:state) (sN:state) : pure_wp
 [@"uninterpreted_by_smt"]
 val va_lemma_weakest_pre_norm (inss:list ins) (s0:state) (sN:state) : PURE unit (va_lemma_weakest_pre_norm_wp inss s0 sN)
 
-(* #reset-options "--log_queries --debug X64.Vale.StrongPost_i --debug_level print_normalized_terms" *)
+(* #reset-options "--log_queries --debug X64.Vale.StrongPost_i --debug print_normalized_terms" *)
 // let test_lemma (s0:state) (sN:state) =
 //     assume (s0.ok);
 //     // assume (Map.contains s0.mem (s0.regs Rsi));

diff --git a/ulib/FStar.Stubs.Tactics.V1.Builtins.fsti b/ulib/FStar.Stubs.Tactics.V1.Builtins.fsti
@@ -189,7 +189,7 @@ of printing [str] on the compiler's standard output. *)
 val print : string -> Tac unit
 
 (** [debugging ()] returns true if the current module has the debug flag
-on, i.e. when [--debug MyModule --debug_level Tac] was passed in. *)
+on, i.e. when [--debug Tac] was passed in. *)
 val debugging : unit -> Tac bool
 
 (** Similar to [print], but will dump a text representation of the proofstate

diff --git a/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti b/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti
@@ -190,7 +190,7 @@ of printing [str] on the compiler's standard output. *)
 val print : string -> Tac unit
 
 (** [debugging ()] returns true if the current module has the debug flag
-on, i.e. when [--debug MyModule --debug_level Tac] was passed in. *)
+on, i.e. when [--debug Tac] was passed in. *)
 val debugging : unit -> Tac bool
 
 (** Similar to [print], but will dump a text representation of the proofstate

diff --git a/ulib/FStar.Tactics.V1.Derived.fst b/ulib/FStar.Tactics.V1.Derived.fst
@@ -137,8 +137,7 @@ let qed () : Tac unit =
     | _ -> fail "qed: not done!"
 
 (** [debug str] is similar to [print str], but will only print the message
-if the [--debug] option was given for the current module AND
-[--debug_level Tac] is on. *)
+if [--debug Tac] is on. *)
 let debug (m:string) : Tac unit =
     if debugging () then print m
 

diff --git a/ulib/FStar.Tactics.V2.Derived.fst b/ulib/FStar.Tactics.V2.Derived.fst
@@ -156,8 +156,7 @@ let qed () : Tac unit =
     | _ -> fail "qed: not done!"
 
 (** [debug str] is similar to [print str], but will only print the message
-if the [--debug] option was given for the current module AND
-[--debug_level Tac] is on. *)
+if [--debug Tac] is on. *)
 let debug (m:string) : Tac unit =
     if debugging () then print m