Repository navigation
Add Jedit-owned Edict flat-text replacement reference - #302
Conversation
flyingrobots
added
the
work-in-progress
|
Important Review skippedToo many files! This PR contains 160 files, which is 60 over the limit of 100. To get a review, reduce the PR to 100 files or fewer by splitting it into smaller PRs or changing its base branch. Upgrade to a paid plan to raise the limit. This review couldn't start because sufficient usage credits or metered capacity aren't available. Add credits or update usage-based reviews in the billing tab, then retry. ⚙️ Run configuration
⛔ Files ignored due to path filters: 8
📒 Files selected for processing: 160
You can disable this status message by setting the
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
|
@codex review please, focus on the three unmet plan items and whether they are reachable at these exact heads. Requesting the fresh independent exact-head operational audit that is item 11 of this PR's plan. Please state the exact commits you audited rather than accepting the ones quoted below. Heads as I read them right now
The pins in the PR body are behind both upstreams, so part of what I need is whether the closure still reproduces byte-identically at current heads or only at the pinned ones. Findings I want checked, not trusted. These are my reads from source this session and I would rather you contradict them than confirm them politely:
What would help most
Not asking you to implement anything. James has asked me to finish this PR and I want an independent read on what finishing actually requires before I touch three repos. |
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. |
|
Codex Review: Didn't find any major issues. Breezy! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
|
Resumed this work in a separate worktree at The source-compiler prerequisite now has an implementation and review PR: flyingrobots/edict#211 (closes flyingrobots/edict#210). Docker validation passed the focused RED/GREEN, the syntax suite, strict Clippy, and A public-build witness using an isolated copy of this PR's source adds Next: establish generic target expression authorization and independent totality validation for the new Core subtraction before advancing executable artifact pins. No rope semantics will be added to Echo, and this observation does not mark the full ReplaceRange algorithm, Tick/WAL/recovery, or production cutover complete. |
|
Progress at
This does not yet establish runtime execution of the new package, the full rope algorithm, or production cutover. Broader malformed-Core/scope coverage, full gates, and runtime evidence remain. Existing Jim source and producer locks are unchanged. No PR is marked ready from these initial witnesses. |
|
Subtraction prerequisite update:
The isolated authored source adds Echo's pinned Rust 1.90 gate also passes the nine new subtraction tests, seven unchanged pure-evaluation tests, two meter tests, and strict focused Clippy. U64 coverage uses the real compiler artifact; deliberate matching-pin mutations exercise U32 bounds, wrong arity/types, and underflow without claiming verifier approval for those mutations. The checked-in #302 source, compiler/provider/evaluator pins, and proof locks remain unchanged at This is prerequisite progress, not completion: authored persistent-rope semantics, generic stateful execution, oracle agreement, and admitted Tick/WAL/receipt/reading/recovery evidence remain required by #296. Review and hosted CI are pending for the new PRs; nothing was merged. |
Preserve the original parser/lexer refusals and failed witness, then reproduce those distinct boundaries with a controlled Rust 1.96 build. Retain raw artifacts, resource-stop qualifications, and source/compiler/provider identities. The decoder remains unexecuted; Edict #226 and Echo #752 own the function prerequisites for Jim #296.
Move the toolchain lock from the Edict 3f81f759 and Echo #724/#726 candidate pins to Edict main e60411fc and Echo main 9b3b9396, and the Rust toolchain to 1.96.0 as Edict main requires. Regenerate the build lock through the harness's --write-locks path. The executable-subject lock is byte-identical, so the verified package did not change. The full proof harness passes 12/12 under Node 22.23.1 and npm 10.9.8 in a container, against isolated clones of both pinned commits. Refs #296, #302
Add DL-0159, a draft representation for the rope that Jim's Edict source reads and writes: every structural relation is a typed Echo edge, facts use canonical CBOR, immutable nodes are content-addressed over their facts and children, each head links to its basis so every version stays inside Echo's state root, and an import head is anchored to its file coordinate and host digest. Add complete drafts of ReplaceRange in Edict source against that representation: a deliberately inefficient flat-text semantic reference and the persistent AVL rope (pure split, join, balance, build, and collect, plus the effectful intent). They do not compile on Edict main; the README classifies every blocker as language, primitive, runtime, resource, or defect, separates confirmed refusals from code reading, and states the evidence plan. Nothing here enters the application gate. Refs #296, #302, #350
Route C: supersession proposal and implementation planDirection (approved by @flyingrobots, pending design review): Jim's rope law is authored in Jim-owned Edict source using generic, independently justified primitives. No native Supersession (proposal, not merged): flyingrobots/echo#889
Done on this branch
Plan (stages; nothing major starts until the designs are reviewed)
#350 (reopen) and save/export must land before any durable or end-to-end editor claim. UI PRs stay untouched. Decisions still open
|
Remove the head-to-predecessor basis edge from DL-0159 and the drafts. It made every version of every buffer permanently reachable, so the state root and retention grew with editing history, and it duplicated the causal history Echo's ticks and receipts already own. The graph now holds the current Buffer, Head, Import, and rope; superseded nodes leave the reachable graph, and their retention and any reconstruction of past states are Echo's retention and replay contract. Every new head copies the anchor edge instead of reaching its Import through a chain, and head identity no longer includes the predecessor. Undo and redo are forward operations. Replace 'UTF-16 length is dropped' with an explicit coordinate contract: byte offsets are authoritative, and whether UTF-16 offsets are derived, cached, or retained is an open decision driven by the interoperability surfaces Jim commits to, not by today's consumers. Refs #296, #302
|
Correction to the plan above (
Route C is unchanged. |
Copying the import anchor to every head preserves where the text came from; it must not imply the rope still matches the file. DL-0159 now keeps three facts apart: import provenance (Import, anchor edge), the current logical content (digest computed over the rope at a crossing, not on every edit), and host synchronization (an Export node with the logical and resulting host digests, reached by a lastExport edge that each save retargets). Save requires the file's host digest to equal the last exported digest, or the import digest if never exported; a mismatch is a typed conflict that needs explicit reconciliation. Reopen compares host digests against the last export, so it never materializes the rope. Refs #296, #302, #350
Add invariant 4: no committed coordinate contains an edge to an absent node, so a retargeted head is never observable before everything it reaches. Validation rejects dangling endpoints with DanglingReference, because GraphStore::upsert_edge_record does not check them, and commit makes partial visibility impossible by binding all effects to one Tick published only after its decided WAL record. State that reads are witnessed through a recording view over a bounded slice rather than declared, and that today's edict_read only counts reads, so this is new instrumentation. State the composition rule for shared structure: an Ensure of an identical existing node is a read, and two Actions creating the same new node conflict under the existing set test, with no new merge rule; a retry sees the node and reads it. Add three concrete execution traces for Jim's reference ReplaceRange: committed, obstructed by a stale basis at evaluation, and rejected at composition. Extend the required tests accordingly. Refs flyingrobots/jedit#302
DL-0159 drops the Export -> Head edge: an Export is evidence of one crossing (file, logical digest, resulting host digest, and the causal event that witnessed it), not a reason to keep a historical rope reachable, and never file authority. A pinned saved snapshot would be an explicit retention lease. Save is now spelled out as a foreign crossing: export intent, host write, read-back observation as witnessed ingress, export outcome, and recovery by re-observation under the same occurrence key. The design no longer claims a digest check prevents a concurrent writer; without a host-side concurrency protocol the guarantee is detection at observation. Add third-party file changes: a buffer's synchronization basis, detection only through witnessed observation, an external change admitted as a new Import, adoption for a clean buffer, and for a dirty buffer an explicit, witnessed keep-mine, take-theirs, merge, or defer. Merge needs the base bytes; when retention no longer has them it refuses with MergeBaseUnavailable. Refs #296, #302, #350
Replace the third-party change notes with an explicit reconciliation contract between Base (last agreed host contents), Local (the current rope), and Host (the latest validated observation), with a decision table. Watchers are hints; decisions use a validated, stable re-read. ObserveExternalFileChange is separate from adoption. Divergence preserves both sides: Reload keeps Local recoverable, Keep local does not grant an overwrite, Overwrite is its own explicit choice against a specific Host, and Reconcile is a forward edit that never invents the external editor's history. Offering Reconcile requires B's bytes, not just its digest. Classify modification, atomic-save rename, deletion, replacement, symlinks, permission changes, and unstable reads; support ordinary files first and refuse ambiguous crossings. Save revalidates and claims detection, not prevention, until a host concurrency protocol exists. Refs #296, #302, #350
Record observed absence as a dependency (missing node or atom, empty or specific outgoing-edge set) against the basis, so a co-scheduled Action that creates the slot invalidates the reader. Align dependency kinds with the Action validity across ticks decision (#837): value and single-key absence are supported; reading edges by type is a topology dependency that keeps the whole-frontier rule until sound edge-set tracking exists there. Make retry identity explicit: a decided outcome, receipt, and attribution never change; a retry is a new submission with its own identity; Echo does not retry on its own; and a never-decided Action recovered after a crash is the same submission, not a retry. Update the composition trace and the required tests accordingly. Refs flyingrobots/jedit#302
An external write is testimony from another authority, not an editor event. DL-0159 now routes it through Echo's existing contracts instead of a filesystem-specific model: a filesystem adapter turns a validated observation into an import proposal under the Continuum Transport import law, and the observation is held, judged, and applied as Participant History as a Braid describes. Jim's Edict-authored law judges B, L, and H into Derived, Plural, Conflict, or Obstruction; divergence is a Conflict that bars dependent operations until settled; only a witnessed forward commit changes the buffer. Each observation carries Echo's Continuum occurrence identity and an explicit receiving context. Re-delivery is idempotent; distinct observations stay distinct; and a digest identifies observed content, not the write that produced it, so the adapter never invents distinct external writes. Filesystem-specific work stays at the adapter boundary. Refs #296, #302, #350
Cite Paper VII directly, checked against the paper: transport precedes judgment, so an observed file version is re-expressed at Jim's receiving frontier, with B as the comparable basis the adapter can actually support (section 4.3); a braid is a comparison carrier, not a merge, and observing, braiding, judging, and admitting are separate acts (Definition 2.4, Remark 2.6), with plurality a lawful outcome (section 4.2); and the optic Psi = (Omega, chi, rho, Pi, Lambda) is Jim's (Definition 3.1). Commitment, folding, and revelation stay separate (section 3.3), the section 6.2 hot-text optic matches the draft's closure read and single head retarget, and section 8 names app-authored optic compilation and export semantics as open seams, which is what this document attempts. The paper is cited as foundation, not as evidence of implementation. Refs #296, #302
…contracts Add an identity chain: submission (Submission Attribution and canonical inbox sequencing), Action (ADR 0023/0025), proposal (new, evidence only, deterministic per Action and basis), and decision (recorded once by submission_id). The bridge removes no admission check, adds no identity root, and persists nothing outside the decided-Tick WAL record. Retries now rest on Echo's existing intake idempotence: identical content returns the existing submission as Duplicate with its original outcome; a real new attempt must differ, which makes it a new submission. The new receipt-entry fields change an encoding that commit hash v3 binds, so they need a new entry format version under Submission Attribution's format rules. Recovery replays decided Ticks and checks the patch digest and commit hash without re-evaluating; scoped-validity Actions follow #837's recomputation; undecided Actions re-evaluate as the same submission. Extend the required tests accordingly. Refs flyingrobots/jedit#302
flyingrobots
changed the title
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 6155218f98
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
|
|
||
| - `edict.lawpack.json` is the reviewable `jedit.text@1` authoring input; | ||
| - `vendor/jedit-text/` is Edict's canonical published lawpack closure; | ||
| - `src/ReplaceRange.edict` is the application-owned source; |
There was a problem hiding this comment.
This change introduces authored ReplaceRange.edict, its published lawpack closure, and an executable package chain, but docs/jim-component-ownership.md:700–706 still explicitly states that the source and complete application-owned lawpack closure do not exist in Jedit. That document is the registered canonical owner of the Jim/Jedit/Edict/Echo ownership model, so the new README and bearing entries leave authoritative current-versus-target guidance contradictory. Update the canonical owner in this change, distinguishing the now-working pure reference from the still-unimplemented stateful rope and installed release. The root AGENTS.md explicitly requires same-change canonical-owner updates for these decisions.
AGENTS.md reference: AGENTS.md:L79-L87
Useful? React with 👍 / 👎.
| COPY edict/replace-range /application-source | ||
| COPY edict/replace-range-probes/basis-identity/ReplaceRange.edict /comparison-sources/ReplaceRange.edict | ||
| COPY edict/replace-range-probes/basis-identity/PayloadEquality.edict /comparison-sources/PayloadEquality.edict |
There was a problem hiding this comment.
Following this probe's documented Docker recipe copies the current application closure, whose vendor/jedit-text/manifest.sha256 is sha256:f385072314ea57af5b66cad9eb4119b51e456df2050ea0c9a6302c7693212dc1, while both comparison sources import sha256:95758c1605894672cc9069fde01bb8b6e11842b053102660c9cd4f4d6f34d64e. build.sh copies that closure and replaces only the source, so the probe cannot build its advertised comparison packages: the imported release does not match the supplied manifest. Preserve a matching historical closure for this pinned witness, or migrate the compiler, provider, closure, and imports together.
Useful? React with 👍 / 👎.
1 participant
Add Jedit-owned Edict source that computes flat-text replacement as prefix + replacement + suffix, with ordered range, UTF-8, offset-boundary and no-op refusals. The public compiler build, independent verification, vendor closure, artifact locks and runtime consume one exact pinned basis: Edict 2b4832efe62de75e1f204cec72f9fe7d00ef9551 and Echo b314f7fd071985edad1f9876df383a85fb491205.
The executable package identity is sha256:4c2b7859f291e97b6b38fb265086e6cb0581ed030d54d38152b0585152120397. Clean macOS and Linux builds emit byte-identical package and verifier-report files. Runtime tests cover nine literal replacements, thirteen semantic refusals and five host-resource refusals. The invalid-original-UTF-8 witness failed against the previous package before passing with the corrected source. The clean pinned Docker package chain, both locked runtime targets and all twelve proof-harness regressions pass.
The branch also retains explicitly classified capability probes and noncompiling persistent-rope drafts outside the application gate, plus the proposed application representation. These are design and evidence artifacts, not executable authority. Canonical ownership, bearing and application documentation describe the boundaries.
This lands the completed flat-text reference and public build foundation. It does not close #296. The full campaign still requires the generic authored effect bridge, persistent AVL implementation, domain-typed outcomes, structural sharing, corpus agreement, atomic admission, Tick/WAL/receipt/readings and fresh-engine recovery. The schema and independent oracle remain separate from executable input. Existing editor integration and production rope behavior are unchanged.
Related: #296, flyingrobots/echo#889, flyingrobots/echo#917.