Skip to content

Commit b98d072

Browse files
MegaRedHandMegaRedHand
committed
ci: add Lean tests to CI
1 parent 975a304 commit b98d072

File tree

1 file changed

+144
-4
lines changed

1 file changed

+144
-4
lines changed

‎.github/workflows/ci.yml‎

Lines changed: 144 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ jobs:
2424
- uses: actions/checkout@v6
2525

2626
- name: Setup Rust
27-
uses: dtolnay/rust-toolchain@master
27+
uses: dtolnay/rust-toolchain@stable
2828
with:
2929
toolchain: "1.92.0"
3030
components: rustfmt, clippy
@@ -54,7 +54,7 @@ jobs:
5454

5555
- name: Cache test fixtures
5656
id: cache-fixtures
57-
uses: actions/cache@v4
57+
uses: actions/cache@v5
5858
with:
5959
path: leanSpec/fixtures
6060
key: leanspec-fixtures-${{ steps.lean-spec.outputs.commit }}
@@ -93,7 +93,7 @@ jobs:
9393
- name: Cache production keys
9494
if: steps.cache-fixtures.outputs.cache-hit != 'true'
9595
id: cache-prod-keys
96-
uses: actions/cache@v4
96+
uses: actions/cache@v5
9797
with:
9898
path: leanSpec/packages/testing/src/consensus_testing/test_keys/prod_scheme
9999
key: prod-keys-${{ steps.prod-keys-url.outputs.hash }}
@@ -114,7 +114,7 @@ jobs:
114114
run: touch leanSpec/fixtures
115115

116116
- name: Setup Rust
117-
uses: dtolnay/rust-toolchain@master
117+
uses: dtolnay/rust-toolchain@stable
118118
with:
119119
toolchain: "1.92.0"
120120

@@ -123,3 +123,143 @@ jobs:
123123

124124
- name: Run tests
125125
run: make test
126+
127+
lean-build:
128+
name: Build Lean
129+
runs-on: ubuntu-latest
130+
steps:
131+
- uses: actions/checkout@v6
132+
133+
- name: Install elan
134+
run: |
135+
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
136+
echo "$HOME/.elan/bin" >> $GITHUB_PATH
137+
138+
- name: Cache Lake packages
139+
uses: actions/cache@v5
140+
with:
141+
path: |
142+
~/.elan
143+
formal/.lake
144+
key: ${{ runner.os }}-lake-${{ hashFiles('formal/lean-toolchain', 'formal/lakefile.toml', 'formal/lake-manifest.json') }}
145+
restore-keys: |
146+
${{ runner.os }}-lake-
147+
148+
- name: Fetch Mathlib cache
149+
working-directory: formal
150+
run: lake exe cache get
151+
152+
- name: Build both libraries
153+
working-directory: formal
154+
run: lake build
155+
156+
- name: Verify zero sorries
157+
working-directory: formal
158+
run: |
159+
if grep -rn "sorry" EthLambda/ EthLambdaProofs/ --include="*.lean"; then
160+
echo "::error::Found sorry in Lean sources"
161+
exit 1
162+
fi
163+
164+
lean-ffi-test:
165+
name: Test with Lean FFI
166+
runs-on: ubuntu-latest
167+
needs: [lean-build, test]
168+
steps:
169+
- uses: actions/checkout@v6
170+
171+
- name: Install elan
172+
run: |
173+
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
174+
echo "$HOME/.elan/bin" >> $GITHUB_PATH
175+
176+
# Reuse the Lake cache from the lean-build job
177+
- name: Cache Lake packages
178+
uses: actions/cache@v5
179+
with:
180+
path: |
181+
~/.elan
182+
formal/.lake
183+
key: ${{ runner.os }}-lake-${{ hashFiles('formal/lean-toolchain', 'formal/lakefile.toml', 'formal/lake-manifest.json') }}
184+
restore-keys: |
185+
${{ runner.os }}-lake-
186+
187+
# Read the pinned leanSpec commit from the Makefile (single source of truth)
188+
- name: Get leanSpec pinned commit
189+
id: lean-spec
190+
run: echo "commit=$(sed -n 's/^LEAN_SPEC_COMMIT_HASH:= *//p' Makefile)" >> $GITHUB_OUTPUT
191+
192+
# Reuse the fixtures cache from the test job
193+
- name: Cache test fixtures
194+
id: cache-fixtures
195+
uses: actions/cache@v5
196+
with:
197+
path: leanSpec/fixtures
198+
key: leanspec-fixtures-${{ steps.lean-spec.outputs.commit }}
199+
200+
# All fixture generation steps are skipped when the cache hits
201+
- name: Checkout leanSpec at pinned commit
202+
if: steps.cache-fixtures.outputs.cache-hit != 'true'
203+
uses: actions/checkout@v6
204+
with:
205+
repository: leanEthereum/leanSpec
206+
ref: ${{ steps.lean-spec.outputs.commit }}
207+
path: leanSpec
208+
209+
- name: Install uv and Python 3.14
210+
if: steps.cache-fixtures.outputs.cache-hit != 'true'
211+
uses: astral-sh/setup-uv@v4
212+
with:
213+
enable-cache: true
214+
cache-dependency-glob: "leanSpec/pyproject.toml"
215+
python-version: "3.14"
216+
217+
- name: Sync leanSpec dependencies
218+
if: steps.cache-fixtures.outputs.cache-hit != 'true'
219+
working-directory: leanSpec
220+
run: uv sync --no-progress
221+
222+
- name: Get production keys URL hash
223+
if: steps.cache-fixtures.outputs.cache-hit != 'true'
224+
id: prod-keys-url
225+
working-directory: leanSpec
226+
run: |
227+
URL=$(uv run python -c "from consensus_testing.keys import KEY_DOWNLOAD_URLS; print(KEY_DOWNLOAD_URLS['prod'])")
228+
HASH=$(echo -n "$URL" | sha256sum | awk '{print $1}')
229+
echo "hash=$HASH" >> $GITHUB_OUTPUT
230+
231+
- name: Cache production keys
232+
if: steps.cache-fixtures.outputs.cache-hit != 'true'
233+
id: cache-prod-keys
234+
uses: actions/cache@v5
235+
with:
236+
path: leanSpec/packages/testing/src/consensus_testing/test_keys/prod_scheme
237+
key: prod-keys-${{ steps.prod-keys-url.outputs.hash }}
238+
239+
- name: Download production keys
240+
if: steps.cache-fixtures.outputs.cache-hit != 'true' && steps.cache-prod-keys.outputs.cache-hit != 'true'
241+
working-directory: leanSpec
242+
run: uv run python -m consensus_testing.keys --download --scheme prod
243+
244+
- name: Generate test fixtures
245+
if: steps.cache-fixtures.outputs.cache-hit != 'true'
246+
working-directory: leanSpec
247+
run: uv run fill --fork=Devnet --scheme prod -o fixtures -n 2
248+
249+
- name: Mark fixtures as up-to-date
250+
run: touch leanSpec/fixtures
251+
252+
- name: Setup Rust
253+
uses: dtolnay/rust-toolchain@stable
254+
with:
255+
toolchain: "1.92.0"
256+
components: clippy
257+
258+
- name: Setup Rust cache
259+
uses: Swatinem/rust-cache@v2
260+
261+
- name: Clippy (lean-ffi)
262+
run: cargo clippy -p ethlambda-lean-ffi -- -D warnings
263+
264+
- name: Test with lean-ffi
265+
run: cargo test --workspace --release --features lean-ffi

0 commit comments

Comments
 (0)