Skip to content

fix: nested try-catch parsing #8252

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
Open
wants to merge 14 commits into
base: master
Choose a base branch
from
Open

fix: nested try-catch parsing #8252

wants to merge 14 commits into from
+119 −7

Conversation

Rob23oba
Copy link
Contributor

@Rob23oba Rob23oba commented May 6, 2025

This PR fixes the parsing of nested try-catch blocks.

Closes #8220

@github-actions github-actions bot added changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN labels May 6, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented May 6, 2025 •
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 edcad9a14b98e6af134dc2afb276cb42e8a2417c --onto af51e3e4b1c655df43476972c4d9aeae76e49046. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-06 21:00:13)
  • 💥 Mathlib branch lean-pr-testing-8252 build failed against this PR. (2025-05-06 21:37:25) View Log
  • 💥 Mathlib branch lean-pr-testing-8252 build failed against this PR. (2025-05-06 22:25:02) View Log
  • ✅ Mathlib branch lean-pr-testing-8252 has successfully built against this PR. (2025-05-06 23:54:11) View Log
  • ✅ Mathlib branch lean-pr-testing-8252 has successfully built against this PR. (2025-05-07 08:25:44) View Log
  • ✅ Mathlib branch lean-pr-testing-8252 has successfully built against this PR. (2025-05-07 10:28:19) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 10bda559f94b4b5bc39f1a0992cb70cb22cc7c26 --onto e681855428032555d8f1f45aebcbb0b4bad85db7. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-12 07:15:16)

@Rob23oba Rob23oba force-pushed the try-catch-catch branch from 2f5a047 to 2b1b3b4 Compare May 6, 2025 21:01
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 6, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#8252
a6c658f
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 6, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#8252
381b363
@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 May 6, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 6, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#8252
88e70b2
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 6, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#8252
798f7dd
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 6, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#8252
6ceaf94
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 6, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#8252
1a66cde
@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 May 6, 2025
@Rob23oba Rob23oba requested a review from kmill as a code owner May 7, 2025 07:12
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 7, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#8252
1de57fc
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 7, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#8252
288b512
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 7, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#8252
42eeca1
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 7, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#8252
b64a16b
eric-wieser
eric-wieser reviewed May 11, 2025
View reviewed changes
src/Lean/Parser/Basic.lean Outdated
@@ -1541,6 +1541,20 @@ def withPositionAfterLinebreak : Parser → Parser := withFn fun f c s =>
let prev := s.stxStack.back
adaptCacheableContextFn (fun c => if checkTailLinebreak prev then { c with savedPos? := s.pos } else c) f c s

def withPositionFromLineStart : Parser → Parser := withFn fun f c s => Id.run do
Copy link
Contributor

Choose a reason for hiding this comment

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

Please write a docstring for this!

eric-wieser
eric-wieser reviewed May 11, 2025
View reviewed changes
@leanprover-bot leanprover-bot added the P-high We will work on this issue label May 13, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@kmill kmill Awaiting requested review from kmill kmill 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 P-high We will work on this issue 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.

Parse issue involving try-catch-catch
4 participants
@Rob23oba @leanprover-community-bot @eric-wieser @leanprover-bot