Fix missing source locations in Python → Laurel translation#843
Merged
Conversation
Three fixes in PythonToLaurel.lean:
1. Return type constraint ensures: Use retTy.ann (the actual return type
expression's source range) instead of returns.ann (the Ann wrapper's
annotation, which is {0,0}).
2. For-loop assume statements: Use mkStmtExprMdWithLoc with md for the
PIn/Any_to_bool assumes and range-based loop checks, instead of
mkStmtExprMd which uses defaultMetadata (unknown location).
3. Return statement: Use mkStmtExprMdWithLoc with md for the LaurelResult
assignment and exit statements.
Updated all expected_laurel test files to reflect the new source locations.
Fixes #842
tautschnig
reviewed
Apr 11, 2026
Address review nit: use f.ann (the FunctionDef's own source range) instead
of returns.ann for the __init__ branch, avoiding the DDM wrapper's {0,0}
source range.
…842-add-missing-source-locations
The merge from main brought in test_for_else_break and test_list_empty which had 'unknown location' in their expected output. Regenerated these files to reflect the correct source locations from our fix.
Collaborator
Author
|
The CI failure was caused by the branch being behind Fix: Merged Verified locally:
|
tautschnig
approved these changes
Apr 12, 2026
MikaelMayer
approved these changes
Apr 13, 2026
Contributor
MikaelMayer
left a comment
There was a problem hiding this comment.
Thank you very much !!
keyboardDrummer-bot
added a commit
that referenced
this pull request
Apr 14, 2026
Conflicts in expected test output files resolved by combining: - main's source location fixes from PR #843 (unknown location → actual locations) - this PR's line number changes from explicit source location propagation
This was referenced Apr 14, 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.
Summary
Fixes #842 — Adds missing source location metadata in
PythonToLaurel.leanso that diagnostics in theexpected_laureltests no longer report "unknown location".Root Cause
Three places in
PythonToLaurel.leanwere producing nodes withdefaultMetadata(which hasFileRange.unknown) instead of passing through the source location from the Python AST:Return type constraint ensures —
pyFuncDefToPythonFunctionDeclusedreturns.ann(theAnnwrapper's annotation, which is{0,0}for DDM-generated optional fields) instead ofretTy.ann(the actual return type expression's source range).For-loop assume statements — The
PIn,Any_to_bool, and range-checkAssumenodes in theForcase oftranslateStmtusedmkStmtExprMd(unknown location) instead ofmkStmtExprMdWithLocwith the for-statement'smd.Return statement — The
LaurelResultassignment andExit "$body"in theReturncase usedmkStmtExprMdinstead ofmkStmtExprMdWithLocwith the return-statement'smd.Changes
Strata/Languages/Python/PythonToLaurel.lean— 3 targeted fixes (described above)StrataTest/Languages/Python/expected_laurel/*.expected— 15 test expectation files updated (allunknown location:prefixes replaced with actualfile(line, col):locations)Verification
lake buildsucceedsrun_py_analyze.shpasses all testsgrep "^unknown location:" expected_laurel/*.expectedreturns zero matches