Zulip Chat Archive

Stream: general

Topic: doc_blame


view this post on Zulip Johan Commelin (Oct 04 2019 at 11:19):

I don't know if this has been reported before, but #doc_blame asks me to give docstrings for the projection foo.to_bar if I define a class foo that extends bar. Since this projection is auto-generated, it is quite hard and unnatural to document it. Is there a solution for this?

view this post on Zulip Rob Lewis (Oct 04 2019 at 12:13):

Doc blame is pretty rudimentary. This is probably fixable but I wouldn't expect it to happen in the near future.

view this post on Zulip Floris van Doorn (Oct 04 2019 at 14:21):

This seems like a omission of is_auto_generated. I'm surprised that these kinds of declarations haven't showed up in #sanity_check (some checks do omit all instances, so that might be the reason).

view this post on Zulip Floris van Doorn (Oct 04 2019 at 14:21):

I'll see if I can fix it, but I don't know if there is a good way to automatically find out that this declaration has been automatically generated.

view this post on Zulip Johan Commelin (Oct 04 2019 at 14:26):

And thanks again.

view this post on Zulip Johan Commelin (Oct 04 2019 at 14:32):

It would be good if #doc_blame could have some more fine-grained options. For example, I want it to nag me about definitions without docstrings, and missing module docstrings, but not about [simp]-lemmas that don't have a docstring.

view this post on Zulip Johan Commelin (Oct 04 2019 at 14:33):

At the moment it is either "nag about everything" or "nag about def'ns only"

view this post on Zulip Johan Commelin (Oct 04 2019 at 14:33):

And once again: @Rob Lewis Thanks a lot for writing these tools in the first place. Don't feel pressed to work on these feature requests.

view this post on Zulip Johan Commelin (Oct 04 2019 at 18:10):

The fact where #doc_blame is reporting projections as undocumented seems to be linked to whether the old_structure_cmd is true or not. I only see the behaviour when it is true...


Last updated: May 08 2021 at 18:17 UTC