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

fix: rebootstrap cache in github CI (#13143)

Browse source 
The old approach isn't smart enough to trick the lake cache anymore.
Making an explicit
update-stage0 commit will make it work again.
This commit is contained in:
Henrik Böving 2026-03-26 21:50:03 +01:00 • committed by GitHub
parent 0975b7136a
commit 144db355ea
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -276,10 +276,10 @@ jobs:
- name: Check rebootstrap
run: |
set -e
# clean rebuild in case of Makefile changes/Lake does not detect uncommited stage 0
# changes yet
git config user.email "stage0@lean-fro.org"
git config user.name "update-stage0"
make -C build update-stage0
make -C build/stage1 clean-stdlib
git commit --allow-empty -m "chore: update-stage0"
time make -C build -j$NPROC
time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/stage1 -j$NPROC
if: matrix.check-rebootstrap