Skip to content

Commit 652db3e

Browse files
CoolRmalCoolRmal
authored
Merge branch 'leanprover-community:master' into main
2 parents 11704fe + eb15deb commit 652db3e

7,424 files changed

Lines changed: 300979 additions & 135356 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/get-mathlib-ci/README.md‎

Lines changed: 75 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,75 @@
1+
# get-mathlib-ci
2+
3+
This action is the source of truth for how workflows in this repository check out
4+
`leanprover-community/mathlib-ci`.
5+
6+
## Policy
7+
8+
Any workflow that needs `mathlib-ci` should use this action instead of writing its
9+
own `actions/checkout` block for `leanprover-community/mathlib-ci`.
10+
11+
The default `ref` in [`action.yml`](./action.yml) is the single canonical pinned
12+
`mathlib-ci` commit for this repository. This is auto-updated regularly by the
13+
[`update_dependencies.yml` workflow](../../workflows/update_dependencies.yml).
14+
15+
## Why
16+
17+
- Keep the pinned `mathlib-ci` ref in one place.
18+
- Avoid drift and copy/paste mistakes across many workflows.
19+
- Make ref bumps a one-file update.
20+
21+
## Usage
22+
23+
In workflows, check out this repository's actions from the running workflow commit,
24+
then use the local action:
25+
26+
```yaml
27+
- name: Checkout local actions
28+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
29+
with:
30+
ref: ${{ github.workflow_sha }}
31+
fetch-depth: 1
32+
sparse-checkout: .github/actions
33+
path: workflow-actions
34+
35+
- name: Get mathlib-ci
36+
uses: ./workflow-actions/.github/actions/get-mathlib-ci
37+
```
38+
39+
Override the ref only when needed:
40+
41+
```yaml
42+
- name: Get mathlib-ci
43+
uses: ./workflow-actions/.github/actions/get-mathlib-ci
44+
with:
45+
ref: master
46+
```
47+
48+
## Outputs
49+
50+
This action also exposes values that later workflow steps can reuse:
51+
52+
- `ref`: the effective `mathlib-ci` ref that was checked out. If the workflow did
53+
not pass `with.ref`, this is the action's default pinned commit.
54+
- `path`: the checkout path used for `mathlib-ci`.
55+
- `scripts_dir`: the absolute path to the checked out `scripts` directory.
56+
57+
The action also exports these environment variables for subsequent steps:
58+
59+
- `CI_CHECKOUT_PATH`: the absolute path to the checked out `mathlib-ci` repository.
60+
- `CI_SCRIPTS_DIR`: the absolute path to the checked out `mathlib-ci/scripts` directory.
61+
62+
If a workflow needs to refer to the exact resolved `mathlib-ci` ref later, use the
63+
action output instead of duplicating the pinned SHA in the workflow:
64+
65+
```yaml
66+
- name: Get mathlib-ci
67+
id: get_mathlib_ci
68+
uses: ./workflow-actions/.github/actions/get-mathlib-ci
69+
70+
- name: Use resolved ref
71+
run: |
72+
echo "Resolved ref: ${{ steps.get_mathlib_ci.outputs.ref }}"
73+
echo "Scripts dir: ${{ steps.get_mathlib_ci.outputs.scripts_dir }}"
74+
echo "Raw URL: https://raw.githubusercontent.com/leanprover-community/mathlib-ci/${{ steps.get_mathlib_ci.outputs.ref }}/scripts/nightly/create-adaptation-pr.sh"
75+
```

‎.github/actions/get-mathlib-ci/action.yml‎

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
# Source of truth for `mathlib-ci` checkout settings in this repository.
2+
# Workflows should use this action instead of duplicating the checkout block
3+
# and hardcoded ref in multiple places.
4+
name: Get mathlib-ci
5+
description: Checkout leanprover-community/mathlib-ci at a shared ref.
6+
inputs:
7+
ref:
8+
description: Git ref (branch, tag, or SHA) for mathlib-ci.
9+
required: false
10+
# Default pinned commit used by workflows unless they explicitly override.
11+
# Update this ref as needed to pick up changes to mathlib-ci scripts
12+
# This is also updated automatically by .github/workflows/update_dependencies.yml
13+
default: 910febac0a5c2751e99cfd464b99f549351f0f1a
14+
path:
15+
description: Checkout destination path.
16+
required: false
17+
default: ci-tools
18+
fetch-depth:
19+
description: Number of commits to fetch.
20+
required: false
21+
default: '1'
22+
outputs:
23+
ref:
24+
description: Effective ref used for the checkout.
25+
value: ${{ inputs.ref }}
26+
path:
27+
description: Checkout path used.
28+
value: ${{ inputs.path }}
29+
scripts_dir:
30+
description: Absolute path to the scripts directory.
31+
value: ${{ steps.paths.outputs.scripts_dir }}
32+
runs:
33+
using: composite
34+
steps:
35+
- name: Get mathlib-ci
36+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
37+
with:
38+
repository: leanprover-community/mathlib-ci
39+
ref: ${{ inputs.ref }}
40+
fetch-depth: ${{ inputs.fetch-depth }}
41+
path: ${{ inputs.path }}
42+
43+
- name: Setup CI Scripts Paths
44+
id: paths
45+
shell: bash
46+
run: |
47+
checkout_path="${GITHUB_WORKSPACE}/${{ inputs.path }}"
48+
scripts_dir="${checkout_path}/scripts"
49+
echo "checkout_path=${checkout_path}" >> "$GITHUB_OUTPUT"
50+
echo "scripts_dir=${scripts_dir}" >> "$GITHUB_OUTPUT"
51+
echo "CI_CHECKOUT_PATH=${checkout_path}" >> "$GITHUB_ENV"
52+
echo "CI_SCRIPTS_DIR=${scripts_dir}" >> "$GITHUB_ENV"

‎.github/actions/get-tools/action.yml‎

Lines changed: 129 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,129 @@
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

Comments
 (0)