Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Style: Add Deprecation sub-section #604

Open
wants to merge 2 commits into
base: lean4
Choose a base branch
from
Open

Style: Add Deprecation sub-section #604

Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
b6ad330
Style: Add Deprecation sub-section
vlad902 Mar 10, 2025
5ab413a
Update templates/contribute/style.md
vlad902 Mar 11, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 25 additions & 1 deletion templates/contribute/style.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -553,7 +553,7 @@ on the direction we want) while the other conversion is more lengthy, we use `hn
*conclusions* of theorems (as this is the more powerful result to use).
A common usage of this rule is with naturals, where `⊥ = 0`.

## Comments
### Comments

Use module doc delimiters `/-! -/` to provide section headers and
separators since these get incorporated into the auto-generated docs,
Expand All @@ -565,3 +565,27 @@ Documentation strings for declarations are delimited with `/-- -/`.

See our [documentation requirements](doc.html) for more suggestions
and examples.

### Deprecation

Deleting, renaming, or changing theorem definitions can cause downstreams projects
that rely on these definitions to fail to compile. Any publicly exposed theorem
definitions that are being changed should be gracefully transitioned by keeping the
Comment on lines +572 to +573
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
that rely on these definitions to fail to compile. Any publicly exposed theorem
definitions that are being changed should be gracefully transitioned by keeping the
that rely on these definitions to fail to compile. Any publicly exposed theorem and
definitions that are being changed should be gracefully transitioned by keeping the

"change" is maybe a bit ambiguous: if I weaken an assumption? Or change an implicit variable to explicit, etc...

If the name doesn't change, it is also hard to use the deprecated attribute.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's a good point. I've updated the wording to say:

Any publicly exposed theorems and definitions that are being removed should be ...

old theorem statement with a `@[deprecated]` attribute, to warn downstream projects to
transition away from deprecated definitions before they are deleted. Renamed theorems
can use a deprecated `alias` to the new name, while in cases where the theorem is not
being replaced, the deprecated theorem definition can be marked with an attribute, like so:

```lean4
theorem new_name : ... := ...
@[deprecated new_name (since := "YYYY-MM-DD")] alias old_name := new_name

@[deprecated "This theorem is deprecated in favor of using ... with ..." (since := "YYYY-MM-DD")]
theorem example_thm ...
```

The [`deprecate to`](/mathlib4_docs/Mathlib/Tactic/DeprecateTo.html) command can help generate
alias definitions. The `@[deprecated]` attribute should always include the deprecation date,
and either the new name for the theorem when it is being renamed or kept substantially the same,
or a string to explain how transition away from the old definition when a new version is no longer
being provided.