## Stream: general

### Topic: doc_blame!

#### Johan Commelin (Sep 02 2019 at 14:23):

@Rob Lewis Thanks for writing this tool! We are now using it (and sanity_check, thanks @Floris van Doorn) in the perfectoid project.
I saw that #doc_blame! is also reporting things like

is_ring_of_integral_elements.drec_on
is_ring_of_integral_elements.drec


That is probably not intended. It isn't too annoying, but just letting you know... if you have time to work on it sometime soon.

#### Johan Commelin (Sep 02 2019 at 14:24):

Ooh, and if you define a structure, it wants you to document all the fields

#### Sebastien Gouezel (Sep 02 2019 at 14:48):

Just played with sanity_check. This is amazing!

#### Floris van Doorn (Sep 02 2019 at 18:10):

@Rob Lewis I recently wrote is_auto_generated which is a more systematic version of the one used in doc_blame. You might want to use that one.

#### Rob Lewis (Sep 03 2019 at 18:58):

For the record, doc_blame is mostly thanks to @Patrick Massot . I'm just getting back online and still mostly on vacation until ITP starts. But if Patrick doesn't do it before then I'll fix this during a talk.

#### Patrick Massot (Sep 03 2019 at 20:43):

https://github.com/leanprover-community/mathlib/pull/1395

Last updated: May 14 2021 at 07:19 UTC