Fix #1146: require command_datatypes to be non-empty#1155
Merged
Conversation
The Core grammar declared command_datatypes as
op command_datatypes (datatypes : NewlineSepBy DatatypeDecl) : Command =>
datatypes ";\\n";
Without @[nonempty] on the field, NewlineSepBy compiles to a zero-or-more
parser, so the trailing ";\\n" production alone matched any stray
";" in the input. This is particularly easy to trip accidentally:
command_fndef's surface syntax has no trailing semicolon, so a user
writing "};" at the end of a function body (by analogy with procedures,
whose grammar does end in ";") silently produced a phantom
command_datatypes op with zero datatypes.
The phantom later tripped an explicit assertion in translateDatatypes:
"Datatype block must contain at least one datatype"
which calls panic!, producing a large backtrace at gen_smt_vcs time with
no useful source location.
Mark the datatypes field @[nonempty]. The stray ";" now surfaces as a
parse error at the point it actually appears, and the original repro
elaborates cleanly.
Add a regression test (StrataTest/Languages/Core/Tests/Issue1146Test.lean)
that pins the canonical form: a program mixing a datatype and a function
can run through gen_smt_vcs without panicking.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
fix-1146-empty-datatypes-command
branch
from
c3f45e4 to
2aaad36
Compare
Contributor
There was a problem hiding this comment.
Pull request overview
This PR fixes a parsing ambiguity in the Core dialect where command_datatypes could match an empty datatype block (i.e. only the trailing ;\n), allowing stray semicolons to be accepted and later triggering a panic during SMT VC generation (Issue #1146). The change tightens the grammar so datatype blocks must contain at least one datatype declaration, and adds a regression test to ensure a mixed datatype+function program no longer panics under gen_smt_vcs.
Changes:
- Require
command_datatypes’datatypeslist to be non-empty via@[nonempty]in the Core grammar. - Add a regression test ensuring
gen_smt_vcsdoesn’t panic on a program that combines a datatype declaration and a function definition.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 1 comment.
| File | Description |
|---|---|
| Strata/Languages/Core/DDMTransform/Grammar.lean | Makes command_datatypes reject empty NewlineSepBy DatatypeDecl parses by adding @[nonempty]. |
| StrataTest/Languages/Core/Tests/Issue1146Test.lean | Adds a regression test that exercises VC generation for a program containing both a datatype and a function. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
The regression test's doc comment described the pre-fix behaviour as a "large panic! backtrace". The ".github/scripts/checkNoPanic.sh" lint runs `grep -F 'panic!'` against added lines and flagged this as a net-new panic call, failing the PR's "Run lint checks (stable)" check. Rephrase the doc comment to describe the behaviour without the literal `panic!` token (the symbol actually lives in `TransM.error`, which still shows up there — unchanged by this PR). No code change; no behavioural change. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Address Copilot's review feedback on PR #1155: the previous Issue1146Test only pinned the positive path (canonical form + gen_smt_vcs succeeds). The original bug was that the stray ';' was silently accepted, so a future regression (e.g. someone removing @[nonempty] from command_datatypes' datatypes field) would not be caught by the positive test alone. Replace the negative-case doc comment with an active #guard_msgs check that elaborates the exact form from issue #1146 (datatype + function with trailing '};') and pins the parser's diagnostic message. Removing the @[nonempty] annotation now fails this test at elaboration time instead of only manifesting at gen_smt_vcs. The pattern '#guard_msgs in def ... := #strata ... #end' is already standard in Core tests — e.g. StrataTest/Languages/Core/Examples/ TypeAlias.lean:18 and StrataTest/Languages/Core/Tests/ PolymorphicDatatypeTest.lean:572 — and my earlier 'would need custom infrastructure' rationale was mistaken. Message stability is flagged inline: the text enumerates valid continuations at that source position, so a new top-level command production in the Core grammar would require updating the expected message. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
joscoh
reviewed
May 15, 2026
Four follow-ups to the PR review thread: 1. Grammar.lean: shrink the 8-line motivation block to a one-line "@[nonempty] is load-bearing: see #1146" reference. The full explanation now lives in the test file alongside the regression itself. 2. Issue1146Test.lean module docstring: drop the before/after history and restate the test's purpose statelessly — what the tests currently exercise rather than how the code used to behave. 3. Replace the "example : smtVCsCorrect ... := by gen_smt_vcs" success case with the canonical Core test idiom "TransM.run Inhabited.default (translateProgram p) |>.snd |>.isEmpty" from Strata.Languages.Core.DDMTransform.Translate. The panic the regression catches was inside translateDatatypes, which translateProgram calls directly, so this is functionally equivalent and matches the rest of StrataTest/Languages/Core/Tests/. Drops the transitive Strata.MetaVerifier import. 4. Drop the meta-commentary about how the parse-error message would change if a new top-level command production were added. The #guard_msgs-pinned assertion is the active contract; the prose describing its brittleness is unnecessary. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
joscoh
approved these changes
May 16, 2026
aqjune-aws
approved these changes
May 18, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The Core grammar declared command_datatypes as
op command_datatypes (datatypes : NewlineSepBy DatatypeDecl) : Command =>
datatypes ";\n";
Without @[nonempty] on the field, NewlineSepBy compiles to a zero-or-more parser, so the trailing ";\n" production alone matched any stray ";" in the input. This is particularly easy to trip accidentally: command_fndef's surface syntax has no trailing semicolon, so a user writing "};" at the end of a function body (by analogy with procedures, whose grammar does end in ";") silently produced a phantom command_datatypes op with zero datatypes.
The phantom later tripped an explicit assertion in translateDatatypes:
"Datatype block must contain at least one datatype"
which calls panic!, producing a large backtrace at gen_smt_vcs time with no useful source location.
Mark the datatypes field @[nonempty]. The stray ";" now surfaces as a parse error at the point it actually appears, and the original repro elaborates cleanly.
Add a regression test (StrataTest/Languages/Core/Tests/Issue1146Test.lean) that pins the canonical form: a program mixing a datatype and a function can run through gen_smt_vcs without panicking.
Fixes: #1146
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.