Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
19 kB · 760 lines
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761# doc_commit: the models of how the documents tools put files on disk# (crates/eukhe-docs/src/write.rs, hashline/mod.rs, documents.rs).## Edit: an edit of many files first locks every path and checks every# file (phase 1): when one file changed since it was staged, the edit# writes nothing. Then it publishes the files in order and stops at the# first publish that fails (phase 2). A publish lands; or lands with a# warning (the rename is done but the directory sync fails, or a move put# its destination in place but could not remove its source); or fails# (nothing of that file lands). The reply calls a file applied only when# it landed.## Write: the write tool replaces a file only when the bytes on disk are a# version the session saw (it read them, grep showed them, or it wrote# them); a missing file is created. The session keeps the last 8 versions# it saw.## Move: an MV never replaces a file: when its destination exists it is# refused and nothing changes.## Sweep: a replace of a file removes the temporary files of that file# that no live writer holds; it keeps every other entry.## The writer's choices (the last section) run as the compiled core# (bend/ffi_doc_commit.bend, called from crates/eukhe-docs write.rs,# hashline/mod.rs, store.rs): Rust locks, reads, compares bytes, hashes,# publishes and removes; each choice is a function of what it met, and# the laws tie each to the models above.
import Base
# Edit# ----
type Op is Data: Update{} # the file gets new content Moving{} # the file moves to a free name
type Fault is Data: Clean{} # no fault Sync{} # the rename is done; the directory sync fails Publish{} # the publish fails: nothing of the file lands Remove{} # a move: the destination lands; the source removal fails
# one file of an edit: changed says that its bytes changed since the edit# staged ittype Doc is Data: Doc{op: Op, changed: Bool, fault: Fault}
# what one publish didtype Out is Data: Landed{warn: Bool} Failed{}
def publish.go(x: Fault, k: Op) -> Out: match x: case Clean{}: Landed{False{}} case Sync{}: Landed{True{}} case Publish{}: Failed{} case Remove{}: match k: case Update{}: Landed{False{}} case Moving{}: Landed{True{}}
def publish(f: Doc) -> Out: match f: case Doc{k, c, x}: publish.go(x, k)
def Fault.fails(x: Fault) -> Bool: match x: case Clean{}: False{} case Sync{}: False{} case Publish{}: True{} case Remove{}: False{}
# phase 1: whether a file changed since the edit staged itdef conflict(fs: List<&2, Doc>) -> Bool: match fs: case Nil{}: False{} case f <> rest: match f: case Doc{k, c, x}: Bool.or(c, conflict(rest))
# whether a publish failsdef failing(fs: List<&2, Doc>) -> Bool: match fs: case Nil{}: False{} case f <> rest: match f: case Doc{k, c, x}: Bool.or(Fault.fails(x), failing(rest))
def landed.put(+n: Nat, rest: List<&2, Nat>, o: Out) -> List<&2, Nat>: match o: case Landed{w}: n <> rest case Failed{}: Nil{}
# the disk: the files (by index, from n) whose new content lands, in orderdef landed.go(fs: List<&2, Doc>, +n: Nat) -> List<&2, Nat>: match fs: case Nil{}: Nil{} case f <> rest: landed.put(n, landed.go(rest, 1n+n), publish(f))
def landed.pick(c: Bool, fs: List<&2, Doc>) -> List<&2, Nat>: match c: case True{}: Nil{} case False{}: landed.go(fs, 0n)
# the files whose new content is on disk after the editdef landed(+fs: List<&2, Doc>) -> List<&2, Nat>: landed.pick(conflict(fs), fs)
def run.put(o: Out, rest: List<&2, Out>) -> List<&2, Out>: match o: case Landed{w}: Landed{w} <> rest case Failed{}: [Failed{}]
# phase 2: the publishes, in order, up to the first that failsdef run(fs: List<&2, Doc>) -> List<&2, Out>: match fs: case Nil{}: Nil{} case f <> rest: run.put(publish(f), run(rest))
# what the reply says of one filetype Report is Data: Applied{warn: Bool} NotWritten{}
def report.put(o: Out, rest: List<&2, Report>) -> List<&2, Report>: match o: case Landed{w}: Applied{w} <> rest case Failed{}: NotWritten{} <> rest
# one report a file, from the publishes: a file with no publish was not# writtendef report(fs: List<&2, Doc>, os: List<&2, Out>) -> List<&2, Report>: match fs: case Nil{}: Nil{} case f <> rest: match os: case Nil{}: NotWritten{} <> report(rest, Nil{}) case o <> more: report.put(o, report(rest, more))
type Reply is Data: Rejected{} # an error: nothing was written Answered{files: List<&2, Report>} # applied, or applied in part
def reply.go(os: List<&2, Out>, fs: List<&2, Doc>) -> Reply: match os: case Nil{}: Answered{report(fs, Nil{})} case o <> more: match o: case Landed{w}: Answered{report(fs, Landed{w} <> more)} case Failed{}: Rejected{}
def reply.pick(c: Bool, +fs: List<&2, Doc>) -> Reply: match c: case True{}: Rejected{} case False{}: reply.go(run(fs), fs)
# the reply of the editdef reply(+fs: List<&2, Doc>) -> Reply: reply.pick(conflict(fs), fs)
def applied(rs: List<&2, Report>, +n: Nat) -> List<&2, Nat>: match rs: case Nil{}: Nil{} case r <> rest: match r: case Applied{w}: n <> applied(rest, 1n+n) case NotWritten{}: applied(rest, 1n+n)
# the files (by index) the reply reports applieddef reported(r: Reply) -> List<&2, Nat>: match r: case Rejected{}: Nil{} case Answered{rs}: applied(rs, 0n)
# the indices of the files, from ndef ids(fs: List<&2, Doc>, +n: Nat) -> List<&2, Nat>: match fs: case Nil{}: Nil{} case f <> rest: n <> ids(rest, 1n+n)
# Write# -----
def mem(+v: Nat, xs: List<&2, Nat>) -> Bool: match xs: case Nil{}: False{} case x <> rest: Bool.or(Nat.is_eq(x, v), mem(v, rest))
def drop.put(+x: Nat, rest: List<&2, Nat>, b: Bool) -> List<&2, Nat>: match b: case True{}: rest case False{}: x <> rest
def drop(+v: Nat, xs: List<&2, Nat>) -> List<&2, Nat>: match xs: case Nil{}: Nil{} case +x <> rest: drop.put(x, drop(v, rest), Nat.is_eq(x, v))
# the versions seen after the session sees v: newest first, once each,# the last 8def saw(+v: Nat, s: List<&2, Nat>) -> List<&2, Nat>: List.take(&2, Nat, v <> drop(v, s), 8n)
# whether the disk holds a version the session did not seedef unseen(d: Maybe<&2, Nat>, +s: List<&2, Nat>) -> Bool: match d: case None{}: False{} case Some{v}: Bool.not(mem(v, s))
# what a write did: whether it wrote, the disk and the seen versions aftertype Wt is Data: Wt{ok: Bool, disk: Maybe<&2, Nat>, seen: List<&2, Nat>}
def write.go(b: Bool, d: Maybe<&2, Nat>, +s: List<&2, Nat>, +c: Nat) -> Wt: match b: case True{}: Wt{False{}, d, s} case False{}: Wt{True{}, Some{c}, saw(c, s)}
# the session writes c over the disk d, having seen the versions sdef write(+d: Maybe<&2, Nat>, +s: List<&2, Nat>, +c: Nat) -> Wt: write.go(unseen(d, s), d, s, c)
# Move# ----
# a file: its name and its contenttype Entry is Data: Entry{name: Nat, body: Nat}
def has(+n: Nat, es: List<&2, Entry>) -> Bool: match es: case Nil{}: False{} case e <> rest: match e: case Entry{m, g}: Bool.or(Nat.is_eq(m, n), has(n, rest))
def get.put(b: Bool, g: Nat, rest: Maybe<&2, Nat>) -> Maybe<&2, Nat>: match b: case True{}: Some{g} case False{}: rest
# the content of the file named ndef get(+n: Nat, es: List<&2, Entry>) -> Maybe<&2, Nat>: match es: case Nil{}: None{} case e <> rest: match e: case Entry{m, g}: get.put(Nat.is_eq(m, n), g, get(n, rest))
def rename.put(+t: Nat, +m: Nat, g: Nat, rest: List<&2, Entry>, b: Bool) -> List<&2, Entry>: match b: case True{}: Entry{t, g} <> rest case False{}: Entry{m, g} <> rest
# the files after the file s takes the name tdef rename(+s: Nat, +t: Nat, es: List<&2, Entry>) -> List<&2, Entry>: match es: case Nil{}: Nil{} case e <> rest: match e: case Entry{+m, g}: rename.put(t, m, g, rename(s, t, rest), Nat.is_eq(m, s))
# what a move did: whether it moved, and the files after ittype Mv is Data: Mv{ok: Bool, es: List<&2, Entry>}
def Mv.ok(m: Mv) -> Bool: match m: case Mv{ok, es}: ok
def Mv.es(m: Mv) -> List<&2, Entry>: match m: case Mv{ok, es}: es
def move.go(+s: Nat, +t: Nat, taken: Bool, es: List<&2, Entry>) -> Mv: match taken: case True{}: Mv{False{}, es} case False{}: Mv{True{}, rename(s, t, es)}
# MV s t over the files esdef move(+s: Nat, +t: Nat, +es: List<&2, Entry>) -> Mv: move.go(s, t, has(t, es), es)
# Sweep# -----
type Sort is Data: Own{} # a temporary file of the target Foreign{} # a temporary file of another target Plain{} # another file
def Sort.own(k: Sort) -> Bool: match k: case Own{}: True{} case Foreign{}: False{} case Plain{}: False{}
# an entry of the target's directory; held: a live writer holds its locktype Temp is Data: Temp{id: Nat, sort: Sort, held: Bool}
# whether the sweep removes the entrydef removes(n: Temp) -> Bool: match n: case Temp{i, k, h}: Bool.and(Sort.own(k), Bool.not(h))
def sweep.put(+n: Temp, rest: List<&2, Temp>, b: Bool) -> List<&2, Temp>: match b: case True{}: n <> rest case False{}: rest
# the entries the sweep removes, in orderdef sweep(ns: List<&2, Temp>) -> List<&2, Temp>: match ns: case Nil{}: Nil{} case +n <> rest: sweep.put(n, sweep(rest), removes(n))
# The writer's choices# --------------------# What the real writer decides from what it met. Content digests are# texts Rust computes (the hash stays Rust); two digests name the same# bytes exactly when they are the same text.
# a and b are the same text, char by chardef same(a: String, b: String) -> Bool: match a b: case SNil{} SNil{}: True{} case SNil{} SCon{y, v}: False{} case SCon{x, u} SNil{}: False{} case SCon{x, u} SCon{y, v}: Bool.and(Char.is_eq(x, y), same(u, v))
# Phase 1: the check of an edit# -----------------------------
# what the check of one file met: its bytes changed since the edit staged# it; a move whose destination existstype Met is Data: Met{changed: Bool, taken: Bool}
type Why is Data: Changed{} # the file changed on disk Taken{} # the move's destination exists
type Check is Data: Go{} # publish every file Stop{at: Nat, why: Why} # write nothing: file `at` is why
def check.met(changed: Bool, taken: Bool, +n: Nat, rest: Check) -> Check: match changed: case True{}: Stop{n, Changed{}} case False{}: match taken: case True{}: Stop{n, Taken{}} case False{}: rest
# the check of the files from index n: the first file that changed or# whose destination exists stops the editdef check.go(ms: List<&2, Met>, +n: Nat) -> Check: match ms: case Nil{}: Go{} case m <> rest: match m: case Met{c, t}: check.met(c, t, n, check.go(rest, 1n+n))
def check(ms: List<&2, Met>) -> Check: check.go(ms, 0n)
# Phase 2: one publish# --------------------
# where a publish put the new bytestype Placed is Data: NotPlaced{} # the write or the rename failed Placed{synced: Bool} # the target holds them; the directory sync
# what one publish mettype Pub is Data: Updated{placed: Placed} # a file got new content Deleted{removed: Bool} # a file was removed (or not) Moved{placed: Placed, removed: Bool} # the destination placed; the source removed
# the warning a landed publish carriestype Warn is Data: NoWarn{} SyncWarn{} # the directory sync failed RemoveWarn{} # a move could not remove its source
type Outcome is Data: Lands{warn: Warn} # the change is on disk: go on Fails{} # nothing of it landed: stop here
def placed.out(p: Placed) -> Outcome: match p: case NotPlaced{}: Fails{} case Placed{s}: match s: case True{}: Lands{NoWarn{}} case False{}: Lands{SyncWarn{}}
def moved.out(p: Placed, removed: Bool) -> Outcome: match p: case NotPlaced{}: Fails{} case Placed{s}: match removed: case False{}: Lands{RemoveWarn{}} case True{}: placed.out(Placed{s})
def removed.out(r: Bool) -> Outcome: match r: case True{}: Lands{NoWarn{}} case False{}: Fails{}
# what one publish diddef outcome(p: Pub) -> Outcome: match p: case Updated{x}: placed.out(x) case Deleted{r}: removed.out(r) case Moved{x, r}: moved.out(x, r)
# The reply of an edit# --------------------
# what became of one staged filetype Fate is Data: Noop{} # nothing to write Wrote{out: Outcome} # its publish Untried{} # a publish before it failed
type Note is Data: Untouched{} # a no-op Written{} # it landed Unwritten{} # its publish failed (its own reason) Skipped{at: Nat} # not tried: file `at` failed first
type Verdict is Data: Failure{} # nothing landed: the first failure is the error Summary{files: List<&2, Note>, partial: Bool} # partial: some file was not written
def lands(o: Outcome) -> Bool: match o: case Lands{w}: True{} case Fails{}: False{}
def fails(o: Outcome) -> Bool: Bool.not(lands(o))
def any.landed(fs: List<&2, Fate>) -> Bool: match fs: case Nil{}: False{} case f <> rest: match f: case Noop{}: any.landed(rest) case Wrote{o}: Bool.or(lands(o), any.landed(rest)) case Untried{}: any.landed(rest)
def any.failed(fs: List<&2, Fate>) -> Bool: match fs: case Nil{}: False{} case f <> rest: match f: case Noop{}: any.failed(rest) case Wrote{o}: Bool.or(fails(o), any.failed(rest)) case Untried{}: any.failed(rest)
def first.put(o: Outcome, +n: Nat, rest: Nat) -> Nat: match o: case Lands{w}: rest case Fails{}: n
# the index of the first failed publish from index n (past the end: none)def first.failed(fs: List<&2, Fate>, +n: Nat) -> Nat: match fs: case Nil{}: n case f <> rest: match f: case Noop{}: first.failed(rest, 1n+n) case Wrote{o}: first.put(o, n, first.failed(rest, 1n+n)) case Untried{}: first.failed(rest, 1n+n)
def report.of(+k: Nat, f: Fate) -> Note: match f: case Noop{}: Untouched{} case Wrote{o}: match o: case Lands{w}: Written{} case Fails{}: Unwritten{} case Untried{}: Skipped{k}
# one report a file; k: the first failed filedef reports(fs: List<&2, Fate>, +k: Nat) -> List<&2, Note>: match fs: case Nil{}: Nil{} case f <> rest: report.of(k, f) <> reports(rest, k)
def unwritten(fs: List<&2, Fate>) -> Bool: match fs: case Nil{}: False{} case f <> rest: match f: case Noop{}: unwritten(rest) case Wrote{o}: Bool.or(fails(o), unwritten(rest)) case Untried{}: True{}
def answer.go(rejected: Bool, +fs: List<&2, Fate>) -> Verdict: match rejected: case True{}: Failure{} case False{}: Summary{reports(fs, first.failed(fs, 0n)), unwritten(fs)}
# the reply of an edit: an error when a publish failed and none landeddef answer(+fs: List<&2, Fate>) -> Verdict: answer.go(Bool.and(any.failed(fs), Bool.not(any.landed(fs))), fs)
# The write tool# --------------
# what the write is based ontype Base is Data: OnSeen{seen: List<&2, String>} # versions the session saw (their digests) OnBytes{} # exactly the bytes the caller holds
# what the target held when the write locked ittype Disk is Data: Absent{} Present{digest: String, expected: Bool} # its digest; expected: the caller's bytes
type Gate is Data: Proceed{} # write Unseen{} # refuse: the session did not see these bytes Stale{} # refuse: the bytes are not the expected ones (or the file is gone)
def member(+d: String, s: List<&2, String>) -> Bool: match s: case Nil{}: False{} case x <> rest: Bool.or(same(x, d), member(d, rest))
def gate.seen(b: Bool) -> Gate: match b: case True{}: Proceed{} case False{}: Unseen{}
def gate.bytes(b: Bool) -> Gate: match b: case True{}: Proceed{} case False{}: Stale{}
# whether the write tool may replace the targetdef gate(b: Base, d: Disk) -> Gate: match b: case OnSeen{s}: match d: case Absent{}: Proceed{} case Present{g, e}: gate.seen(member(g, s)) case OnBytes{}: match d: case Absent{}: Stale{} case Present{g, e}: gate.bytes(e)
def unsee.put(+x: String, rest: List<&2, String>, b: Bool) -> List<&2, String>: match b: case True{}: rest case False{}: x <> rest
def unsee(+d: String, s: List<&2, String>) -> List<&2, String>: match s: case Nil{}: Nil{} case +x <> rest: unsee.put(x, unsee(d, rest), same(x, d))
# the versions seen after the session sees digest d: newest first, once# each, the last 8 (`saw` of the model, on digests)def seen(+d: String, s: List<&2, String>) -> List<&2, String>: List.take(&2, String, d <> unsee(d, s), 8n)
# The temporary files# -------------------
# the name prefix of every temporary file of the writerdef temp() -> String: ".eukhe-tmp-"
# the name prefix of the temporary files of a target whose file name has# the digest hdef prefix(h: String) -> String: String.append(temp(), String.append(h, "-"))
def starts(p: String, s: String) -> Bool: match p: case SNil{}: True{} case SCon{c, q}: match s: case SNil{}: False{} case SCon{d, t}: Bool.and(Char.is_eq(c, d), starts(q, t))
# an entry of the target's directory: its name (lossy UTF-8), and whether# a live writer holds its locktype Ent is Data: Ent{name: String, held: Bool}
def sweeps(+p: String, e: Ent) -> Bool: match e: case Ent{n, h}: Bool.and(starts(p, n), Bool.not(h))
def gone.put(+n: Nat, rest: List<&2, Nat>, b: Bool) -> List<&2, Nat>: match b: case True{}: n <> rest case False{}: rest
def gone.go(+p: String, es: List<&2, Ent>, +n: Nat) -> List<&2, Nat>: match es: case Nil{}: Nil{} case e <> rest: gone.put(n, gone.go(p, rest, 1n+n), sweeps(p, e))
# the entries (by index) the sweep of the target with digest h removesdef gone(h: String, es: List<&2, Ent>) -> List<&2, Nat>: gone.go(prefix(h), es, 0n)