|
| 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@4fcb5062d7ce9bc4382d1a352d19ba3ba2c317c1 # v4.0.1 |
| 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@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 |
| 68 | + with: |
| 69 | + ref: ${{ inputs.pr_branch_ref }} |
| 70 | + fetch-depth: 1 |
| 71 | + path: pr-branch |
| 72 | + persist-credentials: false |
| 73 | + # The build runs this fork PR code sandboxed (landrun) with no persisted |
| 74 | + # credentials, so checking it out under pull_request_target is safe. |
| 75 | + allow-unsafe-pr-checkout: true |
| 76 | + |
| 77 | + # Create empty directories so landrun doesn't complain. |
| 78 | + - name: Create empty directories |
| 79 | + shell: bash # We need to run this outside landrun, as it is a prerequisite for landrun! |
| 80 | + run: | |
| 81 | + mkdir -p pr-branch/.lake/ |
| 82 | + mkdir -p .cache/mathlib/ |
| 83 | + mkdir -p _work |
| 84 | +
|
| 85 | + # NOTE: if you copy this, consider using `leanprover/lean-action` instead. |
| 86 | + # We install manually, to avoid running lean outside landrun. |
| 87 | + - name: install elan |
| 88 | + shell: bash |
| 89 | + run: | |
| 90 | + set -o pipefail |
| 91 | + curl -o elan-init.sh -sSfL https://elan.lean-lang.org/elan-init.sh |
| 92 | + chmod +x elan-init.sh |
| 93 | + ./elan-init.sh -y --default-toolchain none |
| 94 | + echo "$HOME/.elan/bin" >> "${GITHUB_PATH}" |
| 95 | +
|
| 96 | + - name: set toolchain directory |
| 97 | + shell: bash |
| 98 | + run: | |
| 99 | + cd pr-branch |
| 100 | + # Get the lake binary path from elan and extract toolchain directory |
| 101 | + LAKE_PATH=$(elan which lake) |
| 102 | + echo "Lake path: $LAKE_PATH" |
| 103 | +
|
| 104 | + # Extract the toolchain directory by removing /bin/lake from the end |
| 105 | + TOOLCHAIN_DIR=$(dirname "$LAKE_PATH") |
| 106 | + TOOLCHAIN_DIR=$(dirname "$TOOLCHAIN_DIR") |
| 107 | + echo "Toolchain directory: $TOOLCHAIN_DIR" |
| 108 | +
|
| 109 | + # Set it as an environment variable for subsequent steps |
| 110 | + echo "TOOLCHAIN_DIR=$TOOLCHAIN_DIR" >> "$GITHUB_ENV" |
| 111 | +
|
| 112 | + - name: set LEAN_SRC_PATH |
| 113 | + shell: bash |
| 114 | + run: | |
| 115 | + cd pr-branch |
| 116 | +
|
| 117 | + # Start with the base paths |
| 118 | + LEAN_SRC_PATH=".:$TOOLCHAIN_DIR/src/lean/lake" |
| 119 | +
|
| 120 | + # Extract package names from lake-manifest.json and validate them |
| 121 | + # Only allow A-Z, a-z, 0-9, _, and - characters |
| 122 | + # Build the LEAN_SRC_PATH by appending each validated package |
| 123 | + PACKAGE_NAMES=$(jq -r '.packages[].name' lake-manifest.json) |
| 124 | + for pkg in $PACKAGE_NAMES; do |
| 125 | + if [[ "$pkg" =~ ^[A-Za-z0-9_-]+$ ]]; then |
| 126 | + LEAN_SRC_PATH="$LEAN_SRC_PATH:.lake/packages/$pkg" |
| 127 | + else |
| 128 | + echo "Warning: Skipping invalid package name: $pkg" |
| 129 | + fi |
| 130 | + done |
| 131 | +
|
| 132 | + echo "LEAN_SRC_PATH=$LEAN_SRC_PATH" |
| 133 | +
|
| 134 | + # Set it as an environment variable for subsequent steps |
| 135 | + echo "LEAN_SRC_PATH=$LEAN_SRC_PATH" >> "$GITHUB_ENV" |
| 136 | +
|
| 137 | + # Populate `tools-branch/` with the trusted CI tooling (the `cache` binary and |
| 138 | + # the `lake-build-*` helper scripts invoked by path). Fast path: download the |
| 139 | + # prebuilt `tools-bin` artifact published from master (canonical mathlib4 only, |
| 140 | + # and only when the branch under test doesn't change the cache tool — get-tools |
| 141 | + # makes that comparison against `source_dir`). Source build otherwise. See the |
| 142 | + # get-tools action for the full trust rationale. |
| 143 | + - name: Get CI tools |
| 144 | + uses: ./workflow-actions/.github/actions/get-tools |
| 145 | + with: |
| 146 | + use_artifact: ${{ inputs.tools_branch_ref == '' && github.repository == 'leanprover-community/mathlib4' }} |
| 147 | + tools_source_ref: ${{ inputs.tools_branch_ref != '' && inputs.tools_branch_ref || (github.event.pull_request.head.repo.fork && 'master' || inputs.pr_branch_ref) }} |
| 148 | + source_dir: ${{ github.event.pull_request.head.repo.fork != true && 'pr-branch' || '' }} |
| 149 | + github_token: ${{ github.token }} |
| 150 | + |
| 151 | + - name: download dependencies |
| 152 | + # We need network access to download dependencies. We run this inside |
| 153 | + # landrun, but restrict disk access: |
| 154 | + # - --rox access to `~/.elan` and `~/actions-runner/_work` (GitHub CI needs this) |
| 155 | + # - --unrestricted-network as we need this to download dependencies |
| 156 | + # - git needs read only access to `/etc`. |
| 157 | + 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} |
| 158 | + run: | |
| 159 | + cd pr-branch |
| 160 | + lake env |
0 commit comments