leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
3.82k stars 325 forks source link

feat: collect kernel diagnostic information #4082

Closed leodemoura closed 1 week ago

leodemoura commented 1 week ago

We now also track which declarations have been unfolded by the kernel when using

set_option diagnostics true
leanprover-community-mathlib4-bot commented 1 week ago

Mathlib CI status (docs):