Repository navigation
Conversation
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
GTrunSec
force-pushed
the
codex/final-event-offset-aot
branch
from
October 2, 2026 16:31
85f62fe to
9d148da
Compare
Use Gerbil final record contracts for private LR, recognition, event and machine metadata while retaining checked accesses and existing protocols. Add complete-artifact matched request workloads and native Scheme admission of repeated CPU benefit, tails, SDK control and independent image identity. Bind the separate CPU-improvement requirement into locked uv/native Ascent review, with mutation controls and official compiler/research documentation. Keep CI, runtime budgets, allocation admission and public DSL unchanged.
Preserve source-bound Lean, Quint and real AOT controls, rejected scan trials and explicit open throughput gate. No full performance matrix or SMP acceptance is claimed.
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.
Scope
poo-flow-core@e85fd45303b208b23e5957fd316e7004994109a4revision.foldl, and skip unused state-stack prefixes during LR reductions.lalr-then-followconstruction: keep LALR for conflict-free grammars, use follow-partition LR(1) only after unresolved LALR cells, preserve genuine conflict rejection and the selective-GLR route. The default remains LALR.Complete pinned TLA+ corpus closure
c6ecb40dbc6816510b6ad68d3dc68429b89c9531, including main's strict final-token offset validation.tlaplus/Examples@ceeaa904140e3e03781cb2a79cd6c6d8b8b08e10; the Scheme runner verifies the clean checkout and exactly 424 tracked TLA+ files.tla2tools.jarSHA-256936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88).Local verification at 9d148da (implementation) / 567daf9 (test ownership)
MODULE-OK,HARNESS-OK, finalOK, with the five-second watchdog active.git diff --checkpassed.fbaf317) so source-only fixture imports are admitted before gxtest initializes.3654201), keeping the 1 GB heap fence, five-second silence rejection and existing performance thresholds. This prevents all source expansion contexts from accumulating in one heap.ca86a02) to expose actual progress inside exhaustive LR recognition equivalence sweeps; the five-second silence gate remains unchanged.7c15333) so cold macOS imports expose real library progress before gxtest imports a source module. Focused ANTLR, LR equivalence and GQL/Rust generation tests passed with the five-second watchdog.7c1533356585154c8b5d340f64ffefb289d18907: Rust/Rowan, Ubuntu native Gerbil and macOS native Gerbil all SUCCESS. Run 37039132506.c6ecb40dbc6816510b6ad68d3dc68429b89c9531is an ancestor.Evidence boundary
The 424-file syntax receipt closes this immutable corpus. The 72-tree projection is a bounded structural gate, not complete SANY semantic equivalence, full proof hierarchy equivalence, every precedence interval or PlusCal translation. TLC qualification remains a separate gate. Orgize PR #18 remains a downstream consumer and should pin an exact reviewed parser head.
Scheme engine and common language library boundary
language-support/entry; engine entry owns only descriptor dispatch and generic policy execution.language-support/development, with direct caller migration.parser.ssindependent of corpus;parser-test.ssowns the corpus and development entry over the exact production descriptor.grammar.ss, preserving lexical order and removing name-based GQL assumptions from the common adapter.docs/research/scheme-engine-library-boundary.org, including Scheme examples and falsifiable limits.Evidence
Complete language interface alignment
Revision
71efb9fmigrates all eight shipped packages and ten public entries to:grammar.ss: language declarations, lexical/policy data and pinned source metadata.parser.ss: productionLanguageLoader.only; no corpus/build/scanner/test services.parser-test.ss: corpus, optionalLanguageDevelopmentLoader.and independent conformance tests.All 53 accepted/rejected corpus members have production/development dispatch controls for exact descriptor identity, status, complete events and roundtrip. Existing language-specific tests are retained; source workers, HCL generated-backend profiles and build strategies now belong to the development interface. Test and benchmark consumers import the relocated data explicitly.
The extended topology guard rejects development imports and declarations in production interfaces. A new separate all-ten-entry benchmark reports raw samples and nearest-rank P50/P95 with workload identity; the historical four-language measured gate is preserved. English design documentation records ownership and executable scientific questions.
Verification boundaries: Scheme readers confirmed unchanged grammar declarations and relocated corpus bytes; source-overlay boundary controls passed all 53 dispatch comparisons. Affected Rust all-target/all-feature Clippy passed. Interrupted/cold local native attempts and nonzero child exits remain failures, even after success markers. Exact-head Linux/macOS native execution is being qualified by this revision's CI; no complete native or latency improvement claim is inferred from local build output.
All-language qualification follow-up
Previous alignment head:
bbbe76a058786f125d6c382a69d9138476c7f064.0a78ea9and712c65fremain retained evidence. The first combined build stopped during GQL Scheme-to-C translation; after separate translation, both platforms stopped when their largest C frontend jobs began together.bbbe76a: Linux/macOS native jobs failed; Rust passed. These failures are retained. Local receipts did not establish remote qualification.Checked source author frontend — 2026-10-07
Preceding frontend implementation head:
2a55f99feeb81a822b4c4aefb1d4723d6e806d83.syntaxblock and onerulesblock directly indeflanguage, with nativedefgrammar-syntaxvocabulary. No additional required SourceGrammar model was added.deflanguage-sourceauthor declaration and raw profile/strategy exports from the public source facade. Migrated parser receipt and internal test callers directly; no compatibility alias or runnable legacy grammar remains.Remaining boundaries: source plans remain distinct from CFG/LR GrammarIR; macro blame currently covers the rule block; dispatch inference is scoped to the closed shell adapter. General ambiguity analysis, precise expansion provenance, complete module relocation, clean build/downstream installation and performance gains are not claimed. Exact-head GitHub CI for this new commit is pending and is separate from local qualification.
Parser metadata values and optional native POO — 2026-10-07
parser.ss;grammar.ssexports unbound syntax products. Upstream source pins remain grammar inputs..oor prototype declaration. Native inheritance/override is optional. Engine admission binds effective identity once, snapshots identity strings and derives digest fields while retaining either representation.Local qualification and limits
2a55f99, Rust/Rowan CI passed; both native CI jobs exceeded the 240-second conformance compilation fence. The new head's clean CI remains a separate gate. No timeout was widened.Command entry contract migration (1500e75)
Single source compilation and native descriptor ownership (1d2e677)