Conversation
Port the Python-specific CI from the Strata monorepo into this standalone repository, adapted for its layout (StrataPython is the repo root). Fix the Strata dependency: the lakefile required `Strata` at `..`, which does not exist in the standalone repo. Change it to a git require so lake clones Strata; the manifest pins the current Strata SHA. Workflows: - ci.yml: build_and_test_lean (Python steps), check_pending_python, lint_checks, and the build_python matrix (3.11-3.14). - cbmc.yml: build CBMC from source with the in-repo string-support patch plus the Laurel/regex/quantifier patches from the cloned Strata package, then run the Python CBMC pipeline tests. Port the composite actions (install-cvc5/z3, lint actions, lake cache) and lint scripts, plus CODEOWNERS, dependabot, and a PR template. Remove the StrataCLI dependency from the CPython differential test: the old run_test.sh used the `strata` CLI only for an Ion round-trip check. Move that work into a new Lean test, StrataPythonTestExtra/CpythonDiffTest, which does the round-trip in-process via the Strata library. run_cpython_tests.sh keeps the orchestration (clone CPython, pick the version, compute expected failures) and drives the Lean test; run_test.sh is removed. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The cache key included hashFiles('**/*.st'), which is empty at restore
(downstream jobs run before .lake exists) but non-empty at save (the
build_and_test_lean job populates .lake, and the cloned Strata git
dependency brings .st files under it). The mismatched keys made every
downstream job fail at restore with fail-on-cache-miss.
Drop the **/*.st component from both restore-lake-cache and
save-lake-cache. This repo has no committed .st files, and the cloned
dependency is already pinned by the lake-manifest.json hash in the key.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
robin-aws
reviewed
Jun 9, 2026
shigoel
reviewed
Jun 9, 2026
atomb
requested changes
Jun 9, 2026
atomb
left a comment
atomb
left a comment
Contributor
There was a problem hiding this comment.
This mostly looks good, but I think the actions could be simplified.
atomb
reviewed
Jun 9, 2026
atomb
reviewed
Jun 9, 2026
- build_python: replace the hand-rolled z3 install (pip + pinned 4.13.4 wget fallback) with the install-z3 action (install-to: system), matching the cvc5 step and removing version drift. Only the z3 binary is needed; nothing imports the z3 Python module. - run_cpython_tests.sh: use mise's lowercase `python@<ver>` tool name so it resolves for local dev (CI is unaffected; mise isn't installed there and it falls back to python3). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Replace the vendored composite actions (install-cvc5, install-z3, check-copyright-headers, lint-whitespace, check-lean-import, check-no-panic) with strata-org/Strata/.github/actions/<name>@main references, and delete the local copies and their backing scripts. This removes the duplication called out in review. lint-whitespace gets an explicit `directory: .` since its Strata default is `Strata`, which does not exist in this repo's layout. Keep restore-lake-cache and save-lake-cache local: the Strata versions hash `**/*.st` in the cache key, which is unstable here because the cloned Strata dependency drops .st files under .lake between restore and save, breaking fail-on-cache-miss. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
atomb
approved these changes
Jun 9, 2026
shigoel
approved these changes
Jun 9, 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
4 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.
Port the Python-specific CI from the Strata monorepo into this standalone repository, adapted for its layout (StrataPython is the repo root).
Dependency fix
The lakefile required
Strataatpath = "..", which doesn't exist in the standalone repo. Changed it to a git require so lake clones Strata; the manifest pins the current Strata SHA. Verifiedlake build StrataPythonsucceeds against the cloned dependency.Workflows
ci.yml— four jobs, paths collapsed (noStrataPython/prefix):build_and_test_lean— build StrataPython + compile-time tests, then pyInterpret / pyAnalyze-SARIF / pyAnalyze golden-file / regex-differential tests.check_pending_python—run_py_analyze.sh --check-pending.lint_checks— copyright headers, whitespace, bareimport Lean, net-newpanic!.build_python— 3.11–3.14 matrix: PySpec/dispatch tests + CPython differential tests.cbmc— reusable workflow.cbmc.yml— build CBMC from source with the in-repocbmc-string-support.patchplus the Laurel/regex/quantifier patches from the cloned Strata package, then run the Python CBMC pipeline tests only.Dropped non-Python steps (.NET/BoogieToStrata, Java codegen, docs, examples, C_Simp/Laurel CBMC).
Removing the StrataCLI dependency
The old CPython differential test (
run_test.sh) used the LeanstrataCLI only for an Ion round-trip check (toIon+diff). Rather than build a separate StrataCLI package in the standalone repo, that work moved into a new Lean test,StrataPythonTestExtra/CpythonDiffTest.lean, which does the round-trip in-process via the Strata library (Program.fromIon→ re-serialize → re-read → compare commands).run_cpython_tests.shkeeps the orchestration (clone CPython, pick the version, compute expected failures) and drives the Lean test via env vars (CPYTHON_DIR,CPYTHON_EXPECTED_FAILURESplaintext list,CPYTHON_FAIL_FAST).run_test.shis removed.Scaffolding
Ported the composite actions (install-cvc5/z3, lint actions, lake cache) and lint scripts, plus CODEOWNERS, dependabot, and a PR template.