From 37359a7589231e13bf00e62d81ba59d4c6edfcde 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 1/2] 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 = From 3346ace2019df335f9b6218fc3dc561c47f02f36 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sat, 5 Oct 2024 11:46:12 -0700 Subject: [PATCH 2/2] snap --- .../generated/FStar_Extraction_Krml.ml | 48 ++++++++++++------- 1 file changed, 31 insertions(+), 17 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml b/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml index d50b8118269..cb03da40243 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml @@ -3566,9 +3566,13 @@ let (translate_type_decl' : if assumed then (let name3 = FStar_Extraction_ML_Syntax.string_of_mlpath name2 in - FStar_Compiler_Util.print1_warning - "Not extracting type definition %s to KaRaMeL (assumed type)\n" - name3; + (let uu___3 = FStar_Compiler_Debug.any () in + if uu___3 + then + FStar_Compiler_Util.print1_warning + "Not extracting type definition %s to KaRaMeL (assumed type)\n" + name3 + else ()); FStar_Pervasives_Native.None) else (let uu___3 = @@ -3714,11 +3718,15 @@ let (translate_let' : DExternal uu___4 in FStar_Pervasives_Native.Some uu___3 else - ((let uu___5 = - FStar_Extraction_ML_Syntax.string_of_mlpath name2 in - FStar_Compiler_Util.print1_warning - "Not extracting %s to KaRaMeL (polymorphic assumes are not supported)\n" - uu___5); + ((let uu___5 = FStar_Compiler_Debug.any () in + if uu___5 + then + let uu___6 = + FStar_Extraction_ML_Syntax.string_of_mlpath name2 in + FStar_Compiler_Util.print1_warning + "Not extracting %s to KaRaMeL (polymorphic assumes are not supported)\n" + uu___6 + else ()); FStar_Pervasives_Native.None) | { FStar_Extraction_ML_Syntax.mllb_name = name1; FStar_Extraction_ML_Syntax.mllb_tysc = @@ -3758,15 +3766,17 @@ let (translate_let' : (FStar_Compiler_List.length args) t0 in match uu___6 with | (i, eff, t) -> - (if i > Prims.int_zero - then - (let msg = + ((let uu___8 = + (i > Prims.int_zero) && (FStar_Compiler_Debug.any ()) in + if uu___8 + then + let msg = "function type annotation has less arrows than the number of arguments; please mark the return type abbreviation as inline_for_extraction" in - let uu___8 = + let uu___9 = FStar_Extraction_ML_Syntax.string_of_mlpath name2 in FStar_Compiler_Util.print2_warning - "Not extracting %s to KaRaMeL (%s)\n" uu___8 msg) - else (); + "Not extracting %s to KaRaMeL (%s)\n" uu___9 msg + else ()); (let t1 = translate_type env3 t in let binders = translate_binders env3 args in let env4 = add_binders env3 args in @@ -3939,9 +3949,13 @@ let (translate_decl : | FStar_Extraction_ML_Syntax.MLM_Top uu___ -> FStar_Compiler_Effect.failwith "todo: translate_decl [MLM_Top]" | FStar_Extraction_ML_Syntax.MLM_Exn (m, uu___) -> - (FStar_Compiler_Util.print1_warning - "Not extracting exception %s to KaRaMeL (exceptions unsupported)\n" - m; + ((let uu___2 = FStar_Compiler_Debug.any () in + if uu___2 + then + FStar_Compiler_Util.print1_warning + "Not extracting exception %s to KaRaMeL (exceptions unsupported)\n" + m + else ()); []) let (translate_module : FStar_Extraction_ML_UEnv.uenv ->