[Merged by Bors] - chore: rename fields of `LinearOrder` by plp127 · Pull Request #23976 · leanprover-community/mathlib4

plp127 · 2025-04-12T19:53:56Z

Renames LinearOrder.decidable** -> LinearOrder.toDecidable**, and same for ConditionallyCompleteLinearOrder and CompleteLinearOrder

See zulip message #mathlib4 > extending `RCLike` and `LinearOrder` @ 💬

Also fixes lots of potential diamonds caused by not specifying the decidableEq or decidableLT fields when creating an instance.

depends on: [Merged by Bors] - chore(Surreal): dedup instance #23985
depends on: [Merged by Bors] - chore(Data/Finsupp/MonomialOrder/DegLex): dedup instance #24046

github-actions · 2025-04-12T19:55:00Z

PR summary e913090b65

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ instance [DecidableLE α] [DecidableLT α] [DecidableEq α] (s : Flag α) : LinearOrder s
- instance [DecidableLE α] [DecidableLT α] (s : Flag α) : LinearOrder s

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 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).

grunweg · 2025-04-12T20:08:41Z

Can you fix the build, please? Then I'll review this quickly :-)

One question I already have: should there be deprecations for the changed field names? (I guess the answer is no, but I am not sure.)

eric-wieser · 2025-04-12T23:27:56Z

should there be deprecations for the changed field names?

It is not possible to deprecate argument names for the constructor; as for the projections, they are instances so are exempted from our deprecation rules.

Mathlib/SetTheory/Surreal/Multiplication.lean

grunweg

Thanks for doing this. The diff looks straightforward - except for five places where I have tiny questions.

Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean

Mathlib/Data/Sigma/Order.lean

grunweg · 2025-04-13T08:17:11Z

Mathlib/NumberTheory/Zsqrtd/Basic.lean

    le_total := Zsqrtd.le_total
-    decidableLE := Zsqrtd.decidableLE }
+    toDecidableLE := Zsqrtd.decidableLE
+    toDecidableEq := inferInstance }


Just to clarify: toDecidableLT is intentionally not specified?

I saw that toDecidableEq was not specified when we had a DecidableEq lying around, but could not find a DecidableLT so I didn't specify it. I guess you could say it was intentional. Should I mark this any way in the code?

grunweg · 2025-04-13T08:18:05Z

Mathlib/Order/Atoms.lean

            hb (top_unique (le_trans (top_le_iff.mpr (Or.resolve_left
-              (eq_bot_or_eq_top a) ha)) H)) }
+              (eq_bot_or_eq_top a) ha)) H))
+    toDecidableEq := ‹_› }


Just to make sure: you're intentionally not including toDecidableLT here?

(same as above)

Mathlib/LinearAlgebra/AffineSpace/Independent.lean

Co-authored-by: grunweg <rothgami@math.hu-berlin.de>

grunweg · 2025-04-14T06:47:32Z

This looks basically good to go. I have tiny questions about small places, where another pair of eyes would be useful --- if only to say "this is fine" or "add a comment, please". So:
maintainer merge?

github-actions · 2025-04-14T06:47:52Z

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

eric-wieser · 2025-04-14T15:59:43Z

As a reminder for other reviewers, there's a request for a split in #23976 (comment)

Split from #23976 The remaining instance is at https://github.com/leanprover-community/mathlib4/blob/03e9f15f2acafae1d9d3b7e0674ba87ae3cd499c/Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean#L125-L129

mathlib4-dependent-issues-bot · 2025-04-14T20:47:21Z

This PR/issue depends on:

~~[Merged by Bors] - chore(Surreal): dedup instance #23985~~
~~[Merged by Bors] - chore(Data/Finsupp/MonomialOrder/DegLex): dedup instance #24046~~
By Dependent Issues (🤖). Happy coding!

eric-wieser

maintainer merge

Since I suggested this on Zulip, someone else should decide to merge.
This all looks good now, thanks!

github-actions · 2025-04-14T21:14:49Z

🚀 Pull request has been placed on the maintainer queue by eric-wieser.

jcommelin · 2025-04-15T04:56:40Z

Thanks 🎉

bors merge

Renames `LinearOrder.decidable**` -> `LinearOrder.toDecidable**`, and same for `ConditionallyCompleteLinearOrder` and `CompleteLinearOrder` See zulip message [#mathlib4 > extending `RCLike` and `LinearOrder` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/extending.20.60RCLike.60.20and.20.60LinearOrder.60/near/511047785) Also fixes lots of potential diamonds caused by not specifying the `decidableEq` or `decidableLT` fields when creating an instance. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

mathlib-bors · 2025-04-15T06:05:01Z

Pull request successfully merged into master.

Build succeeded:

Split from #23976 The remaining instance is at https://github.com/leanprover-community/mathlib4/blob/03e9f15f2acafae1d9d3b7e0674ba87ae3cd499c/Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean#L125-L129

Renames `LinearOrder.decidable**` -> `LinearOrder.toDecidable**`, and same for `ConditionallyCompleteLinearOrder` and `CompleteLinearOrder` See zulip message [#mathlib4 > extending `RCLike` and `LinearOrder` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/extending.20.60RCLike.60.20and.20.60LinearOrder.60/near/511047785) Also fixes lots of potential diamonds caused by not specifying the `decidableEq` or `decidableLT` fields when creating an instance. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

rename fields

0fd95a0

plp127 added the t-order Order theory label Apr 12, 2025

patch

72e05dd

patch

a717bd4

plp127 added the WIP Work in progress label Apr 12, 2025

plp127 added 8 commits April 12, 2025 16:27

fix char diamond

4f6a098

patch

0ed56e7

patch

78d16bc

diamonds

ae5cb7d

patch

03c3a08

patch

ddcd980

patch

5eb9912

patch

e544754

plp127 added 2 commits April 12, 2025 20:06

patch

c5a81dd

patch

228230e

plp127 added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed WIP Work in progress labels Apr 13, 2025

eric-wieser reviewed Apr 13, 2025

View reviewed changes

Mathlib/SetTheory/Surreal/Multiplication.lean Outdated Show resolved Hide resolved

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 13, 2025

plp127 added 2 commits April 12, 2025 22:15

dedup instance

461b2e7

move edits

a119af5

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 Apr 13, 2025

grunweg reviewed Apr 13, 2025

View reviewed changes

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

Update Mathlib/Data/Sigma/Order.lean

a5e5983

Co-authored-by: grunweg <rothgami@math.hu-berlin.de>

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 14, 2025

eric-wieser added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 14, 2025

plp127 added 3 commits April 14, 2025 14:56

Merge branch 'master' into aliu/linearorder

6a5250b

dedup inst

03e9f15

merge history

35b7715

plp127 mentioned this pull request Apr 14, 2025

[Merged by Bors] - chore(Data/Finsupp/MonomialOrder/DegLex): dedup instance #24046

Closed

plp127 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 14, 2025

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 Apr 14, 2025

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 14, 2025

Merge remote-tracking branch 'origin/master' into aliu/linearorder

e913090

eric-wieser approved these changes Apr 14, 2025

View reviewed changes

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Apr 15, 2025

mathlib-bors bot changed the title ~~chore: rename fields of LinearOrder~~ [Merged by Bors] - chore: rename fields of LinearOrder Apr 15, 2025

mathlib-bors bot closed this Apr 15, 2025

mathlib-bors bot deleted the aliu/linearorder branch April 15, 2025 06:05

Conversation

plp127 commented Apr 12, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Apr 12, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary e913090b65

Import changes for modified files

Declarations diff

Uh oh!

grunweg commented Apr 12, 2025

Uh oh!

eric-wieser commented Apr 12, 2025

Uh oh!

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

grunweg Apr 13, 2025

Choose a reason for hiding this comment

Uh oh!

plp127 Apr 13, 2025

Choose a reason for hiding this comment

Uh oh!

grunweg Apr 13, 2025

Choose a reason for hiding this comment

Uh oh!

plp127 Apr 13, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

grunweg commented Apr 14, 2025

Uh oh!

github-actions bot commented Apr 14, 2025

Uh oh!

eric-wieser commented Apr 14, 2025

Uh oh!

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

Uh oh!

eric-wieser left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Apr 14, 2025

Uh oh!

jcommelin commented Apr 15, 2025

Uh oh!

mathlib-bors bot commented Apr 15, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

plp127 commented Apr 12, 2025 •

edited

Loading

github-actions bot commented Apr 12, 2025 •

edited

Loading