Convert remaining Lean files under /Strata to modules#982
Merged
Conversation
joehendrix
force-pushed
the
jhx/strata_module
branch
from
1a7ebd6 to
d54a5e8
Compare
joehendrix
force-pushed
the
jhx/strata_module
branch
from
d54a5e8 to
50f961b
Compare
joehendrix
changed the title
joehendrix
changed the title
Add public visibility annotations to definitions and instances in TestGen.lean and Verifier.lean that are needed by test files. Add Strata.Util.Random import to TestGenTests.lean. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
joehendrix
force-pushed
the
jhx/strata_module
branch
from
50f961b to
20baf2c
Compare
shigoel
approved these changes
Apr 21, 2026
Contributor
shigoel
left a comment
shigoel
left a comment
There was a problem hiding this comment.
Looks good — thorough, well-documented mechanical migration. CI is green, import all / public section / @[expose] usage is consistent with existing codebase patterns. No functional changes, no new API surface concerns. Nice work.
joscoh
approved these changes
Apr 21, 2026
Contributor
joscoh
left a comment
joscoh
left a comment
There was a problem hiding this comment.
Nothing blocking, just have a few questions about how public and private modifiers work in certain cases.
keyboardDrummer
pushed a commit
to keyboardDrummer/Strata
that referenced
this pull request
May 21, 2026
Migrate 241 of 282 non-Boole StrataTest files to be Lean modules, completing the module migration started in strata-org#982. - **Added `module` keyword** to 241 test files. The Boole test files are excluded because `gen_smt_vcs` produces proof terms that fail kernel type-checking when the file is a module. - **Added `meta import`** for Strata/StrataTest dependencies where `#eval`, `#guard_msgs`, or `#guard` need native implementations from the imported module. - **Added `meta import all`** where proofs use `simp`, `rfl`, or `native_decide` on definitions whose bodies must be visible across the module boundary. - **Added `import all`** where non-meta definitions (types, instances) need access to definition bodies from other StrataTest modules. - **Added `meta section` wrappers** around test code that exercises native implementations, since `#eval`/`#guard_msgs`/`#guard` require meta context to call into compiled code from another module. - **Added `import Strata.DDM.Integration.Lean.HashCommands`** (non-meta) in files using `#strata`/`#dialect` syntax, since the syntax extension must be available at parse time regardless of meta context. - **Updated byte offsets** in `#guard_msgs` docstrings where expected output includes position-dependent labels (e.g., invariant names derived from source positions shifted by added import lines). By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
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
3 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.
Summary
Convert 49 of the 50 remaining non-module
.leanfiles to use the Leanmodulekeyword,making
StrataMainand nearly all files underStrata/proper Lean modules.Changes
Added
modulekeyword to 49 files across all subsystems (CBMC, B3, Boole, C_Simp,Core, Dyn, DL, Transform, Util, MetaVerifier, StrataMain).
Added
public sectionblocks for files that export types or functions used bydownstream consumers. Used
public importwith minimal scope (e.g.public import Lean.Data.Json.Basicrather thanpublic import Lean.Data.Json) tokeep transitive exports narrow.
Added
@[expose]annotations to a handful of upstream definitions(
ListUtils.lean,CmdSemantics.lean,StatementSemantics.lean,ProcBodyVerify.lean,CoreSpecification.lean,Specification.lean) where proof files needed to unfolddefinitions across module boundaries.
MetaVerifier: Moved
metatactic registration outside the mainpublic sectioninto its own
public sectionto satisfy the requirement that tactic elaborationattributes are public.
StrataMain: Added explicit imports for modules that were previously accessible
transitively but became inaccessible once StrataMain became a module.
Not converted
Strata.Languages.C_Simp.StrataToCBMC— has pre-existing build errors (referencesnon-existent
CProverJsonnamespace). Nothing imports this file.Files changed by subsystem
Strata.Backends.CBMCStrata.DL.ImperativeStrata.DL.LambdaStrata.DL.SMTStrata.Languages.B3Strata.Languages.BooleStrata.Languages.C_SimpStrata.Languages.CoreStrata.Languages.DynStrata.MetaVerifierStrata.TransformStrata.UtilStrataMainBy submitting this pull request, I confirm that you can use, modify, copy, and
redistribute this contribution, under the terms of your choice.