max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: use Lake remote cache in CI (#10880)

Browse source 
This PR alters the `Linux Lake` CI job to enable the Lake cache and
upload the builds results to the remote cache storage. It also adds a
`Linux Lake (Cached)` secondary build job which fetches a build from the
Lake remote cache (if possible) and tests it.

---------

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This commit is contained in:
Mac Malone 2026-03-23 20:06:19 -04:00 • committed by GitHub
parent e6df474dd9
commit c381c62060
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 48 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

35
.github/workflows/build-template.yml vendored
View file

@ -78,7 +78,7 @@ jobs:
# (needs to be after "Install *" to use the right shell)
- name: CI Merge Checkout
run: |
git fetch --depth=1 origin ${{ github.sha }}
git fetch --depth=${{ matrix.name == 'Linux Lake (Cached)' && '10' || '1' }} origin ${{ github.sha }}
git checkout FETCH_HEAD flake.nix flake.lock script/prepare-* tests/elab/importStructure.lean
if: github.event_name == 'pull_request'
# (needs to be after "Checkout" so files don't get overridden)
@ -125,7 +125,7 @@ jobs:
else
echo "TARGET_STAGE=stage1" >> $GITHUB_ENV
fi
- name: Build
- name: Configure Build
run: |
ulimit -c unlimited # coredumps
[ -d build ] || mkdir build
@ -162,7 +162,21 @@ jobs:
fi
# contortion to support empty OPTIONS with old macOS bash
cmake .. --preset ${{ matrix.CMAKE_PRESET || 'release' }} -B . ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
time make $TARGET_STAGE -j$NPROC
- name: Build Stage 0 & Configure Stage 1
run: |
ulimit -c unlimited # coredumps
time make -C build stage1-configure -j$NPROC
- name: Download Lake Cache
if: matrix.name == 'Linux Lake (Cached)'
run: |
cd src
../build/stage0/bin/lake cache get --repo=${{ github.repository }}
timeout-minutes: 20 # prevent excessive hanging from network issues
continue-on-error: true
- name: Build Target Stage
run: |
ulimit -c unlimited # coredumps
time make -C build $TARGET_STAGE -j$NPROC
# Should be done as early as possible and in particular *before* "Check rebootstrap" which
# changes the state of stage1/
- name: Save Cache
@ -181,6 +195,21 @@ jobs:
build/stage1/**/*.c
build/stage1/**/*.c.o*' || '' }}
key: ${{ steps.restore-cache.outputs.cache-primary-key }}
- name: Upload Lake Cache
# Caching on cancellation created some mysterious issues perhaps related to improper build
# shutdown. Also, since this needs access to secrets, it cannot be run on forks.
if: matrix.name == 'Linux Lake' && !cancelled() && (github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository)
run: |
curl --version
cd src
time ../build/stage0/bin/lake build -o ../build/lake-mappings.jsonl
time ../build/stage0/bin/lake cache put ../build/lake-mappings.jsonl --repo=${{ github.repository }}
env:
LAKE_CACHE_KEY: ${{ secrets.LAKE_CACHE_KEY }}
LAKE_CACHE_ARTIFACT_ENDPOINT: ${{ vars.LAKE_CACHE_ENDPOINT }}/a1
LAKE_CACHE_REVISION_ENDPOINT: ${{ vars.LAKE_CACHE_ENDPOINT }}/r1
timeout-minutes: 20 # prevent excessive hanging from network issues
continue-on-error: true
- name: Install
run: |
make -C build/$TARGET_STAGE install

20
.github/workflows/ci.yml vendored
View file

@ -244,7 +244,7 @@ jobs:
// portable release build: use channel with older glibc (2.26)
"name": "Linux release",
// usually not a bottleneck so make exclusive to `fast-ci`
"os": large && fast ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
"os": large && fast ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
"release": true,
// Special handling for release jobs. We want:
// 1. To run it in PRs so developers get PR toolchains (so secondary without tests is sufficient)
@ -265,7 +265,7 @@ jobs:
},
{
"name": "Linux Lake",
"os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
"os": large ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
"enabled": true,
"check-rebootstrap": level >= 1,
"check-stage3": level >= 2,
@ -273,7 +273,19 @@ jobs:
// NOTE: `test-bench` currently seems to be broken on `ubuntu-latest`
"test-bench": large && level >= 2,
// We are not warning-free yet on all platforms, start here
"CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror",
"CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror -DUSE_LAKE_CACHE=ON",
},
{
"name": "Linux Lake (Cached)",
"os": large ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
"enabled": true,
"check-rebootstrap": level >= 1,
"check-stage3": level >= 2,
"test": true,
"secondary": true,
// NOTE: `test-bench` currently seems to be broken on `ubuntu-latest`
"test-bench": large && level >= 2,
"CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror -DUSE_LAKE_CACHE=ON",
},
{
"name": "Linux Reldebug",
@ -287,7 +299,7 @@ jobs:
{
"name": "Linux fsanitize",
// Always run on large if available, more reliable regarding timeouts
"os": large ? "nscloud-ubuntu-22.04-amd64-16x32-with-cache" : "ubuntu-latest",
"os": large ? "nscloud-ubuntu-24.04-amd64-16x32-with-cache" : "ubuntu-latest",
"enabled": level >= 2,
// do not fail nightlies on this for now
"secondary": level <= 2,