feat: collect kernel diagnostic information (#4082)

We now also track which declarations have been unfolded by the kernel
when using
```lean
set_option diagnostics true
```

src/Lean/CoreM.lean

@@ -121,13 +121,16 @@ instance : MonadOptions CoreM where
   getOptions := return (← read).options
 
 instance : MonadWithOptions CoreM where
-  withOptions f x :=
+  withOptions f x := do
+    let options := f (← read).options
+    let diag := diagnostics.get options
+    if Kernel.isDiagnosticsEnabled (← getEnv) != diag then
+      modifyEnv fun env => Kernel.enableDiag env diag
     withReader
       (fun ctx =>
-        let options := f ctx.options
         { ctx with
           options
-          diag := diagnostics.get options
+          diag
           maxRecDepth := maxRecDepth.get options })
       x
 

src/Lean/Elab/Command.lean

@@ -157,7 +157,7 @@ private def runCore (x : CoreM α) : CommandElabM α := do
   let s ← get
   let ctx ← read
   let heartbeats ← IO.getNumHeartbeats
-  let env := s.env
+  let env := Kernel.resetDiag s.env
   let scope := s.scopes.head!
   let coreCtx : Core.Context := {
     fileName       := ctx.fileName

src/Lean/Environment.lean

@@ -901,6 +901,55 @@ builtin_initialize namespacesExt : SimplePersistentEnvExtension Name NameSSet
     addEntryFn      := fun s n => s.insert n
   }
 
+structure Kernel.Diagnostics where
+  /-- Number of times each declaration has been unfolded by the kernel. -/
+  unfoldCounter : PHashMap Name Nat := {}
+  /-- If `enabled = true`, kernel records declarations that have been unfolded. -/
+  enabled : Bool := false
+  deriving Inhabited
+
+/--
+Extension for storting diagnostic information.
+
+Remark: We store kernel diagnostic information in an environment extension to simplify
+the interface with the kernel implemented in C/C++. Thus, we can only track
+declarations in methods, such as `addDecl`, which return a new environment.
+`Kernel.isDefEq` and `Kernel.whnf` do not update the statistics. We claim
+this is ok since these methods are mainly used for debugging.
+-/
+builtin_initialize diagExt : EnvExtension Kernel.Diagnostics ←
+  registerEnvExtension (pure {})
+
+@[export lean_kernel_diag_is_enabled]
+def Kernel.Diagnostics.isEnabled (d : Diagnostics) : Bool :=
+  d.enabled
+
+/-- Enables/disables kernel diagnostics. -/
+def Kernel.enableDiag (env : Environment) (flag : Bool) : Environment :=
+  diagExt.modifyState env fun s => { s with enabled := flag }
+
+def Kernel.isDiagnosticsEnabled (env : Environment) : Bool :=
+  diagExt.getState env |>.enabled
+
+def Kernel.resetDiag (env : Environment) : Environment :=
+  diagExt.modifyState env fun s => { s with unfoldCounter := {} }
+
+@[export lean_kernel_record_unfold]
+def Kernel.Diagnostics.recordUnfold (d : Diagnostics) (declName : Name) : Diagnostics :=
+  if d.enabled then
+    let cNew := if let some c := d.unfoldCounter.find? declName then c + 1 else 1
+    { d with unfoldCounter := d.unfoldCounter.insert declName cNew }
+  else
+    d
+
+@[export lean_kernel_get_diag]
+def Kernel.getDiagnostics (env : Environment) : Diagnostics :=
+  diagExt.getState env
+
+@[export lean_kernel_set_diag]
+def Kernel.setDiagnostics (env : Environment) (diag : Diagnostics) : Environment :=
+  diagExt.setState env diag
+
 namespace Environment
 
 /-- Register a new namespace in the environment. -/

src/Lean/Meta/Diagnostics.lean

@@ -75,6 +75,7 @@ def reportDiag : MetaM Unit := do
     let unfoldReducible ← mkDiagSummaryForUnfoldedReducible unfoldCounter
     let heu ← mkDiagSummary (← get).diag.heuristicCounter
     let inst ← mkDiagSummaryForUsedInstances
+    let unfoldKernel ← mkDiagSummary (Kernel.getDiagnostics (← getEnv)).unfoldCounter
     unless unfoldDefault.isEmpty && unfoldInstance.isEmpty && unfoldReducible.isEmpty && heu.isEmpty && inst.isEmpty do
       let m := MessageData.nil
       let m := appendSection m `reduction "unfolded declarations" unfoldDefault
@@ -82,6 +83,7 @@ def reportDiag : MetaM Unit := do
       let m := appendSection m `reduction "unfolded reducible declarations" unfoldReducible
       let m := appendSection m `type_class "used instances" inst
       let m := appendSection m `def_eq "heuristic for solving `f a =?= f b`" heu
+      let m := appendSection m `kernel "unfolded declarations" unfoldKernel
       let m := m ++ "use `set_option diagnostics.threshold <num>` to control threshold for reporting counters"
       logInfo m
 

src/kernel/environment.cpp

@@ -28,6 +28,38 @@ extern "C" object* lean_get_extension(object*, object*);
 extern "C" object* lean_set_extension(object*, object*, object*);
 extern "C" object* lean_environment_set_main_module(object*, object*);
 extern "C" object* lean_environment_main_module(object*);
+extern "C" object* lean_kernel_record_unfold (object*, object*);
+extern "C" object* lean_kernel_get_diag(object*);
+extern "C" object* lean_kernel_set_diag(object*, object*);
+extern "C" uint8* lean_kernel_diag_is_enabled(object*);
+
+void diagnostics::record_unfold(name const & decl_name) {
+    m_obj = lean_kernel_record_unfold(to_obj_arg(), decl_name.to_obj_arg());
+}
+
+scoped_diagnostics::scoped_diagnostics(environment const & env, bool collect) {
+    if (collect) {
+        diagnostics d(env.get_diag());
+        if (lean_kernel_diag_is_enabled(d.to_obj_arg())) {
+            m_diag = new diagnostics(d);
+        } else
+            m_diag = nullptr;
+    } else {
+        m_diag = nullptr;
+    }
+}
+
+scoped_diagnostics::~scoped_diagnostics() {
+    if (m_diag)
+        delete m_diag;
+}
+
+environment scoped_diagnostics::update(environment const & env) const {
+    if (m_diag)
+        return env.set_diag(*m_diag);
+    else
+        return env;
+}
 
 environment mk_empty_environment(uint32 trust_lvl) {
     return get_io_result<environment>(lean_mk_empty_environment(trust_lvl, io_mk_world()));
@@ -37,6 +69,14 @@ environment::environment(unsigned trust_lvl):
     object_ref(mk_empty_environment(trust_lvl)) {
 }
 
+diagnostics environment::get_diag() const {
+    return diagnostics(lean_kernel_get_diag(to_obj_arg()));
+}
+
+environment environment::set_diag(diagnostics const & diag) const {
+    return environment(lean_kernel_set_diag(to_obj_arg(), diag.to_obj_arg()));
+}
+
 void environment::set_main_module(name const & n) {
     m_obj = lean_environment_set_main_module(m_obj, n.to_obj_arg());
 }
@@ -118,13 +158,13 @@ static void check_constant_val(environment const & env, constant_val const & v,
     checker.ensure_sort(sort, v.get_type());
 }
 
-static void check_constant_val(environment const & env, constant_val const & v, definition_safety ds) {
-    type_checker checker(env, ds);
+static void check_constant_val(environment const & env, constant_val const & v, diagnostics * diag, definition_safety ds) {
+    type_checker checker(env, diag, ds);
     check_constant_val(env, v, checker);
 }
 
-static void check_constant_val(environment const & env, constant_val const & v, bool safe_only) {
-  check_constant_val(env, v, safe_only ? definition_safety::safe : definition_safety::unsafe);
+static void check_constant_val(environment const & env, constant_val const & v, diagnostics * diag, bool safe_only) {
+    check_constant_val(env, v, diag, safe_only ? definition_safety::safe : definition_safety::unsafe);
 }
 
 void environment::add_core(constant_info const & info) {
@@ -136,48 +176,50 @@ environment environment::add(constant_info const & info) const {
 }
 
 environment environment::add_axiom(declaration const & d, bool check) const {
+    scoped_diagnostics diag(*this, check);
     axiom_val const & v = d.to_axiom_val();
     if (check)
-        check_constant_val(*this, v.to_constant_val(), !d.is_unsafe());
-    return add(constant_info(d));
+        check_constant_val(*this, v.to_constant_val(), diag.get(), !d.is_unsafe());
+    return diag.update(add(constant_info(d)));
 }
 
 environment environment::add_definition(declaration const & d, bool check) const {
+    scoped_diagnostics diag(*this, check);
     definition_val const & v = d.to_definition_val();
     if (v.is_unsafe()) {
         /* Meta definition can be recursive.
            So, we check the header, add, and then type check the body. */
         if (check) {
-            type_checker checker(*this, definition_safety::unsafe);
+            type_checker checker(*this, diag.get(), definition_safety::unsafe);
             check_constant_val(*this, v.to_constant_val(), checker);
         }
         environment new_env = add(constant_info(d));
         if (check) {
-            type_checker checker(new_env, definition_safety::unsafe);
+            type_checker checker(new_env, diag.get(), definition_safety::unsafe);
             check_no_metavar_no_fvar(new_env, v.get_name(), v.get_value());
             expr val_type = checker.check(v.get_value(), v.get_lparams());
             if (!checker.is_def_eq(val_type, v.get_type()))
                 throw definition_type_mismatch_exception(new_env, d, val_type);
         }
-        return new_env;
+        return diag.update(new_env);
     } else {
         if (check) {
-            type_checker checker(*this);
+            type_checker checker(*this, diag.get());
             check_constant_val(*this, v.to_constant_val(), checker);
             check_no_metavar_no_fvar(*this, v.get_name(), v.get_value());
             expr val_type = checker.check(v.get_value(), v.get_lparams());
             if (!checker.is_def_eq(val_type, v.get_type()))
                 throw definition_type_mismatch_exception(*this, d, val_type);
         }
-        return add(constant_info(d));
+        return diag.update(add(constant_info(d)));
     }
 }
 
 environment environment::add_theorem(declaration const & d, bool check) const {
+    scoped_diagnostics diag(*this, check);
     theorem_val const & v = d.to_theorem_val();
     if (check) {
-        // TODO(Leo): we must add support for handling tasks here
-        type_checker checker(*this);
+        type_checker checker(*this, diag.get());
         if (!checker.is_prop(v.get_type()))
             throw theorem_type_is_not_prop(*this, v.get_name(), v.get_type());
         check_constant_val(*this, v.to_constant_val(), checker);
@@ -186,22 +228,24 @@ environment environment::add_theorem(declaration const & d, bool check) const {
         if (!checker.is_def_eq(val_type, v.get_type()))
             throw definition_type_mismatch_exception(*this, d, val_type);
     }
-    return add(constant_info(d));
+    return diag.update(add(constant_info(d)));
 }
 
 environment environment::add_opaque(declaration const & d, bool check) const {
+    scoped_diagnostics diag(*this, check);
     opaque_val const & v = d.to_opaque_val();
     if (check) {
-        type_checker checker(*this);
+        type_checker checker(*this, diag.get());
         check_constant_val(*this, v.to_constant_val(), checker);
         expr val_type = checker.check(v.get_value(), v.get_lparams());
         if (!checker.is_def_eq(val_type, v.get_type()))
             throw definition_type_mismatch_exception(*this, d, val_type);
     }
-    return add(constant_info(d));
+    return diag.update(add(constant_info(d)));
 }
 
 environment environment::add_mutual(declaration const & d, bool check) const {
+    scoped_diagnostics diag(*this, check);
     definition_vals const & vs = d.to_definition_vals();
     if (empty(vs))
         throw kernel_exception(*this, "invalid empty mutual definition");
@@ -210,7 +254,7 @@ environment environment::add_mutual(declaration const & d, bool check) const {
         throw kernel_exception(*this, "invalid mutual definition, declaration is not tagged as unsafe/partial");
     /* Check declarations header */
     if (check) {
-        type_checker checker(*this, safety);
+        type_checker checker(*this, diag.get(), safety);
         for (definition_val const & v : vs) {
             if (v.get_safety() != safety)
                 throw kernel_exception(*this, "invalid mutual definition, declarations must have the same safety annotation");
@@ -224,7 +268,7 @@ environment environment::add_mutual(declaration const & d, bool check) const {
     }
     /* Check actual definitions */
     if (check) {
-        type_checker checker(new_env, safety);
+        type_checker checker(new_env, diag.get(), safety);
         for (definition_val const & v : vs) {
             check_no_metavar_no_fvar(new_env, v.get_name(), v.get_value());
             expr val_type = checker.check(v.get_value(), v.get_lparams());
@@ -232,7 +276,7 @@ environment environment::add_mutual(declaration const & d, bool check) const {
                 throw definition_type_mismatch_exception(new_env, d, val_type);
         }
     }
-    return new_env;
+    return diag.update(new_env);
 }
 
 environment environment::add(declaration const & d, bool check) const {

src/kernel/environment.h

@@ -29,6 +29,36 @@ public:
     virtual ~environment_extension() {}
 };
 
+/* Wrapper for `Kernel.Diagnostics` */
+class diagnostics : public object_ref {
+public:
+    diagnostics(diagnostics const & other):object_ref(other) {}
+    diagnostics(diagnostics && other):object_ref(other) {}
+    explicit diagnostics(b_obj_arg o, bool b):object_ref(o, b) {}
+    explicit diagnostics(obj_arg o):object_ref(o) {}
+    ~diagnostics() {}
+    void record_unfold(name const & decl_name);
+};
+
+/*
+Store `Kernel.Diagnostics` stored in environment extension in `m_diag` IF
+- `Kernel.Diagnostics.enable = true`
+- `collect = true`. This is a minor optimization.
+
+We use this class to ensure we don't waste time collecting information
+that was not requested.
+*/
+class scoped_diagnostics {
+    diagnostics * m_diag;
+public:
+    scoped_diagnostics(environment const & env, bool collect);
+    scoped_diagnostics(scoped_diagnostics const &) = delete;
+    scoped_diagnostics(scoped_diagnostics &&) = delete;
+    ~scoped_diagnostics();
+    environment update(environment const &) const;
+    diagnostics * get() const { return m_diag; }
+};
+
 class environment : public object_ref {
     friend class add_inductive_fn;
 
@@ -56,6 +86,9 @@ public:
     environment & operator=(environment const & other) { object_ref::operator=(other); return *this; }
     environment & operator=(environment && other) { object_ref::operator=(other); return *this; }
 
+    diagnostics get_diag() const;
+    environment set_diag(diagnostics const & diag) const;
+
     /** \brief Return the trust level of this environment. */
     unsigned trust_lvl() const;
 

src/kernel/inductive.cpp

@@ -124,6 +124,7 @@ optional<recursor_rule> get_rec_rule_for(recursor_val const & rec_val, expr cons
 class add_inductive_fn {
     environment            m_env;
     name_generator         m_ngen;
+    diagnostics *          m_diag;
     local_ctx              m_lctx;
     names      m_lparams;
     unsigned               m_nparams;
@@ -158,8 +159,8 @@ class add_inductive_fn {
     buffer<rec_info>       m_rec_infos;
 
 public:
-    add_inductive_fn(environment const & env, inductive_decl const & decl, bool is_nested):
-        m_env(env), m_ngen(*g_ind_fresh), m_lparams(decl.get_lparams()), m_is_unsafe(decl.is_unsafe()),
+    add_inductive_fn(environment const & env, diagnostics * diag, inductive_decl const & decl, bool is_nested):
+        m_env(env), m_ngen(*g_ind_fresh), m_diag(diag), m_lparams(decl.get_lparams()), m_is_unsafe(decl.is_unsafe()),
         m_is_nested(is_nested) {
         if (!decl.get_nparams().is_small())
             throw kernel_exception(env, "invalid inductive datatype, number of parameters is too big");
@@ -167,7 +168,7 @@ public:
         to_buffer(decl.get_types(), m_ind_types);
     }
 
-    type_checker tc() { return type_checker(m_env, m_lctx, m_is_unsafe ? definition_safety::unsafe : definition_safety::safe); }
+    type_checker tc() { return type_checker(m_env, m_lctx, m_diag, m_is_unsafe ? definition_safety::unsafe : definition_safety::safe); }
 
     /** Return type of the parameter at position `i` */
     expr get_param_type(unsigned i) const {
@@ -1112,10 +1113,11 @@ static pair<names, name_map<name>> mk_aux_rec_name_map(environment const & aux_e
 environment environment::add_inductive(declaration const & d) const {
     elim_nested_inductive_result res = elim_nested_inductive_fn(*this, d)();
     bool is_nested = !res.m_aux2nested.empty();
-    environment aux_env = add_inductive_fn(*this, inductive_decl(res.m_aux_decl), is_nested)();
+    scoped_diagnostics diag(*this, true);
+    environment aux_env = add_inductive_fn(*this, diag.get(), inductive_decl(res.m_aux_decl), is_nested)();
     if (!is_nested) {
         /* `d` did not contain nested inductive types. */
-        return aux_env;
+        return diag.update(aux_env);
     } else {
         /* Restore nested inductives. */
         inductive_decl ind_d(d);
@@ -1170,7 +1172,7 @@ environment environment::add_inductive(declaration const & d) const {
         for (name const & aux_rec : aux_rec_names) {
             process_rec(aux_rec);
         }
-        return new_env;
+        return diag.update(new_env);
     }
 }
 

src/kernel/type_checker.cpp

@@ -477,6 +477,11 @@ expr type_checker::whnf_core(expr const & e, bool cheap_rec, bool cheap_proj) {
                           cheap_rec, cheap_proj);
         } else if (f == f0) {
             if (auto r = reduce_recursor(e, cheap_rec, cheap_proj)) {
+                if (m_diag) {
+                    auto f = get_app_fn(e);
+                    if (is_constant(f))
+                        m_diag->record_unfold(const_name(f));
+                }
                 /* iota-reduction and quotient reduction rules */
                 return whnf_core(*r, cheap_rec, cheap_proj);
             } else {
@@ -513,8 +518,12 @@ optional<constant_info> type_checker::is_delta(expr const & e) const {
 optional<expr> type_checker::unfold_definition_core(expr const & e) {
     if (is_constant(e)) {
         if (auto d = is_delta(e)) {
-            if (length(const_levels(e)) == d->get_num_lparams())
+            if (length(const_levels(e)) == d->get_num_lparams()) {
+                if (m_diag) {
+                    m_diag->record_unfold(d->get_name());
+                }
                 return some_expr(instantiate_value_lparams(*d, const_levels(e)));
+            }
         }
     }
     return none_expr();
@@ -1148,18 +1157,18 @@ expr type_checker::eta_expand(expr const & e) {
     return m_lctx.mk_lambda(fvars, r);
 }
 
-type_checker::type_checker(environment const & env, local_ctx const & lctx, definition_safety ds):
-    m_st_owner(true), m_st(new state(env)),
+type_checker::type_checker(environment const & env, local_ctx const & lctx, diagnostics * diag, definition_safety ds):
+    m_st_owner(true), m_st(new state(env)), m_diag(diag),
     m_lctx(lctx), m_definition_safety(ds), m_lparams(nullptr) {
 }
 
 type_checker::type_checker(state & st, local_ctx const & lctx, definition_safety ds):
-    m_st_owner(false), m_st(&st), m_lctx(lctx),
+    m_st_owner(false), m_st(&st), m_diag(nullptr), m_lctx(lctx),
     m_definition_safety(ds), m_lparams(nullptr) {
 }
 
 type_checker::type_checker(type_checker && src):
-    m_st_owner(src.m_st_owner), m_st(src.m_st), m_lctx(std::move(src.m_lctx)),
+    m_st_owner(src.m_st_owner), m_st(src.m_st), m_diag(src.m_diag), m_lctx(std::move(src.m_lctx)),
     m_definition_safety(src.m_definition_safety), m_lparams(src.m_lparams) {
     src.m_st_owner = false;
 }

src/kernel/type_checker.h

@@ -42,6 +42,7 @@ public:
 private:
     bool                      m_st_owner;
     state *                   m_st;
+    diagnostics *             m_diag;
     local_ctx                 m_lctx;
     definition_safety         m_definition_safety;
     /* When `m_lparams != nullptr, the `check` method makes sure all level parameters
@@ -104,8 +105,8 @@ private:
 public:
     type_checker(state & st, local_ctx const & lctx, definition_safety ds = definition_safety::safe);
     type_checker(state & st, definition_safety ds = definition_safety::safe):type_checker(st, local_ctx(), ds) {}
-    type_checker(environment const & env, local_ctx const & lctx, definition_safety ds = definition_safety::safe);
-    type_checker(environment const & env, definition_safety ds = definition_safety::safe):type_checker(env, local_ctx(), ds) {}
+    type_checker(environment const & env, local_ctx const & lctx, diagnostics * diag = nullptr, definition_safety ds = definition_safety::safe);
+    type_checker(environment const & env, diagnostics * diag = nullptr, definition_safety ds = definition_safety::safe):type_checker(env, local_ctx(), diag, ds) {}
     type_checker(type_checker &&);
     type_checker(type_checker const &) = delete;
     ~type_checker();

tests/lean/run/ack.lean

@@ -3,3 +3,32 @@ def ack : Nat → Nat → Nat
   | x+1, 0   => ack x 1
   | x+1, y+1 => ack x (ack (x+1) y)
 termination_by a b => (a, b)
+
+/--
+info: [reduction] unfolded declarations (max: 1725, num: 4):
+    Nat.rec ↦ 1725
+  ⏎
+  Eq.rec ↦ 1114
+  ⏎
+  Acc.rec ↦ 1050
+  ⏎
+  PSigma.rec ↦ 513[reduction] unfolded reducible declarations (max: 1577, num: 3):
+    Nat.casesOn ↦ 1577
+  ⏎
+  Eq.ndrec ↦ 984
+  ⏎
+  PSigma.casesOn ↦ 513[kernel] unfolded declarations (max: 1193, num: 5):
+    Nat.casesOn ↦ 1193
+  ⏎
+  Nat.rec ↦ 1065
+  ⏎
+  Eq.ndrec ↦ 973
+  ⏎
+  Eq.rec ↦ 973
+   Acc.rec ↦ 754use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+-/
+#guard_msgs in
+set_option diagnostics.threshold 500 in
+set_option diagnostics true in
+theorem ex : ack 3 2 = 29 :=
+  rfl