help with Kerodon tags

Stream: Infinity-Cosmos

[Emily Riehl]

I imagine it would be helpful to folks if we started including Kerodon tags when appropriate but I'm not entirely sure where --- in the Lean code, in the Blueprint? If someone wants to add one or two and show me how it's done that would be great.

[Matthew Ballard]

@Damiano Testa recently implemented Stacks protect tags (see file#Mathlib/Tactic/StacksAttribute) Kerodon should be copy/paste.

[Damiano Testa]

As Matt says: it should be entirely analogous. I won't have time to do it now, as I'm about to have dinner, but I can look into it tomorrow, if no one else wants to try it out.

[Matthew Ballard]

The syntax for the tags themselves is the same so one can reuse the tag parser and just declare

syntax (name := keredon) "keredon " stacksTag ...

[Damiano Testa]

In the interest of simplifying maintainability, I would prefer to avoid copy-pasting too much.

What do you think of adding a field to the docs#Mathlib.Stacks.Tag to disambiguate which project it refers to (Stacks or Kerodon, though maybe the extra field could simply be a String, in case later on some other tag-based project comes along) and then simply define two attributes that increment the relevant project tag and the final tallying commands that retrieve as appropriate?

[Damiano Testa]

(In this case, I would also rename Mathlib.Stacks.Tag to some more generic name, such as Mathlib.Project.Tags or something like it.)

[Matthew Ballard]

#16643 -- feel free to take over. I am done for the day most likely

[Damiano Testa]

Ah, great! I've seen that you've already taken an approach similar to what I mentioned! I won't work on this soon either: it is bedtime here! I may push something tomorrow morning, though.

[Kim Morrison]

I switched the spelling, changed some doc-strings to be more database-generic (but left "Stacks" in most declaration names, I think it's actually more helpful to a reader than something generic, and Kerodon users will understand!), and added some missing doc-strings that were failing CI.

[Kim Morrison]

I also imported it right where we define a category, so anything downstream of that has automatic access.

[Damiano Testa]

I have also added some modifications:

• updated shake,
• I re-opened a namespace (which meant slightly modifying two names whose previous names looked like oversights),
• added a test for #kerodon_tags!.

Other than that, looks good to me!