feat: improve @[deprecated] attr #3968
Conversation
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
|
Thanks. Could you add two tests for |
|
I've pulled #3967 off the queue and will update it once this is in. |
|
The manual is failing and I have no idea how to track down errors in that build step... |
|
@Kha It appears that alectryon is failing because it misses a bug fix not present on the lean4 fork of alectryon. (There is likely another error behind this one, but the one shown in the log seems to be this issue.) |
|
Can we somehow survive for a little longer without touching Alectryon? |
|
Could there be some documentation for how to build the manual (without nix)? All I see is some nix stuff I don't understand and a broken error message due to a bug in an abandoned dependency. I don't even know what sources are being built, it's loading some SHAs from the nix cache? |
| -/ | ||
| syntax (name := deprecated) "deprecated" (ppSpace ident)? : attr | ||
| syntax (name := deprecated) "deprecated" (ppSpace ident)? (ppSpace str)? | ||
| (" (" &"since" " := " str ")")? : attr |
There was a problem hiding this comment.
Can you declare since as a separate syntax so that it gets its own docstring (which can recommend the date format)
There was a problem hiding this comment.
I think it is better to have this documentation on deprecated, because otherwise people won't necessarily know that the clause exists in the first place. The example in deprecated gives at least a bare hint of what the date format should be.
Let's please just fix all deprecation warnings in ICERM2022/ctor.lean and then document everything about the manual when it's redone in Verso |
How did you manage to deduce that this was the problem? That was the issue I was having, the error message is completely opaque. I'm not idly asking for improvements to the manual, I literally don't know how to track down errors in this build step. I understand that this code is on life support but it's still a required build job, so it is important that we can at least fix issues which cause it to fail. Otherwise it should just be removed from the build? |
digama0
force-pushed
the
deprecated_since
branch
from
f8df940 to
ef051fa
Compare
- consistently use the YYYY-MM-DD format - when easily possible, put the date on the same line as the `deprecated` attribute - when easily possible, format the entire declaration on the same line Why these changes? - consistency makes it easier for tools to parse this information - compactness: I don't see a good reason for these declarations taking up more space than needed; as I understand it, deprecated lemmas are not supposed to be used in mathlib anyway - putting the date on the same line as the attribute makes it easier to discover un-dated deprecations; they also ease writing a tool to replace these by a machine-readable version using leanprover/lean4#3968
|
My bad, I thought the line I quoted would clarify how I found it but I guess it's still pretty opaque. If you look at the failing log (which I can't see anymore because of the rebase), you will see that Nix store path I quoted mentioned. If you ignore the hash and file system parts, the relevant part is
If it continues to be an issue, we should just downgrade these examples to basic non-interactive code blocks, yes. But this was the first (perplexing) failure in that part for a long while. |
Occasionally, remove a "deprecated by" or "deprecated since", to fit the line length. This is desirable (to me) because - it's more compact: I don't see a good reason for these declarations taking up more space than needed; as I understand it, deprecated lemmas are not supposed to be used in mathlib anyway - putting the date on the same line as the attribute makes it easier to discover un-dated deprecations; they also ease writing a tool to replace these by a machine-readable version using leanprover/lean4#3968
Yes, I don't understand this either. It does appear that the deprecations are responsible, in the sense that removing the deprecated uses fixed the build, but the code here doesn't touch deprecation reporting at all, and that file contains no deprecated attributes. My best guess is that there are some stage0 shenanigans going on whereby the lean compiler is either reading a deprecation with the wrong syntax or reading an olean deprecation entry as the old type or vice versa, resulting in a failure of the deprecation linter to report errors correctly. |
- consistently use the YYYY-MM-DD format - when easily possible, put the date on the same line as the `deprecated` attribute - when easily possible, format the entire declaration on the same line Why these changes? - consistency makes it easier for tools to parse this information - compactness: I don't see a good reason for these declarations taking up more space than needed; as I understand it, deprecated lemmas are not supposed to be used in mathlib anyway - putting the date on the same line as the attribute makes it easier to discover un-dated deprecations; they also ease writing a tool to replace these by a machine-readable version using leanprover/lean4#3968
Occasionally, remove a "deprecated by" or "deprecated since", to fit the line length. This is desirable (to me) because - it's more compact: I don't see a good reason for these declarations taking up more space than needed; as I understand it, deprecated lemmas are not supposed to be used in mathlib anyway - putting the date on the same line as the attribute makes it easier to discover un-dated deprecations; they also ease writing a tool to replace these by a machine-readable version using leanprover/lean4#3968
- consistently use the YYYY-MM-DD format - when easily possible, put the date on the same line as the `deprecated` attribute - when easily possible, format the entire declaration on the same line Why these changes? - consistency makes it easier for tools to parse this information - compactness: I don't see a good reason for these declarations taking up more space than needed; as I understand it, deprecated lemmas are not supposed to be used in mathlib anyway - putting the date on the same line as the attribute makes it easier to discover un-dated deprecations; they also ease writing a tool to replace these by a machine-readable version using leanprover/lean4#3968
Occasionally, remove a "deprecated by" or "deprecated since", to fit the line length. This is desirable (to me) because - it's more compact: I don't see a good reason for these declarations taking up more space than needed; as I understand it, deprecated lemmas are not supposed to be used in mathlib anyway - putting the date on the same line as the attribute makes it easier to discover un-dated deprecations; they also ease writing a tool to replace these by a machine-readable version using leanprover/lean4#3968
Complement to #3967 , adds a
(since := "<date>")field to@[deprecated]so that metaprogramming code has access to the deprecation date for e.g. bulk removals. Also adds@[deprecated "deprecation message"]to optionally replace the default text "{declName}has been deprecated, use{newName}instead".