Conversation
PR summary 9ce2e31b74
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Tactic | 2168 | 2170 | +2 (+0.09%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Tactic.StacksAttribute |
1 |
Mathlib.Tactic |
2 |
Declarations diff
No declarations were harmed in the making of this PR! 🐙
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
Mathlib/Tactic/StacksAttribute.lean
Outdated
| descr := "Apply a Stacks project tag to a theorem." | ||
| add := fun _decl stx _attrKind => Lean.withRef stx do | ||
| match stx with | ||
| | `(attr| stacks $_:stackTags $_:str) => return |
There was a problem hiding this comment.
Can we validate the stackTag here?
There was a problem hiding this comment.
I just added a check that there are no spaces in the tag itself. By "validate" you mean "make sure that such a tag exists"? That should probably be done by a linter, right?
There was a problem hiding this comment.
Sorry. Something like
syntax num | lit : stacksTagAtom
syntax stacksAtom stacksAtom stacksAtom stacksAtom stacksAtom : stacksTagIs there some uppercase Latin character syntax category? Do we really have to write out stacksAtom 5 times?
There was a problem hiding this comment.
Oh, the length 5 check can be done with the substring and also the uppercase check.
There was a problem hiding this comment.
I don't know if there is any benefit to building into the syntax category itself vs converting to a string and using its methods. Maybe the latter can throw a more informative error? I'll let you decide.
There was a problem hiding this comment.
I have a slight preference for not using the double quotes, which a str would want. If there is a way of parsing a string without quotes, then I would probably prefer that!
|
For the environment extension, do we want to store anything more than a map from the declaration name to the stacks tag as a string? |
For the moment, I think probably not. Maybe in the future we may want to add something else. In the future, I think that also making sure that the tags do exist would be a good check, but I would leave that for a follow up PR. |
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
|
The "other" PR is getting merged, so I'll close this one. Thank you all for your comments: they are part of the other PR anyway! |
This extends the simple attribute of #16179 with an environment extension that tracks also the declaration names and tags. The `#stacks_tags` command 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. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/stacks.20tags)
This extends the simple attribute of #16179 with an environment extension that tracks also the declaration names and tags. The `#stacks_tags` command 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. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/stacks.20tags)
This extends the simple attribute of #16179 with an environment extension that tracks also the declaration names and tags. The `#stacks_tags` command 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. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/stacks.20tags)
This extends the simple attribute of #16179 with an environment extension that tracks also the declaration names and tags. The `#stacks_tags` command 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. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/stacks.20tags)
This PR contains a subset of the code of #16191 and is probably not going to be merged.
Zulip thread