Skip to content

Commit 67d0072

Browse files
tb65536tb65536
committed
Merge branch 'master' into tb_selmer2
2 parents 1069b73 + 4364cad commit 67d0072

510 files changed

Lines changed: 10500 additions & 3998 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/actions/setup-build-env/action.yml‎

Lines changed: 157 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,157 @@
1+
# Shared runner setup for the self-hosted `build` and `test_lint` jobs in
2+
# build_template.yml. Both run on the same Hoskinson pool and need the same
3+
# preparation before they diverge (build → build + stage, test_lint →
4+
# fetch + test + lint): toolchain hygiene, jq, the cache-trust and get-tools
5+
# wiring, the PR-branch checkout, the elan toolchain and LEAN_SRC_PATH
6+
# environment, and the dependency download.
7+
#
8+
# The caller runs `Checkout local actions` (sparse `.github/actions` →
9+
# `workflow-actions/`) before invoking this action: that checkout puts both this
10+
# action and the sibling actions it calls (`cache-trust-dispatch`, `get-tools`)
11+
# on disk under `workflow-actions/`, so the `uses: ./workflow-actions/...` paths
12+
# below resolve relative to the workspace root, as in the calling workflow.
13+
#
14+
# Each `run:` step sets its own `shell:`, since composite steps do not inherit the
15+
# job's landrun `defaults.run.shell`.
16+
name: Set up build environment
17+
description: Shared self-hosted runner setup for the build and test_lint jobs.
18+
19+
inputs:
20+
pr_branch_ref:
21+
description: Git ref of the PR branch to check out and build.
22+
required: true
23+
tools_branch_ref:
24+
description: Git ref to build the CI tools from when not using the prebuilt artifact.
25+
required: false
26+
default: ''
27+
28+
runs:
29+
using: composite
30+
steps:
31+
# Prune old toolchains from `~/.elan`. That directory is mounted from the host
32+
# and shared across the ephemeral job containers, so toolchains accumulate and
33+
# nothing else trims them (host-side housekeeping only trims the mathlib `.ltar`
34+
# cache). Keep the 5 most recent plus `nightly`/`stable`.
35+
- name: prune old toolchains
36+
shell: bash # just deletes old files; safe to run outside landrun
37+
run: |
38+
# Make sure to delete both the `~/.elan/toolchains/X` directory and the `~/.elan/update-hashes/X` file.
39+
# Skip symbolic links (`-type d`), the current directory (`! -name .`), and `nightly` and `stable`.
40+
if cd ~/.elan/toolchains && find . -maxdepth 1 -type d ! -name . -print0 | xargs -0 ls -1td | grep -v 'nightly$' | grep -v 'stable$' | tail -n +6 | xargs -I {} sh -c 'echo {} && rm -rf "{}" && rm "../update-hashes/{}"'; then
41+
: # Do nothing on success
42+
else
43+
: # Do nothing on failure, but suppress errors
44+
fi
45+
46+
# The Hoskinson runners may not have jq installed, so do that now.
47+
- name: 'Setup jq'
48+
uses: dcarbone/install-jq-action@b7ef57d46ece78760b4019dbc4080a1ba2a40b45 # v3.2.0
49+
50+
# Compute the trust-classified container target and read fallback for this
51+
# job. Sets MATHLIB_CACHE_FROM / MATHLIB_CACHE_PRIMARY in env so every
52+
# subsequent `cache get` inherits them without per-call flag plumbing. Loaded
53+
# from the trust-rooted `workflow-actions/` checkout, not the PR branch.
54+
- name: Compute cache trust dispatch
55+
uses: ./workflow-actions/.github/actions/cache-trust-dispatch
56+
with:
57+
repo: ${{ github.event.pull_request.head.repo.full_name || github.repository }}
58+
branch: ${{ github.head_ref || github.ref_name }}
59+
head-sha: ${{ github.event.pull_request.head.sha || github.sha }}
60+
61+
# Checkout the PR branch into a subdirectory. HEAD only (fetch-depth: 1) is
62+
# enough: the cache is fetched HEAD-scoped and warmed from the master snapshot,
63+
# so no parent-commit history is needed. This is untrusted (potentially fork)
64+
# code we build, so don't leave the GITHUB_TOKEN in pr-branch/.git/config where
65+
# that code could read it.
66+
- name: Checkout PR branch
67+
uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
68+
with:
69+
ref: ${{ inputs.pr_branch_ref }}
70+
fetch-depth: 1
71+
path: pr-branch
72+
persist-credentials: false
73+
74+
# Create empty directories so landrun doesn't complain.
75+
- name: Create empty directories
76+
shell: bash # We need to run this outside landrun, as it is a prerequisite for landrun!
77+
run: |
78+
mkdir -p pr-branch/.lake/
79+
mkdir -p .cache/mathlib/
80+
mkdir -p _work
81+
82+
# NOTE: if you copy this, consider using `leanprover/lean-action` instead.
83+
# We install manually, to avoid running lean outside landrun.
84+
- name: install elan
85+
shell: bash
86+
run: |
87+
set -o pipefail
88+
curl -o elan-init.sh -sSfL https://elan.lean-lang.org/elan-init.sh
89+
chmod +x elan-init.sh
90+
./elan-init.sh -y --default-toolchain none
91+
echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
92+
93+
- name: set toolchain directory
94+
shell: bash
95+
run: |
96+
cd pr-branch
97+
# Get the lake binary path from elan and extract toolchain directory
98+
LAKE_PATH=$(elan which lake)
99+
echo "Lake path: $LAKE_PATH"
100+
101+
# Extract the toolchain directory by removing /bin/lake from the end
102+
TOOLCHAIN_DIR=$(dirname "$LAKE_PATH")
103+
TOOLCHAIN_DIR=$(dirname "$TOOLCHAIN_DIR")
104+
echo "Toolchain directory: $TOOLCHAIN_DIR"
105+
106+
# Set it as an environment variable for subsequent steps
107+
echo "TOOLCHAIN_DIR=$TOOLCHAIN_DIR" >> "$GITHUB_ENV"
108+
109+
- name: set LEAN_SRC_PATH
110+
shell: bash
111+
run: |
112+
cd pr-branch
113+
114+
# Start with the base paths
115+
LEAN_SRC_PATH=".:$TOOLCHAIN_DIR/src/lean/lake"
116+
117+
# Extract package names from lake-manifest.json and validate them
118+
# Only allow A-Z, a-z, 0-9, _, and - characters
119+
# Build the LEAN_SRC_PATH by appending each validated package
120+
PACKAGE_NAMES=$(jq -r '.packages[].name' lake-manifest.json)
121+
for pkg in $PACKAGE_NAMES; do
122+
if [[ "$pkg" =~ ^[A-Za-z0-9_-]+$ ]]; then
123+
LEAN_SRC_PATH="$LEAN_SRC_PATH:.lake/packages/$pkg"
124+
else
125+
echo "Warning: Skipping invalid package name: $pkg"
126+
fi
127+
done
128+
129+
echo "LEAN_SRC_PATH=$LEAN_SRC_PATH"
130+
131+
# Set it as an environment variable for subsequent steps
132+
echo "LEAN_SRC_PATH=$LEAN_SRC_PATH" >> "$GITHUB_ENV"
133+
134+
# Populate `tools-branch/` with the trusted CI tooling (the `cache` binary and
135+
# the `lake-build-*` helper scripts invoked by path). Fast path: download the
136+
# prebuilt `tools-bin` artifact published from master (canonical mathlib4 only,
137+
# and only when the branch under test doesn't change the cache tool — get-tools
138+
# makes that comparison against `source_dir`). Source build otherwise. See the
139+
# get-tools action for the full trust rationale.
140+
- name: Get CI tools
141+
uses: ./workflow-actions/.github/actions/get-tools
142+
with:
143+
use_artifact: ${{ inputs.tools_branch_ref == '' && github.repository == 'leanprover-community/mathlib4' }}
144+
tools_source_ref: ${{ inputs.tools_branch_ref != '' && inputs.tools_branch_ref || (github.event.pull_request.head.repo.fork && 'master' || inputs.pr_branch_ref) }}
145+
source_dir: ${{ github.event.pull_request.head.repo.fork != true && 'pr-branch' || '' }}
146+
github_token: ${{ github.token }}
147+
148+
- name: download dependencies
149+
# We need network access to download dependencies. We run this inside
150+
# landrun, but restrict disk access:
151+
# - --rox access to `~/.elan` and `~/actions-runner/_work` (GitHub CI needs this)
152+
# - --unrestricted-network as we need this to download dependencies
153+
# - git needs read only access to `/etc`.
154+
shell: landrun --unrestricted-network --rox /etc --rox /usr --rw /dev --rox /home/lean/.elan --rox /home/lean/actions-runner/_work --rw pr-branch/.lake/ --env PATH --env HOME --env GITHUB_OUTPUT --env CI -- bash -euxo pipefail {0}
155+
run: |
156+
cd pr-branch
157+
lake env

0 commit comments

Comments
 (0)