Skip to content

fix: respect transparency#13342

Draft
datokrat wants to merge 13 commits intodefeq_todo_4from
defeq_todo_4_paul
Draft

fix: respect transparency#13342
datokrat wants to merge 13 commits intodefeq_todo_4from
defeq_todo_4_paul

Conversation

@datokrat
Copy link
Copy Markdown
Contributor

@datokrat datokrat commented Apr 9, 2026

TBA

@datokrat datokrat changed the base branch from master to defeq_todo_4 April 9, 2026 08:04
@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 9, 2026
@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Apr 9, 2026

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-04-06 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-04-09 09:37:23)

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 9, 2026
Update lean-toolchain for testing leanprover/lean4#13342
913e042
@github-actions github-actions bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Apr 9, 2026
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 9, 2026
Update lean-toolchain for testing leanprover/lean4#13342
413d7f1
@mathlib-lean-pr-testing mathlib-lean-pr-testing bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Apr 9, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Apr 9, 2026

Mathlib CI status (docs):

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 10, 2026
Update lean-toolchain for leanprover/lean4#13342
0881754
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 10, 2026
Update lean-toolchain for leanprover/lean4#13342
796b35d
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Apr 10, 2026

Mathlib CI status (docs):

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 10, 2026
Update lean-toolchain for leanprover/lean4#13342
76a1998
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 10, 2026
Update lean-toolchain for leanprover/lean4#13342
314f7c9
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Apr 10, 2026

Mathlib CI status (docs):

hargoniX added 5 commits April 10, 2026 17:42
@hargoniX @datokrat
systematic fix 1
d522c8a 
(cherry picked from commit 7e661fe)
@hargoniX @datokrat
dsimp to simp
bc0a073 
(cherry picked from commit f26c1d4)
@hargoniX @datokrat
change cast
0e228d2 
(cherry picked from commit e71d623)
@hargoniX @datokrat
more simp
c2e4f39 
(cherry picked from commit 77f0e3a)
@hargoniX @datokrat
fix lrat checker
1add505 
(cherry picked from commit 6ecaa8e)
@datokrat datokrat mentioned this pull request Apr 10, 2026
Draft
mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 10, 2026
Update lean-toolchain for leanprover/lean4#13342
040e49d
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 10, 2026
Update lean-toolchain for leanprover/lean4#13342
d80320c
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Apr 10, 2026

Mathlib CI status (docs):

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 10, 2026
Update lean-toolchain for leanprover/lean4#13342
856fa2d
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 10, 2026
Update lean-toolchain for leanprover/lean4#13342
ab0a95a
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Apr 10, 2026

Mathlib CI status (docs):

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@hargoniX hargoniX Awaiting requested review from hargoniX hargoniX will be requested when the pull request is marked ready for review hargoniX is a code owner

@TwoFX TwoFX Awaiting requested review from TwoFX TwoFX will be requested when the pull request is marked ready for review TwoFX is a code owner

@digama0 digama0 Awaiting requested review from digama0 digama0 will be requested when the pull request is marked ready for review digama0 is a code owner

@kim-em kim-em Awaiting requested review from kim-em kim-em will be requested when the pull request is marked ready for review kim-em is a code owner

Assignees

No one assigned

Labels

breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN 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.

4 participants

@datokrat @leanprover-bot @TwoFX @hargoniX