Zulip Chat Archive

Stream: general

Topic: doc_blame!


view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 02 2019 at 14:24):

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

view this post on Zulip Sebastien Gouezel (Sep 02 2019 at 14:48):

Just played with sanity_check. This is amazing!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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