fix: REPL name resolution to match lake build context (#149)#151
Open
LarsenClose wants to merge 1 commit intomainfrom
Open
fix: REPL name resolution to match lake build context (#149)#151LarsenClose wants to merge 1 commit intomainfrom
LarsenClose wants to merge 1 commit intomainfrom
Conversation
Two root causes of REPL/lake build divergence: 1. split_header_body incorrectly treated open, namespace, section, set_option, and variable as body separators. These context-establishing commands now remain in the REPL header so the header environment includes the same namespace openings, options, and variables that lake build sees. 2. lean_verify only checked diagnostics from the #print axioms region, ignoring compilation errors in the file itself. A file with errors (e.g. sorry, unknown identifiers) could pass verification because only the appended #print axioms line was checked. Now collects ALL diagnostics and fails if the original file has compilation errors.
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
2 participants
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.
Closes #149
Summary
split_header_bodyfix: Removedopen,namespace,section,set_option, andvariablefrom the declaration-keyword list that triggers header/body splitting. These context-establishing commands now remain in the REPL header environment, ensuring the REPL sees the same namespace openings, options, and variables thatlake builddoes. Previously, they were placed in the body, causing the cached header env to lack the correct elaboration context.lean_verifyfile error detection: Changedhandle_verifyto collect ALL diagnostics (not just from the#print axiomsappended region). If the original file has compilation errors (e.g.,sorry, unknown identifiers), verification now correctly fails instead of silently passing. File errors are reported with priority over axiom-region errors.Tests: Added 7 new tests for
split_header_bodycoveringopen,namespace,section,set_option,variable, and combined multi-context scenarios. Added a newhandle_verify_detects_file_compilation_errorstest. Updated existing verify tests to includerangeinformation for correct line-based filtering.Test plan
cargo test --all)cargo fmt --all -- --checkpassescargo clippy --all-targets -- -D warningspassesRUSTDOCFLAGS="-D warnings" cargo doc --workspace --no-depspassessplit_header_body_open_in_header— verifiesopenstays in headersplit_header_body_namespace_in_header— verifiesnamespacestays in headersplit_header_body_set_option_in_header— verifiesset_optionstays in headersplit_header_body_variable_in_header— verifiesvariablestays in headersplit_header_body_section_in_header— verifiessectionstays in headersplit_header_body_multiple_context_lines— verifies combined context in headerhandle_verify_detects_file_compilation_errors— verifies file errors block verification