|
| 1 | +# Populates `tools-branch/` with the trusted CI tooling (`cache` binary + the |
| 2 | +# `lake-build-*` helper scripts) that `build_template.yml` invokes by path. |
| 3 | +# |
| 4 | +# Fast path: download the `tools-bin` artifact published by `publish_tools.yml` |
| 5 | +# from its latest successful `master` `push` run, unpack it, and install the |
| 6 | +# matching toolchain. Fallback: check out `tools_source_ref` and build from source |
| 7 | +# (the original behaviour). The fallback also triggers automatically if anything |
| 8 | +# about the download/verification fails, so this action can never make CI worse |
| 9 | +# than building from source. |
| 10 | +# |
| 11 | +# Requires (fast path only): `actions: read` permission. The `gh` CLI is provided |
| 12 | +# by the Hoskinson runner image. Any lookup/download failure falls through to the |
| 13 | +# source build, so the fast path can never make CI worse. |
| 14 | +name: Get CI tools |
| 15 | +description: Download prebuilt CI tools from master, or build them from source. |
| 16 | +inputs: |
| 17 | + use_artifact: |
| 18 | + description: Whether to attempt the prebuilt-artifact fast path ('true'/'false'). |
| 19 | + required: true |
| 20 | + tools_source_ref: |
| 21 | + description: Git ref to check out and build from when not using the artifact. |
| 22 | + required: true |
| 23 | + github_token: |
| 24 | + description: "Token with `actions: read` on artifact_repo (fast path only)." |
| 25 | + required: false |
| 26 | + default: '' |
| 27 | + artifact_repo: |
| 28 | + description: Repository that publishes the tools artifact. |
| 29 | + required: false |
| 30 | + default: leanprover-community/mathlib4 |
| 31 | + artifact_workflow: |
| 32 | + description: Workflow file that publishes the tools artifact. |
| 33 | + required: false |
| 34 | + default: publish_tools.yml |
| 35 | + path: |
| 36 | + description: Destination directory for the tools. |
| 37 | + required: false |
| 38 | + default: tools-branch |
| 39 | +runs: |
| 40 | + using: composite |
| 41 | + steps: |
| 42 | + # Resolve the run-id of the latest successful master push of the publisher. |
| 43 | + # Pure lookup: on any failure (or when the fast path is disabled) we emit an |
| 44 | + # empty run_id, which skips the download and lands us on the source-build path. |
| 45 | + - name: Resolve tools artifact run |
| 46 | + id: resolve |
| 47 | + shell: bash |
| 48 | + env: |
| 49 | + GH_TOKEN: ${{ inputs.github_token }} |
| 50 | + run: | |
| 51 | + set -uo pipefail |
| 52 | + run_id="" |
| 53 | + if [[ "${{ inputs.use_artifact }}" == "true" && -n "${{ inputs.github_token }}" ]]; then |
| 54 | + run_id=$(gh run list \ |
| 55 | + --repo "${{ inputs.artifact_repo }}" \ |
| 56 | + --workflow "${{ inputs.artifact_workflow }}" \ |
| 57 | + --branch master --status success --event push \ |
| 58 | + --limit 1 --json databaseId --jq '.[0].databaseId // empty' 2>/dev/null || true) |
| 59 | + fi |
| 60 | + echo "Resolved publisher run_id: '${run_id}'" |
| 61 | + echo "run_id=${run_id}" >> "$GITHUB_OUTPUT" |
| 62 | +
|
| 63 | + - name: Download tools artifact |
| 64 | + if: ${{ steps.resolve.outputs.run_id != '' }} |
| 65 | + continue-on-error: true |
| 66 | + uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1 |
| 67 | + with: |
| 68 | + name: tools-bin |
| 69 | + path: tools-artifact |
| 70 | + repository: ${{ inputs.artifact_repo }} |
| 71 | + run-id: ${{ steps.resolve.outputs.run_id }} |
| 72 | + github-token: ${{ inputs.github_token }} |
| 73 | + |
| 74 | + # Unpack the tools and install the toolchain the `cache` binary was linked |
| 75 | + # against (the one guarantee the old `lake build` of the tools gave us for |
| 76 | + # free). If the tarball is missing, the unpack fails, or the toolchain won't |
| 77 | + # install, wipe any partial state and signal a source build. |
| 78 | + - name: Unpack tools |
| 79 | + id: finalize |
| 80 | + shell: bash |
| 81 | + run: | |
| 82 | + set -uo pipefail |
| 83 | + result=build |
| 84 | + tarball="tools-artifact/tools-bin.tar.gz" |
| 85 | + if [[ -f "$tarball" ]]; then |
| 86 | + echo "Found downloaded tools artifact; unpacking..." |
| 87 | + rm -rf "${{ inputs.path }}" |
| 88 | + mkdir -p "${{ inputs.path }}" |
| 89 | + if tar -xzf "$tarball" -C "${{ inputs.path }}" \ |
| 90 | + && [[ -x "${{ inputs.path }}/.lake/build/bin/cache" ]]; then |
| 91 | + toolchain="$(cat "${{ inputs.path }}/lean-toolchain")" |
| 92 | + echo "Ensuring tools toolchain is installed: ${toolchain}" |
| 93 | + # `elan toolchain install` exits non-zero when the toolchain is already |
| 94 | + # present (the common case), so install best-effort and then confirm the |
| 95 | + # toolchain is available rather than trusting the install exit code. |
| 96 | + elan toolchain install "$toolchain" || true |
| 97 | + if elan toolchain list | awk '{print $1}' | grep -qxF "$toolchain"; then |
| 98 | + result=artifact |
| 99 | + else |
| 100 | + echo "WARNING: tools toolchain '${toolchain}' is not available; falling back to source build." |
| 101 | + fi |
| 102 | + else |
| 103 | + echo "WARNING: tools artifact unpack/validation failed; falling back to source build." |
| 104 | + fi |
| 105 | + else |
| 106 | + echo "No tools artifact available; will build from source." |
| 107 | + fi |
| 108 | + if [[ "$result" != "artifact" ]]; then |
| 109 | + rm -rf "${{ inputs.path }}" |
| 110 | + fi |
| 111 | + echo "Tools source: ${result}" |
| 112 | + echo "result=${result}" >> "$GITHUB_OUTPUT" |
| 113 | +
|
| 114 | + - name: Checkout tools branch (source build) |
| 115 | + if: ${{ steps.finalize.outputs.result == 'build' }} |
| 116 | + uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3 |
| 117 | + with: |
| 118 | + ref: ${{ inputs.tools_source_ref }} |
| 119 | + path: ${{ inputs.path }} |
| 120 | + |
| 121 | + - name: Build tools from source |
| 122 | + if: ${{ steps.finalize.outputs.result == 'build' }} |
| 123 | + shell: bash # We're only building a trusted branch with the tools, so no need to run inside landrun. |
| 124 | + run: | |
| 125 | + cd "${{ inputs.path }}" |
| 126 | + lake build cache check-yaml graph |
| 127 | + ls .lake/build/bin/cache |
| 128 | + ls .lake/build/bin/check-yaml |
| 129 | + ls .lake/packages/importGraph/.lake/build/bin/graph |
0 commit comments