Skip to content

feat: limit the use of Classical.choice#1698

Draft
riccardobrasca wants to merge 16 commits into
leanprover-community:mainfrom
riccardobrasca:less_choice
Draft

feat: limit the use of Classical.choice#1698
riccardobrasca wants to merge 16 commits into
leanprover-community:mainfrom
riccardobrasca:less_choice

Conversation

@riccardobrasca

@riccardobrasca riccardobrasca commented Feb 24, 2026 •
edited
Loading

Copy link
Copy Markdown
Member

This draft PR is used to monitor the branch less_choice and it's not meant to be merged. See mathlib4#35685 for an explanation on how this is used.

@github-actions github-actions Bot added the WIP work in progress label Feb 24, 2026
@riccardobrasca riccardobrasca removed the WIP work in progress label Feb 24, 2026
mathlib-nightly-testing Bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Feb 24, 2026
@mathlib-nightly-testing
Update Batteries branch for testing leanprover-community/batteries#1698
2f6421c
mathlib-nightly-testing Bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Feb 26, 2026
@mathlib-nightly-testing
Trigger CI for leanprover-community/batteries#1698
ec676db
@mathlib-merge-conflicts mathlib-merge-conflicts Bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Mar 1, 2026
mathlib-nightly-testing Bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 4, 2026
@mathlib-nightly-testing
Trigger CI for leanprover-community/batteries#1698
31668c7
@mathlib-merge-conflicts mathlib-merge-conflicts Bot added merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. and removed merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. labels Mar 4, 2026
mathlib-nightly-testing Bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 4, 2026
@mathlib-nightly-testing
Trigger CI for leanprover-community/batteries#1698
c8cea1c
@mathlib-merge-conflicts mathlib-merge-conflicts Bot added merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. and removed merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. labels Mar 4, 2026
@riccardobrasca @claude
chore: merge upstream/main and bump toolchain to v4.29.0-rc6-less-choice
572a784 
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
mathlib-nightly-testing Bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 10, 2026
@mathlib-nightly-testing
Trigger CI for leanprover-community/batteries#1698
275ea62
@mathlib-merge-conflicts mathlib-merge-conflicts Bot removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Mar 10, 2026
@mathlib-merge-conflicts mathlib-merge-conflicts Bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Mar 23, 2026
mathlib-nightly-testing Bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 24, 2026
@mathlib-nightly-testing
Trigger CI for leanprover-community/batteries#1698
19dab25
@mathlib-merge-conflicts mathlib-merge-conflicts Bot added merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. and removed merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. labels Mar 24, 2026
@riccardobrasca @claude
chore: merge upstream/main and bump toolchain to v4.29.0-rc8-less-choice
9666fe6 
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@mathlib-merge-conflicts mathlib-merge-conflicts Bot removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Mar 25, 2026
mathlib-nightly-testing Bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 25, 2026
@mathlib-nightly-testing
Trigger CI for leanprover-community/batteries#1698
cc6387c
@mathlib-merge-conflicts mathlib-merge-conflicts Bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Mar 27, 2026
mathlib-nightly-testing Bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 31, 2026
@mathlib-nightly-testing
Trigger CI for leanprover-community/batteries#1698
da766c7
@mathlib-merge-conflicts mathlib-merge-conflicts Bot removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Mar 31, 2026
mathlib-nightly-testing Bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 31, 2026
@mathlib-nightly-testing
Trigger CI for leanprover-community/batteries#1698
fa2b013
@mathlib-merge-conflicts mathlib-merge-conflicts Bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Apr 1, 2026
@riccardobrasca
Merge tag 'v4.30.0-rc1' into less_choice
4b265b5 
# Conflicts:
#	lean-toolchain
mathlib-nightly-testing Bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 6, 2026
@mathlib-nightly-testing
Trigger CI for leanprover-community/batteries#1698
ebe4fe3
@mathlib-merge-conflicts mathlib-merge-conflicts Bot removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Apr 6, 2026
@fgdorais fgdorais added the no-action There is no need to act on this label Apr 6, 2026
@fgdorais

fgdorais commented Apr 6, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

I just added the wontfix label. This is just to categorize this PR which, I believe, is all about testing different ideas to avoid choice in Lean. I support your efforts! But this will not be merged for reasons that both you and I know too well. Anyway, I just had to put a label for purely administrative purposes. If you would prefer a different label, I'm happy to fix that for you. I can even create a label for this kind of draft PR.

@fgdorais

fgdorais commented Apr 7, 2026

Copy link
Copy Markdown
Collaborator

I changed the tag name to no-action, which seems both more accurate and much less offensive. I'm still open to other options.

@mathlib-merge-conflicts mathlib-merge-conflicts Bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Apr 17, 2026
@riccardobrasca
Merge tag 'v4.30.0-rc2' into less_choice
2960d0c 
# Conflicts:
#	lean-toolchain
mathlib-nightly-testing Bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 19, 2026
@mathlib-nightly-testing
Trigger CI for leanprover-community/batteries#1698
7943fea
@mathlib-merge-conflicts mathlib-merge-conflicts Bot removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Apr 19, 2026
@mathlib-merge-conflicts mathlib-merge-conflicts Bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label May 26, 2026
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

merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. no-action There is no need to act on this

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@riccardobrasca @fgdorais