chore: CI: fold Linux Lake into Linux release (#13759)
Now that they both use Lake, there's little reason for the duplication
This commit is contained in:
Sebastian Ullrich
GitHub
parent
ebbbec00f7
commit
e09155b6f9
3 changed files with 34 additions and 37 deletions
6
.github/workflows/build-template.yml
vendored
6
.github/workflows/build-template.yml
vendored
|
|
@ -101,7 +101,7 @@ jobs:
|
|||
# NOTE: must be in sync with `save` below and with `restore-cache` in `update-stage0.yml`
|
||||
path: |
|
||||
.ccache
|
||||
${{ matrix.name == 'Linux Lake' && 'build/stage1/**/*.trace
|
||||
${{ matrix.lake-actions-cache && 'build/stage1/**/*.trace
|
||||
build/stage1/**/*.olean*
|
||||
build/stage1/**/*.ilean
|
||||
build/stage1/**/*.ir
|
||||
|
|
@ -188,7 +188,7 @@ jobs:
|
|||
# NOTE: must be in sync with `restore` above
|
||||
path: |
|
||||
.ccache
|
||||
${{ matrix.name == 'Linux Lake' && 'build/stage1/**/*.trace
|
||||
${{ matrix.lake-actions-cache && 'build/stage1/**/*.trace
|
||||
build/stage1/**/*.olean*
|
||||
build/stage1/**/*.ilean
|
||||
build/stage1/**/*.ir
|
||||
|
|
@ -199,7 +199,7 @@ jobs:
|
|||
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)
|
||||
if: matrix.name == 'Linux release' && !cancelled() && (github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository)
|
||||
run: |
|
||||
curl --version
|
||||
cd src
|
||||
|
|
|
|||
39
.github/workflows/ci.yml
vendored
39
.github/workflows/ci.yml
vendored
|
|
@ -264,29 +264,8 @@ 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 ? chonk : "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)
|
||||
// 2. To skip it in merge queues as it takes longer than the
|
||||
// Linux lake build and adds little value in the merge queue
|
||||
// 3. To run it in release (obviously)
|
||||
// 4. To run it for pushes to master so that pushes to master have a Linux toolchain
|
||||
// available as an artifact for Grove to use.
|
||||
"enabled": isPr || level != 1 || isPushToMaster,
|
||||
"test": level >= 1,
|
||||
"secondary": level == 0,
|
||||
"shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
|
||||
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/22.1.4/lean-llvm-x86_64-linux-gnu.tar.zst",
|
||||
"prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
|
||||
"binary-check": "ldd -v",
|
||||
// foreign code may be linked against more recent glibc
|
||||
"CTEST_OPTIONS": "-E 'foreign'",
|
||||
},
|
||||
{
|
||||
"name": "Linux Lake",
|
||||
"os": large ? chonk : "ubuntu-latest",
|
||||
"release": true,
|
||||
"enabled": true,
|
||||
"check-rebootstrap": level >= 1,
|
||||
// Done as part of test-bench
|
||||
|
|
@ -294,8 +273,16 @@ jobs:
|
|||
"test": true,
|
||||
// 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 -DUSE_LAKE_CACHE=ON",
|
||||
"shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
|
||||
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/22.1.4/lean-llvm-x86_64-linux-gnu.tar.zst",
|
||||
"prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
|
||||
"binary-check": "ldd -v",
|
||||
// We are not warning-free yet on all platforms, start with Linux
|
||||
// Do not (yet) use Lake cache on release
|
||||
"CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror" + (level < 3 ? " -DUSE_LAKE_CACHE=ON" : ""),
|
||||
"lake-actions-cache": level < 3,
|
||||
// foreign code may be linked against more recent glibc
|
||||
"CTEST_OPTIONS": "-E 'foreign'",
|
||||
},
|
||||
{
|
||||
"name": "Linux Lake (Cached)",
|
||||
|
|
@ -366,7 +353,9 @@ jobs:
|
|||
"prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
|
||||
"binary-check": "otool -L",
|
||||
"tar": "gtar", // https://github.com/actions/runner-images/issues/2619
|
||||
// See "Linux release" for release job levels; Grove is not a concern here
|
||||
// Run in PRs so developers get PR toolchains (so secondary without tests is sufficient);
|
||||
// skip in merge queues as it takes longer than the Linux release build and adds little
|
||||
// value in the merge queue; run in release (obviously)
|
||||
"enabled": isPr || level != 1,
|
||||
"test": level >= 1,
|
||||
"secondary": level == 0,
|
||||
|
|
|
|||
26
.github/workflows/update-stage0.yml
vendored
26
.github/workflows/update-stage0.yml
vendored
|
|
@ -19,6 +19,10 @@ concurrency:
|
|||
jobs:
|
||||
update-stage0:
|
||||
runs-on: nscloud-ubuntu-22.04-amd64-8x16
|
||||
defaults:
|
||||
run:
|
||||
# like Linux release
|
||||
shell: nix develop .#oldGlibc -c bash -euxo pipefail {0}
|
||||
env:
|
||||
CCACHE_DIR: ${{ github.workspace }}/.ccache
|
||||
CCACHE_COMPRESS: true
|
||||
|
|
@ -30,9 +34,11 @@ jobs:
|
|||
- uses: actions/checkout@v6
|
||||
with:
|
||||
ssh-key: ${{secrets.STAGE0_SSH_KEY}}
|
||||
- run: echo "should_update_stage0=yes" >> "$GITHUB_ENV"
|
||||
- shell: bash
|
||||
run: echo "should_update_stage0=yes" >> "$GITHUB_ENV"
|
||||
- name: Check if automatic update is needed
|
||||
if: github.event_name == 'push'
|
||||
shell: bash
|
||||
run: |
|
||||
if diff -u src/stdlib_flags.h stage0/src/stdlib_flags.h
|
||||
then
|
||||
|
|
@ -41,6 +47,7 @@ jobs:
|
|||
fi
|
||||
- name: Setup git user
|
||||
if: env.should_update_stage0 == 'yes'
|
||||
shell: bash
|
||||
run: |
|
||||
git config --global user.name "Lean stage0 autoupdater"
|
||||
git config --global user.email "<>"
|
||||
|
|
@ -50,12 +57,10 @@ jobs:
|
|||
- name: Open Nix shell once
|
||||
if: env.should_update_stage0 == 'yes'
|
||||
run: true
|
||||
shell: 'nix develop -c bash -euxo pipefail {0}'
|
||||
- name: Set up NPROC
|
||||
if: env.should_update_stage0 == 'yes'
|
||||
run: |
|
||||
echo "NPROC=$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)" >> $GITHUB_ENV
|
||||
shell: 'nix develop -c bash -euxo pipefail {0}'
|
||||
- name: Restore Cache
|
||||
if: env.should_update_stage0 == 'yes'
|
||||
uses: actions/cache/restore@v5
|
||||
|
|
@ -69,20 +74,23 @@ jobs:
|
|||
build/stage1/**/*.ir
|
||||
build/stage1/**/*.c
|
||||
build/stage1/**/*.c.o*
|
||||
key: Linux Lake-build-v4-${{ github.sha }}
|
||||
key: Linux release-build-v4-${{ github.sha }}
|
||||
# fall back to (latest) previous cache
|
||||
restore-keys: |
|
||||
Linux Lake-build-v4
|
||||
Linux release-build-v4
|
||||
- if: env.should_update_stage0 == 'yes'
|
||||
# sync options with `Linux Lake` to ensure cache reuse
|
||||
name: Configure Build
|
||||
# sync options with `Linux release` to ensure cache reuse
|
||||
run: |
|
||||
mkdir -p build
|
||||
cmake --preset release -B build -DWFAIL=ON
|
||||
shell: 'nix develop -c bash -euxo pipefail {0}'
|
||||
cd build
|
||||
wget -q https://github.com/leanprover/lean-llvm/releases/download/22.1.4/lean-llvm-x86_64-linux-gnu.tar.zst
|
||||
PREPARE="$(../script/prepare-llvm-linux.sh lean-llvm*)"
|
||||
eval "OPTIONS=($PREPARE)"
|
||||
cmake .. --preset release -B . -DWFAIL=ON -DLEAN_EXTRA_CXX_FLAGS=-Werror "${OPTIONS[@]}"
|
||||
- if: env.should_update_stage0 == 'yes'
|
||||
run: |
|
||||
make -j$NPROC -C build update-stage0-commit
|
||||
shell: 'nix develop -c bash -euxo pipefail {0}'
|
||||
- if: env.should_update_stage0 == 'yes'
|
||||
run: git show --stat
|
||||
- if: env.should_update_stage0 == 'yes' && github.event_name == 'push'
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue