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

fix: isDefEq, whnf, simp caching and configuration #6053

Merged
merged 16 commits into from
Nov 18, 2024
Merged

fix: isDefEq, whnf, simp caching and configuration #6053

merged 16 commits into from
Nov 18, 2024

Conversation

leodemoura
Copy link
Member

@leodemoura leodemoura commented Nov 13, 2024 •
edited
Loading

This PR fixes the caching infrastructure for whnf and isDefEq, ensuring the cache accounts for all relevant configuration flags. It also cleans up the WHNF.lean module and improves the configuration of whnf.

@leodemoura leodemoura requested a review from kmill as a code owner November 13, 2024 00:12
@leodemoura leodemoura marked this pull request as draft November 13, 2024 00:12
@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 Nov 14, 2024
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Nov 14, 2024 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d5adadc00ec0e1b36d691e3c124e133c096adcaa --onto 5e01e628b2ef90d8881a5ba10340032eeeabc5d4. (2024-11-14 01:49:08)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d5adadc00ec0e1b36d691e3c124e133c096adcaa --onto 1315266dd3faeaf28d1263668cb88f2f3f5e530c. (2024-11-14 02:25:32)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e0d7c3ac79bd9167ce7d295f51bf3779a04f7a07 --onto 1315266dd3faeaf28d1263668cb88f2f3f5e530c. (2024-11-14 20:09:52)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e0d7c3ac79bd9167ce7d295f51bf3779a04f7a07 --onto 9a8543347796e52070ff7936661ae48fcebfea60. (2024-11-15 00:57:38)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 764386734ca3a63ceb6529c10c2b4148dfbd97c1 --onto 9a8543347796e52070ff7936661ae48fcebfea60. (2024-11-16 18:07:27)
  • 💥 Mathlib branch lean-pr-testing-6053 build failed against this PR. (2024-11-16 19:36:20) View Log
  • 🟡 Mathlib branch lean-pr-testing-6053 build against this PR was cancelled. (2024-11-17 10:55:30) View Log
  • 💥 Mathlib branch lean-pr-testing-6053 build failed against this PR. (2024-11-17 11:05:30) View Log
  • 💥 Mathlib branch lean-pr-testing-6053 build failed against this PR. (2024-11-17 11:16:32) View Log
  • 🟡 Mathlib branch lean-pr-testing-6053 build against this PR was cancelled. (2024-11-17 22:57:07) View Log
  • 💥 Mathlib branch lean-pr-testing-6053 build failed against this PR. (2024-11-17 23:07:09) View Log
  • 💥 Mathlib branch lean-pr-testing-6053 build failed against this PR. (2024-11-17 23:23:55) View Log
  • ✅ Mathlib branch lean-pr-testing-6053 has successfully built against this PR. (2024-11-18 00:24:02) View Log
  • ✅ Mathlib branch lean-pr-testing-6053 has successfully built against this PR. (2024-11-18 20:00:40) View Log

@leodemoura leodemoura force-pushed the whnfConfigFixes2 branch 2 times, most recently from 9b1b597 to 56bc8bf Compare November 16, 2024 17:44
@leodemoura
chore: move WhnfCoreConfig to Meta/Basic
6b4d0a6
@leodemoura
refactor: MetaM caching
d7dca55
@leodemoura
refactor: store MetaM configuration at Simp.Context
cb16e0d
@leodemoura
fix: bug at whnfCoreAtDefEq
a77e13c 
`withConfig` was resetting the value of other configuration
options. Example: `trackZetaDelta`
@leodemoura
chore: fix test
b301923
@leodemoura
chore: fix test
75e4e63
@leodemoura
fix: checkInferTypeCache
bce47a7
@leodemoura
fix: ACLt configuration
313fe25
@leodemoura
chore: fix test
d294470
@leodemoura
fix: inferProjType error message
7ec238b
@leodemoura
fix: inferType configuration
9461d0f 
Ensure that the `whnf` configuration used by the caller does not prevent type inference for an expression.
@leodemoura
fix: propagate simp configuration
1d3f02e
@leodemoura
fix: use Expr.equal instead of Expr.eqv
8be8441 
`Expr.equal` takes binder names into account.
@leodemoura
fix: when indexing terms in simp, disable projection reduction
82d8e74
@leodemoura
perf: avoid expensive Config.toKey at withTransparency combinators
f4a3b9a
@leodemoura
chore: fix tests
501f461
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc November 16, 2024 19:33 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 16, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6053
e1406fe
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 16, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6053
cffd7f0
@leodemoura leodemoura added the changelog-language Language features, tactics, and metaprograms label Nov 16, 2024
@leanprover-community-bot leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Nov 16, 2024
@leodemoura leodemoura marked this pull request as ready for review November 16, 2024 19:42
@hrmacbeth hrmacbeth mentioned this pull request Nov 16, 2024
Draft
kim-em added a commit to leanprover-community/batteries that referenced this pull request Nov 17, 2024
@kim-em
fixes for leanprover/lean4#6053
ff8ac6a
kim-em added a commit to leanprover-community/aesop that referenced this pull request Nov 17, 2024
@kim-em
fixes for leanprover/lean4#6053
24d0b61
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 17, 2024
@kim-em
fixes for leanprover/lean4#6053
84d5f25
@kim-em kim-em mentioned this pull request Nov 17, 2024
Closed
@leanprover-community-bot leanprover-community-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 Nov 18, 2024
@leodemoura leodemoura added this pull request to the merge queue Nov 18, 2024
Merged via the queue into master with commit ab162b3 Nov 18, 2024
29 checks passed
mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Nov 18, 2024
@kim-em
chore: backport some simpler proofs from lean-pr-testing-6053 (#19176)
d51f67b 
A few things that break under leanprover/lean4#6053 admit nicer proofs anyway, so backport these more robust proofs.
TobiasLeichtfried pushed a commit to leanprover-community/mathlib4 that referenced this pull request Nov 21, 2024
@kim-em @TobiasLeichtfried
chore: backport some simpler proofs from lean-pr-testing-6053 (#19176)
4ab39ec 
A few things that break under leanprover/lean4#6053 admit nicer proofs anyway, so backport these more robust proofs.
@JovanGerb JovanGerb mentioned this pull request Dec 6, 2024
Open
3 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kmill kmill Awaiting requested review from kmill

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

@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 changelog-language Language features, tactics, 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.
2 participants
@leodemoura @leanprover-community-bot