Repository navigation
Forward merge: release/v0.4 (#305, #365, #256) and main into release/v0.5 - #367
Merged
Merged
Conversation
…tion-coverage line (#34) README: the text-component rows no longer say first, second and third slice; production-coverage is 36 roots across five modules and its coverage of the registry is shared with production, models and reasoning (OR-02's probes cover the rest), as the gate states it. SPEC 4.2: the non-goals list bounds language 1.0 only. SPEC 17.14: points at certificates B and E for the declared Rust machine; rustc agreement stays build evidence. No register row or identity moves. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0135zd5jvsTLg2b9XM19j2Q5
Each public language-class refusal that had only an inline plant now has a committed project under tests/negative, refused with exactly its code and registered in EX-07's prescribed table (285 -> 289): production-package-name-keyword (a Rust keyword as a crate name), gnaf-request-malformed, gnaf-certificate-malformed (a valid committed GNAF request with a truncated certificate), text-window-zero-capacity. The inline plants stay. expected/ written by check-fixtures --write; no existing fixture changed. Targets' digests in the request fixtures bind to the current identity and are re-pinned when #248 lands. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0135zd5jvsTLg2b9XM19j2Q5
…mes its program (#251) collections, higher-order, language-1.2, production, production-coverage, recursion and recursive-data carried the literal example's title on every module. Each now has a path glossary <pkg>.titles (the fold-laws pattern) with one label-word entry per module, the lexicon_source row, and re-pinned lock. fmt --check and check pass for all seven. Source only: the expected/ trees and verified records are regenerated in the next commit (check-golden --write, verify-examples --write), so check-golden is red on this commit by design. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0135zd5jvsTLg2b9XM19j2Q5
…n retitles (#34) Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0135zd5jvsTLg2b9XM19j2Q5
…titled examples (#251)
…_mut, RefCell, Cell) under RB-20
…machineArity (the chain does not parse)
…ntax, the validator rules, the printer, the twin; assemble and the crate header built from the nodes
…inner-attribute nodes; BS-09 at 654 crates and 40 rules; RB-10 and scaffold plants; VERIFICATION and CHANGELOG Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018vK7Tm6xHF5etAwKM6r9HG
… the three nodes and five rules of RB-19 (40 in all), the stale rule-count comment, and the first red lines of one RB-21 and one RB-10 plant Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018vK7Tm6xHF5etAwKM6r9HG
…568 refused, 45 rules)
… the axioms they observe (freeFnOk, memberOk, attributeStep none... see policy), BS-09 at 709/568/45; module member name is checked as an identifier Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018vK7Tm6xHF5etAwKM6r9HG
main receives the v0.4.0 line: release/v0.4 at 93fbe7d, the tag commit Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013QppGKetUURseXowZun9KY
main receives the v0.4.0 line at its tag (e0b74b8). Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013QppGKetUURseXowZun9KY
…ance on the moved identity The renderer record moves with package.rs, runtime.rs, and scaffold.rs, and the compiler-semantics ID with the probe; the fixed point is reached, every project relocks, the production exports and the fixtures are rewritten from this tree. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013QppGKetUURseXowZun9KY
The README is reorganized for a reader arriving cold: a centered header with the logo, the one-line value proposition, the document links and the state badges, then Quickstart (container, binary, source, the §29 literal), How LexLean works (pipeline plus the command table with what each command may claim), Why LexLean, When to use LexLean, the capability register table, the examples, the gate, the evidence rules, the documented deviations, the layout and the license. The gate-relevant content is unchanged: the capability table keeps its exact header, its three cells, its `build` level cell and its 35 rows, so every one of the 457 registered IDs is still claimed exactly once by the row that owns it, and the register-size and honesty-level sentences are still stated. No dash is used as punctuation anywhere in the prose, and no list uses a hyphen marker; hyphens remain only where they are part of an identifier, a path, a command or a table separator, because those are machine-checked tokens. assets/lexlean-logo.svg is new: a QED tombstone with a check mark beside a monospace wordmark, in the repository's own purple, legible on light and dark renderings. SPEC.md §7 lists it, so the added file has the defined role §7 requires.
docs: restyle the README and add the repository logo
…e Atlas, on the moved identity Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013QppGKetUURseXowZun9KY
… thirteen shard artifacts of the first gate run Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013QppGKetUURseXowZun9KY
docs: use the enclosed LexLean logo image and tighten the README
…f a defined path are identifiers (#308) rt_validate.rs applies ident to each lint of a forbid and to each segment of a defined path split at "::"; the RuntimeValidate twin does the same through identErr (colonStep, colonPieces). Eight site plants under RB-19; BS-09 is 717 crates, 576 refused. VERIFICATION.md and the Lean audit follow. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…tstrap export The twin's source moved, so the committed bootstrap packages are rewritten by check-production-export --write; the rust-std provenance of every package follows the bootstrap source, and validate_runtime carries the new checks. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
fadbf3c reflowed the fields of Scaffold, so the plant `, {name: library, type: String}` no longer matched and conformance_rb_10 failed at its uniqueness check. The plant now matches the reflowed text. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…ap-h7-audit #91 H7-audit: the crate header, module wrapper, and definitions as RuntimeSyntax nodes; RB-21 and RB-10 tightened; the shared-write plants
… only Stacked pull requests cannot land on a line, and the pull request that carries the stack into main or release/* runs the whole gate on the tree that lands, so the whole gate on each push to a stacked one was waste. ci-plan.sh reads BASE; RP-14 plants the decisions. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013Asa3QZQru5a9Beo3r4Rfa
Conflicts: CHANGELOG.md (this PR's bullets move to an Unreleased section above 0.4.0), EX-07's prescribed table (298 line classes plus this PR's four = 302), and the seven retitled examples' lexlean.lock and expected/ (regenerated with lexlean lock and cargo xtask check-golden --write; expected/verify needs Lean and is not regenerated here). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013Asa3QZQru5a9Beo3r4Rfa
…igest after the merge The three production-request fixtures pinned the rust-core descriptor digest of the pre-merge line; the line's H6/H7 landings moved it. Each fixture is again refused with exactly its prescribed code (LLB6005, LLB6006, LLB6007, LLT4016) and its committed command.json is unchanged. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013Asa3QZQru5a9Beo3r4Rfa
cargo xtask verify-examples --write with Lean 4.32.1, restricted to collections, higher-order, language-1.2, production, production-coverage, recursion and recursive-data. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013Asa3QZQru5a9Beo3r4Rfa
…es (#251) The exported packages' source digests follow the module titles; cargo xtask check-production-export --write, nothing else changes. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013Asa3QZQru5a9Beo3r4Rfa
RP-14: a ready pull request into a feature branch runs the rest leg only
…nts-off runs verify-examples --write (without uor-atlas, as CI's examples leg runs it) moves the content-addressed LexLeanAudit oracle with the changed RuntimeValidate twin. VERIFICATION quotes the two plants-off runs. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
… the example's titles glossary (#251) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013Asa3QZQru5a9Beo3r4Rfa
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013Asa3QZQru5a9Beo3r4Rfa
check-golden --write moves the RuntimeValidate coverage, map, module and eligibility oracles, and the build manifest, with the changed twin. The plain check-golden passes after it. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…-attr-idents #308 RB-19, BS-09: the lint names of an inner attribute and the segments of a defined path are identifiers
…ve fixtures) into release/v0.5 The generated SPEC.md, CONFORMANCE.md and model/ids.toml take release/v0.5's side; the v0.4 prose and the six register statements it changed (RP-14, RB-10, RB-19, RB-20, RB-21, BS-09) are ported into spec/src. The expected records, locks and packages are regenerated in the next commit. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013Asa3QZQru5a9Beo3r4Rfa
The README takes main's condensed layout and keeps release/v0.5's capability table (RP-11), with the register count 475 and the model-write note in Layout; the SPEC.md layout tree change (assets/) is ported into spec/src/Chapter07. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013Asa3QZQru5a9Beo3r4Rfa
…erification records on the merged identity The renderer record moves to 9bdcbf56b and the language-1.2 compiler-semantics ID to 49a667a8078dc6a386940bc73ea1197f5dabf4236c4e57a1aaf70bccddfd556a (1.1 and 1.0 unchanged). Every project relocks; the goldens, the compiler project's generated files, the fixtures, the production exports, and the normalized verification records of every project but the Atlas (verified by CI) are rewritten from this tree. The four new negative request fixtures are re-pinned to the rust-core descriptor digest of this identity, and the prescribed-code table of EX-07 counts 307 fixtures. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013Asa3QZQru5a9Beo3r4Rfa
…fixed point of the merged identity The first regeneration wrote the compiler project's rust packages against the previous project identity; the second reaches the fixed point (check-calculus equals its generator). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013Asa3QZQru5a9Beo3r4Rfa
afflom
marked this pull request as ready for review
October 31, 2026 20:58
…en shard artifacts of the first gate run Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013Asa3QZQru5a9Beo3r4Rfa
…B of the aarch64 host Each peaks at 5 to 10 GiB; run concurrently by the test harness they used about 22 GiB, and the runner was killed twice in conformance_bs_05. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013Asa3QZQru5a9Beo3r4Rfa
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Requested by Alex · project thread
Merges
release/v0.4(ccbf038: #305 H7 audit, #365 ci-plan base rule, #256 four negative fixtures and the retitled examples) andmain(README #329-#331) intorelease/v0.5, by merge commit.spec/src, and main's SPEC layout change into Chapter07, then regenerated.rust_rendererand the language-1.2 compiler-semantics ID (49a667a8...) move; all locks, goldens, compiler-project packages (at the fixed point, after a second pass), fixtures, production exports and verification records are regenerated. The four new request fixtures are re-pinned to the rust-core descriptor digest. EX-07 counts 307 fixtures.expected/verifyrecords are not regenerated (hours); CI verifies them.Local: fmt, clippy
-D warnings, validate-model, validate-spec-links, check-golden/fixtures/calculus/production-export/reproducibility, bdd, and SP-07, EX-07, SM-23, PX-01, RP-05/07/11/14/18, RB-10/19/20/21, BS-09, NS-01..07 pass.Generated by Claude Code