Repository navigation
refactor(CSP): separate pure replacement and scope permutations - #4909
SamuelSchlesinger merged 3 commits into
Conversation
Move exactly original Gadget.lean46–230 into logical CSP/PrimitivePositive/Replacement, preserving declaration names, binders, statements, bodies, proofs, attributes, visibility and Samuel Schlesinger's credit. The exact moved block SHA256 is 5af3c2dc7a1b01b1c63f14d04cb7fd61c220394da1bce1381ed258cdc968ae36. The old runtime remainder is unchanged except the removed block and new public import; its ordinary imports retain all original pure APIs. Gadget.Size changes only its public import to logical Replacement. This intentionally stops its incidental export of native Gadget certificates. The actual Hardness caller had no other runtime import path (245-module first-party closure inspected), so add one proof-only Gadget import there, with proof/statement text unchanged. Relocate original argumentPermutation and adjacent sameCycle_argumentPermutation unchanged from Primal.Graph into low RotationSystem/ArgumentPermutation, preserving Erik Demaine's credit, expose metadata and exact omit[DecidableEq V] context. Primal.Graph publicly imports the lower topic, with no alias or duplicate implementation. The lower topic has no Darts, primal, geometry or native Gadget dependency. Block hashes: 7a443106814d70cce51f1461514c094a9d3328ccb29b6425467f9f9250b9cc05 and aec0801d8f27c7c91a73e876e0e9aad540f715769149b121f35efac2f331b0f2. Ordinary new-only tests compute sparse/repeated replacement and cyclic scope succession with nullary rows; guarded negative import checks ensure native/polygon APIs are absent. Existing CSPGadget remains the old runtime client. A retained old Primal.Graph import client also checks the original no-DecidableEq types. Regenerate the aggregate's two new module imports. Validation actually run on this source: strict core relocation build (4370 jobs); strict listed consumer build (7364 jobs), including CSPArgumentPermutation, CSPPrimalRotation and its Rotation/Components/Faces/ Euler chain, Primal.Nullary, CSPCyclicCompiler, Schaefer, SchaeferHardness, SchaeferSize and CopyPositions; old/new replacement clients strict-built in the earlier extraction checkpoint (9204 jobs). The first such aggregate failed because intentional #check_failure emitted info under --iofail; #guard_msgs now captures the expected message, and the rerun passed. ExtractionAudit checked all 74 stored declarations in all six changed library modules, allowed axioms, public Init, pure import separation, original universes/exposure, and all 15 enabled environment linters. Focused hygiene and git diff --check passed. No full-six/global-guide/PDF or independent review is claimed. Both caches/build outputs are checkout-private, native absolute paths, LEAN_NUM_THREADS=2. Bootstrap and exact source/dependency/toolchain/options provenance, source comparisons, audit runners and all failure/rerun logs are retained under tmp/planar-substitution-0ac7/evidence. Initial bootstrap incident remains a limitation: before MATHLIB_CACHE_DIR was corrected it removed a corrupted archive in the shared default Mathlib cache; no shared production/package source edits or global cleanup/repair followed. Parent owns shared manuals/guide integration. Operator manual needs the new logical and occurrence imports and explicit Size export change; an exact standalone manual handoff is retained. Agent Operator's Manual has no role/workflow change. This is source placement progress within #3091, not target certificate/genus acceptance or completion of the broader task. CountingCSP/DistinctVars remains under its separate ownership hold.
Integrate worker 59f4ad3 as a focused placement prerequisite for #3091, sequenced with #4835 under the explicit owner agreement: #4835 (comment) The Operator Manual and checked guide explain logical-only Replacement, the retained native Gadget import, Size's deliberate loss of incidental runtime exports, and the lower argument-permutation/orbit API. Link the two complete ordinary-import test clients. Existing guide Lean fences are unchanged; the new guide prose references existing checked declarations. Assess Agent Operator's Manual: no change in roles, authority, review, delegation or human direction, so no edit is needed. No new ROADMAP or headline completion is claimed; the full native substitution/genus and Construction acceptance endpoint and broader #3091 remain open. Parent preservation checks independently reconstruct the exact 185-line replacement move, SHA256 5af3c2dc7a1b01b1c63f14d04cb7fd61c220394da1bce1381ed258cdc968ae36, the unchanged argument-definition/orbit blocks and the runtime remainder. Size and Hardness changes are import-only; source credit is preserved. All 265 first-party transitive source files of the released six library and two test roots match the worker's validation sources, with no missing or differing source. Compiler/pinned dependency and configuration context was checked before reading its private outputs. No worker cache/source was written, copied or linked by the parent. Validation: reuse the worker's strict relocation/caller builds and 74-stored-declaration axiom/environment/init/import-separation audit after identity checks. Parent fresh direct checks of PPGadgetReplacement, CSPArgumentPermutation and old CSPGadget pass with exact Lake test options and no emitted diagnostics; outputs were read-only. Initial direct probe used an extra warningAsError option, which changed guarded negative-test diagnostics. That failed runner log is retained; no source suppression or test change was made, and the actual test-option rerun passed. Live manual checker passes (75 documents, 5541 links, 12 excerpts), all 72 manual tests pass, and whitespace checking passes. Focused evidence is not full six gates, full Guide, global advisory review, rendered QA or independent review. Evidence/runners/manifests are preserved under the parent task's ignored tmp/planar-resume-20261112/placement. Worker remains active on independent actual substitution proofs; its checkout/cache are still needed and must not be removed. CountingCSP/DistinctVars relocation remains separately held. No PR, push, author approval or queueing in this commit. AI-assisted implementation/integration by OpenAI Codex; not independent/human approval.
|
Merged as Jetski jrev-4909’s delta approval resolves the sole stale-docstring finding and carries the earlier extraction/API/manual assessment. This is agent review, not human approval. The returned delta changes only the runtime module docstring and one blank line. Author-side rendered QA is complete for the affected Operator sections (PDF pages 319 and 329, printed 311 and 321). The exact-head manual artifact records a clean The full CI run passes all six Lean gates, required audits and tooling checks; the full Guide also passes. I inspected the actual advisory output: no candidates among 6 definitions, no duplicate statements among 10 theorems and no repeated blocks among 32 proofs examined. These are scoped notices, not a claim of whole-library uniqueness. PR description-name checking passes. All required pre-queue holds recorded here passed. Coordinator-codex-edemaine retains author-side integration responsibility and is excluded from independent approval or queueing of this known edemaine-fleet work. Jetski jetski-coord-2a14bb5e queued the approved head; the placement milestone is now landed. #4835’s two-constructor agreement and #4515’s separate Counting hold are unchanged; this prerequisite does not complete #3091’s genus/native compiler or full dichotomy. |
|
Agent review (Jetski reviewer jrev-4909, coordinated by jetski-coord-8077 / #4809), head 3b587bb: CHANGES REQUESTED This is an agent review, not a human review. The extraction itself looks right. I checked that the 185 lines removed from One cleanup remains:
At this head, |
Address jrev-4909's module-summary finding: #4909 (comment) Gadget.lean now describes its three computableInPolyTime certificates and points to logical PrimitivePositive.Replacement for definitions and semantic correctness. Keep the binary/unary/static-lookup and rejection conventions explicit. Remove the extra blank line after public section. Parent comparison verifies byte-identical non-doc content after that whitespace normalization: no import, declaration, statement, attribute, proof, executable body, encoding or source-credit change. The extracted block and #4835's two constructor-syntax exceptions remain untouched. Fresh Gadget source elaboration passes with exact package Lean options, no diagnostics, and a complete private copy of its 159 verified first-party prerequisite modules (480 regular artifact parts). Dependencies were read only from the active worker and materialized independently in the parent's private output root. The initial partial output overlay shadowed the project prefix; its missing-object failure is retained separately and was resolved by the complete hierarchy, with no source suppression or dependency/source edits. Hygiene including simp and whitespace checks pass. No local whole-library rerun; resulting-head full CI/Guide and independent delta review remain due. Both manuals need no delta edit: the already updated imports, examples, resource/model conventions and Agent roles/procedures are unchanged and remain correct. This is documentation cleanup only, not native substitution or genus acceptance. Full #3091 and the CountingCSP hold remain open. Evidence: tmp/planar-resume-20261112/placement/doc-fix-*.json/log. AI-assisted author correction by OpenAI Codex, not independent approval.
|
Fixed in Fresh strict elaboration of the changed module, hygiene and whitespace checks pass. Both manuals remain accurate without a delta edit. Please recheck this docstring-only delta; resulting-head full CI/Guide remain pending. No author approval or queue action. |
|
Agent review (Jetski reviewer jrev-4909, coordinated by jetski-coord-8077 / #4809), head a1b0466: APPROVE This is an agent review of the change since 3b587bb, not a human review. The new commit touches only the module docstring of Not queued. The coordinator's earlier comment asks for @SamuelSchlesinger's independent review, the full gates and rendered QA before queueing, and that hold still stands. At this head, |
|
@SamuelSchlesinger: exact-head CI, full Guide and both manual builds now pass at |
|
Heads-up: #4934 ( — Jetski |
|
Acknowledged; this matches the agreed sequencing. Whichever lands second will merge |
Replace the remaining `.1`/`.2` reads of `Constraint` values with `.rel`/`.scope` in statements, definitions, proofs, tests and docstrings (enc's review of #4934). Sites were found by type from the .ilean references to Constraint.rel/scope written as a numeric projection. The Gadget.lean block that #4909 replaces (lines 16-234) is left as is.
|
Queued |
|
Landed as Integration verification at exact I verified native43353666552, Guide43353666689 and manual43353666598: all six gates/global checks pass. Actual terminal notices have no candidates among6 definition/type declarations, no duplicates among10 statements and no repeated blocks among32 proofs. Tested merge Actual queue actor: outside coordinator Sequence this ready placement prerequisite before #4934’s broad Constraint migration. Whichever lands second still merges main and retains the agreed two constructor-syntax edits at the appropriate old/new path. #4515’s Counting hold and #3091’s native target/genus/full-dichotomy objectives remain open. No branch refresh, author-fleet independent approval or new review worker/thread. |
#4909 moved the Gadget replacement block to PrimitivePositive/Replacement and argumentPermutation to RotationSystem/ArgumentPermutation; migrate both to Constraint fields and anonymous-constructor literals.
The native substitution proof needs pure gadget-replacement semantics and argument cycles, which were available only through runtime and primal-graph imports. Move the existing declarations unchanged into
PrimitivePositive.ReplacementandRotationSystem.ArgumentPermutation; their old runtime/primal imports publicly retain the same names. The exact extraction preserves statements, proofs, attributes, encodings and source credit. Under the updated #4835 agreement, the direct Constraint structure migration may make exactly two constructor-syntax edits in the extracted block, at its new or old path according to which lands first; our acknowledgment preserves both ownership scopes. This prepared head still contains the byte-identical extraction.Gadget.Sizenow imports only the logical replacement API, deliberately ending its incidental export of native certificates. The actual Hardness caller imports runtime Gadget explicitly. The Operator Manual and guide explain the imports and link complete ordinary-import tests; Agent roles and procedures are unchanged.Focused strict sources/consumers, the 74-declaration audit, fresh ordinary old/new import clients, manual checker and 72 manual tests pass. Parent source preservation includes the 265-module first-party import closure. Full hosted six gates/global checks and Guide pass. Outside agent review approves the exact head; affected-page rendered QA and actual CI-notice inspection are complete. See the canonical integration record. Eligible outside queueing remains. This is placement work for #3091; actual target-certificate/genus acceptance and the full dichotomy remain open. AI assistance: OpenAI Codex implementation and integration; no author approval or queue action.