linter doc_blame with old_structure_cmd

Stream: general

[Oliver Nash]

The following snippet triggers the "missing doc string" complaint from the linter:

set_option old_structure_cmd true

/-- Foo structure -/
structure foo := (x : ℕ)

/-- Bar structure -/
structure bar extends foo := (y : ℕ)

#lint -- #print bar.to_foo /- def missing doc string -/

[Kenny Lau]

then don't use old_structure_cmd

[Oliver Nash]

I note that even though Lean automatically created bar.to_foo regardless of whether I'm using the old_structure_cmd, it is only when this option is true (as above) that the linter complains.

[Mario Carneiro]

well it's not wrong

[Oliver Nash]

@Kenny Lau Oh really? It's much more convenient in some situations I think. I'd be happy to be corrected!

[Kenny Lau]

I was referring to the old joke "Doctor I feel painful when I breathe; doctor: then don't breathe"

[Mario Carneiro]

I would hate for this to be the reason you choose one method over the other

[Oliver Nash]

I had scanned some old threads here before deciding to use it and I thought the current wisdom was that it's fine to use it, and even that the name is a bit of a misnomer but really I'm far from sure.

[Oliver Nash]

@Kenny Lau Ah I see. :laughing:

[Oliver Nash]

@Mario Carneiro Noted, thanks. Perhaps I'll add an appropriate nolint statement and allow the advice to flow in the code review.

[Oliver Nash]

Thank you both.

[Mario Carneiro]

you can also document it

[Mario Carneiro]

there is a command like add_doc_string for adding doc strings to automatic definitions

[Rob Lewis]

The linter generally ignores auto-generated stuff but I guess this doesn't get flagged as auto-generated.

[Gabriel Ebner]

It's called add_decl_doc.

[Oliver Nash]

OK thanks. It feels a bit funny to have to add a doc string to an auto-generated function but I am still glad to learn about add_decl_doc.

[Kevin Buzzard]

You're right that the name is terrible. It implies it's deprecated, whereas in fact for part of the structure heirarchy it's exactly what we want.

[Mario Carneiro]

PR?

[Mario Carneiro]

How about flat_structure instead

[Oliver Nash]

I literally just created one here: https://github.com/leanprover-community/mathlib/pull/2404

[Oliver Nash]

(I'm currently scanning it to make sure I haven't done anything stupid before I request review.)

[Oliver Nash]

I have not previously seen flat_structure. I'd love to learn about it. I just grepped the Mathlib source but didn't find it anywhere!

[Mario Carneiro]

I just made the name up

[Mario Carneiro]

as an alternative to old_structure_cmd which has wrong connotations

[Oliver Nash]

Oh I see: my comment about the possible misnomer. Yeah, flat_structure is nice

[Oliver Nash]

I'd vote for that over old_structure_cmd for sure.