Skip to content

Commit ed25c0a

Browse files
joehendrixclaude
joehendrix
and
claude
authored
Add CI for standalone StrataPython repo (#1)
* Add CI for standalone StrataPython repo 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> * Fix lake cache key instability across jobs 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> * Address PR review: dedup z3 install, lowercase mise tool name - 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> * Reference shared actions from Strata repo instead of vendoring 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> --------- Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
1 parent 9b4da02 commit ed25c0a

12 files changed

Lines changed: 649 additions & 126 deletions

File tree

‎.github/CODEOWNERS‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
# Defaults owners for everything in the repo. unless a later match
2+
# takes precedence
3+
* @strata-org/reviewers

‎.github/actions/restore-lake-cache/action.yml‎

Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,76 @@
1+
# Copyright Strata Contributors
2+
# SPDX-License-Identifier: Apache-2.0 OR MIT
3+
name: Restore lake cache
4+
description: >
5+
Thin wrapper around actions/cache/restore@v5 using the cache key
6+
lake-<os>-<arch>-<lean-toolchain>-<lake-manifest>-<sha>
7+
with two fallback keys dropping each trailing component in turn. The
8+
manifest hash covers the cloned Strata dependency.
9+
inputs:
10+
fail-on-cache-miss:
11+
description: >
12+
If 'true', the step fails when no cache entry matches. Use this in
13+
jobs that depend on a cache saved by an upstream job for the same
14+
SHA (see https://github.com/strata-org/Strata/issues/952).
15+
required: false
16+
default: "false"
17+
path:
18+
description: Cache path(s), newline-separated.
19+
required: false
20+
default: ".lake"
21+
key-prefix:
22+
description: >
23+
Prefix used in the cache key. The action also hashes the
24+
repo-root `lean-toolchain` and `lake-manifest.json`, so changing
25+
only this prefix is appropriate for caches keyed on the same
26+
root-level Lean build (e.g. distinguishing different artifact
27+
names with the same source set). Sub-projects with their own
28+
toolchain/manifest do not currently fit this action and should
29+
not reuse it as-is.
30+
required: false
31+
default: "lake"
32+
use-restore-keys:
33+
description: >
34+
Must be the string `'true'` or `'false'`.
35+
36+
If `'true'` (default), include two fallback `restore-keys` so
37+
that a near match (same toolchain/manifest but different SHA) is
38+
used when no exact-SHA cache exists.
39+
40+
Set to `'false'` for downstream jobs that depend on a cache saved
41+
by an upstream job for the *same* SHA (typically together with
42+
`fail-on-cache-miss: 'true'`); see
43+
https://github.com/strata-org/Strata/issues/952. With fallback
44+
keys present, `fail-on-cache-miss` only triggers when every
45+
fallback also misses, which silently allows stale cross-SHA cache
46+
matches and defeats the safety net.
47+
required: false
48+
default: "true"
49+
50+
outputs:
51+
cache-hit:
52+
description: Whether a cache entry was restored (see actions/cache/restore@v5).
53+
value: ${{ steps.restore-with-fallback.outputs.cache-hit || steps.restore-exact.outputs.cache-hit }}
54+
55+
runs:
56+
using: composite
57+
steps:
58+
- name: Restore lake cache (with fallback keys)
59+
id: restore-with-fallback
60+
if: inputs.use-restore-keys != 'false'
61+
uses: actions/cache/restore@v5
62+
with:
63+
path: ${{ inputs.path }}
64+
key: ${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
65+
restore-keys: |
66+
${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
67+
${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}
68+
fail-on-cache-miss: ${{ inputs.fail-on-cache-miss }}
69+
- name: Restore lake cache (exact SHA only)
70+
id: restore-exact
71+
if: inputs.use-restore-keys == 'false'
72+
uses: actions/cache/restore@v5
73+
with:
74+
path: ${{ inputs.path }}
75+
key: ${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
76+
fail-on-cache-miss: ${{ inputs.fail-on-cache-miss }}

‎.github/actions/save-lake-cache/action.yml‎

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
# Copyright Strata Contributors
2+
# SPDX-License-Identifier: Apache-2.0 OR MIT
3+
name: Save lake cache
4+
description: >
5+
Save the lake build cache.
6+
Companion to `restore-lake-cache`: the two actions share the same key
7+
construction so downstream jobs that consume the saved cache via
8+
`restore-lake-cache` with `use-restore-keys: "false"` will hit it
9+
reliably.
10+
11+
Use this in workflows that produce a fresh build (typically the
12+
`build_and_test_lean` job in ci.yml) to share the result with
13+
downstream jobs at the same SHA.
14+
15+
inputs:
16+
path:
17+
description: Cache path(s), newline-separated.
18+
required: false
19+
default: ".lake"
20+
key-prefix:
21+
description: >
22+
Cache-key prefix; must match the `key-prefix` passed to the
23+
companion `restore-lake-cache` action so that the exact-SHA
24+
restore keys line up.
25+
required: false
26+
default: "lake"
27+
28+
runs:
29+
using: composite
30+
steps:
31+
- name: Save lake cache
32+
uses: actions/cache/save@v5
33+
with:
34+
path: ${{ inputs.path }}
35+
key: ${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}

‎.github/dependabot.yml‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
# https://docs.github.com/en/code-security/dependabot/dependabot-version-updates/configuration-options-for-the-dependabot.yml-file
2+
3+
version: 2
4+
updates:
5+
- package-ecosystem: "github-actions"
6+
directory: "/"
7+
schedule:
8+
interval: "weekly"

‎.github/pull_request_template.md‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
### Description
2+
3+
<!-- Briefly describe what this PR changes and why. -->
4+
5+
### Checklist
6+
7+
- [ ] `lake build StrataPython StrataPythonTest` succeeds locally
8+
- [ ] New `.lean` files start with the standard copyright header
9+
- [ ] No trailing whitespace and files end with a newline

‎.github/workflows/cbmc.yml‎

Lines changed: 72 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,72 @@
1+
name: CBMC
2+
3+
on:
4+
workflow_call:
5+
6+
jobs:
7+
cbmc_test:
8+
name: Run CBMC tests
9+
runs-on: ubuntu-latest
10+
permissions:
11+
contents: read
12+
steps:
13+
- name: Checkout
14+
uses: actions/checkout@v6
15+
- name: Install cvc5
16+
uses: strata-org/Strata/.github/actions/install-cvc5@main
17+
- name: Install z3
18+
uses: strata-org/Strata/.github/actions/install-z3@main
19+
- name: Restore lake cache
20+
# The cache is safe to use here because we just saved it for this exact
21+
# SHA in the build_and_test_lean job from ci.yml. Restoring it also
22+
# brings back the cloned Strata dependency under .lake/packages/Strata,
23+
# which holds the Laurel/regex/quantifier CBMC patches applied below.
24+
# https://github.com/strata-org/Strata/issues/952
25+
uses: ./.github/actions/restore-lake-cache
26+
with:
27+
path: .lake
28+
fail-on-cache-miss: "true"
29+
use-restore-keys: "false"
30+
- name: Prepare ccache
31+
uses: actions/cache@v5
32+
with:
33+
save-always: true
34+
path: .ccache
35+
key: cbmc-${{ runner.os }}-${{ runner.arch }}-cbmc-${{ github.sha }}
36+
restore-keys: |
37+
cbmc-${{ runner.os }}-${{ runner.arch }}-cbmc
38+
- name: Build CBMC from source (with string support patch)
39+
shell: bash
40+
run: |
41+
sudo apt-get -qq update
42+
sudo apt-get -qq install -y cmake ninja-build flex bison ccache
43+
git clone --depth 1 --branch cbmc-6.8.0 https://github.com/diffblue/cbmc.git cbmc-src
44+
cd cbmc-src
45+
STRATA="$GITHUB_WORKSPACE/.lake/packages/Strata"
46+
git apply "$GITHUB_WORKSPACE/StrataPythonTest/cbmc-string-support.patch"
47+
git apply "$STRATA/StrataTest/Languages/Laurel/cbmc-bounds-check.patch"
48+
git apply "$STRATA/StrataTest/Backends/CBMC/cbmc-regex-support.patch"
49+
git apply "$STRATA/StrataTest/Backends/CBMC/cbmc-quantifier-simplify.patch"
50+
export CCACHE_BASEDIR=$PWD
51+
export CCACHE_DIR=$GITHUB_WORKSPACE/.ccache
52+
cmake -S . -B build -G Ninja \
53+
-DCMAKE_BUILD_TYPE=Release \
54+
-DWITH_JBMC=OFF
55+
ccache -z --max-size=500M
56+
ninja -C build cbmc symtab2gb goto-cc goto-instrument
57+
ccache -s
58+
echo "$GITHUB_WORKSPACE/cbmc-src/build/bin/" >> $GITHUB_PATH
59+
- name: Build StrataPython
60+
uses: leanprover/lean-action@v1
61+
with:
62+
auto-config: false
63+
build: true
64+
use-github-cache: false
65+
- uses: actions/setup-python@v6
66+
with:
67+
python-version: '3.14'
68+
- name: Run Python CBMC pipeline tests
69+
shell: bash
70+
run: |
71+
pip install ./.lake/packages/Strata/Tools/Python-base ./Tools/strata-python
72+
./StrataPythonTest/run_py_cbmc_tests.sh

0 commit comments

Comments
 (0)