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: upstream rw? tactic #3719

Merged
merged 3 commits into from
Mar 23, 2024
Merged

feat: upstream rw? tactic #3719

merged 3 commits into from
Mar 23, 2024

Conversation

joehendrix
Copy link
Contributor

This updates the rw? tactic from Mathlib to use lazy discriminator trees and upstreams it.

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 19, 2024 17:01 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 Mar 19, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 19, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#3719
368a307
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 19, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#3719
9edfcbe
@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 Mar 19, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Mar 19, 2024 •
edited
Loading

Mathlib CI status (docs):

  • ❌ Mathlib branch lean-pr-testing-3719 built against this PR, but linting failed. (2024-03-19 17:11:38) View Log
  • ❌ Mathlib branch lean-pr-testing-3719 built against this PR, but linting failed. (2024-03-19 17:32:18) View Log
  • 🟡 Mathlib branch lean-pr-testing-3719 build this PR didn't complete normally. (2024-03-19 17:48:33) View Log
  • 🟡 Mathlib branch lean-pr-testing-3719 build this PR didn't complete normally. (2024-03-19 17:49:58) View Log
  • 🟡 Mathlib branch lean-pr-testing-3719 build against this PR was cancelled. (2024-03-19 17:56:06) View Log
  • ❌ Mathlib branch lean-pr-testing-3719 built against this PR, but testing failed. (2024-03-19 18:54:34) View Log
  • ❌ Mathlib branch lean-pr-testing-3719 built against this PR, but testing failed. (2024-03-20 00:45:14) View Log
  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8ce98e62ac82379caaa4e76243e8f4ac3fccf366 --onto d5a1dce0ae92475c73a9c24fc8fb2c8e0d4acbcd. (2024-03-22 22:40:08)

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 19, 2024 17:14 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 19, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3719
ad0bfe8
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 19, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3719
f3f7657
kim-em
kim-em reviewed Mar 19, 2024
View reviewed changes
tests/lean/run/rewrites.lean
-- set_option trace.Tactic.rewrites.lemmas true

/--
info: Try this: rw [@List.map_append]
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah --- I was just noticing this while otherwise happily using rw_search to repair some proofs in Mathlib. There is a pretty unnecessary @ at the front of each lemma name here, because of the way we've going from Name to Expr. Do you see a way to avoid having this initial @?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Blind guess: use https://leanprover-community.github.io/mathlib4_docs/Std/Lean/Delaborator.html#Lean.ppConst in the right place?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@nomeata Thanks. I just tested it and it seems to work by upstreaming and inserting into Tactic.TryThis.addRewrite suggestion. I'll make a separate PR for it since it's largely orthogonal to this work.

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 19, 2024 23:29 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 19, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3719
880f580
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 19, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3719
797091b
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 22, 2024 02:02 Inactive
@joehendrix joehendrix removed the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Mar 22, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 22, 2024 22:38 Inactive
@joehendrix joehendrix added this pull request to the merge queue Mar 23, 2024
Merged via the queue into master with commit 6c8976a Mar 23, 2024
11 checks passed
@kim-em kim-em added the full-ci label Mar 24, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 24, 2024 00:57 Inactive
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em kim-em left review comments

@nomeata nomeata nomeata left review comments

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

Assignees
No one assigned
Labels
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
@joehendrix @leanprover-community-mathlib4-bot @nomeata @kim-em