[codex] Add finset supremum and infimum convergence lemmas

.git-blame-ignore-revs

@@ -0,0 +1,8 @@
+# 2024-05-20 replace `refine'` with one underscore by `refine` (#13059)
+7493b5f81b4c031b87877c5c124bea1ddc4e567d
+# 2024-05-24 replace many `refine'` with `refine` (#13166)
+fc48848e4374f13c796a7399bfccd2e228f776df
+# 2025-11-19 move Mathlib to the module system (#31786)
+6a54a80825b060ab20dc31751ebdce78b3a3b518
+# 2025-12-01 fix spelling in doc-strings (#32286)
+b728e1450a53133aa4171eeadc0bc8d3ee58415c

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

@@ -0,0 +1,202 @@
+# Single source of truth mapping (repo, ref) → (upload container,
+# read fallback chain) for Mathlib's multi-container cache.
+#
+# Called by build, upload_cache, and post_steps in build_template.yml so
+# trust classification is decided in exactly one place. Lean-side cache
+# logic stays branch-agnostic; this composite is the seam where CI-only
+# trust policy lives.
+
+name: Cache trust dispatch
+description: Compute the cache container target and read fallback for this job.
+
+inputs:
+  repo:
+    description: GitHub repo full name (`owner/name`).
+    required: true
+  branch:
+    description: |
+      Branch name (`github.head_ref || github.ref_name`); on tag-triggered
+      runs this is the tag name, distinguished via `github.ref_type` inside
+      the dispatch step.
+    required: true
+  head-sha:
+    description: |
+      Head commit SHA for the ref being built. Used as the per-commit cache
+      namespace (`MATHLIB_CACHE_REPO_SCOPE`) for fork-trust uploads, so a
+      closed/hidden PR's poisoned artifacts cannot be served to a later
+      honest PR from the same fork.
+    required: true
+
+# Outputs are mirrored to $GITHUB_ENV inside the step, which is what
+# downstream `cache get` / `cache put-staged` calls actually read. We
+# also expose them as action outputs for callers that need them in
+# `with:` blocks (e.g. constructing further `if:` conditions).
+outputs:
+  primary:
+    description: Container name for uploads (master, forks, nightly-testing, pr-toolchain-tests).
+    value: ${{ steps.dispatch.outputs.primary }}
+  read-chain:
+    description: |
+      Comma-separated read fallback chain for `MATHLIB_CACHE_FROM`. Empty
+      when the job should use the cache tool's repo-level default.
+    value: ${{ steps.dispatch.outputs.read-chain }}
+  repo-scope:
+    description: |
+      Per-commit namespace suffix for `MATHLIB_CACHE_REPO_SCOPE`. Set to
+      the head SHA when uploading to fork-trust containers; empty for
+      master / nightly / pr-toolchain-tests uploads where scoping isn't
+      applied.
+    value: ${{ steps.dispatch.outputs.repo-scope }}
+
+runs:
+  using: composite
+  steps:
+    - name: Compute trust dispatch
+      id: dispatch
+      shell: bash
+      run: |
+        REPO="${{ inputs.repo }}"
+        BRANCH="${{ inputs.branch }}"
+        HEAD_SHA="${{ inputs.head-sha }}"
+        # Whether `branch` names a branch or a tag. Read from the run context
+        # rather than an input: unlike `repo`/`branch`, the value does not
+        # depend on which event shape (PR vs push) the caller handles.
+        REF_TYPE="${{ github.ref_type }}"
+        PRIMARY=""
+        READ_CHAIN=""
+        REPO_SCOPE=""
+
+        # Security note: this dispatch is NOT the trust boundary for writes.
+        # The real enforcement is the OIDC bearer token minted in upload_cache:
+        # the token is scoped to a specific container, so a malicious actor
+        # rewriting this case to `--container=master` from a fork build would
+        # be 403'd by Azure regardless. The dispatch exists so the workflow
+        # does the right thing in the honest case; defence in depth is RBAC.
+
+        # Privileged containers (master, nightly-testing, pr-toolchain-tests) are
+        # writable only by a repo's own native CI, whose OIDC token is RBAC-scoped
+        # to match. A cross-repo pull request is built by build_fork.yml with
+        # fork-trust credentials whatever repo the PR head lives on (e.g. a `bump/*`
+        # branch on the mathlib4-nightly-testing fork), so it can only write
+        # `forks`. `GITHUB_REPOSITORY` is the repo the workflow runs as (the base
+        # repo for `pull_request_target`), i.e. the one whose credentials this job
+        # holds; when it differs from `$REPO`, the build is a fork and targets
+        # `forks` regardless of the head repo's own trust class.
+        if [ "$REPO" != "$GITHUB_REPOSITORY" ]; then
+          PRIMARY="forks"
+        else
+        case "$REPO" in
+          "leanprover-community/mathlib4")
+            if [ "$REF_TYPE" = "tag" ]; then
+              case "$BRANCH" in
+                v4.*)
+                  # `v4.*` release tags: release_cache.yml rebuilds off-master
+                  # release commits (patch releases, patched release
+                  # candidates) and publishes them into `master`, the container
+                  # canonical checkouts read. Tag creation is restricted to
+                  # release managers by a tag ruleset, and the
+                  # `cache-upload-master` environment admits `v4.*` tag refs,
+                  # so these builds carry master trust. Reads are `master`-only
+                  # for the same fill-in reason as the master/staging arm
+                  # below.
+                  PRIMARY="master"
+                  READ_CHAIN="master"
+                  ;;
+                *)
+                  # Other tags have no trust class of their own:
+                  # fork-equivalent, like the dev-branch arm below.
+                  PRIMARY="forks"
+                  READ_CHAIN="master,forks,legacy"
+                  ;;
+              esac
+            else
+              case "$BRANCH" in
+                "master"|"staging")
+                  # Master, staging, and `v4.*` release tags (above) are the
+                  # only writers that feed `master` (`staging` is bors's merge
+                  # candidate, which fast-forwards to `master`). Read `master`
+                  # only, not the default [master, legacy]: files the read
+                  # chain serves are skipped at stage time, so keeping `legacy`
+                  # would leave legacy-only files out of `master` for good.
+                  # Reading `master` alone turns them into misses that get
+                  # rebuilt and uploaded, so `master` fills itself into a
+                  # standalone cache. (Only PRIMARY=master does this; other
+                  # runs write to `forks` and keep the wider chain.)
+                  PRIMARY="master"
+                  READ_CHAIN="master"
+                  ;;
+                *)
+                  # `bors trying`, `ci-dev/*`, maintainer dev branches on the
+                  # canonical repo: trust level is fork-equivalent (the OIDC
+                  # token's RBAC scopes them to `forks`). Reads must widen
+                  # past the default [master, legacy] so the post-build
+                  # verification finds the just-uploaded fork-trust artifacts.
+                  PRIMARY="forks"
+                  READ_CHAIN="master,forks,legacy"
+                  ;;
+              esac
+            fi
+            ;;
+          "leanprover-community/mathlib4-nightly-testing")
+            case "$BRANCH" in
+              "nightly-testing"|"nightly-testing-green"|"staging"|bump/*)
+                # Trusted nightly refs use the default [nightly-testing, legacy].
+                # It excludes `pr-toolchain-tests` so an upload from a
+                # `lean-pr-testing-*` branch never reaches a trusted-nightly
+                # consumer.
+                PRIMARY="nightly-testing"
+                ;;
+              *)
+                # `lean-pr-testing-*`, `batteries-pr-testing-*`, etc.:
+                # least-trusted (can build with arbitrary toolchains). Widen
+                # reads to recover this branch's own previously-uploaded
+                # artifacts; trusted-nightly stays preferred where hash
+                # spaces happen to align.
+                PRIMARY="pr-toolchain-tests"
+                READ_CHAIN="pr-toolchain-tests,nightly-testing,legacy"
+                ;;
+            esac
+            ;;
+          *)
+            # Foreign fork. The cache tool's default chain for a fork repo
+            # is [master, forks, legacy] (master-first): master supplies the
+            # bulk of unchanged upstream deps, forks supplies PR-specific
+            # files. No widening needed, so MATHLIB_CACHE_FROM stays unset.
+            PRIMARY="forks"
+            ;;
+        esac
+        fi
+
+        # Per-commit cache namespace, only for fork-trust uploads. Closes the
+        # within-fork temporal replay attack: each commit's CI run gets its
+        # own /f/{repo}/{sha}/... namespace, so artifacts from a closed/
+        # hidden PR cannot be served to a later honest build on the same
+        # fork. Master / nightly / pr-toolchain-tests uploads stay un-scoped:
+        # master has a single writer (no replay risk), and the per-toolchain
+        # hash partitioning isolates nightly and toolchain-test classes via
+        # their root-hash inputs.
+        if [ "$PRIMARY" = "forks" ]; then
+          REPO_SCOPE="$HEAD_SHA"
+        fi
+
+        echo "primary=$PRIMARY"           >> "$GITHUB_OUTPUT"
+        echo "read-chain=$READ_CHAIN"     >> "$GITHUB_OUTPUT"
+        echo "repo-scope=$REPO_SCOPE"     >> "$GITHUB_OUTPUT"
+        echo "MATHLIB_CACHE_PRIMARY=$PRIMARY" >> "$GITHUB_ENV"
+        if [ -n "$READ_CHAIN" ]; then
+          echo "MATHLIB_CACHE_FROM=$READ_CHAIN" >> "$GITHUB_ENV"
+        fi
+        if [ -n "$REPO_SCOPE" ]; then
+          echo "MATHLIB_CACHE_REPO_SCOPE=$REPO_SCOPE" >> "$GITHUB_ENV"
+        fi
+        # Visible in CI logs so a glance at any cache-touching step shows
+        # what trust class the job is operating under.
+        SCOPE_NOTE=""
+        if [ -n "$REPO_SCOPE" ]; then
+          SCOPE_NOTE=", MATHLIB_CACHE_REPO_SCOPE=$REPO_SCOPE"
+        fi
+        if [ -n "$READ_CHAIN" ]; then
+          echo "cache-trust-dispatch: REPO=$REPO BRANCH=$BRANCH → container=$PRIMARY, MATHLIB_CACHE_FROM=$READ_CHAIN$SCOPE_NOTE"
+        else
+          echo "cache-trust-dispatch: REPO=$REPO BRANCH=$BRANCH → container=$PRIMARY, MATHLIB_CACHE_FROM=<default>$SCOPE_NOTE"
+        fi

.github/actions/get-cache/action.yml

@@ -0,0 +1,115 @@
+# Get this commit's oleans, in two phases:
+#   1. Warm the cache from the `cache-snapshot` GitHub artifact (canonical repo only).
+#   2. Fetch this commit's oleans from the remote cache with the trusted master-built binary.
+# The fetch is HEAD-scoped (reads only this commit's own cache scope). The warm is fail-safe
+# (any failure → just the remote fetch) and its source is hardcoded, so nothing can redirect
+# the download off the trusted master pipeline.
+name: Get cache
+description: Get this commit's oleans into the local cache.
+inputs:
+  working_directory:
+    description: The lake project to fetch the cache for (e.g. the checked-out PR branch).
+    required: true
+  cache_bin:
+    description: Path to the trusted `cache` binary, relative to `working_directory`.
+    required: true
+runs:
+  using: composite
+  steps:
+    # 1. Warm cache from the GitHub artifact. Resolve which snapshot to use: the one built
+    #    at this commit's merge-base with master (its unchanged files hash identically
+    #    there), else the newest still-retained one at-or-before it, else the latest (a
+    #    merge-base older than retention, or any failure, lands here). Canonical repo only.
+    - name: Resolve cache snapshot
+      id: resolve
+      if: ${{ github.repository == 'leanprover-community/mathlib4' }}
+      shell: bash
+      env:
+        GH_TOKEN: ${{ github.token }}
+        HEAD_SHA: ${{ github.event.pull_request.head.sha || github.sha }}
+      run: |
+        set -uo pipefail
+        runs="repos/leanprover-community/mathlib4/actions/workflows/build.yml/runs?branch=master&event=push&status=success"
+
+        # Each helper prints a matching successful master-push run-id, or empty.
+        run_at()     { gh api "${runs}&head_sha=$1" --jq '.workflow_runs[0].id // empty' 2>/dev/null || true; }
+        latest_run() { gh api "${runs}&per_page=1"  --jq '.workflow_runs[0].id // empty' 2>/dev/null || true; }
+        # newest run created at-or-before date $1, but not older than cutoff $2
+        newest_before() {
+          gh api "${runs}&per_page=100" 2>/dev/null | jq -r --arg d "$1" --arg c "$2" \
+            '[.workflow_runs[] | select(.created_at <= $d and ($c == "" or .created_at >= $c))][0].id // empty' \
+            2>/dev/null || true
+        }
+        # True if run-id $1 actually carries a `cache-snapshot` artifact. Older runs
+        # predate the feature and artifacts expire, so a successful run is not enough.
+        # Filters server-side by name, but re-checks in jq in case `name` is ignored.
+        has_snapshot() {
+          [[ -n "$(gh api "repos/leanprover-community/mathlib4/actions/runs/$1/artifacts?name=cache-snapshot&per_page=100" \
+            --jq '.artifacts[] | select(.name == "cache-snapshot") | .id' 2>/dev/null | head -1 || true)" ]]
+        }
+
+        # This PR's merge-base with master (+ its commit date), and the cutoff below which
+        # snapshots have expired (retention ~14d).
+        mb_info=$(gh api "repos/leanprover-community/mathlib4/compare/master...${HEAD_SHA}" \
+          --jq '.merge_base_commit | "\(.sha) \(.commit.committer.date)"' 2>/dev/null || true)
+        read -r mb mb_date <<< "${mb_info}"
+        cutoff=$(date -u -d '13 days ago' +%Y-%m-%dT%H:%M:%SZ 2>/dev/null || true)
+
+        # Prefer the merge-base's snapshot (while still retained), then the newest one
+        # before it, then the latest of all.
+        run_id=""
+        if [[ -n "${mb}" && ( -z "${cutoff}" || "${mb_date}" > "${cutoff}" ) ]]; then
+          run_id=$(run_at "${mb}")
+          [[ -z "${run_id}" ]] && run_id=$(newest_before "${mb_date}" "${cutoff}")
+        fi
+        [[ -z "${run_id}" ]] && run_id=$(latest_run)
+
+        # The resolved run may carry no `cache-snapshot` artifact: an older merge-base
+        # predating the feature, or one whose artifact already expired (older-than-today
+        # runs often won't have one). Rather than let the download step hard-error on a
+        # missing artifact, confirm it's present; if not, fall back to the latest master
+        # run, and warm only if that one has it.
+        if [[ -n "${run_id}" ]] && ! has_snapshot "${run_id}"; then
+          echo "Run ${run_id} has no cache-snapshot artifact; falling back to latest master run."
+          run_id=$(latest_run)
+          if [[ -n "${run_id}" ]] && ! has_snapshot "${run_id}"; then
+            run_id=""
+          fi
+        fi
+
+        echo "Resolved cache-snapshot run_id: '${run_id}' (merge-base: ${mb:-unknown})"
+        echo "run_id=${run_id}" >> "$GITHUB_OUTPUT"
+
+    - name: Warm cache from GitHub artifact
+      if: ${{ steps.resolve.outputs.run_id != '' }}
+      continue-on-error: true # fail-safe: fall back to the remote fetch (step 2)
+      uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
+      with:
+        name: cache-snapshot
+        path: /home/lean/.cache/mathlib
+        repository: leanprover-community/mathlib4
+        run-id: ${{ steps.resolve.outputs.run_id }}
+        github-token: ${{ github.token }}
+
+    # 2. Fetch this commit's oleans from the remote cache with the trusted `cache` binary
+    #    (outside landrun). Runs on every repo; the warm above just gives the canonical
+    #    repo a local head start. HEAD-scoped: reads only this commit's own cache scope.
+    - name: Fetch cache from remote
+      shell: bash
+      env:
+        WORKDIR: ${{ inputs.working_directory }}
+        CACHE_BIN: ${{ inputs.cache_bin }}
+        CACHE_REPO: ${{ github.event.pull_request.head.repo.full_name || github.repository }}
+      run: |
+        set -eo pipefail
+        cd "${WORKDIR}"
+        rm -rf .lake/build/lib/lean/Mathlib
+        log="${RUNNER_TEMP:-/tmp}/cache-get.log"
+        # --repo so fork PRs also read their own repo-namespaced cache (master is read flat,
+        # so this still gets the master bulk); for in-repo runs it resolves to the same repo.
+        "${CACHE_BIN}" --repo="${CACHE_REPO}" get 2>&1 | tee "${log}"
+        # Warmth = how much the snapshot covered HEAD: files already cached locally
+        # (just decompressed) vs downloaded from Azure. Parsed best-effort from the log.
+        warm=$(grep -oE 'Decompressing [0-9]+ already-cached' "${log}" | grep -oE '[0-9]+' | head -1 || true)
+        cold=$(grep -oE 'Attempting to download [0-9]+' "${log}" | grep -oE '[0-9]+' | head -1 || true)
+        echo "Cache warmth: ${warm:-0} already-cached (warm) / ${cold:-0} downloaded from Azure (cold)"

.github/actions/get-mathlib-ci/README.md

@@ -25,7 +25,7 @@ then use the local action:
 
 ```yaml
 - name: Checkout local actions
-  uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+  uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
   with:
     ref: ${{ github.workflow_sha }}
     fetch-depth: 1

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

@@ -10,7 +10,7 @@ inputs:
     # Default pinned commit used by workflows unless they explicitly override.
     # Update this ref as needed to pick up changes to mathlib-ci scripts
     # This is also updated automatically by .github/workflows/update_dependencies.yml
-    default: 5aee9d4ce5a39050c72b4aa46015a824b0c189ac
+    default: 57c68e7faac5aea96e58a94ca4a334a1999f0d31
   path:
     description: Checkout destination path.
     required: false
@@ -33,7 +33,7 @@ runs:
   using: composite
   steps:
     - name: Get mathlib-ci
-      uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+      uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
       with:
         repository: leanprover-community/mathlib-ci
         ref: ${{ inputs.ref }}