The stacks and kerodon attributes

This allows tagging of mathlib results with the corresponding tags from the Stacks Project and Kerodon.

While the Stacks Project is the main focus, because the tag format at Kerodon is compatible, the attribute can be used to tag results with Kerodon tags as well.

inductive Mathlib.StacksTag.Database : Type

Web database users of projects tags

• kerodon : Database
• stacks : Database

@[implicit_reducible]

instance Mathlib.StacksTag.instBEqDatabase : BEq Database

def Mathlib.StacksTag.instBEqDatabase.beq : Database → Database → Bool

@[implicit_reducible]

instance Mathlib.StacksTag.instHashableDatabase : Hashable Database

def Mathlib.StacksTag.instHashableDatabase.hash : Database → UInt64

structure Mathlib.StacksTag.Tag : Type

Tag is the structure that carries the data of a project tag and a corresponding Mathlib declaration.

• declName : Lean.Name

  The name of the declaration with the given tag.

• database : Database

  The online database where the tag is found.

• tag : String

  The database tag.

• comment : String

  The (optional) comment that comes with the given tag.

def Mathlib.StacksTag.instBEqTag.beq : Tag → Tag → Bool

@[implicit_reducible]

instance Mathlib.StacksTag.instBEqTag : BEq Tag

@[implicit_reducible]

instance Mathlib.StacksTag.instHashableTag : Hashable Tag

def Mathlib.StacksTag.instHashableTag.hash : Tag → UInt64

opaque Mathlib.StacksTag.tagExt : Lean.SimplePersistentEnvExtension Tag (Array (Array Tag))

Defines the tagExt extension for storing all Tags in the environment. addImportedFn is a constant function to avoid a performance overhead during initialization.

def Mathlib.StacksTag.addTagEntry {m : Type → Type} [Lean.MonadEnv m] (declName : Lean.Name) (db : Database) (tag comment : String) : m Unit

addTagEntry declName tag comment takes as input the Name declName of a declaration and the Strings tag and comment of the stacks attribute. It extends the Tag environment extension with the data declName, tag, comment.

@[reducible, inline]

abbrev Mathlib.StacksTag.stacksTagKind : Lean.SyntaxNodeKind

stacksTag is the node kind of Stacks Project Tags: a sequence of digits and uppercase letters.

def Mathlib.StacksTag.stacksTagFn : Lean.Parser.ParserFn

The main parser for Stacks Project Tags: it accepts any sequence of 4 digits or uppercase letters.

def Mathlib.StacksTag.stacksTagNoAntiquot : Lean.Parser.Parser

The main parser for Stacks Project Tags: it accepts any sequence of 4 digits or uppercase letters.

def Mathlib.StacksTag.stacksTagParser : Lean.Parser.Parser

The main parser for Stacks Project Tags: it accepts any sequence of 4 digits or uppercase letters.

def Lean.TSyntax.getStacksTag (stx : TSyntax Mathlib.StacksTag.stacksTagKind) : CoreM String

Extract the underlying tag as a string from a stacksTag node.

def Lean.PrettyPrinter.Formatter.stacksTagNoAntiquot.formatter : Formatter

The formatter for Stacks Project Tags syntax.

def Lean.PrettyPrinter.Parenthesizer.stacksTagAntiquot.parenthesizer : Parenthesizer

The parenthesizer for Stacks Project Tags syntax.

def Mathlib.StacksTag.stacksTagDB.quot : Lean.ParserDescr

def Lean.Parser.Category.stacksTagDB : Category

The syntax category for the database name.

def Mathlib.StacksTag.stacksTagDBKerodon : Lean.ParserDescr

The syntax for a "kerodon" database identifier in a @[kerodon] attribute.

def Mathlib.StacksTag.stacksTagDBStacks : Lean.ParserDescr

The syntax for a "stacks" database identifier in a @[stacks] attribute.

def Mathlib.StacksTag.stacksTag : Lean.ParserDescr

The stacksTag attribute. Use it as @[kerodon TAG "Optional comment"] or @[stacks TAG "Optional comment"] depending on the database you are referencing.

The TAG is mandatory and should be a sequence of 4 digits or uppercase letters.

See the Tags page in the Stacks project or Tags page in the Kerodon project for more details.

def Mathlib.StacksTag.traceStacksTags (db : Database) (verbose : Bool := false) : Lean.Elab.Command.CommandElabM Unit

traceStacksTags db verbose prints the tags of the database db to the user and inlines the theorem statements if verbose is true.

def Mathlib.StacksTag.stacksTags : Lean.ParserDescr

#stacks_tags retrieves all declarations that have the stacks attribute.

For each found declaration, it prints a line

'declaration_name' corresponds to tag 'declaration_tag'.

The variant #stacks_tags! also adds the theorem statement after each summary line.

def Mathlib.StacksTag.kerodonTags : Lean.ParserDescr

The #kerodon_tags command retrieves all declarations that have the kerodon attribute.

For each found declaration, it prints a line

'declaration_name' corresponds to tag 'declaration_tag'.

The variant #kerodon_tags! also adds the theorem statement after each summary line.