From 1f63fd4def3643980b5393f2c3da3daa56d91bd5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 18 Sep 2024 10:55:36 -0700 Subject: [PATCH 1/3] Tactics_Load.ml: do not print to stderr (in red) for simple diag messages It's distracting --- ocaml/fstar-lib/FStar_Tactics_Load.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/ocaml/fstar-lib/FStar_Tactics_Load.ml b/ocaml/fstar-lib/FStar_Tactics_Load.ml index aeee4e835c3..c22edf02074 100644 --- a/ocaml/fstar-lib/FStar_Tactics_Load.ml +++ b/ocaml/fstar-lib/FStar_Tactics_Load.ml @@ -6,12 +6,14 @@ module EC = FStar_Errors_Codes module EM = FStar_Errors_Msg module O = FStar_Options +let pout s = if FStar_Compiler_Debug.any () then U.print_string s +let pout1 s x = if FStar_Compiler_Debug.any () then U.print1 s x let perr s = if FStar_Compiler_Debug.any () then U.print_error s let perr1 s x = if FStar_Compiler_Debug.any () then U.print1_error s x let dynlink (fname:string) : unit = try - perr ("Attempting to load " ^ fname ^ "\n"); + pout ("Attempting to load " ^ fname ^ "\n"); Dynlink.loadfile fname with Dynlink.Error e -> E.log_issue_doc FStar_Compiler_Range.dummyRange EC.Error_PluginDynlink [ @@ -25,7 +27,7 @@ let dynlink (fname:string) : unit = let load_tactic tac = dynlink tac; - perr1 "Loaded %s\n" tac + pout1 "Loaded %s\n" tac let load_tactics tacs = List.iter load_tactic tacs From 971288feba61f413b6de8042e932869ad300f8b9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 17 Sep 2024 20:37:17 -0700 Subject: [PATCH 2/3] Tc: Core: nit in error message --- src/typechecker/FStar.TypeChecker.Core.fst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/typechecker/FStar.TypeChecker.Core.fst b/src/typechecker/FStar.TypeChecker.Core.fst index 35dc2b1b7ba..b85c39de4a7 100644 --- a/src/typechecker/FStar.TypeChecker.Core.fst +++ b/src/typechecker/FStar.TypeChecker.Core.fst @@ -1413,7 +1413,7 @@ and do_check (g:env) (e:term) ) ) else ( - fail "Let binding is effectful" + fail (format1 "Let binding is effectful (lbeff = %s)" (show lb.lbeff)) ) | Tm_match {scrutinee=sc; ret_opt=None; brs=branches; rc_opt} -> From 1b38d86fb7c0984d8d95c64e7a7a694e7e7e8dc4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sat, 5 Oct 2024 10:28:25 -0700 Subject: [PATCH 3/3] snap --- ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml index 5fa1cbe3830..d91781037a5 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml @@ -5270,7 +5270,14 @@ and (do_check : Success uu___6 | err -> err) | Error err -> Error err) - else fail "Let binding is effectful")) + else + (let uu___4 = + let uu___5 = + FStar_Class_Show.show FStar_Ident.showable_lident + lb.FStar_Syntax_Syntax.lbeff in + FStar_Compiler_Util.format1 + "Let binding is effectful (lbeff = %s)" uu___5 in + fail uu___4))) | FStar_Syntax_Syntax.Tm_match { FStar_Syntax_Syntax.scrutinee = sc; FStar_Syntax_Syntax.ret_opt = FStar_Pervasives_Native.None;