feat: require indentation in commands, allow empty tactic sequences by nomeata · Pull Request #13229 · leanprover/lean4

nomeata · 2026-04-01T10:05:18Z

This PR wraps the top-level command parser with withPosition to enforce indentation in by blocks, combined with an empty-by fallback for better error messages.

This subsumes #3215 (which introduced withPosition commandParser but without the empty-by fallback). It is also related to #9524, which explores elaboration with empty tactic sequences — this PR reuses that idea for the empty-by fallback, so that a by not followed by an indented tactic produces an elaboration error (unsolved goals) rather than a parse error.

Changes:

topLevelCommandParserFn now uses (withPosition commandParser).fn, setting the saved position at the start of each top-level command
tacticSeqIndentGt gains an empty tactic sequence fallback (pushNone) so that missing indentation produces an elaboration error (unsolved goals) instead of a parse error
isEmptyBy in goalsAt? removed: with strict by indentation, empty by blocks parse successfully via pushNone (producing empty nodes) rather than producing .missing syntax, making the isEmptyBy check dead code. The isEmpty helper in isSyntheticTacticCompletion continues to work correctly because it handles both .missing and empty nodes from pushNone (via the vacuously-true args.all isEmpty on #[])
Test files updated to indent by blocks and expression continuations that were previously at column 0

Behavior:

Top-level by blocks now require indentation (column > 0 for commands at column 0)
Commands indented inside section require proofs to be indented past the command's column
#guard_msgs in example : True := by works because tactic indentation is checked against the outermost command's column
Expression continuations (not just by) must also be indented past the command, which is slightly more strict but more consistent
have : True := by followed by a dedent now correctly puts this in scope in the outer tactic block (the have is structurally complete with an unsolved-goal error, rather than a parse error)

Code changes observed in practice (lean4 test suite + Mathlib):

by blocks: top-level theorem ... := by / decreasing_by followed by tactics at column 0 must be indented
variable continuations: variable {A : Type*} [Foo A]\n{B : Type*} where the second line starts at column 0 must be indented (most common category in Mathlib)
Expression continuations: def f : T :=\nexpr or #synth Foo\n[args] where the body/arguments start at column 0
Structure literals: .symm\n{ toFun := ... where the struct literal starts at column 0

🤖 Generated with Claude Code

Co-Authored-By: Claude Opus 4.6 noreply@anthropic.com

leanprover-bot · 2026-04-01T11:06:05Z

Reference manual CI status:

❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-25 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. (2026-04-01 11:06:05)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase acae2b44fd8bb0c0009b4428529da9da6212df08 --onto 861bc19e0c1c45b5766cc5c9ef0488568368b236. You can force reference manual CI using the force-manual-ci label. (2026-04-03 07:15:58)

mathlib-lean-pr-testing · 2026-04-01T11:15:37Z

Mathlib CI status (docs):

🟡 Mathlib branch lean-pr-testing-13229 build against this PR was cancelled. (2026-04-01 11:15:36) View Log
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase acae2b44fd8bb0c0009b4428529da9da6212df08 --onto fc0cf68539ad3b481a1802414c22c44506519c9d. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-03 07:15:56)

mathlib-lean-pr-testing · 2026-04-01T11:33:50Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-13229 build failed against this PR. (2026-04-01 11:33:48) View Log

mathlib-lean-pr-testing · 2026-04-01T12:42:03Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-13229 build failed against this PR. (2026-04-01 12:42:01) View Log

mathlib-lean-pr-testing · 2026-04-01T13:43:25Z

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-13229 has successfully built against this PR. (2026-04-01 13:43:22) View Log

mathlib-lean-pr-testing · 2026-04-01T19:35:43Z

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-13229 has successfully built against this PR. (2026-04-01 19:35:41) View Log

mathlib-lean-pr-testing · 2026-04-01T22:00:45Z

Mathlib CI status (docs):

🟡 Mathlib branch lean-pr-testing-13229 build against this PR was cancelled. (2026-04-01 22:00:44) View Log

mathlib-lean-pr-testing · 2026-04-01T22:51:16Z

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-13229 has successfully built against this PR. (2026-04-01 22:51:14) View Log

…approach) This uses `withPosition commandParser` at the top level to enforce indentation in `by` blocks, combined with an empty-by fallback for better error messages. Compare with checkColPosGt approach in #13217. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

This adds a `notFollowedBy checkColGt` guard on the empty-by fallback in `tacticSeqIndentGt`. When indented non-tactic content follows `by`, this produces a tactic-level parse error ("expected '{' or tactic") rather than silently producing an empty tactic sequence. Also adds a comparison test for first-line vs second-line non-tactic errors. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

This reverts the `notFollowedBy checkColGt` guard on the empty-by fallback. Indented non-tactic content now consistently gets "unsolved goals" + "unexpected token; expected command", matching the behavior when non-tactic content appears on subsequent lines after a valid tactic. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

This adds server_interactive hover tests verifying that goal display works correctly when the empty-by `pushNone` fallback fires. Tests hovering on `by`, after `by`, and below an empty `by` block. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Move the pushNone fallback hover tests out of plainGoal.lean (which ends with an EOF test) into a dedicated plainGoalEmptyBy.lean test file. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

mathlib-lean-pr-testing · 2026-04-02T10:42:41Z

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-13229 has successfully built against this PR. (2026-04-02 10:42:39) View Log

Add `--⬑` test marker variant that targets the column of `--` itself (enabling column 0 tests, which `--^` cannot reach). Test tactic completion in empty `by` blocks for both top-level `by` (with `withPosition commandParser`) and nested `by` (inside `id <| have := by`). For each, test completion at various column positions: indented past `by`, at column 2, and at column 0. Current behavior: top-level empty `by` offers completions at all positions; nested empty `by` only offers completions when indented past the `by` token. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Add `--⬑` test marker variant that targets the column of `--` itself (enabling column 0 tests, which `--^` cannot reach). Add completion assertion mode: `--^ completion: has "skip"` checks that a completion item with the given label exists, and `--^ completion: is empty` checks that no completions are returned. This avoids logging the full completion JSON, making tests stable against docstring changes. Test tactic completion in empty `by` blocks for both top-level `by` and nested `by` (inside `id <| have := by`). For each, test completion at various column positions on the line below `by`: indented past `by`, at column 2, and at column 0. All positions currently offer tactic completions. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…ctives Remove the completion assertion mode (has/is empty) from the test runner and use plain `completion` directives in the empty-by tests instead. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

# Conflicts: # src/Lean/Server/Test/Runner.lean # tests/server_interactive/completionEmptyBy.lean # tests/server_interactive/completionEmptyBy.lean.out.expected

With strict `by` indentation, empty `by` blocks are now parsed successfully via `pushNone` instead of producing `.missing` syntax. This makes the `isEmptyBy` check in `goalsAt?` dead code — remove it. The `isEmpty` helper in `isSyntheticTacticCompletion` still works correctly because it handles both `.missing` and empty nodes from `pushNone` (via the vacuously-true `args.all isEmpty` on `#[]`). The `have : True := by` followed by a dedent now correctly puts `this` in scope in the outer tactic block. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…chim/body-indent

nomeata added the changelog-language Language features and metaprograms label Apr 1, 2026

nomeata changed the title ~~feat: use withPosition at command level for by indentation~~ feat: require indenentation in commands, allow empty tactic sequences Apr 1, 2026

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Apr 1, 2026

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 1, 2026

Update lean-toolchain for testing leanprover/lean4#13229

c0286d9

github-actions bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Apr 1, 2026

mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 1, 2026

Update lean-toolchain for testing leanprover/lean4#13229

b465a60

mathlib-lean-pr-testing bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Apr 1, 2026

nomeata changed the title ~~feat: require indenentation in commands, allow empty tactic sequences~~ feat: require indentation in commands, allow empty tactic sequences Apr 1, 2026

mathlib-lean-pr-testing 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 Apr 1, 2026

nomeata mentioned this pull request Apr 1, 2026

feat: enforce indentation of command contents #3215

Closed

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 1, 2026

Update lean-toolchain for leanprover/lean4#13229

645e49d

mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 1, 2026

Update lean-toolchain for leanprover/lean4#13229

7845a1a

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 1, 2026

Update lean-toolchain for leanprover/lean4#13229

21b86a5

mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 1, 2026

Update lean-toolchain for leanprover/lean4#13229

e533fde

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 1, 2026

Update lean-toolchain for leanprover/lean4#13229

6c58796

mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 1, 2026

Update lean-toolchain for leanprover/lean4#13229

37ec501

nomeata and others added 5 commits April 2, 2026 09:46

test: add test for empty-by fallback on indented non-tactic content

f5af89c

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

test: move empty-by hover tests to separate plainGoalEmptyBy file

bd665d1

Move the pushNone fallback hover tests out of plainGoal.lean (which ends with an EOF test) into a dedicated plainGoalEmptyBy.lean test file. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 2, 2026

Update lean-toolchain for leanprover/lean4#13229

7c36ea4

mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 2, 2026

Update lean-toolchain for leanprover/lean4#13229

3602bc0

nomeata and others added 5 commits April 2, 2026 11:00

refactor: revert completion assertion mode, use plain completion dire…

f85a6f3

…ctives Remove the completion assertion mode (has/is empty) from the test runner and use plain `completion` directives in the empty-by tests instead. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Merge branch 'joachim/emptyByCompletion' into joachim/body-indent

64250a5

# Conflicts: # src/Lean/Server/Test/Runner.lean # tests/server_interactive/completionEmptyBy.lean # tests/server_interactive/completionEmptyBy.lean.out.expected

nomeata force-pushed the joachim/body-indent branch from aa77588 to 04386e5 Compare April 2, 2026 12:46

nomeata mentioned this pull request Apr 2, 2026

feat: require indented tactic sequence after top-level by #13217

Closed

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 2, 2026

Update lean-toolchain for leanprover/lean4#13229

cc13c0b

nomeata added 2 commits April 3, 2026 06:19

Merge branch 'master' of https://github.com/leanprover/lean4 into joa…

6412dbd

…chim/body-indent

Some manual test tweaking

1fb734d

nomeata marked this pull request as ready for review April 3, 2026 06:37

nomeata requested a review from mhuisi as a code owner April 3, 2026 06:37

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: require indentation in commands, allow empty tactic sequences#13229

feat: require indentation in commands, allow empty tactic sequences#13229
nomeata wants to merge 13 commits intomasterfrom
joachim/body-indent

nomeata commented Apr 1, 2026 •

edited

Loading

Uh oh!

leanprover-bot commented Apr 1, 2026 •

edited

Loading

Uh oh!

mathlib-lean-pr-testing bot commented Apr 1, 2026 •

edited

Loading

Uh oh!

mathlib-lean-pr-testing bot commented Apr 1, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Apr 1, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Apr 1, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Apr 1, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Apr 1, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Apr 1, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Apr 2, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

nomeata commented Apr 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented Apr 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib-lean-pr-testing bot commented Apr 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib-lean-pr-testing bot commented Apr 1, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Apr 1, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Apr 1, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Apr 1, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Apr 1, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Apr 1, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Apr 2, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

nomeata commented Apr 1, 2026 •

edited

Loading

leanprover-bot commented Apr 1, 2026 •

edited

Loading

mathlib-lean-pr-testing bot commented Apr 1, 2026 •

edited

Loading