Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC