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

source
inductive Mathlib.StacksTag.Database :
Type

Web database users of projects tags

- kerodon : Database
- stacks : Database

Instances For

source
instance Mathlib.StacksTag.instBEqDatabase :
BEq Database
Equations

- Mathlib.StacksTag.instBEqDatabase = { beq := Mathlib.StacksTag.instBEqDatabase.beq }

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

- Mathlib.StacksTag.instBEqDatabase.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

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

- Mathlib.StacksTag.instHashableDatabase.hash Mathlib.StacksTag.Database.kerodon = 0
- Mathlib.StacksTag.instHashableDatabase.hash Mathlib.StacksTag.Database.stacks = 1

Instances For

source
instance Mathlib.StacksTag.instHashableDatabase :
Hashable Database
Equations

- Mathlib.StacksTag.instHashableDatabase = { hash := Mathlib.StacksTag.instHashableDatabase.hash }

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

Instances For

source
instance Mathlib.StacksTag.instBEqTag :
BEq Tag
Equations

- Mathlib.StacksTag.instBEqTag = { beq := Mathlib.StacksTag.instBEqTag.beq }

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

- One or more equations did not get rendered due to their size.
- Mathlib.StacksTag.instBEqTag.beq x✝¹ x✝ = false

Instances For

source
instance Mathlib.StacksTag.instHashableTag :
Hashable Tag
Equations

- Mathlib.StacksTag.instHashableTag = { hash := Mathlib.StacksTag.instHashableTag.hash }

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

- Mathlib.StacksTag.instHashableTag.hash { declName := a, database := a_1, tag := a_2, comment := a_3 } = mixHash (mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)) (hash a_3)

Instances For

source
opaque Mathlib.StacksTag.tagExt :
Lean.SimplePersistentEnvExtension Tag (Std.HashSet Tag)

Defines the `tagExt` extension for adding a `HashSet` of `Tag`s to the environment.

source
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 `String`s `tag` and `comment` of the `stacks` attribute. It extends the `Tag` environment extension with the data `declName, tag, comment`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[reducible, inline]
abbrev Mathlib.StacksTag.stacksTagKind :
Lean.SyntaxNodeKind

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

Equations

- Mathlib.StacksTag.stacksTagKind = `stacksTag

Instances For

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

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

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

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

Equations

- Mathlib.StacksTag.stacksTagNoAntiquot = { info := Lean.Parser.mkAtomicInfo "stacksTag", fn := Mathlib.StacksTag.stacksTagFn }

Instances For

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

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

Equations

- Mathlib.StacksTag.stacksTagParser = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "stacksTag" Mathlib.StacksTag.stacksTagKind) Mathlib.StacksTag.stacksTagNoAntiquot

Instances For

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

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

Equations

- stx.getStacksTag = match Lean.Syntax.isLit? Mathlib.StacksTag.stacksTagKind stx.raw with | some val => pure val | x => Lean.throwError (Lean.toMessageData "Malformed Stacks tag")

Instances For

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

The formatter for Stacks Project Tags syntax.

Equations

- Lean.PrettyPrinter.Formatter.stacksTagNoAntiquot.formatter = Lean.PrettyPrinter.Formatter.visitAtom Mathlib.StacksTag.stacksTagKind

Instances For

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

The parenthesizer for Stacks Project Tags syntax.

Equations

- Lean.PrettyPrinter.Parenthesizer.stacksTagAntiquot.parenthesizer = Lean.PrettyPrinter.Parenthesizer.visitToken

Instances For

source
def Lean.Parser.Category.stacksTagDB :
Category

The syntax category for the database name.

Equations

- Lean.Parser.Category.stacksTagDB = { }

Instances For

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

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.StacksTag.stacksTagDBKerodon :
Lean.ParserDescr

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

Equations

- Mathlib.StacksTag.stacksTagDBKerodon = Lean.ParserDescr.node `Mathlib.StacksTag.stacksTagDBKerodon 1024 (Lean.ParserDescr.symbol "kerodon")

Instances For

source
def Mathlib.StacksTag.stacksTagDBStacks :
Lean.ParserDescr

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

Equations

- Mathlib.StacksTag.stacksTagDBStacks = Lean.ParserDescr.node `Mathlib.StacksTag.stacksTagDBStacks 1024 (Lean.ParserDescr.symbol "stacks")

Instances For

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

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

Equations

- One or more equations did not get rendered due to their size.

Instances For