[Merged by Bors] - chore(Data/Complex): move analysis files to under Analysis#28948
[Merged by Bors] - chore(Data/Complex): move analysis files to under Analysis#28948grunweg wants to merge 1 commit intoleanprover-community:masterfrom
Conversation
PR summary ce5fb4ce2a
|
| Files | Import difference |
|---|---|
Mathlib.Data.Complex.ExponentialBounds |
-1877 |
Mathlib.Data.Complex.Trigonometric |
-1300 |
Mathlib.Data.Complex.Exponential |
-1299 |
Mathlib.Analysis.Complex.Exponential |
1299 |
Mathlib.Analysis.Complex.Trigonometric |
1300 |
Mathlib.Analysis.Complex.ExponentialBounds |
1877 |
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.
No changes to technical debt.
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
note: file Mathlib/Data/Complex/Exponential.lean` was renamed to `Mathlib/Analysis/Complex/Exponential.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!
note: file Mathlib/Data/Complex/ExponentialBounds.lean` was renamed to `Mathlib/Analysis/Complex/ExponentialBounds.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!
note: file Mathlib/Data/Complex/Trigonometric.lean` was renamed to `Mathlib/Analysis/Complex/Trigonometric.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!
1c8bea1 to
3328a44
Compare
YaelDillies
left a comment
There was a problem hiding this comment.
Thanks! 🚀
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
|
Thanks! |
Continuation of #28909. Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
|
Pull request successfully merged into master. Build succeeded: |
…r-community#28948) Continuation of leanprover-community#28909. Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
|
I was brought here (eventually) by failing imports in FLT. Are we going to deprecate the now-missing modules? |
|
Yes, we've got another two weeks before the next stable release |
|
But definitely I shouldn't be only bumping FLT every time a new stable Lean comes out. Is the mathlib procedure really "move modules but you don't have to bother deprecating them until a new stable version of Lean is pending"? I would imagine that I'm not the only downstream project that is going to suffer, if this is the the rule. |
|
The current procedure is "the PR author makes a deprecation PR very soon after the PR", but this is not enforced. So, in my opinion: the fact that no deprecation was added yet is not supposed to happen (imho, they should be added "right after", not towards the end of a release cycle), and we really need the automation for this. |
|
I'm sorry for the annoyance this has caused you. |
|
I simply meant to point out that the real deadline here is the new stable being cut, but of course earlier is always better. I personally haven't had time to add the deprecated modules myself yet. |
These modules were renamed in #28948 and #28909, and this is semi-autogenerated PR to deprecate the old module names. These are 9 `Data.{Complex, Real}.xxx` files that have been renamed to `Analysis.{Complex, Real}.xxx`. I had forgotten about running `lake exe mk_all` after the deprecated modules had been generated.
Oh I'm not annoyed at all! I was just pointing out what seemed to be a deficiency in the system. I just had to chase up what had happened manually, and was under the impression that we were trying to avoid this. |
These modules were renamed in leanprover-community#28948 and leanprover-community#28909, and this is semi-autogenerated PR to deprecate the old module names. These are 9 `Data.{Complex, Real}.xxx` files that have been renamed to `Analysis.{Complex, Real}.xxx`. I had forgotten about running `lake exe mk_all` after the deprecated modules had been generated.
These modules were renamed in leanprover-community#28948 and leanprover-community#28909, and this is semi-autogenerated PR to deprecate the old module names. These are 9 `Data.{Complex, Real}.xxx` files that have been renamed to `Analysis.{Complex, Real}.xxx`. I had forgotten about running `lake exe mk_all` after the deprecated modules had been generated.
These modules were renamed in leanprover-community#28948 and leanprover-community#28909, and this is semi-autogenerated PR to deprecate the old module names. These are 9 `Data.{Complex, Real}.xxx` files that have been renamed to `Analysis.{Complex, Real}.xxx`. I had forgotten about running `lake exe mk_all` after the deprecated modules had been generated.
These modules were renamed in leanprover-community#28948 and leanprover-community#28909, and this is semi-autogenerated PR to deprecate the old module names. These are 9 `Data.{Complex, Real}.xxx` files that have been renamed to `Analysis.{Complex, Real}.xxx`. I had forgotten about running `lake exe mk_all` after the deprecated modules had been generated.
Continuation of #28909.