ci.yml

name: CI

on:
  # PR builds moved to pr-build.yml, which sandboxes untrusted PR code under bwrap in a
  # trusted (base-defined) workflow. This run is only the post-merge health check on main.
  push:
    branches: [main]

permissions:
  contents: read
  pull-requests: read  # scripts/lint-scope.sh reads the merged PRs' labels and branches

# Keep the cache publisher live under a burst of main pushes. GitHub retains at
# most one running and one pending run in this group: the running build is never
# cancelled before it can publish, while superseded pending commits do not each
# start an expensive cache-miss rebuild. In a burst, this deliberately coalesces
# intermediate commits' post-merge checks too; the newest pending tip rechecks
# the entire tree, though localizing a failure may then require bisection.
# Dependency reconciliation uses conclusive runs as evidence for the current
# pin, skipping coalesced commits without a completed build.
concurrency:
  group: main-ci-cache-publisher
  cancel-in-progress: false

env:
  # Temporary escape hatch for `lake exe cache get`, kept only for an easy rollback
  # during the transition to the cache tool's new default read endpoint. Set the
  # variable to `1` to send cache reads back to the legacy storage endpoint. Clear it to
  # return reads to the default endpoint on the next run: the cache tool treats unset,
  # empty, `0`, and `false` alike as off.
  MATHLIB_CACHE_DEBUG_USE_LEGACY: ${{ vars.MATHLIB_CACHE_DEBUG_USE_LEGACY }}

jobs:
  # Infrastructure regression suites run separately in infrastructure-tests.yml.
  build:
    runs-on: ubuntu-latest
    # Read by publish-lake-cache below, the only job that ever holds the upload secret.
    # Neither output reveals the secret's value or whether it is set, and neither is trusted
    # there: `staged` only decides whether that job runs at all, and `reported-toolchain` is
    # cross-checked against the pin that job reads for itself.
    outputs:
      staged: ${{ steps.stage.outputs.staged }}
      reported-toolchain: ${{ steps.stage.outputs.toolchain }}
    steps:
      # We expect the 262k default to be relevant at around 10m LOC, and this raised limit to be relevant at around 40m LOC.
      - name: Raise vm.max_map_count
        run: |
          target=1048576
          if [ "$(cat /proc/sys/vm/max_map_count)" -lt "$target" ]; then
            sudo -n sysctl -w vm.max_map_count="$target" >/dev/null 2>&1 \
              || sysctl -w vm.max_map_count="$target" >/dev/null 2>&1 || true
          fi
          now="$(cat /proc/sys/vm/max_map_count)"
          echo "vm.max_map_count=$now"
          [ "$now" -ge "$target" ] || echo "::warning::vm.max_map_count is $now, below $target"
      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262
        with:
          # This job elaborates every LMLExplore module, and Lean runs code at elaboration time.
          # Without this, checkout leaves an http.extraheader carrying GITHUB_TOKEN in the
          # workspace .git/config for the whole job, within reach of that code. Nothing here
          # needs it: no step calls the GitHub API or pushes, `lake exe cache get` talks to
          # Mathlib's own server, scripts/lake-cache-get.sh does anonymous GETs, and
          # `lake cache get` reads the local revision from .git without authenticating.
          persist-credentials: false
          # The immutable push base must be present for the complete local scope diff.
          # Bors batches can contain 128 commits, already exceeding the old depth of
          # 100. Full history also supports cache ancestor lookup without another fetch.
          fetch-depth: 0

      - name: Prepare pinned shared tools
        uses: TauCetiProject/TauCetiTools/.github/actions/setup@68ca7893e90b82454ab58ba64dca753a05cd2720
        with:
          tools-repository: TauCetiProject/TauCetiTools
          tools-ref: 68ca7893e90b82454ab58ba64dca753a05cd2720
          project-directory: .
      - name: Import-boundary guard (LMLExplore/ and LMLExplore.lean ⊬ roadmap/review)
        run: |
          if grep -rIn -E '^[[:space:]]*import[[:space:]]+(LMLRoadmaps|TauCetiReview)\b' LMLExplore/ LMLExplore.lean; then
            echo "::error::LMLExplore/ and LMLExplore.lean must not import LMLRoadmaps or TauCetiReview"
            exit 1
          fi

      # Option overrides, heartbeat instrumentation, and explicit metaprogramming are forbidden.
      # This cheap scan ignores comments without double quotes, conservatively includes
      # strings and names, and never elaborates code.
      - name: Reject option overrides and metaprogramming (allow local macros)
        run: |
          python3 scripts/check_source_options.py LMLExplore/ LMLExplore.lean

      # Restore only Mathlib's compressed, content-addressed `.ltar` download store. This is
      # deliberately narrower than a cache of the whole multi-gigabyte `./.lake` tree: `lake exe
      # cache get` remains authoritative, locally selects and unpacks the linked hashes, and
      # downloads anything this best-effort snapshot does not contain. The exact key makes a
      # repeated pin cheap; the same-toolchain prefix lets a new Mathlib pin reuse unchanged
      # blobs. The local action credits the corresponding Mathlib design and owns the shared key
      # namespace. Bump its `mathlib-ltar-v1` token if an incompatible or poisoned immutable entry
      # must be abandoned.
      - name: Restore Mathlib's compressed download cache
        id: mathlib_ltar_restore
        uses: ./.github/actions/restore-mathlib-ltars
        with:
          project-dir: .

      # Install elan from a pinned leanprover/elan release, verified by SHA-256, then install the
      # toolchain `lean-toolchain` names. This replaces leanprover/lean-action, which resolved
      # from a floating major tag and installed elan by piping an unpinned installer to `sh`; with
      # its build, test, lint and cache inputs all off, toolchain setup was all it did here. The
      # Mathlib fetch stays an explicit step below so a failed normal fetch can be retried with
      # `get!`, which force-downloads and unpacks every linked file instead of trusting a possibly
      # malformed restored `.ltar`. scripts/test_elan_pin.py keeps the copies of the pin honest.
      - name: Install elan (pinned + checksum) and the toolchain
        env:
          ELAN_SHA256: df0b2b3a439961ffcbb3985214365ffe40f49bc871df04dff268c7d8e21ca8b2
          ELAN_VER: v4.2.3
        run: |
          curl -sSL -H "Accept: application/octet-stream" \
            "https://github.com/leanprover/elan/releases/download/${ELAN_VER}/elan-x86_64-unknown-linux-gnu.tar.gz" -o elan.tar.gz
          echo "${ELAN_SHA256}  elan.tar.gz" | sha256sum -c -
          tar -xzf elan.tar.gz elan-init
          ./elan-init -y --default-toolchain none
          rm -f elan.tar.gz elan-init
          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
          export PATH="$HOME/.elan/bin:$PATH"
          elan toolchain install "$(cat lean-toolchain)"
          lean --version
          lake --version

      - name: Fetch Mathlib oleans, retrying with a forced full refetch
        run: |
          if ! lake exe cache get; then
            echo "::warning::lake exe cache get failed; forcing a full refetch"
            lake exe cache get!
          fi

      # Publish only official Mathlib downloads before LMLExplore source executes, so a cold
      # root compilation cannot delay warming for other jobs. PR builds remain restore-only.
      # GitHub cache keys are immutable; an exact restore needs no redundant save, while a
      # prefix restore is extended with the newly downloaded hashes under the exact current key.
      # Pruning is essential: without it, every prefix restore would carry all old pins forward
      # and each immutable snapshot would grow monotonically. If pruning itself breaks, leave main
      # green but skip publication rather than saving an unbounded snapshot.
      - name: Prune Mathlib's download cache to the current pin
        id: mathlib_ltar_prune
        if: ${{ steps.mathlib_ltar_restore.outputs.cache-hit != 'true' }}
        continue-on-error: true
        run: lake exe cache clean

      - name: Save Mathlib's compressed download cache
        if: ${{ steps.mathlib_ltar_restore.outputs.cache-hit != 'true' && steps.mathlib_ltar_prune.outcome == 'success' }}
        continue-on-error: true
        uses: actions/cache/save@0057852bfaa89a56745cba8c7296529d2fc39830
        with:
          path: ${{ steps.mathlib_ltar_restore.outputs.cache-dir }}/*.ltar
          key: ${{ steps.mathlib_ltar_restore.outputs.cache-primary-key }}

      # --- Lake artifact-cache restore (dormant until configured) --------------------
      # Restore LMLExplore's OWN oleans before building, exactly as pr-build.yml does. Without
      # this, the post-merge run recompiled the whole library from scratch on every push,
      # spending about 49 minutes to reproduce oleans the merge-queue build had produced
      # minutes earlier. Because the publisher is serialized, that capped publication at
      # roughly one snapshot an hour while several commits an hour were landing, and the
      # permanently stale snapshot is what pushed merge-queue builds onto the roughly
      # 55 minute cold-cache path.
      # No-op until the LAKE_CACHE_*_PUBLIC repo variables are set, as on the consuming side.
      - name: Configure the Lake artifact cache (no-op unless the public endpoints are set)
        env:
          PUBLIC_ARTIFACT_ENDPOINT: ${{ vars.LAKE_CACHE_ARTIFACT_ENDPOINT_PUBLIC }}
          PUBLIC_REVISION_ENDPOINT: ${{ vars.LAKE_CACHE_REVISION_ENDPOINT_PUBLIC }}
        run: |
          if [ -n "$PUBLIC_ARTIFACT_ENDPOINT" ] && [ -n "$PUBLIC_REVISION_ENDPOINT" ]; then
            {
              echo "LAKE_CACHE_DIR=$GITHUB_WORKSPACE/.lake/cache"
              echo "LAKE_ARTIFACT_CACHE=true"
              echo "LAKE_RESTORE_ARTIFACTS=true"
              echo "TAUCETI_CACHE_ENABLED=1"
            } >> "$GITHUB_ENV"
            echo "::notice::Lake artifact cache enabled — restoring LMLExplore's oleans and building incrementally"
          else
            echo "::notice::Lake artifact cache not configured — building LMLExplore/ from scratch (set the LAKE_CACHE_*_PUBLIC repo variables to enable)"
          fi

      # Anonymous GETs from the PUBLIC read host, the same trusted, publisher-built data
      # pr-build restores. The shared script retains hash-verified artifacts between attempts,
      # then discards the partial cache only if every attempt remains incomplete; see its header.
      #
      # What this does NOT establish: that a restored module matches what a compile of the
      # checked-out source would produce. Lake keys artifacts by an input hash that is a single
      # UInt64 and explicitly not cryptographic (Lake/Build/Trace.lean carries a TODO to replace
      # it), so content addressing is a deduplication scheme here, not an integrity guarantee.
      # Restoring on main also gives up main's former role as the one build that took nothing on
      # faith. nightly-verify.yml reinstates it on a daily cadence: it rebuilds from source with the
      # cache off and compares the resulting oleans byte for byte against a cache-restored build of
      # the same commit. That is a detector, not an equivalent guarantee, and its own header spells
      # out the exposure window it leaves. The two are a pair; do not enable this restore without
      # that nightly running.
      - name: Fetch LMLExplore's own oleans from the Lake cache
        if: ${{ env.TAUCETI_CACHE_ENABLED == '1' }}
        env:
          # Passed under non-LAKE_ names so Lake never sees the deprecated endpoint
          # environment variables; the script hands it the endpoints through a `--service` config.
          PUBLIC_ARTIFACT_ENDPOINT: ${{ vars.LAKE_CACHE_ARTIFACT_ENDPOINT_PUBLIC }}
          PUBLIC_REVISION_ENDPOINT: ${{ vars.LAKE_CACHE_REVISION_ENDPOINT_PUBLIC }}
        run: bash scripts/lake-cache-get.sh .

      - name: Save verified Lake archive records before building
        run: python3 scripts/lake_cache_reuse.py snapshot . "$RUNNER_TEMP/lake-cache-reuse.json"

      - name: Audit import headers against the complete source inventory
        run: python3 scripts/check-imports.py

      # No aggregator check: the root LMLExplore.lean is intentionally empty and imports nothing.
      # The build globs every LMLExplore/ module directly, so nothing depends on a root that
      # re-exports the library.
      - name: Build
        env:
          # Restore only from the locally-populated $LAKE_CACHE_DIR the step above filled;
          # never let the build itself reach a remote cache service. Same rule as the
          # sandboxed build in pr-build.yml and as the publish step below.
          LAKE_NO_CACHE: "true"
        # `--iofail`, as in the sandboxed PR build (TauCetiTools' sandbox-build.sh): the build
        # fails if any module, dependencies included, logs a warning or an info message. A plain
        # `lake build` here let main stay green while every PR build failed on deprecation
        # warnings in LML.
        run: lake build --iofail

      # The same shared checks as trusted PR builds, compiled from merged main's sources.
      - name: Shared ownership and axiom audits
        run: |
          bash scripts/build-audit-driver.sh . scripts "$RUNNER_TEMP/audit-driver"
          lake env "$RUNNER_TEMP/audit-driver/audit-driver"

      # Read compiled module flags with the canonical direct-artifact checker.
      - name: Module-system audit (every LMLExplore file opts into module)
        env:
          LAKE_NO_CACHE: "true"
        run: lake exe module-system

      # Environment lint. A compiled driver (scripts/LintEnvDriver.lean) imports the LMLExplore/
      # modules in scope and runs Mathlib's default `#lint` set minus docBlame (simpNF,
      # checkType, synTaut, ...) plus a module-system-reliable docstring scan (the
      # docBlame linter is blind across module boundaries; see the script header),
      # comparing linter-qualified violations against the grandfathered baseline in
      # scripts/lint-baseline.txt: new violations fail, fixed baseline entries print
      # a ratchet reminder. `@[nolint <linter>]` applications must be accounted for
      # in scripts/lint-nolints-allowlist.txt, per (linter, declaration) pair.
      # PR-time enforcement runs inside the
      # bwrap sandbox in pr-build.yml (this lint executes the linted code); this
      # post-merge run is the health check on main, like the audits above.
      # Like PR builds and the merge queue, this lints only the LMLExplore modules the push changed
      # (the whole library if a merged PR was labelled full-lint or was a lint repair PR); the
      # daily lint-full.yml run lints everything. Superseded runs of this workflow are cancelled,
      # so a push's scope can be skipped here, but its merge group already linted it.
      - name: Decide the environment-lint scope
        env:
          GH_TOKEN: ${{ github.token }}
          REPO: ${{ github.repository }}
          EVENT: push
          BASE: ${{ github.event.before }}
          HEAD: ${{ github.sha }}
          SCOPE_REPO: .
        run: bash scripts/lint-scope.sh "$RUNNER_TEMP/lint-scope"

      - name: Environment lint (default linters + docstring scan vs grandfathered baseline)
        env:
          LAKE_NO_CACHE: "true"
        run: bash scripts/lint-env.sh

      - name: Dot-notation namespace lint (Mathlib type namespaces stay at root)
        run: python3 scripts/lint-dot-notation.py

      # Source style lint. The wrapper validates one complete LMLExplore/** source list, applies
      # Mathlib's copyright/Authors checks directly (the empty LMLExplore.lean root is exempt), and
      # generates an import-all module under .lake/ for lint-style's text-based checks. This is
      # deliberately narrower than the command header linter's unrelated import and module-doc
      # checks; the empty root makes that command linter skip every library module at this pin.
      - name: Source style lint (copyright headers + text linters)
        run: bash scripts/lint-style.sh

      # --- Lake artifact-cache publish (dormant until configured) ---------------------
      # Publish LMLExplore's OWN oleans (root-package only) to the Lake cache, so pr-build can
      # fetch them and recompile only a PR's changed modules instead of the whole library.
      # Mathlib's oleans are never uploaded: `-o` records only root-package outputs, and
      # Mathlib stays on `lake exe cache get`. See pr-build.yml for the consuming side.
      #
      # The upload is split across two jobs, and the split is the security boundary rather
      # than a convenience. THIS job runs `lake build` unsandboxed, as the runner user, on
      # whatever landed on main, and Lean executes code at elaboration time: `run_cmd`,
      # `initialize` and macro-time IO are all unrestricted, since the scope, import-boundary
      # and set_option guards are textual scans. Such code can therefore rewrite
      # `$HOME/.elan/bin/lake`, prepend a directory of its own to every later step's PATH
      # through `$GITHUB_PATH`, or set LD_PRELOAD or BASH_ENV for every later step through
      # `$GITHUB_ENV`. A secret given to any later step of this job is a secret given to code
      # that landed on main, whatever that step does with it. So this job only stages the
      # artifacts, and publish-lake-cache below, a fresh runner with only a sparse pin/helper
      # checkout and no project workspace, is the only place the key exists. The helper stays
      # inert until the key-bearing step has exited.
      - name: Configure the Lake cache staging (no-op unless the S3 endpoints are set)
        id: cachecfg
        env:
          # The secret is deliberately not referenced anywhere in this job, not even to test
          # whether it is set. The endpoints alone decide whether staging runs; the publish
          # job skips with a notice if the key turns out to be missing.
          S3_ARTIFACT_ENDPOINT: ${{ vars.LAKE_CACHE_ARTIFACT_ENDPOINT }}
          S3_REVISION_ENDPOINT: ${{ vars.LAKE_CACHE_REVISION_ENDPOINT }}
        run: |
          if [ -n "$S3_ARTIFACT_ENDPOINT" ] && [ -n "$S3_REVISION_ENDPOINT" ]; then
            echo "enabled=true" >> "$GITHUB_OUTPUT"
            echo "::notice::Lake cache upload configured; staging LMLExplore's oleans"
          else
            echo "enabled=false" >> "$GITHUB_OUTPUT"
            echo "::notice::Lake cache upload not configured, skipping (set the LAKE_CACHE_ARTIFACT_ENDPOINT / LAKE_CACHE_REVISION_ENDPOINT repo variables and the LAKE_CACHE_KEY secret to enable)"
          fi

      # Merge-group CI normally publishes and publicly confirms the exact commit before GitHub
      # lands it. Avoid packing and transferring the same map again on main when that happened.
      # This is deliberately fail-open: only a downloaded, structurally valid exact map sets
      # exists=true. A direct human merge has no map, and any 404, timeout, service error or
      # malformed response therefore retains the staging/publication fallback below.
      - name: Probe for this exact cache on the public endpoint
        id: exact_cache
        if: ${{ steps.cachecfg.outputs.enabled == 'true' }}
        env:
          PUBLIC_REVISION_ENDPOINT: ${{ vars.LAKE_CACHE_REVISION_ENDPOINT_PUBLIC }}
          REVISION: ${{ github.sha }}
        run: |
          echo "exists=false" >> "$GITHUB_OUTPUT"
          TOOLCHAIN="$(cat lean-toolchain 2>/dev/null || true)"
          if python3 scripts/lake_cache_probe.py \
              "$PUBLIC_REVISION_ENDPOINT" "$TOOLCHAIN" "$REVISION"; then
            echo "exists=true" >> "$GITHUB_OUTPUT"
            echo "::notice::Exact Lake cache map is already public; skipping duplicate staging and publication"
          else
            echo "::notice::Exact Lake cache map is absent or unreadable; retaining main's publication fallback"
          fi

      - name: Stage LMLExplore's oleans for the publish job
        id: stage
        if: ${{ steps.cachecfg.outputs.enabled == 'true' && steps.exact_cache.outputs.exists != 'true' }}
        env:
          # Restated at step level, and the same values the restore step sets job-wide when the
          # public endpoints are configured, so staging works either way: with the restore on,
          # the health-check build already packed these artifacts; with it off, the pack below
          # is what puts them in the cache directory for `lake_cache_publish.py stage` to find.
          LAKE_ARTIFACT_CACHE: "true"
          LAKE_RESTORE_ARTIFACTS: "true"
          # Don't download during the packing build — we only want to PUT, not GET. (The
          # S3 host needs SigV4 even for reads, so an anonymous GET here would 403 anyway.)
          LAKE_NO_CACHE: "true"
          LAKE_CACHE_DIR: ${{ github.workspace }}/.lake/cache
          PUBLIC_ARTIFACT_ENDPOINT: ${{ vars.LAKE_CACHE_ARTIFACT_ENDPOINT_PUBLIC }}
          LAKE_CACHE_FULL_PUBLICATION: ${{ vars.LAKE_CACHE_FULL_PUBLICATION }}
        run: |
          # Pack the already-built oleans into the local Lake cache (no recompile, since the
          # health-check build above left matching traces), emit the root-package
          # input->output mappings. The key-free planner keeps the FULL map and stages
          # new archives plus availability-check misses, reusing only matching downloaded
          # records saved before the build. The isolated publisher SHA-256 checks inherited bytes.
          lake build >/dev/null
          python3 scripts/lake_cache_reuse.py reconnect . "$RUNNER_TEMP/lake-cache-reuse.json"
          # Hash the linked archives themselves, ignoring any old .ltar.hash sidecars.
          lake build --no-build --rehash -o .lake/outputs.jsonl
          echo "root-package mapping entries: $(wc -l < .lake/outputs.jsonl)"
          python3 scripts/lake_cache_publish.py stage . "$RUNNER_TEMP/lake-cache-staging" \
            --index "$RUNNER_TEMP/lake-cache-reuse.json"
          # The isolated publisher never configures the workspace, so it cannot derive
          # the toolchain and platform halves of the upload scope. It supplies them from the sparse pin
          # instead, which is right only while the package config keeps the two assumptions
          # below. Check them here, where the workspace does exist: `platformIndependent` is
          # what makes Lake leave the platform out of the scope (the publisher's map scope), while
          # `fixedToolchain` or `bootstrap` would make Lake leave the toolchain out of it (which
          # the publisher is told to include). Either silent mismatch would publish under a scope
          # pr-build's `lake cache get --service ... --repo` never reads, i.e. a cache never hit.
          if ! grep -Eq '^[[:space:]]*platformIndependent[[:space:]]*=[[:space:]]*true' lakefile.toml; then
            echo "::error::lakefile.toml no longer sets platformIndependent = true; publish-lake-cache must now include the platform scope"
            exit 1
          fi
          if grep -Eq '^[[:space:]]*(fixedToolchain|bootstrap)[[:space:]]*=[[:space:]]*true' lakefile.toml; then
            echo "::error::lakefile.toml now sets fixedToolchain or bootstrap; Lake drops the toolchain from the scope for such a package, so publish-lake-cache must stop including the toolchain scope"
            exit 1
          fi
          # `lake env` reports the workspace's own view of the toolchain, which is exactly the
          # `Env.toolchain` Lake scopes an upload by. The publish job does not take this on
          # faith: it reads lean-toolchain itself and fails if the two disagree. Reporting it
          # anyway turns a disagreement into a loud failure instead of a silent wrong scope.
          TOOLCHAIN="$(lake env printenv ELAN_TOOLCHAIN || true)"
          if [ -z "$TOOLCHAIN" ]; then
            echo "::error::could not determine the Lean toolchain that scopes the cache upload"
            exit 1
          fi
          printf 'toolchain=%s\n' "$TOOLCHAIN" >> "$GITHUB_OUTPUT"
          echo "staged=true" >> "$GITHUB_OUTPUT"

      - name: Hand the staged oleans to the publish job
        if: ${{ steps.stage.outputs.staged == 'true' }}
        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
        with:
          name: lake-cache-staging
          path: ${{ runner.temp }}/lake-cache-staging
          if-no-files-found: error
          # Long enough to inspect a failed publish, short enough not to accumulate a
          # 60 MB artifact per push to main.
          retention-days: 1
          # The staged files are already-compressed `.ltar` archives; recompressing them
          # burns CPU on both ends and saves nothing.
          compression-level: 0

  # Run the secret-bearing upload on a fresh runner through the same hardened publisher used
  # by merge-group CI. Main publication remains a fallback: merge groups normally publish the
  # exact commit before landing, while this covers human-owned changes and operational retries.
  publish-lake-cache:
    needs: [build]
    if: ${{ needs.build.result == 'success' && needs.build.outputs.staged == 'true' }}
    permissions:
      contents: read
    uses: ./.github/workflows/publish-lake-cache.yml
    with:
      tools_repository: TauCetiProject/TauCetiTools
      tools_ref: 68ca7893e90b82454ab58ba64dca753a05cd2720
      revision: ${{ github.sha }}
      artifact-name: lake-cache-staging
      reported-toolchain: ${{ needs.build.outputs.reported-toolchain }}
      publication-required: false
    secrets:
      LAKE_CACHE_KEY: ${{ secrets.LAKE_CACHE_KEY }}