Skip to content

feat: Lean.Grind.IsCharP#7870

Merged
kim-em merged 42 commits intomasterfrom
grind_isCharP
Apr 10, 2025
Merged

feat: Lean.Grind.IsCharP#7870
kim-em merged 42 commits intomasterfrom
grind_isCharP

Conversation

@kim-em
Copy link
Copy Markdown
Collaborator

@kim-em kim-em commented Apr 8, 2025

This PR adds a mixin typeclass for Lean.Grind.CommRing recording the characteristic of the ring, and constructs instances for Int, IntX, UIntX, and BitVec.

kim-em added 2 commits April 8, 2025 20:42
@kim-em
feat: Lean.Grind.IsCharP
56736d1 
looks reasonable

looks reasonable

.
@kim-em
BitVec
525cfc5
@kim-em kim-em added the changelog-language Language features and metaprograms label Apr 8, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc April 8, 2025 11:19 Inactive
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Apr 8, 2025
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 8, 2025
Update lean-toolchain for testing leanprover/lean4#7870
6978994
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 8, 2025
Update lean-toolchain for testing leanprover/lean4#7870
9b8d511
@ghost ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Apr 8, 2025
@ghost
Copy link
Copy Markdown

ghost commented Apr 8, 2025 •
edited by ghost
Loading

Mathlib CI status (docs):

  • 💥 Mathlib branch lean-pr-testing-7870 build failed against this PR. (2025-04-08 11:45:55) View Log
  • 💥 Mathlib branch lean-pr-testing-7870 build failed against this PR. (2025-04-08 23:10:19) View Log
  • 💥 Mathlib branch lean-pr-testing-7870 build failed against this PR. (2025-04-09 03:50:23) View Log
  • 💥 Mathlib branch lean-pr-testing-7870 build failed against this PR. (2025-04-09 05:53:45) View Log
  • 💥 Mathlib branch lean-pr-testing-7870 build failed against this PR. (2025-04-09 07:17:27) View Log
  • 💥 Mathlib branch lean-pr-testing-7870 build failed against this PR. (2025-04-09 08:04:41) View Log
  • 💥 Mathlib branch lean-pr-testing-7870 build failed against this PR. (2025-04-09 13:53:39) View Log
  • 🟡 Mathlib branch lean-pr-testing-7870 build against this PR was cancelled. (2025-04-09 14:26:30) View Log
  • 💥 Mathlib branch lean-pr-testing-7870 build failed against this PR. (2025-04-09 15:13:03) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 985cd71f23357edb176a7f67021e1a3b2583b338 --onto 388b6f045bd6d79df9b503d55eef6688ceb8f647. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-09 23:53:27)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 61d7716ad86948bee2f0f62b151aac9f2a8ef967 --onto 388b6f045bd6d79df9b503d55eef6688ceb8f647. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-10 01:37:43)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 97a00b3881f6bceb659216a7f13c50b21169b858 --onto 388b6f045bd6d79df9b503d55eef6688ceb8f647. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-10 02:23:45)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase acf42bd30bcae919a5e0bced30d4af58610814c0 --onto 388b6f045bd6d79df9b503d55eef6688ceb8f647. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-10 05:37:04)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase deef1c2739a331899b0e536312e65e9815059014 --onto 388b6f045bd6d79df9b503d55eef6688ceb8f647. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-10 07:05:14)
  • 🟡 Mathlib branch lean-pr-testing-7870 build this PR didn't complete normally. (2025-04-10 07:17:07) View Log
  • 🟡 Mathlib branch lean-pr-testing-7870 build this PR didn't complete normally. (2025-04-10 07:20:03) View Log

ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 8, 2025
Trigger CI for leanprover/lean4#7870
ab095c5
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 8, 2025
Trigger CI for leanprover/lean4#7870
e77e469
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 9, 2025
Trigger CI for leanprover/lean4#7870
483f185
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 9, 2025
Trigger CI for leanprover/lean4#7870
bfe52a7
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 9, 2025
Trigger CI for leanprover/lean4#7870
cda2d46
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 9, 2025
Trigger CI for leanprover/lean4#7870
90c1cc4
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 9, 2025
Trigger CI for leanprover/lean4#7870
1bab4d2
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 9, 2025
Trigger CI for leanprover/lean4#7870
be4bc19
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 9, 2025
Trigger CI for leanprover/lean4#7870
187b10f
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 9, 2025
Trigger CI for leanprover/lean4#7870
c15f012
@kim-em kim-em removed the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Apr 10, 2025
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Apr 10, 2025
@kim-em
Copy link
Copy Markdown
Collaborator Author

kim-em commented Apr 10, 2025

With the latest change, moving OfNat from a parameter to a field, I'm happy with how things work out in Mathlib.

The relevant diff is leanprover-community/mathlib4@lean-pr-testing-7873...lean-pr-testing-7870.

@kim-em kim-em enabled auto-merge April 10, 2025 08:21
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc April 10, 2025 08:33 Inactive
@kim-em kim-em added this pull request to the merge queue Apr 10, 2025
Merged via the queue into master with commit bffa642 Apr 10, 2025
16 checks passed
kmill added a commit to leanprover-community/mathlib4 that referenced this pull request Apr 19, 2025
@kmill @kim-em
@TwoFX @Rob23oba @digama0 @jcommelin
chore: adaptations for nightly-2025-04-16 (#24202)
f0b7487 
* fixes

* fix test

* fix

* chore: adaptations for leanprover/lean4#7797

* stricter rfl check

* fix merge

* Trigger CI for leanprover/lean4#7797

* Trigger CI for leanprover/lean4#7797

* Trigger CI for leanprover/lean4#7797

* inverse construction

* Update lean-toolchain for testing leanprover/lean4#7791

* lake update

* Fix

* Fix

* Fix

* chore: bump to nightly-2025-04-03

* more fixes

* merge lean-pr-testing-6325

* bump proofwidgets

* Update lean-toolchain for testing leanprover/lean4#7812

* shake

* fix shake

* fix tests

* import mathlib.init

* Update lean-toolchain for testing leanprover/lean4#7816

* Trigger CI for leanprover/lean4#7816

* Update lean-toolchain for testing leanprover/lean4#7802

* Fix

* fixes

* Fix (pending upstream changes)

* Trigger CI for leanprover/lean4#7802

* fix

* chore: bump to nightly-2025-04-04

* Fix

* Fix

* Fix

* Fix

* Fix

* Fix

* Update lean-toolchain for testing leanprover/lean4#7818

* Fix

* Fix

* Fix

* Merge master into nightly-testing

* Fix

* Fix comments

* fixes

* Trigger CI for leanprover/lean4#7816

* fix

* fix

* missing doc-string?

* chore: bump to nightly-2025-04-05

* chore: bump to nightly-2025-04-06

* move Batteries to nightly-testing

* lake update

* lint

* fix

* chore: bump to nightly-2025-04-07

* sprinkle noncomputable

* fix: relativize file paths

fix for leanprover/lean4#7822

* chore: reset cache

* chore: bump to nightly-2025-04-07

* shake

* fix: relativize more

* Update lean-toolchain for testing leanprover/lean4#7856

* Update lean-toolchain for testing leanprover/lean4#7851

* Fix

* Fix

* Fix

* Fix

* chore: bump to nightly-2025-04-08

* Update lean-toolchain for testing leanprover/lean4#7870

* Trigger CI for leanprover/lean4#7870

* Trigger CI for leanprover/lean4#7870

* Trigger CI for leanprover/lean4#7870

* wip

* Trigger CI for leanprover/lean4#7870

* .

* chore: bump to nightly-2025-04-09

* Trigger CI for leanprover/lean4#7870

* .

* bump

* lake update

* fixes for leanprover/lean4#7873

* fixes

* deprecations

* chore: bump to nightly-2025-04-10

* chore: `Option.zipWith` -> `Option.merge`

* lake update

* toolchain

* fix

* fix

* Update lean-toolchain for testing leanprover/lean4#7897

* Trigger CI for leanprover/lean4#7897

* fix

* lake update and fix

* Fix

* Fix

* Trigger CI for leanprover/lean4#7897

* fix merge

* chore: adaptations for nightly-2025-04-10

* chore: bump to nightly-2025-04-14

* fix

* .

* annotate changed goal state

* fixes (adaptation notes)

* cleanup imports

* cleanup

* Update lean-toolchain for testing leanprover/lean4#7933

* Fix

* Fix

* Update lean-toolchain for testing leanprover/lean4#7975

* remove adaptation notes

* chore: bump to nightly-2025-04-16

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: github-actions <github-actions@github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@kim-em