Skip to content

Commit

Permalink
Extraction: reduce krml output unless -d/--debug
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
mtzguido committed Oct 5, 2024
1 parent 34744ec commit a823b28
Showing 1 changed file with 7 additions and 4 deletions.
11 changes: 7 additions & 4 deletions src/extraction/FStar.Extraction.Krml.fst
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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

Expand All @@ -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
Expand Down Expand Up @@ -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 =
Expand Down

0 comments on commit a823b28

Please sign in to comment.