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

perf: use withSynthesize when elaborating let/have type #4096

Merged
merged 2 commits into from
May 9, 2024
Merged

perf: use withSynthesize when elaborating let/have type #4096

merged 2 commits into from
May 9, 2024

Conversation

leodemoura
Copy link
Member

closes #4051

cc @semorrison

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc May 7, 2024 19:40 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 May 7, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc May 8, 2024 00:05 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 8, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#4096
f4fbd97
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 8, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#4096
6247337
@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 May 8, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

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

Mathlib CI status (docs):

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc May 8, 2024 01:02 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 8, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4096
fa3d41d
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 8, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4096
344a300
@kim-em
Copy link
Collaborator

kim-em commented May 8, 2024

There are a couple of places in Mathlib where we'll need to replace have p : x ∈ ⊤ := Set.mem_univ x with have p : x ∈ (⊤ : Set β) := Set.mem_univ x.

Is this unavoidable collateral damage?

@kim-em
Copy link
Collaborator

kim-em commented May 8, 2024

There is still fallout in Mathlib. Let's not merge this until I've had a chance to look a bit further through this.

@leodemoura
Copy link
Member Author

There are a couple of places in Mathlib where we'll need to replace have p : x ∈ ⊤ := Set.mem_univ x with have p : x ∈ (⊤ : Set β) := Set.mem_univ x.

Is this unavoidable collateral damage?

@semorrison Could you please create a mwe for this one? It is useful to have it in our test suite.

leodemoura added 2 commits May 8, 2024 13:40
@leodemoura
perf: use withSynthesize when elaborating let/have type
b54be54 
closes #4051
@leodemoura
feat: add withSynthesize (postpone := partial) k
29477b3 
It forces pending elaboration problems and tactics to be executed, but
allows TC ones to be postponed.
@leodemoura leodemoura requested a review from kim-em as a code owner May 8, 2024 20:50
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc May 8, 2024 21:05 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 8, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4096
dd48c40
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 8, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4096
b13b4ef
@leodemoura
Copy link
Member Author

@semorrison I pushed a fix, but did not manage to test because of a linter failure in Mathlib.

@kim-em kim-em mentioned this pull request May 9, 2024
Closed
@kim-em kim-em added this pull request to the merge queue May 9, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels May 9, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc May 9, 2024 01:33 Inactive
Merged via the queue into master with commit ec87283 May 9, 2024
34 of 35 checks passed
mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 9, 2024
@kim-em
feat: backport changes from lean-pr-testing-4096 (#12772)
b72ddd8 
These changes will be required after leanprover/lean4#4096, but they all look like positive readability changes to me anyway (the things being filled in are sort of hard to work out with time travelling to later lines in the proofs!), so I think we can backport them all to `master`.

Co-authored-by: Scott Morrison <[email protected]>
apnelson1 pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 12, 2024
@kim-em @apnelson1
feat: backport changes from lean-pr-testing-4096 (#12772)
5edc936 
These changes will be required after leanprover/lean4#4096, but they all look like positive readability changes to me anyway (the things being filled in are sort of hard to work out with time travelling to later lines in the proofs!), so I think we can backport them all to `master`.

Co-authored-by: Scott Morrison <[email protected]>
callesonne pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 16, 2024
@kim-em @callesonne
feat: backport changes from lean-pr-testing-4096 (#12772)
d86e071 
These changes will be required after leanprover/lean4#4096, but they all look like positive readability changes to me anyway (the things being filled in are sort of hard to work out with time travelling to later lines in the proofs!), so I think we can backport them all to `master`.

Co-authored-by: Scott Morrison <[email protected]>
@Kha Kha mentioned this pull request Aug 16, 2024
Closed
3 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR 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.

Elaboration of explicit term proof significantly slower than equivalent tactic proof
3 participants
@leodemoura @leanprover-community-mathlib4-bot @kim-em