Enable queue validation and independent project metadata

[Vilin97]

Repeated edits to the shared project registry and root import list cause conflicts and force otherwise independent PRs to restart CI. Strict branch updates and direct metadata pushes add more churn. This prepares the transferred organization repository for GitHub's native merge queue and a separate project card per project.

The queue tests the combined proposed result against current main while retaining every build, warning, lint, style, quality, documentation and applicable minimal-file gate. Each constituent PR keeps its content-separation check. Verified PR build outputs and only that PR's own validation results can warm the group; source, inventory, pinned settings and normal Lake dependency checks still decide reuse. Missing evidence falls back to normal checks. Generated statistics and attribution move through a protected PR whose head stays fixed during validation. PRs that touch the exposition verification pipeline publish their exact-tree build for the minimal-file gate, avoiding a second cold whole-pool compilation; normal PRs omit the large archive. A separate prerequisite waits for the exact-head producer without consuming the verifier job’s six-hour execution window. The consumer checks the tree and pinned settings, then still runs Lake, extraction and the real minimal-file verifier. Failed or cancelled preparation fails the required gate; missing artifacts retain the ordinary build fallback.

Lake discovers all LeanPool sources directly. The registry reader supports both historical LeanPool/projects.yml and independent LeanPool/projects/<slug>.yaml mappings, rejecting mixed layouts and malformed cards. Linters, attribution, exposition, review, importers and historical comparisons use that reader. The subsequent content-only migration removes the shared registry and makes LeanPool.lean fixed; this infrastructure PR changes no pooled Lean sources or project metadata.

Public repository and Pages links point to LeanPool/lean-pool. The original repository was transferred with its PR numbers and history preserved. Azure review/daily-worker configuration and Greptile access have been repaired separately. The queue ruleset is staged disabled until the workflow hooks are on main; existing protection remains active. Deployment details are in python/merge-queue.md.

Validation: 679 Python tests passed, 2 skipped; Ruff checks and formatting, Actionlint for all workflows, shell syntax checks, generated-index consistency and the whole pool's static quality checks passed. Real pinned-Lean tests prove restored unchanged proofs are not rebuilt, changed imported definitions force invalid dependent proofs to rebuild and fail, and directory discovery rejects an unlisted broken source. Queue tests cover separate PR policies, owned validation results, exact successful queue heads, historical reads, card corruption and submitted attribution snapshots. Remote review reads all 289 cards in one complete GraphQL directory request (verified against the actual migration branch), rejecting truncated or binary blobs. Importers also support the staged legacy layout until the content migration merges. NOTICE header wording describes the registry without depending on its storage layout.

Hosted CI and real queue throughput measurements are still pending. No queue speedup is claimed from the local tests or previous PR benchmarks.

The two reviewed attribution blockers are repaired: required Lean/documentation checks now report on every PR, including NOTICE-only and other infrastructure changes; ordinary PRs validate any authored NOTICE against the exact submitted head before regenerating the combined test view. Main and queue groups also verify edited snapshots. Regression cases reject incorrect authored attribution while accepting both inherited stale files and valid older snapshots.

Three further review findings are repaired: main pushes validate snapshots independently of queue commit titles and use GitHub’s merged-PR association only for legitimate older metadata snapshots; classifier failures explicitly fail the required Python and minimal-file checks; an explicitly selected custom project-card directory retains the aggregator’s merged-project markers. Regression tests failed before the repairs and passed afterward, including valid and invalid attribution under preserved PR history.

Scheduled/manual verification no longer waits for a nonexistent scheduled producer. Explicit custom registry files and missing custom paths retain their selected meaning, with regression coverage.

Maintainer authorized merging PR610 and PR611 without waiting for exposition verification. All other checks and branch protections remain in force; the exposition workflow remains enabled and its result is not claimed as passing.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[High risk] Adds merge queue validation and restructures project metadata storage.

The PR appears safe to merge; the weekly wait is fixed and no new blocking issue was found.

Summary

This PR prepares merge-queue checks, independent project cards, verified build reuse, and protected metadata updates. It also updates repository links after the transfer.

• Since the previous review, scheduled and manual verification no longer wait for a matching producer.
• Explicit alternate registry files and directories retain their own project selection.
• No new actionable issues were found. The numbered finding from the previous review is fixed.

_{Reviews (6) · Last reviewed commit: "Fix scheduled verification preparation a..." · Reviewed by Greptile}

[Vilin97]

Independent source review at 9925386: two P2 findings in the scope-job failure handling and explicit project-card directory reader. I reviewed the central queue reuse, registry/discovery and related workflow contracts. The four reader/ruleset source blobs are unchanged from the independently reviewed 83bc213 version. The two updated workflows were read in full and preserve the reported scope handling. This is a bounded static review; I have not run the test/build results stated in the PR body or a real merge_group. The checked-in queue ruleset is disabled, so the required-check finding describes its behavior when enabled. No gate edits, activation or merge were performed.

Follow-up at b230555: both reported P2 issues are addressed in the source. The required Python and exposition jobs now run on classifier failure and fail before validation; a successful irrelevant-change classification still skips them. The directory reader now accepts the explicitly selected directory. I checked the updated workflow bodies and reader change. This is a targeted static follow-up; overall CI and merge-group validation remain outside this result.

[Vilin97]

Independent source follow-up at fa62886. The earlier classifier-failure and explicit-directory findings are resolved. There is one distinct P2 in selection of an explicit historical registry file; see the inline comment. The scheduled build wait already reported by Greptile is also confirmed, without duplicating that comment. Scope: current identities for all 65 changed files, whole source review of 22 critical files and five test files. Tests/workflows were not executed by this review; this is not whole-PR approval. The rollout owner retains all branch edits, validation and protected integration. No branch, gate, queue activation or merge change.

Follow-up at 0e0cb33: the explicit historical-registry P2 is addressed. Only the canonical projects.yml request falls back to sibling project cards; an explicit alternate file is read directly and a missing alternate file raises FileNotFoundError. Explicit custom directories also ignore an unrelated legacy file. I read the whole current registry.py and test_registry.py and the complete registry diff from fa62886. The two regression tests cover alternate/missing file selection and custom-directory selection. I did not execute the tests or recertify the rest of the changed PR. Rollout validation and protected integration remain with the rollout owner; the competing-merge hold remains in force.