Skip to content

[Merged by Bors] - chore: deprecate the file AnalyticManifold#20979

Closed
sgouezel wants to merge 12 commits intomasterfrom
SG_depre
Closed

[Merged by Bors] - chore: deprecate the file AnalyticManifold#20979
sgouezel wants to merge 12 commits intomasterfrom
SG_depre

Conversation

@sgouezel
Copy link
Copy Markdown
Contributor

@sgouezel sgouezel commented Jan 23, 2025 •
edited
Loading

It's now superseded by the generic IsManifold.

Open in Gitpod

@sgouezel sgouezel added the t-differential-geometry Manifolds etc label Jan 23, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 23, 2025 •
edited
Loading

PR summary a5d0b2bb9b

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Geometry.Manifold.AnalyticManifold 1
Mathlib.Deprecated.AnalyticManifold (new file) 1692

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.

Increase in tech debt: (relative, absolute) = (2.45, 0.41)
Current number Change Type
6 1 Deprecated files
737 180 total LoC in Deprecated files

Current commit a5d0b2bb9b
Reference commit 5d914f0689

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@sgouezel sgouezel added the WIP Work in progress label Jan 23, 2025
@sgouezel
Copy link
Copy Markdown
Contributor Author

sgouezel commented Jan 23, 2025

Marked as WIP, as I'd like to add a linter warning downstream users that the file has been moved. See https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60Deprecated.60.20folder/near/495451394

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 23, 2025
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 29, 2025
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 13, 2025
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Apr 13, 2025

This PR/issue depends on:

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 13, 2025
@sgouezel sgouezel removed the WIP Work in progress label Apr 14, 2025
@grunweg grunweg self-assigned this Apr 14, 2025
grunweg
grunweg reviewed Apr 14, 2025
View reviewed changes
Mathlib/Geometry/Manifold/AnalyticManifold.lean Outdated


end AnalyticManifold
deprecated_module (since "2025-04-13")
Copy link
Copy Markdown
Contributor

@grunweg grunweg Apr 14, 2025

Choose a reason for hiding this comment

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

Can you add a deprecation message, explaining that analytic manifolds are integrated into the smoothness hierarchy now --- so one should use IsManifold I \omega M instead of AnalyticManifold I M?

grunweg
grunweg reviewed Apr 14, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@grunweg grunweg left a comment

Choose a reason for hiding this comment

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

Thanks for creating separate commits for this; that made reviewing really easy. Looks great!
maintainer delegate

@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 14, 2025

🚀 Pull request has been placed on the maintainer queue by grunweg.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 14, 2025
jcommelin
jcommelin reviewed Apr 14, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 14, 2025

✌️ sgouezel can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Apr 14, 2025
sgouezel and others added 2 commits April 14, 2025 12:26
@sgouezel @grunweg
Apply suggestions from code review
1a0e2d7 
Co-authored-by: grunweg <rothgami@math.hu-berlin.de>
@grunweg
Merge branch 'master' into SG_depre
5222169
@grunweg grunweg mentioned this pull request Apr 14, 2025
Closed
1 task
@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Apr 16, 2025

This passes CI, by the way: is there anything else left to be done?

@sgouezel
Copy link
Copy Markdown
Contributor Author

sgouezel commented Apr 17, 2025

bors r+

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Apr 17, 2025
mathlib-bors bot pushed a commit that referenced this pull request Apr 17, 2025
@sgouezel @grunweg
chore: deprecate the file AnalyticManifold (#20979)
9d67969 
It's now superseded by the generic `IsManifold`.



Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 17, 2025

Build failed:

@sgouezel
Copy link
Copy Markdown
Contributor Author

sgouezel commented Apr 17, 2025

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Apr 17, 2025
@sgouezel @grunweg
chore: deprecate the file AnalyticManifold (#20979)
d4fc037 
It's now superseded by the generic `IsManifold`.



Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 17, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: deprecate the file AnalyticManifold [Merged by Bors] - chore: deprecate the file AnalyticManifold Apr 17, 2025
@mathlib-bors mathlib-bors bot closed this Apr 17, 2025
@mathlib-bors mathlib-bors bot deleted the SG_depre branch April 17, 2025 08:06
tannerduve pushed a commit that referenced this pull request May 13, 2025
@sgouezel @grunweg @tannerduve
chore: deprecate the file AnalyticManifold (#20979)
a7741f2 
It's now superseded by the generic `IsManifold`.



Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

@grunweg grunweg grunweg left review comments

Assignees

@grunweg grunweg

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors. t-differential-geometry Manifolds etc

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@sgouezel @mathlib4-dependent-issues-bot @grunweg @jcommelin @leanprover-community-bot-assistant