Enable queue validation and independent project metadata

.github/CODE_QUALITY.md

@@ -34,15 +34,15 @@ The generated module-system indexes import every library file, so building them
 
 Current checks:
 
-- every `.lean` file under `LeanPool/`, plus `LeanPool.lean`, is reachable from `LeanPool.lean`
+- Lake discovers every `.lean` file under `LeanPool/`; every project source is also reachable from its public `Imports.lean`
 - every content `.lean` file except `LeanPool.lean` has the exact four-line file header
 - content files do not contain `set_option`, `nolint` waivers, broad `import Mathlib`, `sorry`, `admit`, unchecked declarations (`axiom`, `constant`, `unsafe`, `partial`, `opaque`, `@[extern]`), or diagnostic commands (`#check`, `#print`, `#eval`, `#reduce`, `#guard_msgs`, `#lint`)
 - content files do not manipulate elaborator options programmatically: option-API tokens (`withOptions`, `modifyOptions`, `withRecDepth`, `withCurrHeartbeats`, `KVMap`/`Options`/`Option` setters, ...) and gated option names (`maxRecDepth`, `maxHeartbeats`, `maxSynthPendingDepth`, `linter.*`) are forbidden in code (comments are fine) — ``withOptions (fun o => o.set `maxRecDepth 100000)`` inside an elaborator is still `set_option maxRecDepth 100000`
 - Lake configuration does not pass forbidden option overrides, trace options, linter disables, or heartbeat / recursion-depth overrides
 - the style-linter allowlist `scripts/nolints-style.txt` has no active entries
 - no Lean content file exceeds 10000 non-blank, non-comment code lines
 - no theorem/lemma proof body exceeds 200 non-blank, non-comment code lines, using the current text heuristic
-- `LeanPool/projects.yml` exists, is valid YAML, and contains a `projects` list
+- `LeanPool/projects/` contains one valid YAML mapping per project, with its filename matching the unique slug; duplicate fields, nested cards, and mixed old/new registries fail validation
 - project entries have required fields: `slug`, `title`, `entry_module`, `authors`, `source`, `status`, `provenance`, `main_declarations`, and `tags`
 - project entries also carry documentation metadata: `summary`, `branch`, `main_results`, and `msc`
 - project `status` is `verified`
@@ -52,30 +52,29 @@ Current checks:
 - project summaries and branches are nonempty strings, MSC codes are a nonempty string list, and `main_results` is a nonempty list of `declaration` / `informal` entries
 - project `main_results[*].declaration` values include every `main_declarations` entry, so compact project cards and richer documentation metadata cannot drift
 - project `slug` and `entry_module` values are unique
-- every registered project `entry_module` is imported directly by `LeanPool.lean`
+- every registered project `entry_module` is imported by its project’s public `Imports.lean`
 - every project has a top-level entry file `LeanPool/<Project>.lean`, including projects with nested registered entry modules
 - every nested registered entry module is reachable through its top-level entry file's imports
 - every top-level project module `LeanPool/Foo.lean`, except `LeanPool/Basic.lean`, belongs to the namespace of a registered `entry_module`
 - project entry modules and listed main declarations resolve in Lean
-- generated entry-point project cards match `LeanPool/projects.yml`
+- generated entry-point project cards match `LeanPool/projects/*.yaml`
 - public declarations depend only on the allowed axiom set: `Classical.choice`, `propext`, and `Quot.sound`
 - a Lean environment audit (run via `lake env lean --run` with extensions disabled, so project notation cannot interfere) walks **every** declaration compiled into a pool module — including elaborator auxiliaries and generated declarations the textual scans cannot see — and rejects any that references option-manipulating constants, embeds a gated option-name literal (however the `Name` was assembled), directly references an axiom-injecting constant (`sorryAx`, `ofReduceBool`, ...), or is itself an axiom declared inside a pool module (which is how `native_decide` and `addDecl`-of-an-axiom backdoors surface)
 
-The checker also has `--write-project-cards` to regenerate entry-point module docstrings from `LeanPool/projects.yml`.
+The checker also has `--write-project-cards` to regenerate entry-point module docstrings from `LeanPool/projects/*.yaml`.
 
 ### 3. PR Separation
 
 [`content-pr-guard.yml`](workflows/content-pr-guard.yml) enforces PR scope separation.
 
 Content files are:
 
-- `LeanPool.lean`
 - `LeanPool/**/*.lean`
-- `LeanPool/projects.yml`
+- `LeanPool/projects/*.yaml`
 
 A PR may touch only content files or only non-content files. Mixing these categories fails CI, except that a Lean/Mathlib version bump may pair content with the toolchain, manifest, lakefile, their `docbuild/` equivalents, and this workflow.
 
-Branch protection to require these checks before merge is future work.
+Branch protection requires the build, separation and documentation gates; the merge queue validates their combined result on current main.
 
 ### 4. Python CI
 
@@ -148,7 +147,7 @@ The following items are documented goals but are not fully implemented or enforc
 - branch protection requiring the CI gates before merge
 - scheduled Lean/Mathlib update checks
 - LeanExplore semantic dedup comments in PRs; the prototype CLI is [`python/lean_pool/semantic_dedup.py`](../python/lean_pool/semantic_dedup.py)
-- controlled tag vocabulary for `LeanPool/projects.yml`; tags are currently only checked as nonempty strings
+- controlled tag vocabulary for `LeanPool/projects/*.yaml`; tags are currently only checked as nonempty strings
 - generated domain/status indexes
 - directory index-file policy: every directory under `LeanPool/` containing Lean files should have an import-only index file with a module docstring
 - AST-aware proof-size measurement; the current 200-line proof cap uses a text heuristic

.github/merge-queue-ruleset.json

@@ -0,0 +1,84 @@
+{
+  "name": "Validated merge queue",
+  "target": "branch",
+  "enforcement": "disabled",
+  "bypass_actors": [],
+  "conditions": {
+    "ref_name": {
+      "include": [
+        "refs/heads/main"
+      ],
+      "exclude": []
+    }
+  },
+  "rules": [
+    {
+      "type": "deletion"
+    },
+    {
+      "type": "non_fast_forward"
+    },
+    {
+      "type": "pull_request",
+      "parameters": {
+        "dismiss_stale_reviews_on_push": false,
+        "require_code_owner_review": false,
+        "require_last_push_approval": false,
+        "required_approving_review_count": 0,
+        "required_review_thread_resolution": true
+      }
+    },
+    {
+      "type": "required_status_checks",
+      "parameters": {
+        "strict_required_status_checks_policy": false,
+        "required_status_checks": [
+          {
+            "context": "Build project",
+            "integration_id": 15368
+          },
+          {
+            "context": "Content / non-content separation",
+            "integration_id": 15368
+          },
+          {
+            "context": "Documentation preflight",
+            "integration_id": 15368
+          },
+          {
+            "context": "Lint (ruff)",
+            "integration_id": 15368
+          },
+          {
+            "context": "Test (pytest)",
+            "integration_id": 15368
+          },
+          {
+            "context": "actionlint",
+            "integration_id": 15368
+          },
+          {
+            "context": "SHA-pinned Actions",
+            "integration_id": 15368
+          },
+          {
+            "context": "Verify minimal Lean files",
+            "integration_id": 15368
+          }
+        ]
+      }
+    },
+    {
+      "type": "merge_queue",
+      "parameters": {
+        "check_response_timeout_minutes": 240,
+        "grouping_strategy": "ALLGREEN",
+        "max_entries_to_build": 3,
+        "max_entries_to_merge": 10,
+        "merge_method": "SQUASH",
+        "min_entries_to_merge": 1,
+        "min_entries_to_merge_wait_minutes": 0
+      }
+    }
+  ]
+}

.github/workflows/auto-rebase.yml

@@ -46,6 +46,7 @@ permissions:
 
 jobs:
   list:
+    if: vars.USE_MERGE_QUEUE != 'true'
     runs-on: ubuntu-latest
     name: List open PRs
     outputs:

.github/workflows/content-pr-guard.yml

@@ -4,6 +4,8 @@ name: PR Separation Guard
 # Lean/Mathlib version bumps may also include their Lake/toolchain metadata.
 
 on:
+  merge_group:
+    types: [checks_requested]
   pull_request:
     types: [opened, synchronize, reopened]
   workflow_dispatch:
@@ -22,15 +24,30 @@ concurrency:
   # the input PR number; otherwise group by the live PR number as before.
   group: >-
     content-pr-guard-${{ github.event.pull_request.number ||
-      inputs.pr_number }}
+      inputs.pr_number || github.ref }}
   cancel-in-progress: true
 
 jobs:
   guard:
     runs-on: ubuntu-latest
     name: Content / non-content separation
     steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
+        with:
+          fetch-depth: 0
+          persist-credentials: false
+
+      - name: Check every PR in the combined queue commit
+        if: github.event_name == 'merge_group'
+        env:
+          BASE_SHA: ${{ github.event.merge_group.base_sha }}
+          HEAD_SHA: ${{ github.event.merge_group.head_sha }}
+        run: >-
+          PYTHONPATH=python python3 -m lean_pool.queue_guard
+          --base "$BASE_SHA" --head "$HEAD_SHA"
+
       - name: Reject mixed content and non-content changes
+        if: github.event_name != 'merge_group'
         env:
           GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
           REPO: ${{ github.repository }}
@@ -42,7 +59,13 @@ jobs:
           printf '%s\n' "$files" | sed 's/^/  /'
           echo
 
-          content_re='^(LeanPool\.lean|LeanPool/.+\.lean|LeanPool/projects\.yml)$'
+          base=$(gh api "repos/$REPO/pulls/$PR_NUMBER" --jq '.base.sha')
+          content_re='^(LeanPool\.lean|LeanPool/.+\.lean|LeanPool/projects\.yml|LeanPool/projects/[A-Za-z0-9_-]+\.yaml)$'
+          if ! git cat-file -e "$base:LeanPool/projects.yml" 2>/dev/null \
+            && printf '%s\n' "$files" | grep -qx 'LeanPool.lean'; then
+            echo '::error::LeanPool.lean is fixed; PRs must not edit the shared root.'
+            exit 1
+          fi
           content="$(printf '%s\n' "$files" | { grep -E "$content_re" || true; })"
           non_content="$(printf '%s\n' "$files" | { grep -vE "$content_re" || true; })"
 
@@ -63,9 +86,8 @@ jobs:
 
             echo "::error::This PR mixes content and non-content changes."
             echo "Content files may be changed only in content-only PRs:"
-            echo "  - LeanPool.lean"
             echo "  - LeanPool/**/*.lean"
-            echo "  - LeanPool/projects.yml"
+            echo "  - LeanPool/projects/*.yaml"
             echo "(Exception: a version bump may also touch lean-toolchain,"
             echo " lake-manifest.json, and lakefile.toml.)"
             echo

.github/workflows/docs.yml

@@ -1,11 +1,14 @@
 name: Documentation
 
 on:
+  merge_group:
+    types: [checks_requested]
   push:
     branches:
       - main
     paths:
       - '**/*.lean'
+      - 'LeanPool/projects/**'
       - 'LeanPool/projects.yml'
       - 'lakefile.toml'
       - 'lake-manifest.json'
@@ -22,28 +25,6 @@ on:
   pull_request:
     branches:
       - main
-    paths:
-      - 'README.md'
-      # Attribution-only and CI-only PRs must still produce the required
-      # `Documentation preflight` check.
-      - 'NOTICE.extra.yml'
-      - '.github/workflows/lean_action_ci.yml'
-      - 'scripts/ci/**'
-      - '**/*.lean'
-      - 'LeanPool/projects.yml'
-      - 'lakefile.toml'
-      - 'lake-manifest.json'
-      - 'lean-toolchain'
-      - 'docbuild/**'
-      - 'python/lean_pool/exposition/**'
-      - 'python/lean_pool/quality.py'
-      - 'python/lean_pool/validation_cache.py'
-      - 'python/lean_pool/ci_artifacts.py'
-      - 'python/lean_pool/ci_cache.py'
-      - 'python/lean_pool/rebase_fastpath.py'
-      - 'scripts/exposition/**'
-      - '.github/workflows/notice.yml'
-      - '.github/workflows/docs.yml'
   workflow_dispatch:
     inputs:
       preview:
@@ -81,6 +62,11 @@ jobs:
         with:
           fetch-depth: 0
 
+      - name: Install Python tooling runtime
+        uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff
+        with:
+          enable-cache: true
+
       - name: Identify compiled Lean sources
         id: build-identity
         run: |
@@ -91,9 +77,9 @@ jobs:
       - name: Detect README-only change
         id: scope
         env:
-          BASE_SHA: ${{ github.event.pull_request.base.sha }}
+          BASE_SHA: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }}
           EVENT_NAME: ${{ github.event_name }}
-          HEAD_SHA: ${{ github.event.pull_request.head.sha }}
+          HEAD_SHA: ${{ github.event.merge_group.head_sha || github.event.pull_request.head.sha }}
         run: |
           set -euo pipefail
           readme_only=false
@@ -113,10 +99,10 @@ jobs:
           GH_TOKEN: ${{ github.token }}
           REPOSITORY: ${{ github.repository }}
           PR_NUMBER: ${{ github.event.pull_request.number }}
-          HEAD_SHA: ${{ github.event.pull_request.head.sha }}
-          BASE_SHA: ${{ github.event.pull_request.base.sha }}
+          HEAD_SHA: ${{ github.event.merge_group.head_sha || github.event.pull_request.head.sha }}
+          BASE_SHA: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }}
         run: |
-          decision=$(PYTHONPATH=python python3 -m lean_pool.rebase_fastpath decide \
+          decision=$(PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath decide \
             --workflow docs.yml --repository "$REPOSITORY" --number "$PR_NUMBER" \
             --head "$HEAD_SHA" --base "$BASE_SHA")
           echo "rebase_only=$(echo "$decision" | python3 -c 'import json,sys; print(str(json.load(sys.stdin)["eligible"]).lower())')" >> "$GITHUB_OUTPUT"
@@ -188,7 +174,7 @@ jobs:
 
       - name: Check regenerated LeanPool root without Lean
         if: steps.rebase.outputs.rebase_only == 'true'
-        run: PYTHONPATH=python python3 -m lean_pool.rebase_fastpath check-index
+        run: PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath check-index
 
   # Runs in parallel with the doc-gen4 build; its (small) artifact is merged
   # into the Pages tree by the `deploy` job. Restores the root build cache but