Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: switching List lookup normal forms to L[n] and L[n]? #4400

Merged
merged 21 commits into from
Jun 15, 2024
Merged

feat: switching List lookup normal forms to L[n] and L[n]? #4400

merged 21 commits into from
Jun 15, 2024

Conversation

kim-em
Copy link
Collaborator

@kim-em kim-em commented Jun 7, 2024

This is presumably going to have significant breakage downstream.

@kim-em kim-em changed the title wip: switching List lookup normal forms to L[n] and L[n]? feat: switching List lookup normal forms to L[n] and L[n]? Jun 7, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc June 8, 2024 05:26 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 Jun 8, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Jun 8, 2024 •
edited
Loading

Mathlib CI status (docs):

@kim-em kim-em added the release-ci Enable all CI checks for a PR, like is done for releases label Jun 11, 2024
@kim-em
Copy link
Collaborator Author

kim-em commented Jun 11, 2024

I have Batteries working against this. Next up, Mathlib?

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc June 11, 2024 06:06 Inactive
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Jun 11, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc June 12, 2024 01:06 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc June 12, 2024 02:39 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc June 12, 2024 03:54 Inactive
@kim-em
Copy link
Collaborator Author

kim-em commented Jun 12, 2024 •
edited
Loading

I have a local Mathlib build now (finally!), although I expected the simpNF linter will still have some complaints.

and now the linter is happy too!

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc June 12, 2024 05:22 Inactive
@kim-em kim-em marked this pull request as ready for review June 12, 2024 06:23
@kim-em kim-em requested a review from digama0 as a code owner June 12, 2024 06:23
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc June 13, 2024 00:17 Inactive
@kim-em kim-em force-pushed the getElem branch 3 times, most recently from 8f6933f to c9030be Compare June 13, 2024 05:20
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc June 13, 2024 05:33 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc June 13, 2024 06:09 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc June 13, 2024 06:37 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc June 13, 2024 08:49 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc June 13, 2024 08:55 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc June 13, 2024 11:00 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc June 13, 2024 23:54 Inactive
@kim-em kim-em added the awaiting-review Waiting for someone to review the PR label Jun 14, 2024
@kim-em kim-em mentioned this pull request Jun 14, 2024
Merged
@kim-em kim-em removed the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Jun 14, 2024
@kim-em kim-em mentioned this pull request Jun 14, 2024
Closed
2 tasks
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Jun 14, 2024
@kim-em kim-em enabled auto-merge June 15, 2024 06:37
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc June 15, 2024 06:45 Inactive
@kim-em
Copy link
Collaborator Author

kim-em commented Jun 15, 2024

!bench

@kim-em kim-em added this pull request to the merge queue Jun 15, 2024
@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 0e662f7.
There were no significant changes against commit fe0cb97.

Merged via the queue into master with commit e10a37d Jun 15, 2024
22 checks passed
This was referenced Jun 16, 2024
Merged
Closed
mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jun 17, 2024
@kim-em
chore: adaptations for nightly-2024-06-16 (#13886)
883421c 
This is mostly adaptation for leanprover/lean4#4400.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@digama0 digama0 Awaiting requested review from digama0 digama0 is a code owner

Assignees
No one assigned
Labels
awaiting-review Waiting for someone to review the PR builds-mathlib CI has verified that Mathlib builds against this PR release-ci Enable all CI checks for a PR, like is done for releases 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.
3 participants
@kim-em @leanprover-community-mathlib4-bot @leanprover-bot