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

chore: ci: build Linux toolchain for master commits (but not merge queue runs) (#9010)

Browse source
This commit is contained in:
Markus Himmel 2025-06-26 10:20:04 +02:00 • committed by GitHub
parent 70b4b2b36c
commit 4f1d828541
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -145,6 +145,7 @@ jobs:
// use large runners where available (original repo)
let large = ${{ github.repository == 'leanprover/lean4' }};
const isPr = "${{ github.event_name }}" == "pull_request";
const isPushToMaster = "${{ github.event_name }}" == "push" && "${{ github.ref_name }}" == "master";
let matrix = [
/* TODO: to be updated to new LLVM
{
@ -167,11 +168,13 @@ jobs:
"os": large && level < 2 ? "nscloud-ubuntu-22.04-amd64-4x16" : "ubuntu-latest",
"release": true,
// Special handling for release jobs. We want:
// 1. To run it in PRs so developrs get PR toolchains (so secondary is sufficient)
// 1. To run it in PRs so developers get PR toolchains (so secondary 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)
"check-level": isPr ? 0 : 2,
// 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.
"check-level": (isPr || isPushToMaster) ? 0 : 2,
"secondary": isPr,
"shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",