fix(ci): Update Strata/StrataDDM pins, fix CBMC path, adapt to API changes#9
Draft
robin-aws wants to merge 4 commits into
Draft
fix(ci): Update Strata/StrataDDM pins, fix CBMC path, adapt to API changes#9robin-aws wants to merge 4 commits into
robin-aws wants to merge 4 commits into
Conversation
…anges - Bump Strata to ee0b2ecb (latest main with all CI fixes) - Bump StrataDDM to 4ea13cd3 (adds noExponent, Hashable for Decimal) - Fix cbmc-bounds-check.patch path (moved to CBMC/ subdirectory) - Move InterpretTests.lean to StrataPythonTestExtra (requires Python) - Add missing Pure case to fmtHighType in ToLaurelTest.lean
robin-aws
marked this pull request as draft
July 22, 2026 19:57
Tools/Python-base was deleted and Tools/strata-python was moved to Python/strata-python in commit 4b2d5f0, but the CI workflows were not updated. The strata base dependency is not available on PyPI (it's provided by StrataDDM on Brazil), so we use --no-deps.
These tests were ported to in-process Lean tests (SarifTest.lean, RegexDiffTest.lean) in commit 4b2d5f0 and the Python scripts were deleted, but the CI steps were not removed.
The strata base package (DDM datatypes + Ion serialization) was deleted in 4b2d5f0 because on Brazil it's provided by StrataDDM's runtime farm. On GitHub CI, the Python tests need it installed locally. Restore it at Python/strata-base/ and install both packages in CI.
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
1 participant
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 CI failures caused by stale dependency pins and path changes from the Strata repo restructuring.
Changes
ee0b2ecb(latest main, includes all CI fixes from fix(ci): Missing edits, lake update Strata#1440)4ea13cd3(addsnoExponentmetadata,Hashable for Decimal)cbmc-bounds-check.patchmoved toCBMC/subdirectory in StrataInterpretTests.leanfromStrataPythonTest/CI/toStrataPythonTestExtra/CI/(requires Python runtime, which isn't available during the compile-time test phase)Purecase tofmtHighTypeinToLaurelTest.lean(newHighTypeconstructor added in Strata)Verification
lake build StrataPython StrataPythonTestsucceeds locally (259 jobs)Supersedes #7 (includes those changes plus additional fixes).