From a823b28f361539b1edf9d58c51d7cd2e7a093bc9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 18 Sep 2024 17:07:31 -0700 Subject: [PATCH] Extraction: reduce krml output unless -d/--debug Karamel extraction prints many warnings when definitions cannot be extracted, but most of these are benign, since they are just types, or ghost code, etc. This patch disables these warnings unless some debugging is enabled. --- src/extraction/FStar.Extraction.Krml.fst | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/extraction/FStar.Extraction.Krml.fst b/src/extraction/FStar.Extraction.Krml.fst index 8e3568c8acd..af08c1438dc 100644 --- a/src/extraction/FStar.Extraction.Krml.fst +++ b/src/extraction/FStar.Extraction.Krml.fst @@ -1331,7 +1331,8 @@ let translate_type_decl' env ty: option decl = Some (DTypeAbstractStruct name) else if assumed then let name = string_of_mlpath name in - BU.print1_warning "Not extracting type definition %s to KaRaMeL (assumed type)\n" name; + if Debug.any () then + BU.print1_warning "Not extracting type definition %s to KaRaMeL (assumed type)\n" name; // JP: TODO: shall we be smarter here? None else @@ -1381,7 +1382,8 @@ let translate_let' env flavor lb: option decl = if List.length tvars = 0 then Some (DExternal (translate_cc meta, translate_flags meta, name, translate_type env t0, arg_names)) else begin - BU.print1_warning "Not extracting %s to KaRaMeL (polymorphic assumes are not supported)\n" (Syntax.string_of_mlpath name); + if Debug.any () then + BU.print1_warning "Not extracting %s to KaRaMeL (polymorphic assumes are not supported)\n" (Syntax.string_of_mlpath name); None end @@ -1405,7 +1407,7 @@ let translate_let' env flavor lb: option decl = in let name = env.module_name, name in let i, eff, t = find_return_type E_PURE (List.length args) t0 in - if i > 0 then begin + if i > 0 && Debug.any () then begin let msg = "function type annotation has less arrows than the \ number of arguments; please mark the return type abbreviation as \ inline_for_extraction" in @@ -1509,7 +1511,8 @@ let translate_decl env d: list decl = failwith "todo: translate_decl [MLM_Top]" | MLM_Exn (m, _) -> - BU.print1_warning "Not extracting exception %s to KaRaMeL (exceptions unsupported)\n" m; + if Debug.any () then + BU.print1_warning "Not extracting exception %s to KaRaMeL (exceptions unsupported)\n" m; [] let translate_module uenv (m : mlpath & option (mlsig & mlmodule) & mllib) : file =