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
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):
Last updated: May 14 2021 at 07:19 UTC