feat(ModelTheory): quantifier elimination from elementary extension p…

.git-blame-ignore-revs

@@ -0,0 +1,6 @@
+# 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

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

@@ -66,6 +66,18 @@ runs:
         # 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")
             case "$BRANCH" in
@@ -121,6 +133,7 @@ runs:
             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

.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: 0cd6cbc879d9241f3b4f6cb7e8291e34128c5654
   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 }}

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

@@ -139,7 +139,7 @@ runs:
 
     - name: Checkout tools branch (source build)
       if: ${{ steps.finalize.outputs.result == 'build' }}
-      uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+      uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
       with:
         ref: ${{ inputs.tools_source_ref }}
         path: ${{ inputs.path }}

.github/actions/setup-build-env/action.yml

@@ -0,0 +1,160 @@
+# Shared runner setup for the self-hosted `build` and `test_lint` jobs in
+# build_template.yml. Both run on the same Hoskinson pool and need the same
+# preparation before they diverge (build → build + stage, test_lint →
+# fetch + test + lint): toolchain hygiene, jq, the cache-trust and get-tools
+# wiring, the PR-branch checkout, the elan toolchain and LEAN_SRC_PATH
+# environment, and the dependency download.
+#
+# The caller runs `Checkout local actions` (sparse `.github/actions` →
+# `workflow-actions/`) before invoking this action: that checkout puts both this
+# action and the sibling actions it calls (`cache-trust-dispatch`, `get-tools`)
+# on disk under `workflow-actions/`, so the `uses: ./workflow-actions/...` paths
+# below resolve relative to the workspace root, as in the calling workflow.
+#
+# Each `run:` step sets its own `shell:`, since composite steps do not inherit the
+# job's landrun `defaults.run.shell`.
+name: Set up build environment
+description: Shared self-hosted runner setup for the build and test_lint jobs.
+
+inputs:
+  pr_branch_ref:
+    description: Git ref of the PR branch to check out and build.
+    required: true
+  tools_branch_ref:
+    description: Git ref to build the CI tools from when not using the prebuilt artifact.
+    required: false
+    default: ''
+
+runs:
+  using: composite
+  steps:
+    # Prune old toolchains from `~/.elan`. That directory is mounted from the host
+    # and shared across the ephemeral job containers, so toolchains accumulate and
+    # nothing else trims them (host-side housekeeping only trims the mathlib `.ltar`
+    # cache). Keep the 5 most recent plus `nightly`/`stable`.
+    - name: prune old toolchains
+      shell: bash # just deletes old files; safe to run outside landrun
+      run: |
+        # Make sure to delete both the `~/.elan/toolchains/X` directory and the `~/.elan/update-hashes/X` file.
+        # Skip symbolic links (`-type d`), the current directory (`! -name .`), and `nightly` and `stable`.
+        if cd ~/.elan/toolchains && find . -maxdepth 1 -type d ! -name . -print0 | xargs -0 ls -1td | grep -v 'nightly$' | grep -v 'stable$' | tail -n +6 | xargs -I {} sh -c 'echo {} && rm -rf "{}" && rm "../update-hashes/{}"'; then
+            : # Do nothing on success
+        else
+            : # Do nothing on failure, but suppress errors
+        fi
+
+    # The Hoskinson runners may not have jq installed, so do that now.
+    - name: 'Setup jq'
+      uses: dcarbone/install-jq-action@4fcb5062d7ce9bc4382d1a352d19ba3ba2c317c1 # v4.0.1
+
+    # Compute the trust-classified container target and read fallback for this
+    # job. Sets MATHLIB_CACHE_FROM / MATHLIB_CACHE_PRIMARY in env so every
+    # subsequent `cache get` inherits them without per-call flag plumbing. Loaded
+    # from the trust-rooted `workflow-actions/` checkout, not the PR branch.
+    - name: Compute cache trust dispatch
+      uses: ./workflow-actions/.github/actions/cache-trust-dispatch
+      with:
+        repo: ${{ github.event.pull_request.head.repo.full_name || github.repository }}
+        branch: ${{ github.head_ref || github.ref_name }}
+        head-sha: ${{ github.event.pull_request.head.sha || github.sha }}
+
+    # Checkout the PR branch into a subdirectory. HEAD only (fetch-depth: 1) is
+    # enough: the cache is fetched HEAD-scoped and warmed from the master snapshot,
+    # so no parent-commit history is needed. This is untrusted (potentially fork)
+    # code we build, so don't leave the GITHUB_TOKEN in pr-branch/.git/config where
+    # that code could read it.
+    - name: Checkout PR branch
+      uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+      with:
+        ref: ${{ inputs.pr_branch_ref }}
+        fetch-depth: 1
+        path: pr-branch
+        persist-credentials: false
+        # The build runs this fork PR code sandboxed (landrun) with no persisted
+        # credentials, so checking it out under pull_request_target is safe.
+        allow-unsafe-pr-checkout: true
+
+    # Create empty directories so landrun doesn't complain.
+    - name: Create empty directories
+      shell: bash # We need to run this outside landrun, as it is a prerequisite for landrun!
+      run: |
+        mkdir -p pr-branch/.lake/
+        mkdir -p .cache/mathlib/
+        mkdir -p _work
+
+    # NOTE: if you copy this, consider using `leanprover/lean-action` instead.
+    # We install manually, to avoid running lean outside landrun.
+    - name: install elan
+      shell: bash
+      run: |
+        set -o pipefail
+        curl -o elan-init.sh -sSfL https://elan.lean-lang.org/elan-init.sh
+        chmod +x elan-init.sh
+        ./elan-init.sh -y --default-toolchain none
+        echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
+
+    - name: set toolchain directory
+      shell: bash
+      run: |
+        cd pr-branch
+        # Get the lake binary path from elan and extract toolchain directory
+        LAKE_PATH=$(elan which lake)
+        echo "Lake path: $LAKE_PATH"
+
+        # Extract the toolchain directory by removing /bin/lake from the end
+        TOOLCHAIN_DIR=$(dirname "$LAKE_PATH")
+        TOOLCHAIN_DIR=$(dirname "$TOOLCHAIN_DIR")
+        echo "Toolchain directory: $TOOLCHAIN_DIR"
+
+        # Set it as an environment variable for subsequent steps
+        echo "TOOLCHAIN_DIR=$TOOLCHAIN_DIR" >> "$GITHUB_ENV"
+
+    - name: set LEAN_SRC_PATH
+      shell: bash
+      run: |
+        cd pr-branch
+
+        # Start with the base paths
+        LEAN_SRC_PATH=".:$TOOLCHAIN_DIR/src/lean/lake"
+
+        # Extract package names from lake-manifest.json and validate them
+        # Only allow A-Z, a-z, 0-9, _, and - characters
+        # Build the LEAN_SRC_PATH by appending each validated package
+        PACKAGE_NAMES=$(jq -r '.packages[].name' lake-manifest.json)
+        for pkg in $PACKAGE_NAMES; do
+          if [[ "$pkg" =~ ^[A-Za-z0-9_-]+$ ]]; then
+            LEAN_SRC_PATH="$LEAN_SRC_PATH:.lake/packages/$pkg"
+          else
+            echo "Warning: Skipping invalid package name: $pkg"
+          fi
+        done
+
+        echo "LEAN_SRC_PATH=$LEAN_SRC_PATH"
+
+        # Set it as an environment variable for subsequent steps
+        echo "LEAN_SRC_PATH=$LEAN_SRC_PATH" >> "$GITHUB_ENV"
+
+    # Populate `tools-branch/` with the trusted CI tooling (the `cache` binary and
+    # the `lake-build-*` helper scripts invoked by path). Fast path: download the
+    # prebuilt `tools-bin` artifact published from master (canonical mathlib4 only,
+    # and only when the branch under test doesn't change the cache tool — get-tools
+    # makes that comparison against `source_dir`). Source build otherwise. See the
+    # get-tools action for the full trust rationale.
+    - name: Get CI tools
+      uses: ./workflow-actions/.github/actions/get-tools
+      with:
+        use_artifact: ${{ inputs.tools_branch_ref == '' && github.repository == 'leanprover-community/mathlib4' }}
+        tools_source_ref: ${{ inputs.tools_branch_ref != '' && inputs.tools_branch_ref || (github.event.pull_request.head.repo.fork && 'master' || inputs.pr_branch_ref) }}
+        source_dir: ${{ github.event.pull_request.head.repo.fork != true && 'pr-branch' || '' }}
+        github_token: ${{ github.token }}
+
+    - name: download dependencies
+      # We need network access to download dependencies. We run this inside
+      # landrun, but restrict disk access:
+      # - --rox access to `~/.elan` and `~/actions-runner/_work` (GitHub CI needs this)
+      # - --unrestricted-network as we need this to download dependencies
+      # - git needs read only access to `/etc`.
+      shell: landrun --unrestricted-network --rox /etc --rox /usr --rw /dev --rox /home/lean/.elan --rox /home/lean/actions-runner/_work --rw pr-branch/.lake/ --env PATH --env HOME --env GITHUB_OUTPUT --env CI -- bash -euxo pipefail {0}
+      run: |
+        cd pr-branch
+        lake env

.github/workflows/PR_summary.yml

@@ -17,16 +17,19 @@ jobs:
 
     steps:
     - name: Checkout code
-      uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+      uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
       with:
         ref: ${{ github.event.pull_request.head.sha }}
         fetch-depth: 0
         path: pr-branch
         # Untrusted (potentially fork) checkout: don't persist the GITHUB_TOKEN into its .git/config.
         persist-credentials: false
+        # Only trusted base-repo scripts run against this checkout, so checking out
+        # fork PR code under pull_request_target is safe.
+        allow-unsafe-pr-checkout: true
 
     - name: Checkout local actions
-      uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+      uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
       with:
         ref: ${{ github.workflow_sha }}
         fetch-depth: 1
@@ -64,7 +67,7 @@ jobs:
         fi
 
     - name: Set up Python
-      uses: actions/setup-python@a309ff8b426b58ec0e2a45f0f869d46889d02405 # v6.2.0
+      uses: actions/setup-python@ece7cb06caefa5fff74198d8649806c4678c61a1 # v6.3.0
       with:
         python-version: 3.12
 
@@ -230,6 +233,16 @@ jobs:
         echo "Compute technical debt changes"
         techDebtVar="$("${CI_SCRIPTS_DIR}/reporting/technical-debt-metrics.sh" pr_summary)"
 
+        # If the PR decreased technical debt, add the `tech debt` label.
+        # The metrics script emits a summary line "Decrease in <level> tech debt:" for each
+        # level (strong/weak) that went down (and "Increase ..."/"No changes ..." otherwise),
+        # so matching either of those two lines means the PR reduced some tech debt.
+        if grep -qE "Decrease in (strong|weak) tech debt" <<< "${techDebtVar}"
+        then
+          printf $'Adding "tech debt" label to PR %s\n' "${PR}"
+          gh pr edit "${PR}" --add-label "tech debt"
+        fi
+
         echo "Compute documentation reminder"
         workflowFilesChanged="$(grep '^\.github/workflows/' changed_files.txt || true)"
         if [ -n "${workflowFilesChanged}" ]

.github/workflows/actionlint.yml

@@ -9,7 +9,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
 
       - name: suggester / actionlint
         uses: reviewdog/action-actionlint@6fb7acc99f4a1008869fa8a0f09cfca740837d9d # v1.72.0
@@ -21,7 +21,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
 
       # Using our fork's PR branch until upstream merges the improved error reporting:
       # https://github.com/zgosalvez/github-actions-ensure-sha-pinned-actions/pull/288

.github/workflows/add_label_from_diff.yaml

@@ -22,7 +22,7 @@ jobs:
     if: github.repository == 'leanprover-community/mathlib4'
     steps:
     - name: Checkout master branch to build autolabel from
-      uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+      uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
       with:
         ref: master
         path: tools
@@ -38,13 +38,16 @@ jobs:
       run: |
         lake build autolabel
     - name: Checkout branch to label
-      uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+      uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
       with:
         ref: ${{ github.event.pull_request.head.sha || github.sha }}
         fetch-depth: 0
         path: pr-branch
         # Untrusted (potentially fork) checkout: don't persist the GITHUB_TOKEN into its .git/config.
         persist-credentials: false
+        # autolabel is built from the trusted base checkout and only reads these files,
+        # so checking out fork PR code under pull_request_target is safe.
+        allow-unsafe-pr-checkout: true
     - name: Run autolabel
       working-directory: pr-branch
       run: |