doc_blame

Stream: general

[Johan Commelin]

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?

[Rob Lewis]

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

[Floris van Doorn]

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).

[Floris van Doorn]

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.

[Johan Commelin]

And thanks again.

[Johan Commelin]

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.

[Johan Commelin]

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

[Johan Commelin]

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.

[Johan Commelin]

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...