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.

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

fix: make dsimp? use and report simprocs #3654

Merged
merged 3 commits into from
Mar 12, 2024

Conversation

thorimur
Copy link
Contributor

Modifies dsimpLocation' (which implements dsimp?) to take a simprocs : SimprocsArray argument, like simpLocation and dsimpLocation. This ensures that the behavior of dsimp matches dsimp?.


Closes #3653

@thorimur thorimur requested a review from kim-em as a code owner March 12, 2024 00:11
@thorimur thorimur force-pushed the dsimp-simprocs-3653 branch 2 times, most recently from 887641e to de3a7f2 Compare March 12, 2024 00:49
@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 12, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Mar 12, 2024

Mathlib CI status (docs):

  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c43a6b53413f1f597eb5144692730a9132c3e473 --onto 32dcc6eb895b58df3d3241a2521963e64995b621. (2024-03-12 01:05:46)
  • ❗ Std CI can not be attempted yet, as the nightly-testing-2024-03-11 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Std CI should run now. (2024-03-12 01:26:44)
  • 💥 Mathlib branch lean-pr-testing-3654 build failed against this PR. (2024-03-12 04:07:56) View Log
  • 💥 Mathlib branch lean-pr-testing-3654 build failed against this PR. (2024-03-12 04:54:08) View Log

@github-actions github-actions bot added the awaiting-review Waiting for someone to review the PR label Mar 12, 2024
@thorimur thorimur force-pushed the dsimp-simprocs-3653 branch from de3a7f2 to 04a39f1 Compare March 12, 2024 01:09
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 12, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 12, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan full-ci labels Mar 12, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 12, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 12, 2024
@kim-em kim-em added this pull request to the merge queue Mar 12, 2024
Merged via the queue into leanprover:master with commit 5cf4db7 Mar 12, 2024
29 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
awaiting-review Waiting for someone to review the PR breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Development

Successfully merging this pull request may close these issues.

dsimp? fails to report simprocs
3 participants