From ada71571670278ba387711e3b58dfcf4c02a199d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 9 Jan 2025 20:13:29 -0800 Subject: [PATCH 1/2] Debug: nit --- src/basic/FStarC.Compiler.Debug.fst | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/src/basic/FStarC.Compiler.Debug.fst b/src/basic/FStarC.Compiler.Debug.fst index 4eea278f0cd..864ac786b69 100644 --- a/src/basic/FStarC.Compiler.Debug.fst +++ b/src/basic/FStarC.Compiler.Debug.fst @@ -84,15 +84,17 @@ let set_level_high () = dbg_level := 3 let set_level_extreme () = dbg_level := 4 let enable_toggles (keys : list string) : unit = - if Cons? keys then enable (); + if Cons? keys then + enable (); keys |> List.iter (fun k -> - if k = "Low" then set_level_low () - else if k = "Medium" then set_level_medium () - else if k = "High" then set_level_high () - else if k = "Extreme" then set_level_extreme () - else - let t = get_toggle k in - t := true + match k with + | "Low" -> set_level_low () + | "Medium" -> set_level_medium () + | "High" -> set_level_high () + | "Extreme" -> set_level_extreme () + | _ -> + let t = get_toggle k in + t := true ) let disable_all () : unit = From c1f0d5c935e090c1826c3596c18a5708fb3fcfb6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 9 Jan 2025 20:13:36 -0800 Subject: [PATCH 2/2] Tc: prevent reset of -d across modules And respect --debug_all_modules --- src/typechecker/FStarC.TypeChecker.Tc.fst | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/src/typechecker/FStarC.TypeChecker.Tc.fst b/src/typechecker/FStarC.TypeChecker.Tc.fst index c4900c7c30f..666d19baeb6 100644 --- a/src/typechecker/FStarC.TypeChecker.Tc.fst +++ b/src/typechecker/FStarC.TypeChecker.Tc.fst @@ -1135,9 +1135,9 @@ let tc_partial_modul env modul = if Debug.any () then BU.print3 "Now %s %s of %s\n" action label (string_of_lid modul.name); - Debug.disable_all (); - if Options.should_check (string_of_lid modul.name) // || Options.debug_all_modules () - then Debug.enable_toggles (Options.debug_keys ()); + let dsnap = Debug.snapshot () in + if not (Options.should_check (string_of_lid modul.name)) && not (Options.debug_all_modules ()) + then Debug.disable_all (); let name = BU.format2 "%s %s" (if modul.is_interface then "interface" else "module") (string_of_lid modul.name) in let env = {env with Env.is_iface=modul.is_interface; admit=not verify} in @@ -1148,6 +1148,7 @@ let tc_partial_modul env modul = (string_of_lid modul.name) (if modul.is_interface then " (interface)" else "")) (fun () -> let ses, env = tc_decls env modul.declarations in + Debug.restore dsnap; {modul with declarations=ses}, env ) @@ -1222,9 +1223,9 @@ let load_checked_module (en:env) (m:modul) :env = module. *) (* Reset debug flags *) - if Options.should_check (string_of_lid m.name) // || Options.debug_all_modules () - then Debug.enable_toggles (Options.debug_keys ()) - else Debug.disable_all (); + let dsnap = Debug.snapshot () in + if not (Options.should_check (string_of_lid m.name)) && not (Options.debug_all_modules ()) + then Debug.disable_all (); let m = deep_compress_modul m in let env = load_checked_module_sigelts en m in @@ -1232,6 +1233,7 @@ let load_checked_module (en:env) (m:modul) :env = //except with the flag `must_check_exports` set to false, since this is already a checked module //the second true flag is for iface_exists, used to determine whether should extract interface or not let _, env = finish_partial_modul true true env m in + Debug.restore dsnap; env let load_partial_checked_module (en:env) (m:modul) : env =