From 5639459f542a0e6e716b96facdf8faf5cd843a2f Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 28 Aug 2019 17:25:44 -0400 Subject: [PATCH 1/4] feat(sanity_check): improve sanity_check - add hole command for sanity check (note: hole commands only work when an expression is expected, not when a command is expected, which is unfortunate) - print the type of the unused arguments - print whether an unused argument is a duplicate - better check to filter automatically generated declarations - do not print arguments of type `parse _` - The binding brackets from `tactic.where` are moved to `meta.expr`. The definition is changed so that strict implicit arguments are printed as `{{ ... }}` --- src/meta/expr.lean | 46 +++++++++++++++ src/tactic/core.lean | 26 ++++++++- src/tactic/sanity_check.lean | 105 +++++++++++++++++++++-------------- src/tactic/where.lean | 8 +-- test/sanity_check.lean | 2 + 5 files changed, 138 insertions(+), 49 deletions(-) diff --git a/src/meta/expr.lean b/src/meta/expr.lean index 10f84b2802649..741cbe71b07fb 100644 --- a/src/meta/expr.lean +++ b/src/meta/expr.lean @@ -15,6 +15,19 @@ Authors: Mario Carneiro, Simon Hudon, Scott Morrison, Keeley Hoek, Robert Y. Lew expr, name, declaration, level, environment, meta, metaprogramming, tactic -/ +namespace binder_info + +instance : inhabited binder_info := ⟨ binder_info.default ⟩ + +/-- The brackets corresponding to a given binder_info. -/ +def brackets : binder_info → string × string +| binder_info.implicit := ("{", "}") +| binder_info.strict_implicit := ("{{", "}}") +| binder_info.inst_implicit := ("[", "]") +| _ := ("(", ")") + +end binder_info + namespace name /-- Find the largest prefix `n` of a `name` such that `f n ≠ none`, then replace this prefix @@ -305,4 +318,37 @@ meta def is_axiom : declaration → bool | (ax _ _ _) := tt | _ := ff +/-- Checks whether a declaration is automatically generated in the environment -/ +meta def is_auto_generated (e : environment) (d : declaration) : bool := +e.is_constructor d.to_name ∨ +(e.is_projection d.to_name).is_some ∨ +(e.is_constructor d.to_name.get_prefix ∧ + d.to_name.last ∈ ["inj", "inj_eq", "sizeof_spec", "inj_arrow"]) ∨ +(e.is_inductive d.to_name.get_prefix ∧ + d.to_name.last ∈ ["below", "binduction_on", "brec_on", "cases_on", "dcases_on", "drec_on", "drec", + "rec", "rec_on", "no_confusion", "no_confusion_type", "sizeof", "ibelow", "has_sizeof_inst"]) + end declaration + +/-- The type of binders containing a name, the binding info and the binding type -/ +@[derive decidable_eq] +meta structure binder := + (name : name) + (info : binder_info) + (type : expr) + +namespace binder +/- Turn a binder into a string. Uses expr.to_string for the type. -/ +protected meta def to_string (b : binder) : string := +let (l, r) := b.info.brackets in +l ++ b.name.to_string ++ " : " ++ b.type.to_string ++ r + +open tactic +meta instance : inhabited binder := ⟨⟨default _, default _, default _⟩⟩ +meta instance : has_to_string binder := ⟨ binder.to_string ⟩ +meta instance : has_to_format binder := ⟨ λ b, b.to_string ⟩ +meta instance : has_to_tactic_format binder := +⟨ λ b, let (l, r) := b.info.brackets in + (λ e, l ++ b.name.to_string ++ " : " ++ e ++ r) <$> pp b.type ⟩ + +end binder diff --git a/src/tactic/core.lean b/src/tactic/core.lean index 2b519fe9affac..50a4dcd7e8484 100644 --- a/src/tactic/core.lean +++ b/src/tactic/core.lean @@ -105,8 +105,18 @@ meta def mk_user_fresh_name : tactic name := do nm ← mk_fresh_name, return $ `user__ ++ nm.pop_prefix.sanitize_name ++ `user__ + +/-- Checks whether n' has attribute n. -/ +meta def has_attribute' : name → name → tactic bool | n n' := +succeeds (has_attribute n n') + +/-- Checks whether the name is a simp lemma -/ meta def is_simp_lemma : name → tactic bool := -succeeds ∘ tactic.has_attribute `simp +has_attribute' `simp + +/-- Checks whether the name is an instance. -/ +meta def is_instance : name → tactic bool := +has_attribute' `instance meta def local_decls : tactic (name_map declaration) := do e ← tactic.get_env, @@ -315,6 +325,20 @@ whnf type >>= get_expl_pi_arity_aux meta def get_expl_arity (fn : expr) : tactic nat := infer_type fn >>= get_expl_pi_arity +/-- Auxilliary defintion for `get_pi_binders`. -/ +meta def get_pi_binders_aux : list binder → expr → tactic (list binder × expr) +| es (expr.pi n bi d b) := + do m ← mk_fresh_name, + let l := expr.local_const m n bi d, + let new_b := expr.instantiate_var b l, + get_pi_binders_aux (⟨n, bi, d⟩::es) new_b +| es e := return (es, e) + +/-- Get the binders and target of a pi-type. Instantiates bound variables by + local constants. -/ +meta def get_pi_binders : expr → tactic (list binder × expr) | e := +do (es, e) ← get_pi_binders_aux [] e, return (es.reverse, e) + /-- variation on `assert` where a (possibly incomplete) proof of the assertion is provided as a parameter. diff --git a/src/tactic/sanity_check.lean b/src/tactic/sanity_check.lean index 50552319a8227..a0ad89df36e9a 100644 --- a/src/tactic/sanity_check.lean +++ b/src/tactic/sanity_check.lean @@ -29,7 +29,7 @@ meta def fold_over_with_cond {α} (tac : declaration → tactic (option α)) : tactic (list (declaration × α)) := do e ← get_env, e.mfold [] $ λ d ds, - if name.is_internal d.to_name then return ds else + if d.to_name.is_internal || d.is_auto_generated e then return ds else do o ← tac d, if h : o.is_some then return $ (d, option.get h)::ds else return ds @@ -38,14 +38,14 @@ meta def fold_over_with_cond_sorted {α} (tac : declaration → tactic (option tactic (list (string × list (declaration × α))) := do e ← get_env, ds ← fold_over_with_cond tac, - let ds₂ := rb_lmap.of_list (ds.map (λ x, ((e.decl_olean x.1.to_name).get_or_else "", x))), + let ds₂ := rb_lmap.of_list (ds.map (λ x, ((e.decl_olean x.1.to_name).iget, x))), return $ ds₂.to_list /-- Make the output of `fold_over_with_cond` printable, in the following form: - #print -- -/ + #print -/ meta def print_decls {α} [has_to_format α] (ds : list (declaration × α)) : format := ds.foldl - (λ f x, f ++ format.line ++ to_fmt "#print " ++ to_fmt x.1.to_name ++ " -- " ++ to_fmt x.2) + (λ f x, f ++ format.line ++ to_fmt "#print " ++ to_fmt x.1.to_name ++ " /- " ++ to_fmt x.2 ++ " -/") format.nil /-- Make the output of `fold_over_with_cond_sorted` printable, with the file path + name inserted.-/ @@ -76,36 +76,54 @@ do ml ← get_mathlib_dir, return $ print_decls_sorted $ f.map (λ x, ⟨x.1.popn ml.length, x.2⟩) /-- Auxilliary definition for `check_unused_arguments_aux` -/ -meta def check_unused_arguments_aux : list ℕ → ℕ → ℕ → expr → list ℕ -:= λ l n n_max e, +meta def check_unused_arguments_aux : list ℕ → ℕ → ℕ → expr → list ℕ | l n n_max e := if n > n_max then l else -if ¬is_lambda e then - if e = const `true.intro [] ∨ e = const `trivial [] then [] else l -- don't return if the target is true -else +if ¬is_lambda e ∧ ¬is_pi e then l else let b := e.binding_body in let l' := if b.has_var_idx 0 then l else n :: l in check_unused_arguments_aux l' (n+1) n_max b /-- Check which arguments of a declaration are not used. Prints a list of natural numbers corresponding to which arguments are not used (e.g. this outputs [1, 4] if the first and fourth arguments are unused). - We return [] if the body of `e` is `true.intro` or `trivial`, - to filter many automatically generated declarations. - We don't print arguments that are larger than the arity of the type of the declaration. -/ + Checks both the type and the value of `d` for whether the argument is used + (in rare cases an argument is used in the type but not in the value). + We return [] if the declaration was automatically generated. + We print arguments that are larger than the arity of the type of the declaration + (without unfolding definitions). -/ meta def check_unused_arguments (d : declaration) : option (list ℕ) := -let l := check_unused_arguments_aux [] 1 (d.type.pi_arity) d.value in -if l = [] then none else l.reverse - -/-- Get all declarations with unused arguments -/ +let l := check_unused_arguments_aux [] 1 d.type.pi_arity d.value in +if l = [] then none else +let l2 := check_unused_arguments_aux [] 1 d.type.pi_arity d.type in +(l.filter $ λ n, n ∈ l2).reverse + +/- Check for unused arguments and print them in a nice way. + See also `check_unused_arguments`. + This tactic additionally filters out all unused arguments of type `parse _` -/ +meta def prettify_unused_arguments (d : declaration) : tactic (option format) := +do + let ns := check_unused_arguments d, + if ¬ ns.is_some then return none else do + let ns := ns.iget, + (ds, _) ← get_pi_binders d.type, + let ns := ns.map (λ n, (n, (ds.nth $ n - 1).iget)), + let ns := ns.filter (λ x, x.2.type.get_app_fn ≠ const `interactive.parse []), + if ns = [] then return none else do + ds' ← ds.mmap pp, + ns ← ns.mmap (λ ⟨n, b⟩, (λ s, to_fmt "argument " ++ to_fmt n ++ ": " ++ s ++ + (if ds.countp (λ b', b.type = b'.type) ≥ 2 then " (duplicate)" else "")) <$> pp b), + return $ some $ ns.to_string_aux tt + +/-- Print all declarations with unused arguments -/ meta def get_all_unused_args : tactic unit := -print_all_decls (return ∘ check_unused_arguments) >>= trace +print_all_decls prettify_unused_arguments >>= trace -/-- Get all declarations in mathlib with unused arguments -/ +/-- Print all declarations in mathlib with unused arguments -/ meta def get_all_unused_args_mathlib : tactic unit := -print_decls_mathlib (return ∘ check_unused_arguments) >>= trace +print_decls_mathlib prettify_unused_arguments >>= trace -/-- Get all declarations in current file with unused arguments. -/ +/-- Print all declarations in current file with unused arguments. -/ meta def get_all_unused_args_current_file : tactic unit := -print_decls_current_file (return ∘ check_unused_arguments) >>= trace +print_decls_current_file prettify_unused_arguments >>= trace /-- Checks whether the correct declaration constructor (definition of theorem) by comparing it to its sort. This will automatically remove all instances and automatically generated @@ -114,45 +132,50 @@ meta def incorrect_def_lemma (d : declaration) : tactic (option string) := do e ← get_env, expr.sort n ← infer_type d.type, - if d.is_constant ∨ d.is_axiom ∨ (e.is_projection d.to_name).is_some ∨ - (d.is_definition : bool) = (n ≠ level.zero : bool) ∨ - (d.to_name.last ∈ ["inj","inj_eq","sizeof_spec"] ∧ - e.is_constructor d.to_name.get_prefix) ∨ - (d.to_name.last ∈ ["dcases_on","drec_on","drec","cases_on","rec_on","binduction_on"] ∧ - e.is_inductive d.to_name.get_prefix) + let is_def : Prop := d.is_definition, + if d.is_constant ∨ d.is_axiom ∨ is_def ↔ (n ≠ level.zero) then return none - else (option.is_some <$> try_core (has_attribute `instance d.to_name)) >>= - λ b, return $ if b then none + else is_instance d.to_name >>= λ b, return $ + if b then none else if (d.is_definition : bool) then "is a def, should be a lemma/theorem" else "is a lemma/theorem, should be a def" -/-- Get all declarations in mathlib incorrectly marked as def/lemma -/ +/-- Print all declarations in mathlib incorrectly marked as def/lemma -/ meta def incorrect_def_lemma_mathlib : tactic unit := -print_decls_mathlib (return ∘ check_unused_arguments) >>= trace +print_decls_mathlib prettify_unused_arguments >>= trace + +/-- Return the message printed by `#sanity_check`. -/ +meta def sanity_check : tactic format := +do + let s := to_fmt "/- Note: This command is still in development. -/\n\n", + f ← print_decls_current_file (prettify_unused_arguments), + let s := s ++ if f.is_nil then "/- OK: No unused arguments in the current file. -/\n\n" + else to_fmt "/- Unused arguments in the current file: -/" ++ f ++ "\n\n", + f ← print_decls_current_file incorrect_def_lemma, + let s := s ++ if f.is_nil then "/- OK: All declarations correctly marked as def/lemma -/\n\n" + else to_fmt "/- Declarations incorrectly marked as def/lemma: -/" ++ f ++ "\n", + return s /-- The command `#sanity_check` at the bottom of a file will warn you about some common mistakes in that file. -/ @[user_command] meta def sanity_check_cmd (_ : parse $ tk "#sanity_check") : parser unit := -do - trace "/- Note: This command is still in development. -/\n", - f ← print_decls_current_file (return ∘ check_unused_arguments), - if f.is_nil then trace "/- OK: No unused arguments in the current file. -/" - else trace (to_fmt "/- Unused arguments in the current file: -/" ++ f ++ format.line), - f ← print_decls_current_file incorrect_def_lemma, - if f.is_nil then trace "/-OK: All declarations correctly marked as def/lemma -/" - else trace (to_fmt "/- Declarations incorrectly marked as def/lemma: -/" ++ f ++ format.line), - skip +do s ← sanity_check, trace s /-- The command `#sanity_check_mathlib` checks all of mathlib for certain mistakes. -/ @[user_command] meta def sanity_check_mathlib_cmd (_ : parse $ tk "#sanity_check_mathlib") : parser unit := do trace "/- Note: This command is still in development. -/\n", - f ← print_decls_mathlib (return ∘ check_unused_arguments), + f ← print_decls_mathlib (prettify_unused_arguments), trace (to_fmt "/- UNUSED ARGUMENTS: -/" ++ f ++ format.line), f ← print_decls_mathlib incorrect_def_lemma, trace (to_fmt "/- INCORRECT DEF/LEMMA: -/" ++ f ++ format.line), skip +@[hole_command] meta def sanity_check_hole_cmd : hole_command := +{ name := "Sanity Check", + descr := "Sanity check: Find mistakes in current file.", + action := λ es, do s ← sanity_check, return [(s.to_string,"")] } + -- #sanity_check -- #sanity_check_mathlib diff --git a/src/tactic/where.lean b/src/tactic/where.lean index badc167e77d06..0b32f4bc6bbe9 100644 --- a/src/tactic/where.lean +++ b/src/tactic/where.lean @@ -53,12 +53,6 @@ meta def get_def_variables (n : name) : tactic (list (name × binder_info × exp meta def get_includes_core (flag : name) : tactic (list (name × binder_info × expr)) := get_def_variables flag -meta def binder_brackets : binder_info → string × string -| binder_info.implicit := ("{", "}") -| binder_info.strict_implicit := ("{", "}") -| binder_info.inst_implicit := ("[", "]") -| _ := ("(", ")") - meta def binder_priority : binder_info → ℕ | binder_info.implicit := 1 | binder_info.strict_implicit := 2 @@ -126,7 +120,7 @@ let n := to_string n, (ns, ins) := collect_implicit_names ns in if n.front = '_' then (ns, n :: ins) else (n :: ns, ins) meta def format_variable : expr × binder_info × list name → tactic string -| (e, bi, ns) := do let (l, r) := binder_brackets bi, +| (e, bi, ns) := do let (l, r) := bi.brackets, e ← pp e, let (ns, ins) := collect_implicit_names ns, let ns := " ".intercalate $ ns.map to_string, diff --git a/test/sanity_check.lean b/test/sanity_check.lean index ab889b73c302c..271c2ce85ed43 100644 --- a/test/sanity_check.lean +++ b/test/sanity_check.lean @@ -22,3 +22,5 @@ run_cmd do let e2 : list (name × _) := e.map $ λ x, ⟨x.1.to_name, x.2⟩, guard $ ∃(x ∈ e2), (x : name × _).1 = `foo2, guard $ ∃(x ∈ e2), (x : name × _).1 = `foo3 + +-- #sanity_check_mathlib From ca86ff9e2f26368d8fe26c6ecfc37dac8f403a7c Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 28 Aug 2019 17:36:30 -0400 Subject: [PATCH 2/4] typos --- src/meta/expr.lean | 2 +- src/tactic/sanity_check.lean | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/meta/expr.lean b/src/meta/expr.lean index 741cbe71b07fb..127df31a1ba42 100644 --- a/src/meta/expr.lean +++ b/src/meta/expr.lean @@ -338,7 +338,7 @@ meta structure binder := (type : expr) namespace binder -/- Turn a binder into a string. Uses expr.to_string for the type. -/ +/-- Turn a binder into a string. Uses expr.to_string for the type. -/ protected meta def to_string (b : binder) : string := let (l, r) := b.info.brackets in l ++ b.name.to_string ++ " : " ++ b.type.to_string ++ r diff --git a/src/tactic/sanity_check.lean b/src/tactic/sanity_check.lean index a0ad89df36e9a..cd009ee38ccdb 100644 --- a/src/tactic/sanity_check.lean +++ b/src/tactic/sanity_check.lean @@ -148,7 +148,7 @@ print_decls_mathlib prettify_unused_arguments >>= trace meta def sanity_check : tactic format := do let s := to_fmt "/- Note: This command is still in development. -/\n\n", - f ← print_decls_current_file (prettify_unused_arguments), + f ← print_decls_current_file prettify_unused_arguments, let s := s ++ if f.is_nil then "/- OK: No unused arguments in the current file. -/\n\n" else to_fmt "/- Unused arguments in the current file: -/" ++ f ++ "\n\n", f ← print_decls_current_file incorrect_def_lemma, @@ -166,7 +166,7 @@ do s ← sanity_check, trace s parser unit := do trace "/- Note: This command is still in development. -/\n", - f ← print_decls_mathlib (prettify_unused_arguments), + f ← print_decls_mathlib prettify_unused_arguments, trace (to_fmt "/- UNUSED ARGUMENTS: -/" ++ f ++ format.line), f ← print_decls_mathlib incorrect_def_lemma, trace (to_fmt "/- INCORRECT DEF/LEMMA: -/" ++ f ++ format.line), From f5ed98affaae1bd1396068999be19712a78dbfe8 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 28 Aug 2019 17:42:37 -0400 Subject: [PATCH 3/4] improve docstring --- src/tactic/sanity_check.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/tactic/sanity_check.lean b/src/tactic/sanity_check.lean index cd009ee38ccdb..033f2ab3fc5f1 100644 --- a/src/tactic/sanity_check.lean +++ b/src/tactic/sanity_check.lean @@ -96,7 +96,8 @@ if l = [] then none else let l2 := check_unused_arguments_aux [] 1 d.type.pi_arity d.type in (l.filter $ λ n, n ∈ l2).reverse -/- Check for unused arguments and print them in a nice way. +/- Check for unused arguments, and print them with their position, variable name, type and whether + the argument is a duplicate. See also `check_unused_arguments`. This tactic additionally filters out all unused arguments of type `parse _` -/ meta def prettify_unused_arguments (d : declaration) : tactic (option format) := From 028d49aef18fc8840fc4759aceb03eff0176fb6f Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 28 Aug 2019 18:01:57 -0400 Subject: [PATCH 4/4] Also check for duplicated namespaces Fun fact: I had to remove an unused argument from `decidable_chain'` for my function to work. --- src/data/list/defs.lean | 2 +- src/tactic/sanity_check.lean | 25 ++++++++++++++++++------- 2 files changed, 19 insertions(+), 8 deletions(-) diff --git a/src/data/list/defs.lean b/src/data/list/defs.lean index a2c0bf66ae7a2..3f1d5c08dbd69 100644 --- a/src/data/list/defs.lean +++ b/src/data/list/defs.lean @@ -395,7 +395,7 @@ variable {R} instance decidable_chain [decidable_rel R] (a : α) (l : list α) : decidable (chain R a l) := by induction l generalizing a; simp only [chain.nil, chain_cons]; resetI; apply_instance -instance decidable_chain' [decidable_rel R] (a : α) (l : list α) : decidable (chain' R l) := +instance decidable_chain' [decidable_rel R] (l : list α) : decidable (chain' R l) := by cases l; dunfold chain'; apply_instance end chain diff --git a/src/tactic/sanity_check.lean b/src/tactic/sanity_check.lean index 033f2ab3fc5f1..11393c084aab8 100644 --- a/src/tactic/sanity_check.lean +++ b/src/tactic/sanity_check.lean @@ -45,14 +45,14 @@ do e ← get_env, #print -/ meta def print_decls {α} [has_to_format α] (ds : list (declaration × α)) : format := ds.foldl - (λ f x, f ++ format.line ++ to_fmt "#print " ++ to_fmt x.1.to_name ++ " /- " ++ to_fmt x.2 ++ " -/") + (λ f x, f ++ "\n" ++ to_fmt "#print " ++ to_fmt x.1.to_name ++ " /- " ++ to_fmt x.2 ++ " -/") format.nil /-- Make the output of `fold_over_with_cond_sorted` printable, with the file path + name inserted.-/ meta def print_decls_sorted {α} [has_to_format α] (ds : list (string × list (declaration × α))) : format := ds.foldl - (λ f x, f ++ format.line ++ format.line ++ to_fmt "-- " ++ to_fmt x.1 ++ print_decls x.2) + (λ f x, f ++ "\n" ++ "\n" ++ to_fmt "-- " ++ to_fmt x.1 ++ print_decls x.2) format.nil /- Print all (non-internal) declarations where tac return `some x`-/ @@ -127,8 +127,7 @@ meta def get_all_unused_args_current_file : tactic unit := print_decls_current_file prettify_unused_arguments >>= trace /-- Checks whether the correct declaration constructor (definition of theorem) by comparing it - to its sort. This will automatically remove all instances and automatically generated - definitions -/ + to its sort. Instances will not be printed -/ meta def incorrect_def_lemma (d : declaration) : tactic (option string) := do e ← get_env, @@ -145,6 +144,13 @@ do meta def incorrect_def_lemma_mathlib : tactic unit := print_decls_mathlib prettify_unused_arguments >>= trace +/-- Checks whether a declaration has a namespace twice consecutively in its name -/ +meta def dup_namespace (d : declaration) : tactic (option string) := +return $ let nm := d.to_name.components in if nm.chain' (≠) then none + else let s := (nm.find $ λ n, nm.count n ≥ 2).iget.to_string in + some $ "The namespace " ++ s ++ " is duplicated in the name" + + /-- Return the message printed by `#sanity_check`. -/ meta def sanity_check : tactic format := do @@ -154,7 +160,10 @@ do else to_fmt "/- Unused arguments in the current file: -/" ++ f ++ "\n\n", f ← print_decls_current_file incorrect_def_lemma, let s := s ++ if f.is_nil then "/- OK: All declarations correctly marked as def/lemma -/\n\n" - else to_fmt "/- Declarations incorrectly marked as def/lemma: -/" ++ f ++ "\n", + else to_fmt "/- Declarations incorrectly marked as def/lemma: -/" ++ f ++ "\n\n", + f ← print_decls_current_file dup_namespace, + let s := s ++ if f.is_nil then "/- OK: No declarations have a duplicate namespace -/\n\n" + else to_fmt "/- Declarations with a namespace duplicated: -/" ++ f ++ "\n\n", return s /-- The command `#sanity_check` at the bottom of a file will warn you about some common mistakes @@ -168,9 +177,11 @@ do s ← sanity_check, trace s do trace "/- Note: This command is still in development. -/\n", f ← print_decls_mathlib prettify_unused_arguments, - trace (to_fmt "/- UNUSED ARGUMENTS: -/" ++ f ++ format.line), + trace (to_fmt "/- UNUSED ARGUMENTS: -/" ++ f ++ "\n"), f ← print_decls_mathlib incorrect_def_lemma, - trace (to_fmt "/- INCORRECT DEF/LEMMA: -/" ++ f ++ format.line), + trace (to_fmt "/- INCORRECT DEF/LEMMA: -/" ++ f ++ "\n"), + f ← print_decls_mathlib dup_namespace, + trace (to_fmt "/- DUPLICATED NAMESPACES IN NAME: -/" ++ f ++ "\n"), skip @[hole_command] meta def sanity_check_hole_cmd : hole_command :=