Skip to content

fix: simp? output order - #9117

Closed
Rob23oba wants to merge 3 commits into
leanprover:masterfrom
Rob23oba:simp-trace-order
Closed

fix: simp? output order#9117
Rob23oba wants to merge 3 commits into
leanprover:masterfrom
Rob23oba:simp-trace-order

Conversation

@Rob23oba

@Rob23oba Rob23oba commented Jul 1, 2025

Copy link
Copy Markdown
Contributor

This PR fixes the output order of simp? and similar tactics to roundtrip more consistently.

Breaking change: many functions related to generating simp only calls (e.g. mkSimpCallStx) now require a Simp.Context and a Simp.SimprocsArray in order to reorder the lemmas correctly

Closes #4615

@Rob23oba
Rob23oba marked this pull request as ready for review July 1, 2025 11:25
@github-actions github-actions Bot added changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN labels Jul 1, 2025
@ghost

ghost commented Jul 1, 2025

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-06-30 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-07-01 11:46:06)

@leanprover-bot

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-06-30 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-07-01 11:46:07)

@leanprover-bot leanprover-bot added the P-low We are not planning to work on this issue label Jul 21, 2025
@kim-em

kim-em commented Sep 1, 2026

Copy link
Copy Markdown
Collaborator

This hasn't been touched in over a year, and has a merge conflict. I'm closing now; please re-open if you think appropriate.

@kim-em kim-em closed this Sep 1, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-language Language features and metaprograms P-low We are not planning to work on this issue 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.

Running simp? output produces different goal than simp

3 participants