Skip to content

Commit bf3278d

Browse files
tb65536tb65536
committed
Merge branch 'master' into tb_ramram
2 parents c69fc5c + 9b785f9 commit bf3278d

4,985 files changed

Lines changed: 73206 additions & 31743 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.

‎.devcontainer/devcontainer.json‎

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,13 @@
11
{
22
"name": "Mathlib4 dev container",
3+
"remoteUser": "vscode",
34

45
"build": {
56
"dockerfile": "Dockerfile"
67
},
78

89
"onCreateCommand": "lake exe cache get!",
10+
"postCreateCommand": "gh auth status || gh auth login",
911

1012
"hostRequirements": {
1113
"cpus": 4,
@@ -16,5 +18,14 @@
1618
"vscode": {
1719
"extensions": ["leanprover.lean4"]
1820
}
19-
}
21+
},
22+
23+
"features": {
24+
// install `gh`
25+
"ghcr.io/devcontainers/features/github-cli:1": {}
26+
},
27+
28+
"mounts": [
29+
"source=${localEnv:HOME}/.gitconfig,target=/home/vscode/.gitconfig,type=bind,consistency=cached"
30+
]
2031
}

‎.github/actions/cache-trust-dispatch/action.yml‎

Lines changed: 157 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,157 @@
1+
# Single source of truth mapping (repo, branch) → (upload container,
2+
# read fallback chain) for Mathlib's multi-container cache.
3+
#
4+
# Called by build, upload_cache, and post_steps in build_template.yml so
5+
# trust classification is decided in exactly one place. Lean-side cache
6+
# logic stays branch-agnostic; this composite is the seam where CI-only
7+
# trust policy lives.
8+
9+
name: Cache trust dispatch
10+
description: Compute the cache container target and read fallback for this job.
11+
12+
inputs:
13+
repo:
14+
description: GitHub repo full name (`owner/name`).
15+
required: true
16+
branch:
17+
description: Branch name (`github.head_ref || github.ref_name`).
18+
required: true
19+
head-sha:
20+
description: |
21+
Head commit SHA for the ref being built. Used as the per-commit cache
22+
namespace (`MATHLIB_CACHE_REPO_SCOPE`) for fork-trust uploads, so a
23+
closed/hidden PR's poisoned artifacts cannot be served to a later
24+
honest PR from the same fork.
25+
required: true
26+
27+
# Outputs are mirrored to $GITHUB_ENV inside the step, which is what
28+
# downstream `cache get` / `cache put-staged` calls actually read. We
29+
# also expose them as action outputs for callers that need them in
30+
# `with:` blocks (e.g. constructing further `if:` conditions).
31+
outputs:
32+
primary:
33+
description: Container name for uploads (master, forks, nightly-testing, pr-toolchain-tests).
34+
value: ${{ steps.dispatch.outputs.primary }}
35+
read-chain:
36+
description: |
37+
Comma-separated read fallback chain for `MATHLIB_CACHE_FROM`. Empty
38+
when the job should use the cache tool's repo-level default.
39+
value: ${{ steps.dispatch.outputs.read-chain }}
40+
repo-scope:
41+
description: |
42+
Per-commit namespace suffix for `MATHLIB_CACHE_REPO_SCOPE`. Set to
43+
the head SHA when uploading to fork-trust containers; empty for
44+
master / nightly / pr-toolchain-tests uploads where scoping isn't
45+
applied.
46+
value: ${{ steps.dispatch.outputs.repo-scope }}
47+
48+
runs:
49+
using: composite
50+
steps:
51+
- name: Compute trust dispatch
52+
id: dispatch
53+
shell: bash
54+
run: |
55+
REPO="${{ inputs.repo }}"
56+
BRANCH="${{ inputs.branch }}"
57+
HEAD_SHA="${{ inputs.head-sha }}"
58+
PRIMARY=""
59+
READ_CHAIN=""
60+
REPO_SCOPE=""
61+
62+
# Security note: this dispatch is NOT the trust boundary for writes.
63+
# The real enforcement is the OIDC bearer token minted in upload_cache:
64+
# the token is scoped to a specific container, so a malicious actor
65+
# rewriting this case to `--container=master` from a fork build would
66+
# be 403'd by Azure regardless. The dispatch exists so the workflow
67+
# does the right thing in the honest case; defence in depth is RBAC.
68+
69+
case "$REPO" in
70+
"leanprover-community/mathlib4")
71+
case "$BRANCH" in
72+
"master"|"staging")
73+
# Master / staging are the only writers that feed `master`
74+
# (`staging` is bors's merge candidate, which fast-forwards to
75+
# `master`). Read `master` only, not the default [master,
76+
# legacy]: files the read chain serves are skipped at stage
77+
# time, so keeping `legacy` would leave legacy-only files out of
78+
# `master` for good. Reading `master` alone turns them into
79+
# misses that get rebuilt and uploaded, so `master` fills itself
80+
# into a standalone cache. (Only PRIMARY=master does this; other
81+
# runs write to `forks` and keep the wider chain.)
82+
PRIMARY="master"
83+
READ_CHAIN="master"
84+
;;
85+
*)
86+
# `bors trying`, `ci-dev/*`, maintainer dev branches on the
87+
# canonical repo: trust level is fork-equivalent (the OIDC
88+
# token's RBAC scopes them to `forks`). Reads must widen
89+
# past the default [master, legacy] so the post-build
90+
# verification finds the just-uploaded fork-trust artifacts.
91+
PRIMARY="forks"
92+
READ_CHAIN="master,forks,legacy"
93+
;;
94+
esac
95+
;;
96+
"leanprover-community/mathlib4-nightly-testing")
97+
case "$BRANCH" in
98+
"nightly-testing"|"nightly-testing-green"|"staging"|bump/*)
99+
# Trusted nightly refs use the default [nightly-testing, legacy].
100+
# It excludes `pr-toolchain-tests` so an upload from a
101+
# `lean-pr-testing-*` branch never reaches a trusted-nightly
102+
# consumer.
103+
PRIMARY="nightly-testing"
104+
;;
105+
*)
106+
# `lean-pr-testing-*`, `batteries-pr-testing-*`, etc.:
107+
# least-trusted (can build with arbitrary toolchains). Widen
108+
# reads to recover this branch's own previously-uploaded
109+
# artifacts; trusted-nightly stays preferred where hash
110+
# spaces happen to align.
111+
PRIMARY="pr-toolchain-tests"
112+
READ_CHAIN="pr-toolchain-tests,nightly-testing,legacy"
113+
;;
114+
esac
115+
;;
116+
*)
117+
# Foreign fork. The cache tool's default chain for a fork repo
118+
# is [master, forks, legacy] (master-first): master supplies the
119+
# bulk of unchanged upstream deps, forks supplies PR-specific
120+
# files. No widening needed, so MATHLIB_CACHE_FROM stays unset.
121+
PRIMARY="forks"
122+
;;
123+
esac
124+
125+
# Per-commit cache namespace, only for fork-trust uploads. Closes the
126+
# within-fork temporal replay attack: each commit's CI run gets its
127+
# own /f/{repo}/{sha}/... namespace, so artifacts from a closed/
128+
# hidden PR cannot be served to a later honest build on the same
129+
# fork. Master / nightly / pr-toolchain-tests uploads stay un-scoped:
130+
# master has a single writer (no replay risk), and the per-toolchain
131+
# hash partitioning isolates nightly and toolchain-test classes via
132+
# their root-hash inputs.
133+
if [ "$PRIMARY" = "forks" ]; then
134+
REPO_SCOPE="$HEAD_SHA"
135+
fi
136+
137+
echo "primary=$PRIMARY" >> "$GITHUB_OUTPUT"
138+
echo "read-chain=$READ_CHAIN" >> "$GITHUB_OUTPUT"
139+
echo "repo-scope=$REPO_SCOPE" >> "$GITHUB_OUTPUT"
140+
echo "MATHLIB_CACHE_PRIMARY=$PRIMARY" >> "$GITHUB_ENV"
141+
if [ -n "$READ_CHAIN" ]; then
142+
echo "MATHLIB_CACHE_FROM=$READ_CHAIN" >> "$GITHUB_ENV"
143+
fi
144+
if [ -n "$REPO_SCOPE" ]; then
145+
echo "MATHLIB_CACHE_REPO_SCOPE=$REPO_SCOPE" >> "$GITHUB_ENV"
146+
fi
147+
# Visible in CI logs so a glance at any cache-touching step shows
148+
# what trust class the job is operating under.
149+
SCOPE_NOTE=""
150+
if [ -n "$REPO_SCOPE" ]; then
151+
SCOPE_NOTE=", MATHLIB_CACHE_REPO_SCOPE=$REPO_SCOPE"
152+
fi
153+
if [ -n "$READ_CHAIN" ]; then
154+
echo "cache-trust-dispatch: REPO=$REPO BRANCH=$BRANCH → container=$PRIMARY, MATHLIB_CACHE_FROM=$READ_CHAIN$SCOPE_NOTE"
155+
else
156+
echo "cache-trust-dispatch: REPO=$REPO BRANCH=$BRANCH → container=$PRIMARY, MATHLIB_CACHE_FROM=<default>$SCOPE_NOTE"
157+
fi

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ inputs:
1010
# Default pinned commit used by workflows unless they explicitly override.
1111
# Update this ref as needed to pick up changes to mathlib-ci scripts
1212
# This is also updated automatically by .github/workflows/update_dependencies.yml
13-
default: 78f34ded6a5f5aa11ea5b7c3120fe5d8422db1da
13+
default: 5aee9d4ce5a39050c72b4aa46015a824b0c189ac
1414
path:
1515
description: Checkout destination path.
1616
required: false

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

Lines changed: 155 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,155 @@
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+
source_dir:
40+
description: >
41+
Optional path to a local checkout under test. When set and the artifact
42+
fast path is in play, the action compares this checkout's tool sources
43+
against the artifact's `master` baseline; if they differ it skips the
44+
prebuilt artifact and builds from source, so a branch that changes the
45+
tool is tested with its own tool. Empty disables the comparison.
46+
required: false
47+
default: ''
48+
runs:
49+
using: composite
50+
steps:
51+
# Resolve the run-id of the latest successful master push of the publisher.
52+
# Pure lookup: on any failure (or when the fast path is disabled) we emit an
53+
# empty run_id, which skips the download and lands us on the source-build path.
54+
- name: Resolve tools artifact run
55+
id: resolve
56+
shell: bash
57+
env:
58+
GH_TOKEN: ${{ inputs.github_token }}
59+
run: |
60+
set -uo pipefail
61+
run_id=""
62+
if [[ "${{ inputs.use_artifact }}" == "true" && -n "${{ inputs.github_token }}" ]]; then
63+
run_id=$(gh run list \
64+
--repo "${{ inputs.artifact_repo }}" \
65+
--workflow "${{ inputs.artifact_workflow }}" \
66+
--branch master --status success --event push \
67+
--limit 1 --json databaseId --jq '.[0].databaseId // empty' 2>/dev/null || true)
68+
69+
# If a local checkout under test is provided and its tool sources differ
70+
# from the artifact's master baseline, the prebuilt tool would mask the
71+
# change — drop it and build from source. Local git only; no API call.
72+
# These are the source paths that determine the bundled tools (the
73+
# `cache` binary and the build-helper scripts in publish_tools.yml); they
74+
# live here so callers don't have to duplicate the list.
75+
if [[ -n "$run_id" && -n "${{ inputs.source_dir }}" ]]; then
76+
git -C "${{ inputs.source_dir }}" fetch --no-tags --depth=1 \
77+
"https://github.com/${{ inputs.artifact_repo }}.git" master || true
78+
# Fail safe toward building: a failed fetch/diff leaves $? non-zero.
79+
if ! git -C "${{ inputs.source_dir }}" diff --quiet FETCH_HEAD -- \
80+
Cache scripts/lake-build-with-retry.sh scripts/lake-build-wrapper.py; then
81+
echo "Tool sources in '${{ inputs.source_dir }}' differ from master; building from source."
82+
run_id=""
83+
fi
84+
fi
85+
fi
86+
echo "Resolved publisher run_id: '${run_id}'"
87+
echo "run_id=${run_id}" >> "$GITHUB_OUTPUT"
88+
89+
- name: Download tools artifact
90+
if: ${{ steps.resolve.outputs.run_id != '' }}
91+
continue-on-error: true
92+
uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
93+
with:
94+
name: tools-bin
95+
path: tools-artifact
96+
repository: ${{ inputs.artifact_repo }}
97+
run-id: ${{ steps.resolve.outputs.run_id }}
98+
github-token: ${{ inputs.github_token }}
99+
100+
# Unpack the tools and install the toolchain the `cache` binary was linked
101+
# against (the one guarantee the old `lake build` of the tools gave us for
102+
# free). If the tarball is missing, the unpack fails, or the toolchain won't
103+
# install, wipe any partial state and signal a source build.
104+
- name: Unpack tools
105+
id: finalize
106+
shell: bash
107+
run: |
108+
set -uo pipefail
109+
result=build
110+
tarball="tools-artifact/tools-bin.tar.gz"
111+
if [[ -f "$tarball" ]]; then
112+
echo "Found downloaded tools artifact; unpacking..."
113+
rm -rf "${{ inputs.path }}"
114+
mkdir -p "${{ inputs.path }}"
115+
if tar -xzf "$tarball" -C "${{ inputs.path }}" \
116+
&& [[ -x "${{ inputs.path }}/.lake/build/bin/cache" ]]; then
117+
toolchain="$(cat "${{ inputs.path }}/lean-toolchain")"
118+
echo "Ensuring tools toolchain is installed: ${toolchain}"
119+
# `elan toolchain install` exits non-zero when the toolchain is already
120+
# present (the common case), so install best-effort and then confirm the
121+
# toolchain is available rather than trusting the install exit code.
122+
elan toolchain install "$toolchain" || true
123+
if elan toolchain list | awk '{print $1}' | grep -qxF "$toolchain"; then
124+
result=artifact
125+
else
126+
echo "WARNING: tools toolchain '${toolchain}' is not available; falling back to source build."
127+
fi
128+
else
129+
echo "WARNING: tools artifact unpack/validation failed; falling back to source build."
130+
fi
131+
else
132+
echo "No tools artifact available; will build from source."
133+
fi
134+
if [[ "$result" != "artifact" ]]; then
135+
rm -rf "${{ inputs.path }}"
136+
fi
137+
echo "Tools source: ${result}"
138+
echo "result=${result}" >> "$GITHUB_OUTPUT"
139+
140+
- name: Checkout tools branch (source build)
141+
if: ${{ steps.finalize.outputs.result == 'build' }}
142+
uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
143+
with:
144+
ref: ${{ inputs.tools_source_ref }}
145+
path: ${{ inputs.path }}
146+
147+
- name: Build tools from source
148+
if: ${{ steps.finalize.outputs.result == 'build' }}
149+
shell: bash # We're only building a trusted branch with the tools, so no need to run inside landrun.
150+
run: |
151+
cd "${{ inputs.path }}"
152+
lake build cache check-yaml graph
153+
ls .lake/build/bin/cache
154+
ls .lake/build/bin/check-yaml
155+
ls .lake/packages/importGraph/.lake/build/bin/graph

‎.github/workflows/PR_summary.yml‎

Lines changed: 12 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -17,14 +17,16 @@ jobs:
1717

1818
steps:
1919
- name: Checkout code
20-
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
20+
uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
2121
with:
2222
ref: ${{ github.event.pull_request.head.sha }}
2323
fetch-depth: 0
2424
path: pr-branch
25+
# Untrusted (potentially fork) checkout: don't persist the GITHUB_TOKEN into its .git/config.
26+
persist-credentials: false
2527

2628
- name: Checkout local actions
27-
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
29+
uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
2830
with:
2931
ref: ${{ github.workflow_sha }}
3032
fetch-depth: 1
@@ -211,10 +213,16 @@ jobs:
211213
declDiff=$("${CI_SCRIPTS_DIR}/pr_summary/declarations_diff.sh")
212214
if [ "$(printf '%s' "${declDiff}" | wc -l)" -gt 15 ]
213215
then
214-
declDiff="$(printf '<details><summary>\n\n%s\n\n</summary>\n\n%s\n\n</details>\n' "#### Declarations diff" "${declDiff}")"
216+
declDiff="$(printf '<details><summary>\n\n%s\n\n</summary>\n\n%s\n\n</details>\n' "#### Declarations diff (regex)" "${declDiff}")"
215217
else
216-
declDiff="$(printf '#### Declarations diff\n\n%s\n' "${declDiff}")"
218+
declDiff="$(printf '#### Declarations diff (regex)\n\n%s\n' "${declDiff}")"
217219
fi
220+
# Append a placeholder for the post-build, Lean-aware diff. The
221+
# `decls-diff.yml` workflow replaces the region between the markers (see
222+
# mathlib-ci's `updateDeclsDiffSection.py`); the regex block above is left
223+
# as-is. The markers are HTML comments (invisible when rendered), and the
224+
# heading carries the status (`pending` → `(Lean)` / `(Lean -- unavailable)`).
225+
declDiff="$(printf '%s\n\n<!-- DECLS_DIFF_LEAN_BEGIN -->\n#### Declarations diff (Lean -- pending)\n\n_Computed after the build finishes._\n<!-- DECLS_DIFF_LEAN_END -->\n' "${declDiff}")"
218226
git checkout "${currentHash}" --
219227
hashURL="https://github.com/${{ github.repository }}/pull/${{ github.event.pull_request.number }}/commits/${currentHash}"
220228
printf 'hashURL: %s' "${hashURL}"

0 commit comments

Comments
 (0)