From 39e19373ce609267f696f9e01c1bb5115b6eccca Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Sun, 27 Sep 2026 06:06:17 +0000 Subject: [PATCH] chore(deps): use noah-emp/bend-sha256 and bump bend Point sha256 at https://github.com/noah-emp/bend-sha256, rev 1319f22. The pin is temporary. Bend's flake input is the commit that names 2.0.31. eztoml, snap, ezhttp and bolt move to the revs that build on that Bend. The binary and each proof start from a file above the tree. Co-authored-by: noah-emp --- .github/workflows/ci.yml | 6 +- AGENTS.md | 2 +- README.md | 4 +- SPEC.md | 14 +-- add/PROOF.bend | 26 ++-- add/hub.bend | 24 ++-- add/plan.bend | 10 +- add/run.bend | 4 +- check/oracle.bend | 2 +- check/world.bend | 2 +- docs/rfc/ez-spec.md | 13 +- doctor/run.bend | 2 +- ez.bend | 7 ++ ez.lock.toml | 110 ++++++++--------- ez.toml | 40 +++---- ez/LAWS.bend | 16 +-- ez/PROOF.bend | 6 +- ez/cache.bend | 2 +- ez/cap.bend | 4 +- ez/clock.bend | 2 +- ez/cmd.bend | 4 +- ez/ends.bend | 2 +- ez/env.bend | 2 +- ez/key.bend | 28 ++--- ez/main.bend | 2 +- ez/pass.bend | 2 +- ez/pass.c | 2 +- ez/pass.js | 2 + ez/prove.bend | 72 +++++++++-- ez/say.bend | 2 +- ez/test.bend | 4 +- fetch/LAWS.bend | 2 +- fetch/PROOF.bend | 16 +-- fetch/plan.bend | 46 +++---- fetch/run.bend | 2 +- flake.lock | 7 +- flake.nix | 4 +- git/git.bend | 2 +- hub/hub.bend | 12 +- ledger/LAWS.bend | 2 +- lock/LAWS.bend | 27 ++--- lock/PROOF.bend | 80 ++++++------- lock/lock.bend | 46 +++---- lock/plan.bend | 12 +- lock/run.bend | 10 +- lock/world.bend | 24 ++-- pkg/LAWS.bend | 42 +++---- pkg/PROOF.bend | 252 +++++++++++++++++++-------------------- pkg/pkg.bend | 76 ++++++------ pub/run.bend | 2 +- run/bend.bend | 2 +- sha/LAWS.bend | 4 +- sha/PROOF.bend | 2 +- sha/nar.bend | 26 ++-- sha/sha.bend | 28 ++--- tests/check.bend | 2 +- tests/cli.bend | 2 +- tests/fetch.bend | 2 +- tests/fresh.bend | 2 +- tests/git.bend | 2 +- tests/hub.bend | 2 +- tests/init.bend | 2 +- tests/nix.bend | 2 +- tests/publish.bend | 2 +- tests/publishing.bend | 2 +- tests/relock.bend | 2 +- toml/toml.bend | 2 +- tool/PROOF.bend | 10 +- tool/plan.bend | 8 +- tool/run.bend | 4 +- 70 files changed, 634 insertions(+), 556 deletions(-) create mode 100644 ez.bend diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 07d855f..15f8007 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -18,8 +18,8 @@ jobs: readme: runs-on: ubuntu-latest env: - BEND_VERSION: 2.0.27 - BEND_SHA256: 58adc86af6605ed0c48f7d84e4c23028f78893ce4a867a20a4f004b11582687b + BEND_VERSION: 2.0.31 + BEND_SHA256: f7dbecc8ef5991fe15d9953b8b33911bc62a120c735e2e5902aa031e22055bad steps: - uses: actions/checkout@fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09 # v5.1.0 - name: Install bend @@ -32,5 +32,5 @@ jobs: echo "$RUNNER_TEMP/bend/bin" >> "$GITHUB_PATH" - run: sh bootstrap.sh - run: mkdir -p bin - - run: BEND_LIB=$PWD/.ez/lib bend ez/main.bend -o bin/ez.bin + - run: BEND_LIB=$PWD/.ez/lib bend ez.bend -o bin/ez.bin - run: bin/ez.bin prove diff --git a/AGENTS.md b/AGENTS.md index db650d1..59d8434 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -11,7 +11,7 @@ ez is a project manager for Bend 2, written in Bend. Each command is a pure plan ```bash sh bootstrap.sh mkdir -p bin -BEND_LIB=$PWD/.ez/lib bend ez/main.bend -o bin/ez.bin +BEND_LIB=$PWD/.ez/lib bend ez.bend -o bin/ez.bin bin/ez.bin prove # the proof gate: every PROOF.bend must pass bin/ez.bin tool run bolt -- --gpu off # lint: 0 errors bin/ez.bin lock # must leave ez.lock.toml unchanged unless you meant to change it diff --git a/README.md b/README.md index 6e6fbad..8e2cca6 100644 --- a/README.md +++ b/README.md @@ -18,10 +18,10 @@ git clone https://github.com/Emerging-Patterns/ez cd ez sh bootstrap.sh mkdir -p bin -BEND_LIB=$PWD/.ez/lib bend ez/main.bend -o bin/ez.bin +BEND_LIB=$PWD/.ez/lib bend ez.bend -o bin/ez.bin ``` -ez runs on Bend 2.0.27, the version CI builds with. Its dependencies are +ez runs on Bend 2.0.31, the version CI builds with. Its dependencies are pinned to git revs, and `ez fetch` is what fetches them, which ez cannot run before it is built. `bootstrap.sh` is that one step, and the one helper script in the repo: it reads `ez.lock.toml`, fetches each package at its pinned rev diff --git a/SPEC.md b/SPEC.md index b319e7e..305c96c 100644 --- a/SPEC.md +++ b/SPEC.md @@ -1,6 +1,6 @@ # ez specification -This is the list of every behavior ez guarantees, each under a stable requirement ID. Every requirement has one of two levels. A **Proved** requirement holds for every input, and is backed by a quantified law in a LAWS.bend that passes the proof gate. A **Trusted** requirement is an assumption about something ez cannot check from inside its own gate, and it is listed in the trust boundary below. A Proved requirement whose law has not landed yet has status **pending**: we intend to prove it, and until then it is not guaranteed. The proof gate is this check: for every PROOF.bend in the tree, the first line `bend PROOF.bend` prints is exactly `All terms check.` `ez prove` runs it, and it is the check CI runs. +This is the list of every behavior ez guarantees, each under a stable requirement ID. Every requirement has one of two levels. A **Proved** requirement holds for every input, and is backed by a quantified law in a LAWS.bend that passes the proof gate. A **Trusted** requirement is an assumption about something ez cannot check from inside its own gate, and it is listed in the trust boundary below. A Proved requirement whose law has not landed yet has status **pending**: we intend to prove it, and until then it is not guaranteed. The proof gate is this check: for every PROOF.bend in the tree, bend is started from a file above the tree that imports it, and the first line bend prints is exactly `All terms check.` Bend 2.0.28 names each file from the program that starts it, so that start is what gives each file one name. `ez prove` runs it, and it is the check CI runs. The reasoning behind each requirement, and the decisions that shaped them, are in [docs/rfc/ez-spec.md](docs/rfc/ez-spec.md). @@ -151,9 +151,9 @@ EZ-DOC-3 reads the committed tree as bend reads it. A hub import line is a root EZ-VEN-1 is proved for `ez add`, `ez remove` and `ez lock --upgrade`. Over the line-level function `I.lines` (ledger/ignore.bend), its allowlist lines are exactly the vendored hashes, each once, in the order the ledger first names them, and every other line is kept in order; the file `I.sync` writes reads back (`I.file.lines`) as those lines, whatever the file it read ended with, and applying it twice is applying it once; each for a ledger whose vendored hashes hold no newline. `ez remove` and `ez add` leave `.gitignore` holding exactly `I.sync`'s text over the ledger they leave (`remove_syncs_allowlist`, `add_syncs_allowlist`). `ez lock --upgrade`: every `.gitignore` its plan writes has the allowlist of the hashes the upgrade commits and keeps every other line of the file it read, when no source it read is at `.gitignore`; an upgrade that does not refuse and leaves `.gitignore` unwritten read one whose allowlist is already those hashes (`upgrade_allowlist_kept_in_sync`); and the hashes it commits are the vendored hashes of the model it renders when it writes ez.toml (`upgrade_vends_the_ledger`) and of ez.toml as it is when it does not (`upgrade_unmoved_vends_the_ledger`). `ez add`'s half and the upgrade's hold of ez.toml's bytes, since the ledger they leave reads back as the model they render (EZ-LED-4). -EZ-DOC-1 is trusted, not proved: the lock is written as eztoml's `render` of the document ez assembles (`T.normal`, `toml/toml.bend`) and read through eztoml's `parse`, so it reads back when eztoml's round trip holds, which is EZ-TRUST-8, pending in eztoml v0.4.0. ez still writes no lock that `lockable.named` refuses: `lockable` refuses a hash, key or value holding `"`, `\` or a newline, a hash written twice, and a file path holding `=`. eztoml v0.4.0 escapes strings and reads a quoted key whole, so these refusals are no longer needed for eztoml; they are kept for `bootstrap.sh`, whose awk cuts a pair at its first `=` and reads no escape. What the lock records is the packages in hash order with each one's files in path order and each once, each tool pin without `vendor`, and the names in name order and each once. Until ez moved to eztoml 0.4 this row was proved against the v0.1.0 reader (`lock_reads_back` and its tools, names and hub laws); the maintainer chose to move ahead of eztoml's proofs, and those laws went with the reader they unfolded. +EZ-DOC-1 is trusted, not proved: the lock is written as eztoml's `render` of the document ez assembles (`T.normal`, `toml/toml.bend`) and read through eztoml's `parse`, so it reads back when eztoml's round trip holds, which is EZ-TRUST-8, proved in eztoml v0.5.0 and not re-checked here. ez still writes no lock that `lockable.named` refuses: `lockable` refuses a hash, key or value holding `"`, `\` or a newline, a hash written twice, and a file path holding `=`. eztoml v0.4.0 escapes strings and reads a quoted key whole, so these refusals are no longer needed for eztoml; they are kept for `bootstrap.sh`, whose awk cuts a pair at its first `=` and reads no escape. What the lock records is the packages in hash order with each one's files in path order and each once, each tool pin without `vendor`, and the names in name order and each once. Until ez moved to eztoml 0.4 this row was proved against the v0.1.0 reader (`lock_reads_back` and its tools, names and hub laws); the maintainer chose to move ahead of eztoml's proofs, and those laws went with the reader they unfolded. -EZ-LED-4 is proved relative to EZ-TRUST-8. `ledger/LAWS.bend` states the read-back as a premise, `ReadsBack`: every ledger `Rend.renderable` accepts reads back, from the text `Rend.show` writes, as itself. `Rend.show` is eztoml's `render` of the document ez assembles (`Rend.text`) and `M.parse` reads through eztoml's `parse`, so the premise is eztoml's round trip, pending in eztoml v0.4.0, and ez does not prove it. What ez proves is the rest: every command that writes ez.toml refuses a ledger that is not renderable, with no effect (EZ-OUT-2), and writes one that reads back, given the premise, as the model its laws are stated over: `ez init` the package and entry it was given (`init_ledger_reads_back`), `ez add` the ledger with the dependency added (`add_ledger_reads_back`, `add_named_reads_back`), and `ez remove` the ledger with it dropped (`remove_ledger_reads_back`). `renderable` refuses a name or value holding `"`, `\` or a newline, a dependency with no hash, and a git source that names no repo or no root. A ledger written before ez used eztoml 0.4 reads to the same model: `toml/toml.bend` passes over the tables a dotted header implies, and `tests/toml.bend` reads an old ledger and lock and their new forms to the same sections. +EZ-LED-4 is proved relative to EZ-TRUST-8. `ledger/LAWS.bend` states the read-back as a premise, `ReadsBack`: every ledger `Rend.renderable` accepts reads back, from the text `Rend.show` writes, as itself. `Rend.show` is eztoml's `render` of the document ez assembles (`Rend.text`) and `M.parse` reads through eztoml's `parse`, so the premise is eztoml's round trip, proved in eztoml v0.5.0, and ez does not prove it. What ez proves is the rest: every command that writes ez.toml refuses a ledger that is not renderable, with no effect (EZ-OUT-2), and writes one that reads back, given the premise, as the model its laws are stated over: `ez init` the package and entry it was given (`init_ledger_reads_back`), `ez add` the ledger with the dependency added (`add_ledger_reads_back`, `add_named_reads_back`), and `ez remove` the ledger with it dropped (`remove_ledger_reads_back`). `renderable` refuses a name or value holding `"`, `\` or a newline, a dependency with no hash, and a git source that names no repo or no root. A ledger written before ez used eztoml 0.4 reads to the same model: `toml/toml.bend` passes over the tables a dotted header implies, and `tests/toml.bend` reads an old ledger and lock and their new forms to the same sections. The upgrade laws of phase three, for EZ-RES-4, EZ-RES-5, EZ-RES-6, EZ-RES-8 and the `ez lock --upgrade` half of EZ-VEN-1, are stated over the ledger model the upgrade renders into ez.toml, and hold of the file's bytes because those bytes read back as that model (EZ-LED-4). The design is in [docs/rfc/ez-lock-planner.md](docs/rfc/ez-lock-planner.md). EZ-RES-4 and EZ-RES-6 are proved so: their laws (`lock/LAWS.bend`) are over `P.ledger.next`, the model an upgrade renders, and over `P.wants.up`, the questions it asks, and what they say of ez.toml's bytes, and of the lock made from those bytes read back, holds by EZ-LED-4. EZ-RES-6's `NAME` is a nonempty `--package`; an empty one is no filter, as `ez lock --upgrade` alone. @@ -194,15 +194,15 @@ These assumptions sit outside the proofs. They are the complete list of Trusted | EZ-TRUST-1 | The Bend checker is sound. | We cannot check it from inside Bend. The BendTT paper and a Lean formalization exist, and the release notes report mismatches between the formalization and the implementation. | | EZ-TRUST-2 | The interpreter reads the World and executes plans faithfully. | It makes no decisions and is kept small enough to review line by line. | | EZ-TRUST-3 | The hub serves, for a hash, what was published under it. | ez checks every hub body against the hash it asked for (EZ-FETCH-1), so this reduces to availability and EZ-HASH-6. | -| EZ-TRUST-4 | `ez prove` runs `bend` on every PROOF.bend in the tree and passes only on an exact `All terms check.` first line. | It is ez code run by `mkProofs`, not a law. CI builds from a clean tree, so nothing is cached. | -| EZ-TRUST-5 | HTTP framing and URL parsing are correct. | Proved in ezhttp v0.5.0, the rev ez.toml pins; ez's gate does not re-check it. | +| EZ-TRUST-4 | `ez prove` runs `bend` on a file above the tree that imports every PROOF.bend, and passes only on an exact `All terms check.` first line. | It is ez code run by `mkProofs`, not a law. CI builds from a clean tree, so nothing is cached. Bend 2.0.28 names a file from the program that starts it, so the start is above the tree. | +| EZ-TRUST-5 | HTTP framing and URL parsing are correct. | Proved in ezhttp v0.6.0, the rev ez.toml pins; ez's gate does not re-check it. | | EZ-TRUST-6 | A `@` the hub answered once names the same hash forever. | The hub never moves a name once it is taken, so a name is resolved once and pinned in the lock. The package it names is still checked against its hash (EZ-FETCH-1). | | EZ-TRUST-7 | Command-line parsing is correct: `parse` binds a line as shake's spec says, `help_path` names a request for help and only one, `path_of` and `at` follow the selected path, and `get`, `on` and `help` read and render it. | Proved in shake v0.2.0, the rev ez.toml pins (SHAKE-PARSE-1 to SHAKE-PARSE-10, SHAKE-GET-1, SHAKE-GET-2, SHAKE-HELP-1, SHAKE-ERR-1, SHAKE-ERR-2); ez imports only its interface, `main.bend`, and its gate does not re-check it. In particular `ez help ` with a word that names no command there fails as `Unexpected`, not as a request for help (SHAKE-PARSE-8). | -| EZ-TRUST-8 | A document eztoml v0.4.0 renders reads back as itself, and a text it reads without error renders back as the same document: its TOML-RT-1, TOML-RT-2 and TOML-RT-3. | Pending in eztoml v0.4.0, the rev ez.toml pins, which states them and has not proved them yet. ez relies on them for EZ-DOC-1 and EZ-LED-4; the maintainer chose to move to eztoml 0.4 ahead of the proofs. Revisit when eztoml proves them. ez's step between its sections and eztoml's document (`toml/toml.bend`) is ez code with no law: `tests/toml.bend` checks it on an old and a new ledger and lock. | +| EZ-TRUST-8 | A document eztoml v0.5.0 renders reads back as itself, and a text it reads without error renders back as the same document: its TOML-RT-1, TOML-RT-2 and TOML-RT-3. | Proved in eztoml v0.5.0, the rev ez.toml pins; ez's gate does not re-check it. ez relies on it for EZ-DOC-1 and EZ-LED-4. ez's step between its sections and eztoml's document (`toml/toml.bend`) is ez code with no law: `tests/toml.bend` checks it on an old and a new ledger and lock. | | EZ-DOC-1 | Parsing a rendered lock yields the packages, hub, names and tools that were rendered. | It is EZ-TRUST-8 for the document ez assembles for the lock. | | EZ-RES-7 | git reports refs, tags, and ancestry accurately. | The World model takes git's answers as given. | | EZ-HASH-4 | ez's 0x hash matches `bend --publish`. | The publisher is a separate program. | | EZ-HASH-5 | ez's narHash matches nix. | nix is a separate program. What ez trusts of its own walk is GNU `find`'s listing of the tree, each path's type, `%M` mode, name and link target, and the file effect's read of each file's bytes. The walk takes the executable bit from the owner's exec bit of that mode, as nix's dumper does, and reads names and targets as listed (EZ-HASH-7). Submodules are not part of the tree: ez weighs a checkout without them, and its nix side asks `fetchgit` for the same. | -| EZ-HASH-6 | `Sha.raw` computes the SHA-256 digest of its bytes, and `Sha.hex` of its text's UTF-8. | Proved in Giulio2002/bend-sha256 against an executable FIPS 180-4 specification, at the hash ez vendors; ez's gate does not re-check it. Collision resistance is also assumed. | +| EZ-HASH-6 | `Sha.raw` computes the SHA-256 digest of its bytes, and `Sha.hex` of its text's UTF-8. | Proved in noah-emp/bend-sha256 against an executable FIPS 180-4 specification, at the hash ez vendors; ez's gate does not re-check it. The git pin is temporary. Collision resistance is also assumed. | EZ-VEN-2 and EZ-VEN-3 are proved for the moves an upgrade makes (`ledger/LAWS.bend` `moves.ok`): each old hash names something, no hash holds `/` or a newline, as a `0x` name never does, and no move's new hash is the old hash of a move after it. That last is the premise the spec's notes call for: swaps apply one after another, so a new hash that is a later move's old one would be moved again. The text laws are over `U.reimport.many`, and the plan laws carry them to what `ez lock --upgrade` leaves at a `.bend` source it read and the World names once (`found`, with `pre` and `post` around it), when the lock does not refuse; that the sources the upgrade reads are the `.bend` files outside `.ez` and `.git` is the interpreter's (EZ-TRUST-2). A line names a hash when it starts `import /` at column 0; the new hash a line names is the one the first move of its old hash sends it to. diff --git a/add/PROOF.bend b/add/PROOF.bend index ce2b1f8..51f0b2b 100644 --- a/add/PROOF.bend +++ b/add/PROOF.bend @@ -309,7 +309,7 @@ def wf(k: K.Walked) -> List<&2, K.Source>: case K.Refused{_why}: [] -def ws(k: K.Walked) -> List<&2, K.File>: +def ws(k: K.Walked) -> List<&2, K.Member>: match k: case K.Walked{_h, _r, _fs, ss}: ss @@ -438,7 +438,7 @@ law edits_of: for +h: String for +a: String for fs: List<&2, K.Source> - for ss: List<&2, K.File> + for ss: List<&2, K.Member> for +m: M.Manifest for +w: A.World {P.put.in(AP.effects.of(d, h, a, fs, ss, m, w), "ez.toml") @@ -522,7 +522,7 @@ law syncs_of: for +h: String for +a: String for fs: List<&2, K.Source> - for ss: List<&2, K.File> + for ss: List<&2, K.Member> for +m: M.Manifest for +w: A.World {AP.after(P.put.in(AP.effects.of(d, h, a, fs, ss, m, w), ".gitignore"), A.ignore(w)) @@ -602,7 +602,7 @@ law says_of: for +h: String for +a: String for fs: List<&2, K.Source> - for ss: List<&2, K.File> + for ss: List<&2, K.Member> for +m: M.Manifest for +w: A.World {AP.last.go(P.said.in(AP.effects.of(d, h, a, fs, ss, m, w)), "") == Git.import.line(h, a) @@ -894,7 +894,7 @@ law fixed_judge: def fixed_judge(ok, _bad, root, pre, out): match ok: case True{}: - %Equal.sym(List<&2, K.File>, K.placed(pre, K.hit.sums(out)), + %Equal.sym(List<&2, K.Member>, K.placed(pre, K.hit.sums(out)), K.laid.sums(K.laid(pre, out)), Pk.placed_is_laid(pre, out)) : {K.Walked{K.hash_of(K.files_of(K.laid.sums(K.laid(pre, out)))), root, K.laid(pre, out), K.files_of(K.laid.sums(K.laid(pre, out)))} @@ -1048,19 +1048,19 @@ def last_snoc(xs, at, text): # LAW: the found files as laid, weighed, are the walk's laid files weighed law weigh_srcs: for fs: List<&2, K.Source> - {W.weighs(AP.srcs(fs)) == K.laid.sums(fs) : List<&2, K.File>} + {W.weighs(AP.srcs(fs)) == K.laid.sums(fs) : List<&2, K.Member>} def weigh_srcs(fs): match fs: case []: {==} case K.Source{at, text} <> t: - Equal.cong(List<&2, K.File>, List<&2, K.File>, ys => K.File{at, Sha.hex(text)} <> ys, + Equal.cong(List<&2, K.Member>, List<&2, K.Member>, ys => K.Member{at, Sha.hex(text)} <> ys, W.weighs(AP.srcs(t)), K.laid.sums(t), weigh_srcs(t)) # a package's file list, weighed from its texts, and the files a `Lay` # writes for it -def lsum(fs: List<&2, K.Source>) -> List<&2, K.File>: +def lsum(fs: List<&2, K.Source>) -> List<&2, K.Member>: K.files_of(K.laid.sums(fs)) def lh(fs: List<&2, K.Source>) -> String: @@ -1081,7 +1081,7 @@ def lay_canon(fs): : {Bool.and(String.eq(lh(fs), K.hash_of(K.files_of(W.weighs(_)))), String.eq(P.last(lay.files(fs)), K.manifest_of(K.files_of(W.weighs(_))))) == True{} : Bool} - %Equal.sym(List<&2, K.File>, W.weighs(AP.srcs(fs)), K.laid.sums(fs), weigh_srcs(fs)) + %Equal.sym(List<&2, K.Member>, W.weighs(AP.srcs(fs)), K.laid.sums(fs), weigh_srcs(fs)) : {Bool.and(String.eq(lh(fs), K.hash_of(K.files_of(_))), String.eq(P.last(lay.files(fs)), K.manifest_of(K.files_of(_)))) == True{} : Bool} %Equal.sym(String, P.last(lay.files(fs)), K.manifest_of(lsum(fs)), @@ -1451,7 +1451,7 @@ law entry_fit: for +h: String for +r: String for fs: List<&2, K.Source> - for ss: List<&2, K.File> + for ss: List<&2, K.Member> for +w: A.World for s: {win(AP.outcome.entry(g, K.Walked{h, r, fs, ss}, w)) == True{} : Bool} {Rend.renderable(Rend.add.keep(A.manifest.of(A.read(w)), AP.dep.of(h, r, w))) == True{} : Bool} @@ -2282,7 +2282,7 @@ def lnv(+hash: String, v: W.Verdict) -> Bool: law lnv.laid: for ok: Bool for +hash: String - for +fs: List<&2, K.File> + for +fs: List<&2, K.Member> for +ss: List<&2, String> for e: {String.eq(hash, W.named(W.laid(fs, ss))) == ok : Bool} {lnv(hash, W.body.laid(ok, hash, fs, ss)) == True{} : Bool} @@ -2297,7 +2297,7 @@ def lnv.laid(ok, _hash, _fs, _ss, e): law lnv.sums: for ok: Bool for +hash: String - for +fs: List<&2, K.File> + for +fs: List<&2, K.Member> for +ss: List<&2, String> {lnv(hash, W.body.sums(ok, hash, fs, ss)) == True{} : Bool} @@ -2312,7 +2312,7 @@ law lnv.escape: for clean: Bool for +bad: String for +hash: String - for +fs: List<&2, K.File> + for +fs: List<&2, K.Member> for +ss: List<&2, String> {lnv(hash, W.body.escape.go(clean, bad, hash, fs, ss)) == True{} : Bool} diff --git a/add/hub.bend b/add/hub.bend index 3a64409..d7176a5 100644 --- a/add/hub.bend +++ b/add/hub.bend @@ -83,7 +83,7 @@ def heard(rs: List<&2, W.Reply>, +key: String) -> Maybe<&2, W.Answer>: # every answer is in, with the hash the hub named and the package it serves # checked against it; a question is still open; or the add refuses type Verdict is Data: - Go{hash: String, files: List<&2, K.File>, srcs: List<&2, String>} + Go{hash: String, files: List<&2, K.Member>, srcs: List<&2, String>} Wait{asks: List<&2, W.Ask>} Stop{why: String} @@ -187,7 +187,7 @@ def decide(+world: A.World) -> Verdict: # the entry # whether a package holds a file at this path -def holds(fs: List<&2, K.File>, +at: String) -> Bool: +def holds(fs: List<&2, K.Member>, +at: String) -> Bool: match fs: case []: False{} @@ -209,7 +209,7 @@ def top.at(hit: Bool, +at: String, rest: Unit -> String) -> String: rest(Unit{}) # the first top-level `.bend` file, in manifest order, "" for none -def top(fs: List<&2, K.File>) -> String: +def top(fs: List<&2, K.Member>) -> String: match fs: case []: "" @@ -217,7 +217,7 @@ def top(fs: List<&2, K.File>) -> String: top.at(top.one(K.file.at(h)), K.file.at(h), _u => top(t)) # `main.bend` when the package holds one, else its first top-level file -def entry.main(held: Bool, fs: List<&2, K.File>) -> String: +def entry.main(held: Bool, fs: List<&2, K.Member>) -> String: match held: case True{}: "main.bend" @@ -226,11 +226,11 @@ def entry.main(held: Bool, fs: List<&2, K.File>) -> String: # the entry a package is recorded with when none was asked for: its # `main.bend`, else its first top-level `.bend` file, else none -def entry.of(+fs: List<&2, K.File>) -> String: +def entry.of(+fs: List<&2, K.Member>) -> String: entry.main(holds(fs, "main.bend"), fs) # the entry asked for, or, when none was, the package's own -def entry.pick(none: Bool, +fs: List<&2, K.File>, +asked: String) -> String: +def entry.pick(none: Bool, +fs: List<&2, K.Member>, +asked: String) -> String: match none: case True{}: entry.of(fs) @@ -238,14 +238,14 @@ def entry.pick(none: Bool, +fs: List<&2, K.File>, +asked: String) -> String: asked # the entry recorded: the one asked for, else the package's own -def entry(+fs: List<&2, K.File>, +world: A.World) -> String: +def entry(+fs: List<&2, K.Member>, +world: A.World) -> String: entry.pick(String.is_empty(asked(world)), fs, asked(world)) # --------------------------------------------------------------------------- # the plan # the dependency recorded for a package the hub named by this hash -def dep.of(+hash: String, +fs: List<&2, K.File>, +world: A.World) -> M.Dep: +def dep.of(+hash: String, +fs: List<&2, K.Member>, +world: A.World) -> M.Dep: M.Dep{key(world), hash, entry(fs, world), M.Hub{nv(world)}} # the ledger with the package added, once it is known to read back. A @@ -267,7 +267,7 @@ def outcome.entry(held: Bool, fit: Bool, +at: String, +world: A.World) -> P.Outc P.Refused{"ez: " ++ at ++ " is not in " ++ nv(world)} # how an add ends once the package is in hand -def outcome.of(+hash: String, +fs: List<&2, K.File>, +world: A.World) -> P.Outcome: +def outcome.of(+hash: String, +fs: List<&2, K.Member>, +world: A.World) -> P.Outcome: outcome.entry(Bool.or(String.is_empty(asked(world)), holds(fs, Path.norm(asked(world)))), Rend.renderable(Rend.add.keep(A.manifest.of(A.read(world)), dep.of(hash, fs, world))), asked(world), world) @@ -325,7 +325,7 @@ def seal(es: List<&2, P.Effect>, outcome: P.Outcome) -> P.Plan: P.Plan{[], P.Refused{why}} # the plan once the package is in hand -def made(+hash: String, +fs: List<&2, K.File>, +ss: List<&2, String>, +world: A.World) -> P.Plan: +def made(+hash: String, +fs: List<&2, K.Member>, +ss: List<&2, String>, +world: A.World) -> P.Plan: seal(effects.of(dep.of(hash, fs, world), hash, W.laid(fs, ss), A.manifest.of(A.read(world)), world), outcome.of(hash, fs, world)) @@ -385,7 +385,7 @@ def verdict.hash(verdict: Verdict) -> String: case Stop{_why}: "" -def verdict.files(verdict: Verdict) -> List<&2, K.File>: +def verdict.files(verdict: Verdict) -> List<&2, K.Member>: match verdict: case Go{_hash, fs, _ss}: fs @@ -399,7 +399,7 @@ def hash(+world: A.World) -> String: verdict.hash(decide(world)) # the package's files, as the hub served them -def files(+world: A.World) -> List<&2, K.File>: +def files(+world: A.World) -> List<&2, K.Member>: verdict.files(decide(world)) # the dependency `ez add @` records on a World diff --git a/add/plan.bend b/add/plan.bend index af37444..64ba17a 100644 --- a/add/plan.bend +++ b/add/plan.bend @@ -564,7 +564,7 @@ def effects.of( +hash: String, +at: String, fs: List<&2, K.Source>, - ss: List<&2, K.File>, + ss: List<&2, K.Member>, +manifest: M.Manifest, +world: A.World ) -> List<&2, P.Effect>: @@ -790,7 +790,7 @@ def refuses.command(+world: A.World) -> Bool: type Next is Data: AskGit{asks: List<&2, Up.Ask>} AskHub{asks: List<&2, W.Ask>} - Done{plan: P.Plan} + Ready{plan: P.Plan} # the git planner's step def next.git(st: Step) -> Next: @@ -798,13 +798,13 @@ def next.git(st: Step) -> Next: case Asking{asks}: AskGit{asks} case Run{pl}: - Done{pl} + Ready{pl} # the hub planner's step: its questions, or its plan once there are none def next.hub(asks: List<&2, W.Ask>, +world: A.World) -> Next: match asks: case []: - Done{H.plan(world)} + Ready{H.plan(world)} case h <> t: AskHub{h <> t} @@ -826,5 +826,5 @@ def next.asks(nx: Next) -> Bool: True{} case AskHub{_asks}: True{} - case Done{_pl}: + case Ready{_pl}: False{} diff --git a/add/run.bend b/add/run.bend index ce17cb2..3bb24bc 100644 --- a/add/run.bend +++ b/add/run.bend @@ -10,7 +10,7 @@ # exits 1 with the reason when the plan refuses. It decides nothing; that it # reads and executes faithfully is EZ-TRUST-2. import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../io/file.bend as F import ../lock/run.bend as Run import ../lock/up.bend as Up @@ -40,7 +40,7 @@ def loop.step(st: AP.Next, +lib: String, world: A.World, go: A.World -> IO(Unit) do IO: rs : List<&2, W.Reply> <- Run.answer.all(lib, asks) go(more.hub(world, rs)) - case AP.Done{pl}: + case AP.Ready{pl}: Run.exec.plan(lib, pl) # the loop, under fuel. Every round adds an answer, since the planner never diff --git a/check/oracle.bend b/check/oracle.bend index 61544ba..aa5b54e 100644 --- a/check/oracle.bend +++ b/check/oracle.bend @@ -19,7 +19,7 @@ import Base import ../sha/sha.bend as Sha import ../io/file.bend as F -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ./serve.bend as S # a list with its last element gone, the head held back one step so the walk can diff --git a/check/world.bend b/check/world.bend index c06809d..94f77e6 100644 --- a/check/world.bend +++ b/check/world.bend @@ -6,7 +6,7 @@ # directory, and `setsid --fork` returns as soon as the child is a session of # its own. Nothing here goes through a shell. import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R # the non-empty strings, which is what a program's output amounts to once its # trailing newline has been counted as a line diff --git a/docs/rfc/ez-spec.md b/docs/rfc/ez-spec.md index 37fb727..b4045b3 100644 --- a/docs/rfc/ez-spec.md +++ b/docs/rfc/ez-spec.md @@ -129,7 +129,7 @@ Every requirement carries exactly one level. We considered intermediate levels for "checked on examples" and "agrees with an external oracle", and rejected both (see Abandoned Ideas). The short version is that Bend's gate is a proof checker, and anything it checks on a single example is a test wearing a law's syntax. Two levels keep the spec honest: if a claim is not proved for all inputs, we say we are trusting it, and a reader knows exactly how much weight to put on it. -A guarantee proved in a dependency is Trusted from ez's side. The SHA-256 digest comes from Giulio2002/bend-sha256, whose own laws hold it to an executable FIPS 180-4 specification, and HTTP framing is proved in ezhttp, which replaced `net/` in #50. Those proofs are real, but ez's gate does not re-check them, so ez records them as trust with the dependency and pinned hash as the reason. +A guarantee proved in a dependency is Trusted from ez's side. The SHA-256 digest comes from noah-emp/bend-sha256, whose own laws hold it to an executable FIPS 180-4 specification. The git pin is temporary. HTTP framing is proved in ezhttp, which replaced `net/` in #50. Those proofs are real, but ez's gate does not re-check them, so ez records them as trust with the dependency and pinned hash as the reason. A Proved requirement whose law has not landed yet is marked **pending** in `SPEC.md`. Pending is a status, not a third level: it means "intended to be Proved, not yet guaranteed", and the spec says so plainly. Because the gate fails on any undischarged law, a pending requirement's law stays out of LAWS.bend until its proof is written, and the statement lives in `SPEC.md` until then. @@ -502,12 +502,12 @@ These assumptions sit outside the proofs. They are the complete list of Trusted | EZ-TRUST-2 | The interpreter reads the World and executes plans faithfully. | It makes no decisions and is kept small enough to review line by line. | | EZ-TRUST-3 | The hub serves, for a hash, what was published under it. | ez checks every hub body against the hash it asked for (EZ-FETCH-1), so this reduces to availability and EZ-HASH-6. | | EZ-TRUST-4 | `ez prove` runs `bend` on every PROOF.bend in the tree and passes only on an exact `All terms check.` first line. | It is ez code run by `mkProofs`, not a law. CI builds from a clean tree, so nothing is cached. | -| EZ-TRUST-5 | HTTP framing and URL parsing are correct. | Proved in ezhttp v0.4.0, the rev ez.toml pins; ez's gate does not re-check it. | +| EZ-TRUST-5 | HTTP framing and URL parsing are correct. | Proved in ezhttp v0.6.0, the rev ez.toml pins; ez's gate does not re-check it. | | EZ-TRUST-6 | A `@` the hub answered once names the same hash forever. | The hub never moves a name once it is taken, so a name is resolved once and pinned in the lock. The package it names is still checked against its hash (EZ-FETCH-1). | | EZ-RES-7 | git reports refs, tags, and ancestry accurately. | The World model takes git's answers as given. | | EZ-HASH-4 | ez's 0x hash matches `bend --publish`. | The publisher is a separate program. | | EZ-HASH-5 | ez's narHash matches nix. | nix is a separate program. What ez trusts of its own walk is GNU `find`'s listing of the tree, each path's type, `%M` mode, name and link target, and the file effect's read of each file's bytes. The walk takes the executable bit from the owner's exec bit of that mode, as nix's dumper does, and reads names and targets as listed (EZ-HASH-7). Submodules are not part of the tree: ez weighs a checkout without them, and its nix side asks `fetchgit` for the same. | -| EZ-HASH-6 | `Sha.raw` computes the SHA-256 digest of its bytes, and `Sha.hex` of its text's UTF-8. | Proved in Giulio2002/bend-sha256 against an executable FIPS 180-4 specification, at the hash ez vendors; ez's gate does not re-check it. Collision resistance is also assumed. | +| EZ-HASH-6 | `Sha.raw` computes the SHA-256 digest of its bytes, and `Sha.hex` of its text's UTF-8. | Proved in noah-emp/bend-sha256 against an executable FIPS 180-4 specification, at the hash ez vendors; ez's gate does not re-check it. The git pin is temporary. Collision resistance is also assumed. | EZ-TRUST-3 is narrowed from the first draft: ez verifies hub content itself (EZ-FETCH-1), so what remains is that the hub serves the hash at all, which is what lets EZ-DOC-3 leave hub content out of `inputs`. @@ -585,6 +585,8 @@ Moving to eztoml v0.4.0 (WP32) changes the layout of ez.toml and ez.lock.toml, a Reading the code also turned up behavior that looked accidental and is not a requirement. Besides the ledger changes above, two such fixes were worth making, and both have landed. Every command, `ez help` included, created `.ez` and `bin` in the current directory, because `Env.make()` ran before the line was parsed; `Env.dirs` now names only the directories a command writes into, and nothing for most commands (`dirs_other`, `dirs_check`, `dirs_build`, `dirs_build_out`). And `ez doctor` failed a project with no dependencies, because it counted a lock that names no package as a problem even when the ledger needed none. The rest of what looked accidental was either covered by a decided change above or left alone as incidental, and what remains open is under "Known gaps". +The sha256 dependency is pinned at https://github.com/noah-emp/bend-sha256, rev `1319f22df2d5072a861cc71740c93258c44ac4ff`, for a Bend that can build it. The pin is temporary. Bend's flake input is the commit that names 2.0.31. eztoml moves to v0.5.0, where TOML-RT-1, TOML-RT-2 and TOML-RT-3 are proved; ez still does not re-check them (EZ-TRUST-8). snap moves to v1.1.0, ezhttp to v0.6.0 and bolt to v1.9.0, which register effects the way Bend 2.0.28 reads them. The binary bend starts is `ez.bend`, at the project root, because Bend 2.0.28 names a file from the program that starts it and a start inside `ez/` gives one file two names. `ez prove` starts each proof the same way. + ### Known gaps These are the things we know ez does not yet do, or does in a way we have not decided to guarantee. None of them is a requirement, and none weakens a proved row; each is here so that a reader does not have to rediscover it. @@ -649,7 +651,7 @@ The second phase enables the traceability check in bolt, reading `SPEC.md`. Pend The third phase introduces the World model and converts `ez lock` to planner form, then proves EZ-DOC-1 through EZ-DOC-5, EZ-RES-4 through EZ-RES-6 and EZ-RES-8, EZ-VEN-1 through EZ-VEN-3, and EZ-HASH-2, deleting the closed laws each one subsumes. EZ-DOC-3 is proved once the lock input changes have landed. `ez lock` goes first because its guarantees are the most important. The design for this phase, with its World, its laws and its work packages, is in [ez-lock-planner.md](ez-lock-planner.md). The phase's upgrade laws (EZ-RES-4 to EZ-RES-6, EZ-RES-8 and the upgrade half of EZ-VEN-1) are stated over the ledger model the plan renders into ez.toml, so they held of the file's bytes only relative to EZ-LED-4, which was not in this phase. WP21 proved EZ-LED-4, and they now hold of the bytes. -EZ-DOC-1 was proved against the pinned eztoml v0.1.0 reader, with a file path holding `=` refused (see "Decided behavior changes"). The rollout meant to move ez to eztoml once eztoml proved its own render and parse round trip. The maintainer chose to move ahead of those proofs (WP32): ez is on eztoml v0.4.0, whose round trip TOML-RT-1 to TOML-RT-3 it states and has not yet proved, and accepted the new lock and ledger layout that comes with writing through it. EZ-DOC-1 is now Trusted, and EZ-LED-4's laws take the read-back as a premise; both rest on EZ-TRUST-8, to revisit when eztoml proves those rows. +EZ-DOC-1 was proved against the pinned eztoml v0.1.0 reader, with a file path holding `=` refused (see "Decided behavior changes"). The rollout meant to move ez to eztoml once eztoml proved its own render and parse round trip. The maintainer chose to move ahead of those proofs (WP32): ez moved to eztoml v0.4.0, whose round trip it stated and had not proved, and accepted the new lock and ledger layout that comes with writing through it. EZ-DOC-1 stayed Trusted, and EZ-LED-4's laws take the read-back as a premise. eztoml v0.5.0 proves TOML-RT-1 to TOML-RT-3, and ez pins that rev without re-checking the proofs (EZ-TRUST-8). The next phase converts `ez add` and `ez remove`, with `ez init`, and makes the package walk a pure function of a checkout's files. It proves EZ-LED-2, EZ-LED-3, EZ-LED-7, EZ-RES-1 and EZ-RES-2, and lands the add and remove halves of EZ-LED-1, EZ-LED-6, EZ-LED-8, EZ-VEN-1, EZ-HASH-3 and EZ-OUT-2. Its design, with its Worlds, its laws and its work packages, is in [ez-add-planner.md](ez-add-planner.md). Later phases convert `ez fetch`, `ez publish`, `ez doctor` and the tool commands in the same way, one command per phase, each ending with its requirements proved. @@ -695,6 +697,7 @@ The rollout above ran as planned, with the command conversions split into work p | WP30 | `ez publish` asks the ledger's hub about every hub package the package imports, by hash and by name, and refuses, sending nothing, when one is not there or the hub cannot be asked. | EZ-PUB-5, EZ-OUT-2 | | WP31 | shake v0.2.0 through its interface alone, snap v1.0.0, sha256 by its published walk, and ezhttp v0.5.0; the line laws restated over shake's `help_path`, `path_of` and `at`, resting on shake's proofs (EZ-TRUST-7). | EZ-OUT-1 | | WP32 | eztoml v0.4.0 through its interface alone: ez.toml and ez.lock.toml written by eztoml's `render`, in its layout, and read by its `parse`, old layouts included. EZ-DOC-1 becomes Trusted, and the EZ-LED-4 and upgrade laws take the ledger's read-back as a premise (EZ-TRUST-8). | EZ-LED-4, EZ-DOC-4 | +| WP33 | sha256 pinned at noah-emp/bend-sha256, Bend at the flake that names 2.0.31, eztoml at v0.5.0, snap at v1.1.0, ezhttp at v0.6.0 and bolt at v1.9.0. The binary and each proof start from a file above the tree. | EZ-HASH-6, EZ-TRUST-8, EZ-TRUST-4, EZ-TRUST-5 | Proving also found bugs that reading the code had missed, and each was fixed where it was found: WP6 found that WP2's upgrade read an empty refusal reason as no refusal (a case the interpreter never built, so the binary did not change), WP5b found that a tool pin with a rev and no narHash moved on the next upgrade, WP7 found the allowlist written twice for a shared tree, and WP10 found a lock that accepted a manifest `ez fetch` would then refuse. The proofs are long, as the risks below expected: `lock/PROOF.bend` grew by about 4,800 lines in WP5b alone, most of them one lemma per step of the upgrade. @@ -728,6 +731,6 @@ Every Proved requirement assumes the Bend checker is sound (EZ-TRUST-1). We cann The same structure applies directly to the sibling libraries. ezjson, eztoml, and ezhttp already describe their laws in terms of external standards (TOML 1.0, RFC 9110, RFC 3986), and a shared traceability rule in bolt would cover all of them with the same two levels. ezhttp now owns the HTTP laws, and ez's EZ-TRUST-5 row points at them. Re-checking a dependency's PROOF.bend at its pinned hash inside ez's gate would turn such a row back into a proof without a third level. -ez moved to eztoml v0.4.0 before eztoml proved its render and parse round trip, so EZ-DOC-1 and EZ-LED-4 rest on rows eztoml states and has not proved (EZ-TRUST-8). Until it does, a bug in eztoml's renderer or reader could write a lock or ledger that reads back as something else, and no ez law would catch it; `tests/toml.bend` and the fresh-clone check (EZ-DOC-3) are what would. When eztoml proves those rows, EZ-TRUST-8 is closed, and the lock's refusal of a path holding `=` can lift with `bootstrap.sh`'s awk. +ez pins eztoml v0.5.0, which proves TOML-RT-1, TOML-RT-2 and TOML-RT-3. ez does not re-check those proofs (EZ-TRUST-8). The lock still refuses a path holding `=` because `bootstrap.sh`'s awk cuts a pair at its first `=`. Once `ez lock` and `ez add` are both in planner form, the World model makes cross-command guarantees expressible, such as "`ez add` followed by `ez lock` on a fresh clone reproduces the lock `ez add` wrote." Those end-to-end statements are the strongest description of what ez is for, and they become provable only once individual commands are pure. diff --git a/doctor/run.bend b/doctor/run.bend index 5497aa9..cdfa346 100644 --- a/doctor/run.bend +++ b/doctor/run.bend @@ -14,7 +14,7 @@ # is. None of these writes anything, and the plan writes nothing either. It # decides nothing; that it reads and executes faithfully is EZ-TRUST-2. import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../run/bend.bend as Bend import ../io/file.bend as F import ../ez/args.bend as Args diff --git a/ez.bend b/ez.bend new file mode 100644 index 0000000..fb32fb8 --- /dev/null +++ b/ez.bend @@ -0,0 +1,7 @@ +# The program bend starts. Its directory is the project root, above every +# file, so Bend 2.0.28 gives each file one name. The program is ez/main.bend. +import Base +import ./ez/main.bend as Ez + +def main() -> IO(Unit): + Ez.main() diff --git a/ez.lock.toml b/ez.lock.toml index 9dfd90d..6835892 100644 --- a/ez.lock.toml +++ b/ez.lock.toml @@ -17,81 +17,46 @@ LICENSE = "309f5aae946e4db157750e002fb179a74ed0fe27fce09a7be68a6977b14f205f" "src/args.bend" = "cb408b31dc02aa0525dc07f7a3119798f6d1d96f244361dc941797bb90653b24" "src/check.bend" = "ad47c820def9bb1b77ea52b8097e4a62a7f1bbe6aac3c753ddf089c29f9c012a" "src/cli.bend" = "c8b1c75699e77ca233aac1125cff8565246ae230aee25752c52f05e608f41362" -[packages.0x0a372da4a053652f70ded7d6e0d19330] -[packages.0x0a372da4a053652f70ded7d6e0d19330.source] +[packages.0x5e4e2a9db839a0214ace6923b04b685b] +[packages.0x5e4e2a9db839a0214ace6923b04b685b.source] kind = "git" url = "https://github.com/Emerging-Patterns/ezhttp" -rev = "f71ca6b9e7857212a485ae2bbfb71aa31ff99b38" +rev = "a5279268547ee43b5c48b6c8ada235b4a4596f4c" entry = "ezhttp/main.bend" root = "ezhttp" -narHash = "sha256-KEv4FQyH584qdm+JKmOI13f/ry9XB2O47TLxQTDbRvo=" -tag = "v0.5.0" -[packages.0x0a372da4a053652f70ded7d6e0d19330.files] +narHash = "sha256-Xn6zaCwV8mdIorktU04few1qfhCRobo16yF9H4osPRk=" +tag = "v0.6.0" +[packages.0x5e4e2a9db839a0214ace6923b04b685b.files] "b64.bend" = "7bf2cd0e2947db17a299e739fa8defa91b6275ef5b4fac70c87809bafb0a6420" "body.bend" = "3f45a3613417b1e6a430e6a85bffd9dc52eccec1274cb96d15bcd9e8650b3399" "cache.bend" = "f2f348b05c396c7e121425cc5b49d13ae828f6110d26cb8420c7356ac478c1ae" "client.bend" = "8ec4c45d3adb9cf889151def84d26cf513bad85d6b765b6579111ec6012b4d10" "cookie.bend" = "c8264b3f3d371872dd8d87c7f7f528a0379fa361817560a531f05e993a5a5e08" "cors.bend" = "cad2e8e7eedbd87cc37fbf65f720584ae035aada5ff5cb3c18daba54ff6a2a7d" -"effs/wire.c" = "37a1e2b4a3d39ae08216a90f8b460051beb3139088addb412b8274ace8f16c8d" -"effs/wire.js" = "051ccf59ac03d33a49efcc9cf5ea503a287330bf16809ea5d4a9aea10d8bfd4f" +"effs/wire.c" = "957c6561c6da3d204a0e34b806d063a9e77690572b1bc5759342cb123ca814b5" +"effs/wire.js" = "5616d8369dda12f6513daacf8860795836bcc4011eb9214bf862c3ac30412e6a" "http.bend" = "7622e0cd3da5f669f8a15bfce44fa90b9af77b156c39228e8c637247887f7e7a" "main.bend" = "e0a0906566d4064045a49cf2c0a2b21d286c9091de619a48702ab698e84a9171" "server.bend" = "ebec77b7c2a73ec8e7d8230c336c139fdddb1152d759216deb0b42f4f4504108" "url.bend" = "a13c8acd86c5643c5f3b02e30550aeb2af9d043b5abbfe1fee2980b1c0aae254" "wire.bend" = "e6d672218e3fafeaf83a6178c32622a921bd41ae54d36864ab2eaaf438b9609c" -[packages.0x103d0af04de36ab98b311e537366ec67] -[packages.0x103d0af04de36ab98b311e537366ec67.source] -kind = "git" -url = "https://github.com/Emerging-Patterns/snap" -rev = "ced24e103db518e37f565c577ef312602c217cf5" -entry = "main.bend" -root = "." -narHash = "sha256-dEO94GFkcgssyzOqz4A5VveB3npPq4/zpDpI+EvqnvI=" -tag = "v1.0.0" -[packages.0x103d0af04de36ab98b311e537366ec67.files] -LICENSE = "309f5aae946e4db157750e002fb179a74ed0fe27fce09a7be68a6977b14f205f" -"main.bend" = "68a5a2f373983f652dc260683c57261930bbe1fba3b89f05973066697a4e8d43" -"src/answer.bend" = "cfeb97ada7d0708c49abae1164af3e988a32c7fbdfb6591c61ce148b46d0738d" -"src/argv.bend" = "6a3a6e8669fb5dab77f843fdd778402593d898c52a0dcd8738b689d95ff35856" -"src/effect.bend" = "d0db20f66f1d55128b865d369a6bccfe8353dc05ec7f8b1b9576317ecaba8d8d" -"src/exec.c" = "76f3490075a1640af38dc0422f9e9ebe849f60ad6e9b001f97313dbdaa03880d" -"src/exec.js" = "0a4f99c247fd0e8346b6f541ceeb67e477e450332c5c1942a082280af75bc986" -"src/file.bend" = "261a8f461bf0203e3e33bb3dfe0e21f88b1be1ffad8d9bb088827dcd3904c8f8" -"src/par.bend" = "c5c316830a377d4f6b5390e12e0dd886f00351d882e6e8803b3514491bf5964e" -"src/par.c" = "4843bf8fa1e76c69cf33fa769fa4b8e9f22df69aff990cb5a3de08ecfe9034bc" -"src/par.js" = "791ced8192ca1d7238919629db661bfd3799db24d9483b397052e054f12d4225" -"src/start.c" = "7306425871c0d4b859c6809f34b83ae7947b2065781fd2a8fe8ac8806a77391b" -"src/start.js" = "d45eca4a2782e3fdbc1b7abc798fc3f131dc87dde34ab9cfa6dd917fff2ea04c" -[packages.0xb652b3fca73c8a28ae49abaa395bb530] -[packages.0xb652b3fca73c8a28ae49abaa395bb530.source] -kind = "git" -url = "https://github.com/Emerging-Patterns/eztoml" -rev = "44f7cf6ada497f0c0807cd6ce37e575ecf7e5228" -entry = "main.bend" -root = "." -narHash = "sha256-9M590w5vQRf+13vUUxCqJmyPN3ZlpW3V9VU7Bw38/yQ=" -tag = "v0.4.0" -[packages.0xb652b3fca73c8a28ae49abaa395bb530.files] -LICENSE = "309f5aae946e4db157750e002fb179a74ed0fe27fce09a7be68a6977b14f205f" -"main.bend" = "8ee1876ba66fc895b76b4200d5c17caa94d2165446c33bfa77a3816c4c381846" -[packages.0xda83506fb9f059ead7afcfa2f498df5f] -[packages.0xda83506fb9f059ead7afcfa2f498df5f.source] +[packages.0xa17f0215fb4dd22e26fd007661489402] +[packages.0xa17f0215fb4dd22e26fd007661489402.source] kind = "git" -url = "https://github.com/Giulio2002/bend-sha256" -rev = "5887e7cefa273ff7f90e3edfd6e90b815bbc79ed" +url = "https://github.com/noah-emp/bend-sha256" +rev = "1319f22df2d5072a861cc71740c93258c44ac4ff" entry = "package.bend" root = "." -narHash = "sha256-FLTyFw5HkOrl/T6E8hbs/XVwL05oGmcJARW9I9eHdgA=" -[packages.0xda83506fb9f059ead7afcfa2f498df5f.files] +narHash = "sha256-XYNpKGNHcpV5vRjFMOSlVVBchSdrpJrxgbGzd4dXXAQ=" +[packages.0xa17f0215fb4dd22e26fd007661489402.files] "CORRECTNESS.bend" = "fbdac9b5ab17dca383263b6f8a8809c310573b5eb84f82be8c11bd6086a4099c" "LAWS.bend" = "5fff64c5b3d5c301a11fc1e9d12f2781b1ddb33caa07cf7794dcfd93b8dc6ce0" "PROOF.bend" = "7128c765e4f258105b452c87674206dc316ac0cf82749f3973c2b8fe85f6200f" "buffer.bend" = "c01ad104fa1906c1952398c08245dcd8a38977f379a87bccf7f2da9881223c7d" "buffer_proof.bend" = "4157894db68b98847a88e74bc8599f5f943936d0df4eea165cb32e6a2c78fa87" -"conformance.bend" = "05481c7fe1f23db2fbb3c85bec71cf0812537d7e7d2dc4ea2d6c67698074066c" -"core.bend" = "a754ea9cf6f16eaceec17b7cd6a4ee89da621d6d623a5e2782a0359332d51a3f" -"core_model.bend" = "a77f248472b6b99cba28cb50f473244f5bfb89022b5b04aeef3858013798b031" +"conformance.bend" = "ef8708ff54859828421b56e2b753220f3649d55a77fb0c31c3eef0f8b1689dbe" +"core.bend" = "bece2919b7a164b125bce89c0b893448067971ef3f754febd519c47408b94706" +"core_model.bend" = "86a391b9721e3fcc3c4ede6f172f4bd2713bde298871a4f366a306834381b72a" "fips.bend" = "f11c04cc7e6c319ead48623f73ffb7353fedf3f8ce8751b9330be27aad541ba8" "legacy_model.bend" = "596c955b4b65c2d59a5e0e76a919bfb7e5cf1ff78db32f85cc522f9b7e3bcd75" "list_proofs.bend" = "b71b8a1223944f86b31fce2e1c60fe31b15fc20b320e9fe2364c440c553cd75f" @@ -103,10 +68,45 @@ narHash = "sha256-FLTyFw5HkOrl/T6E8hbs/XVwL05oGmcJARW9I9eHdgA=" "padding_proof.bend" = "ed0f9b4069d3bb2f956adb2d3c53ebe0880cf564beffa37a53b0ea02ba622eff" "sha256.bend" = "995cca1d2f9c8b4863de92ade74ccf91aa4f1f73ef613fd918aec2483bb5de20" "state.bend" = "24b4bb267fe94bd1615a8cff6aa090fff766c9009b5f9aa1c08a865b87d06230" +[packages.0xabe575924687afad4cee1a2c1194d639] +[packages.0xabe575924687afad4cee1a2c1194d639.source] +kind = "git" +url = "https://github.com/Emerging-Patterns/snap" +rev = "fcabc81830c9e21d86d4968810285b287da49c12" +entry = "main.bend" +root = "." +narHash = "sha256-uKIWgjm98bQAYaNiMD/UOfwg55LWcAj2oC9AzSQuNBA=" +tag = "v1.1.0" +[packages.0xabe575924687afad4cee1a2c1194d639.files] +LICENSE = "309f5aae946e4db157750e002fb179a74ed0fe27fce09a7be68a6977b14f205f" +"main.bend" = "68a5a2f373983f652dc260683c57261930bbe1fba3b89f05973066697a4e8d43" +"src/answer.bend" = "cfeb97ada7d0708c49abae1164af3e988a32c7fbdfb6591c61ce148b46d0738d" +"src/argv.bend" = "6a3a6e8669fb5dab77f843fdd778402593d898c52a0dcd8738b689d95ff35856" +"src/effect.bend" = "d0db20f66f1d55128b865d369a6bccfe8353dc05ec7f8b1b9576317ecaba8d8d" +"src/exec.c" = "1478ed5e6315c40f220bfa717d1d6a32103446641e713593c5f6557f484c607e" +"src/exec.js" = "70268064b34529d651b670fb180027703d15ec494f6ea9dd7dcfc878dbb30a74" +"src/file.bend" = "261a8f461bf0203e3e33bb3dfe0e21f88b1be1ffad8d9bb088827dcd3904c8f8" +"src/par.bend" = "c5c316830a377d4f6b5390e12e0dd886f00351d882e6e8803b3514491bf5964e" +"src/par.c" = "7edbca9e791b0d202e78543e7863b8d74d38e79b7f1fcb645dd15fbdb6ffcde0" +"src/par.js" = "33ff4eca5d524264d28da36a9caf0a8252036efd44b92358a4c07daeb3ba69c9" +"src/start.c" = "1bec197312b644549c176463e9476986301b28f6e01e5c34ea508f396cda1aec" +"src/start.js" = "8ea49fe5324a2608342b4629b29d841a81d72ee8006869ac06971a0fb1aed53a" +[packages.0xd79254973edee82bcf56616220876efe] +[packages.0xd79254973edee82bcf56616220876efe.source] +kind = "git" +url = "https://github.com/Emerging-Patterns/eztoml" +rev = "10c3079194db0d6adc9dfb908e877f785a442669" +entry = "main.bend" +root = "." +narHash = "sha256-oWGYok7TMYvBF1ctGYXZ6J10TRMcffDTrRNjgOH6qi0=" +tag = "v0.5.0" +[packages.0xd79254973edee82bcf56616220876efe.files] +LICENSE = "309f5aae946e4db157750e002fb179a74ed0fe27fce09a7be68a6977b14f205f" +"main.bend" = "7d4c33ce8e68895b3bc76cff3f374601e9a3dc4d460cd00bf3159c71c41c65db" [tools] [tools.bolt] git = "https://github.com/Emerging-Patterns/bolt" -rev = "02fb09377f5c0fbddb5f6b7c32c8ab4ae14240df" -tag = "v1.8.0" +rev = "d5a67600a96ba423f2212bd661a30c1fba38eb55" +tag = "v1.9.0" root = "." -narHash = "sha256-53zE+3lZ/jn9GvIeGoavvNMaFyUs5dEFWd7fwP49TlM=" +narHash = "sha256-HmJ8J1xDshBdSWXIiEp48GZ9qHsm+bmpHw06ZWwcDVE=" diff --git a/ez.toml b/ez.toml index d03715c..15864a4 100644 --- a/ez.toml +++ b/ez.toml @@ -1,14 +1,14 @@ [package] name = "ez" entry = "ledger/manifest.bend" -bin = "ez/main.bend" +bin = "ez.bend" [deps] [deps.sha256] -hash = "0xda83506fb9f059ead7afcfa2f498df5f" -git = "https://github.com/Giulio2002/bend-sha256" -rev = "5887e7cefa273ff7f90e3edfd6e90b815bbc79ed" +hash = "0xa17f0215fb4dd22e26fd007661489402" +git = "https://github.com/noah-emp/bend-sha256" +rev = "1319f22df2d5072a861cc71740c93258c44ac4ff" root = "." -narHash = "sha256-FLTyFw5HkOrl/T6E8hbs/XVwL05oGmcJARW9I9eHdgA=" +narHash = "sha256-XYNpKGNHcpV5vRjFMOSlVVBchSdrpJrxgbGzd4dXXAQ=" entry = "package.bend" [deps.shake] hash = "0x085b03c84ca37125e38dddede7b91e55" @@ -19,33 +19,33 @@ root = "." narHash = "sha256-o5NRUjz6OBNMecXY8CZzYQpqoGFxdolD/ST8rIgAnLo=" entry = "main.bend" [deps.snap] -hash = "0x103d0af04de36ab98b311e537366ec67" +hash = "0xabe575924687afad4cee1a2c1194d639" git = "https://github.com/Emerging-Patterns/snap" -rev = "ced24e103db518e37f565c577ef312602c217cf5" -tag = "v1.0.0" +rev = "fcabc81830c9e21d86d4968810285b287da49c12" +tag = "v1.1.0" root = "." -narHash = "sha256-dEO94GFkcgssyzOqz4A5VveB3npPq4/zpDpI+EvqnvI=" +narHash = "sha256-uKIWgjm98bQAYaNiMD/UOfwg55LWcAj2oC9AzSQuNBA=" entry = "main.bend" [deps.ezhttp] -hash = "0x0a372da4a053652f70ded7d6e0d19330" +hash = "0x5e4e2a9db839a0214ace6923b04b685b" git = "https://github.com/Emerging-Patterns/ezhttp" -rev = "f71ca6b9e7857212a485ae2bbfb71aa31ff99b38" -tag = "v0.5.0" +rev = "a5279268547ee43b5c48b6c8ada235b4a4596f4c" +tag = "v0.6.0" root = "ezhttp" -narHash = "sha256-KEv4FQyH584qdm+JKmOI13f/ry9XB2O47TLxQTDbRvo=" +narHash = "sha256-Xn6zaCwV8mdIorktU04few1qfhCRobo16yF9H4osPRk=" entry = "ezhttp/main.bend" [deps.eztoml] -hash = "0xb652b3fca73c8a28ae49abaa395bb530" +hash = "0xd79254973edee82bcf56616220876efe" git = "https://github.com/Emerging-Patterns/eztoml" -rev = "44f7cf6ada497f0c0807cd6ce37e575ecf7e5228" -tag = "v0.4.0" +rev = "10c3079194db0d6adc9dfb908e877f785a442669" +tag = "v0.5.0" root = "." -narHash = "sha256-9M590w5vQRf+13vUUxCqJmyPN3ZlpW3V9VU7Bw38/yQ=" +narHash = "sha256-oWGYok7TMYvBF1ctGYXZ6J10TRMcffDTrRNjgOH6qi0=" entry = "main.bend" [tools] [tools.bolt] git = "https://github.com/Emerging-Patterns/bolt" -rev = "02fb09377f5c0fbddb5f6b7c32c8ab4ae14240df" -tag = "v1.8.0" +rev = "d5a67600a96ba423f2212bd661a30c1fba38eb55" +tag = "v1.9.0" root = "." -narHash = "sha256-53zE+3lZ/jn9GvIeGoavvNMaFyUs5dEFWd7fwP49TlM=" +narHash = "sha256-HmJ8J1xDshBdSWXIiEp48GZ9qHsm+bmpHw06ZWwcDVE=" diff --git a/ez/LAWS.bend b/ez/LAWS.bend index dc6236a..db715f2 100644 --- a/ez/LAWS.bend +++ b/ez/LAWS.bend @@ -23,7 +23,7 @@ import ../ez/line.bend as L import ../ez/ends.bend as E import ../ez/start.bend as S import ../lock/plan.bend as LP -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R # quiet: bend's chatter is not the program's output @@ -207,7 +207,7 @@ law key_rev_differs: for +f1: String for +b1: String for e: {False{} == String.eq(r0, r1) : Bool} - {K.reuse(K.Key{r0, f0, b0}, K.Key{r1, f1, b1}) == False{} : Bool} + {K.reuse(K.Stamp{r0, f0, b0}, K.Stamp{r1, f1, b1}) == False{} : Bool} # LAW: a binary built from another file is built again, so a pin's `bin` or # `entry` and a free run of the same commit do not share one @@ -220,7 +220,7 @@ law key_file_differs: for +f1: String for +b1: String for e: {False{} == String.eq(f0, f1) : Bool} - {K.reuse(K.Key{r0, f0, b0}, K.Key{r1, f1, b1}) == False{} : Bool} + {K.reuse(K.Stamp{r0, f0, b0}, K.Stamp{r1, f1, b1}) == False{} : Bool} # LAW: a binary another bend built is built again # EZ-TOOL-2 @@ -232,15 +232,15 @@ law key_bend_differs: for +f1: String for +b1: String for e: {False{} == String.eq(b0, b1) : Bool} - {K.reuse(K.Key{r0, f0, b0}, K.Key{r1, f1, b1}) == False{} : Bool} + {K.reuse(K.Stamp{r0, f0, b0}, K.Stamp{r1, f1, b1}) == False{} : Bool} # LAW: with no commit, whatever was recorded, the binary is built again # EZ-TOOL-2 law key_no_rev: - for was: K.Key + for was: K.Stamp for +f: String for +b: String - {K.reuse(was, K.Key{"", f, b}) == False{} : Bool} + {K.reuse(was, K.Stamp{"", f, b}) == False{} : Bool} # LAW: a record that did not read, such as one written before the file and # the bend were recorded, reuses nothing @@ -249,7 +249,7 @@ law key_none_misses: for +f: String for +b: String for e: {False{} == String.is_empty(r) : Bool} - {K.reuse(K.none(), K.Key{r, f, b}) == False{} : Bool} + {K.reuse(K.none(), K.Stamp{r, f, b}) == False{} : Bool} # LAW: the same commit, file and bend reuse the binary # EZ-TOOL-2 @@ -258,7 +258,7 @@ law key_same_reuses: for +f: String for +b: String for e: {False{} == String.is_empty(r) : Bool} - {K.reuse(K.Key{r, f, b}, K.Key{r, f, b}) == True{} : Bool} + {K.reuse(K.Stamp{r, f, b}, K.Stamp{r, f, b}) == True{} : Bool} # LAW: a checkout of another commit is cloned again. The file and the bend # are not asked. diff --git a/ez/PROOF.bend b/ez/PROOF.bend index aa5fdbc..f971cd6 100644 --- a/ez/PROOF.bend +++ b/ez/PROOF.bend @@ -20,7 +20,7 @@ import ../ez/line.bend as L import ../ez/ends.bend as E import ../ez/start.bend as S import ../lock/plan.bend as LP -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../check/eq.bend as Eq import ./LAWS.bend as Laws @@ -1208,7 +1208,7 @@ def Laws.key_bend_differs(r0, f0, _b0, r1, f1, _b1, e): # the empty commit computes, and the `and` stops at it whatever was recorded def Laws.key_no_rev(was, _f, _b): match was: - case K.Key{_r0, _f0, _b0}: + case K.Stamp{_r0, _f0, _b0}: {==} # the resolved commit has a first char, so the empty one on record is not @@ -1216,7 +1216,7 @@ def Laws.key_no_rev(was, _f, _b): def Laws.key_none_misses(r, f, b, e): match r: case SNil{}: - Eq.bit.absurd(&2, {K.reuse(K.none(), K.Key{"", f, b}) == False{} : Bool}, + Eq.bit.absurd(&2, {K.reuse(K.none(), K.Stamp{"", f, b}) == False{} : Bool}, e) case SCon{_h, _t}: {==} diff --git a/ez/cache.bend b/ez/cache.bend index 4ebc7ac..76609fa 100644 --- a/ez/cache.bend +++ b/ez/cache.bend @@ -3,7 +3,7 @@ # name. `tests/fresh.bend` records it beside a built `bin/ez.bin` and holds the # binary to it. import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../run/bend.bend as Bend import ../ez/env.bend as Env diff --git a/ez/cap.bend b/ez/cap.bend index 9bf4425..fefbd89 100644 --- a/ez/cap.bend +++ b/ez/cap.bend @@ -7,7 +7,7 @@ # kills for memory looks exactly like one that succeeded and happened to write # no binary. The cap is what turns that into a legible exit 137. import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../ez/env.bend as Env import ../ez/args.bend as Args @@ -27,7 +27,7 @@ def gb() -> IO(String): # fails when the program is absent, and it fails when the program is present # and the user bus is not. Either failure is no cap. A probe that would # wait on a password fails closed instead. -def ok() -> IO(Bool): +def ready() -> IO(Bool): do IO: +out : String <- R.exec(["systemd-run", "--user", "--scope", "-q", "--collect", "--no-ask-password", "true"]) diff --git a/ez/clock.bend b/ez/clock.bend index 2a337d2..4bbdc7e 100644 --- a/ez/clock.bend +++ b/ez/clock.bend @@ -11,7 +11,7 @@ # programs ez already runs the way it runs `find` and `mkdir`, with no shell # between. import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../ez/env.bend as Env # how many seconds a whole run may take. Five minutes is what the gate is held diff --git a/ez/cmd.bend b/ez/cmd.bend index 573ed8c..f7bd5d5 100644 --- a/ez/cmd.bend +++ b/ez/cmd.bend @@ -3,7 +3,7 @@ # Base has neither mkdir nor readdir: snap's `exec` for a program whose answer # ez reads, and `ez/pass.bend` for the one `ez run` hands the terminal to. import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../io/file.bend as F import ../lock/run.bend as Run import ../lock/plan.bend as P @@ -94,7 +94,7 @@ def build.go(start: S.Start, +out: String) -> IO(Unit): case S.Starts{line}: do IO: Env.make(Env.dirs("build", out)) - +cap : Bool <- Cap.ok() + +cap : Bool <- Cap.ready() Cap.warn(cap) +g : String <- Cap.gb() +bin : String <- Cap.run(cap, line) diff --git a/ez/ends.bend b/ez/ends.bend index 614e0ab..fdcaf0b 100644 --- a/ez/ends.bend +++ b/ez/ends.bend @@ -6,7 +6,7 @@ # That the answer is what bend printed is EZ-TRUST-2. `ez run` reads no # answer: it exits with the program's own status (`code` in ez/start.bend). import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../lock/plan.bend as P # a command that ends on whether it passed: success, or a refusal whose diff --git a/ez/env.bend b/ez/env.bend index e0dbbe9..3286c61 100644 --- a/ez/env.bend +++ b/ez/env.bend @@ -5,7 +5,7 @@ # of the command as `env BEND_LIB=... bend ...`. `env` is coreutils and is # execvp'd like any other program, so no shell is involved. import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../ez/args.bend as Args # a value, or the fallback when the variable was unset or empty diff --git a/ez/key.bend b/ez/key.bend index 49eb335..5847ef9 100644 --- a/ez/key.bend +++ b/ez/key.bend @@ -6,40 +6,40 @@ import Base # the commit, the file handed to bend, and the bend that built it -type Key is Data: - Key{rev: String, file: String, bend: String} +type Stamp is Data: + Stamp{rev: String, file: String, bend: String} # the record that matches nothing: an empty commit is never reused -def none() -> Key: - Key{"", "", ""} +def none() -> Stamp: + Stamp{"", "", ""} # the record as it is written, one field to a line -def show(key: Key) -> String: +def show(key: Stamp) -> String: match key: - case Key{+r, +f, +b}: + case Stamp{+r, +f, +b}: r ++ "\n" ++ f ++ "\n" ++ b ++ "\n" # exactly three lines, or no record. A cache written before the file and the # bend were recorded holds the commit alone, and that reads as no record. -def read.third(+rev: String, +file: String, ls: List<&2, String>) -> Key: +def read.third(+rev: String, +file: String, ls: List<&2, String>) -> Stamp: match ls: case []: none() case +b <> t: match t: case []: - Key{rev, file, b} + Stamp{rev, file, b} case _h <> _t: none() -def read.second(+rev: String, ls: List<&2, String>) -> Key: +def read.second(+rev: String, ls: List<&2, String>) -> Stamp: match ls: case []: none() case +f <> t: read.third(rev, f, t) -def read.lines(ls: List<&2, String>) -> Key: +def read.lines(ls: List<&2, String>) -> Stamp: match ls: case []: none() @@ -47,7 +47,7 @@ def read.lines(ls: List<&2, String>) -> Key: read.second(r, t) # a record's text, as `show` wrote it and a file read trimmed it -def read(+text: String) -> Key: +def read(+text: String) -> Stamp: read.lines(String.split(text, '\n')) # the checkout is this commit, and there is a commit at all. The checkout's @@ -57,11 +57,11 @@ def checkout(+was: String, +now: String) -> Bool: # the three fields the same, and a commit at all. An empty commit is a dirty # tree or a directory that is not a checkout, and those are built every time. -def reuse(was: Key, now: Key) -> Bool: +def reuse(was: Stamp, now: Stamp) -> Bool: match was: - case Key{+r0, +f0, +b0}: + case Stamp{+r0, +f0, +b0}: match now: - case Key{+r1, +f1, +b1}: + case Stamp{+r1, +f1, +b1}: Bool.and(Bool.not(String.is_empty(r1)), Bool.and(String.eq(r0, r1), Bool.and(String.eq(f0, f1), String.eq(b0, b1)))) diff --git a/ez/main.bend b/ez/main.bend index d5376db..02dba35 100644 --- a/ez/main.bend +++ b/ez/main.bend @@ -5,7 +5,7 @@ # prints and exits as they say and runs the command, which is trusted under # EZ-TRUST-2. `IO.args()` is copied so each word can be read more than once. # Build it -# native (`bend ez/main.bend -o bin/ez.bin`); interpreted, bend's own CLI +# native (`bend ez.bend -o bin/ez.bin`); interpreted, bend's own CLI # would take the flags meant for ez. import Base import 0x085b03c84ca37125e38dddede7b91e55/main.bend as Shake diff --git a/ez/pass.bend b/ez/pass.bend index c40abad..a49c685 100644 --- a/ez/pass.bend +++ b/ez/pass.bend @@ -6,7 +6,7 @@ # the person, and ez only waits for it and exits with its status (`S.code` # and `TP.code`, EZ-OUT-1). import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R # the program and its arguments, newline separated, run with no shell between # and nothing captured. The answer is the status it exited with: 128 plus the diff --git a/ez/pass.c b/ez/pass.c index 9479043..05eef86 100644 --- a/ez/pass.c +++ b/ez/pass.c @@ -56,5 +56,5 @@ Term ezpass_run_run(Env e, Term* f, IoWork* w) { } static void __attribute__((constructor)) ezpass_run_use(void) { - io_eff(CID_EZPASS_RUN, ezpass_run_run, 0); + io_eff(CID(ezpass.run), ezpass_run_run, 0); } diff --git a/ez/pass.js b/ez/pass.js index 710c43a..6e19b48 100644 --- a/ez/pass.js +++ b/ez/pass.js @@ -13,3 +13,5 @@ function ezpass_run(cmd) { } return r.status; } + +io_eff(CID(ezpass.run), ezpass_run); diff --git a/ez/prove.bend b/ez/prove.bend index 665bfa0..b96033b 100644 --- a/ez/prove.bend +++ b/ez/prove.bend @@ -1,7 +1,8 @@ -# ez/prove: the proof gate. Every PROOF.bend in the tree is run through `bend`, -# all of them at once, and a proof passes only when the first line bend prints -# is exactly `All terms check.` Nothing is cached: a gate CI leans on answers -# for the tree in front of it, not for one it saw before. +# ez/prove: the proof gate. Every PROOF.bend in the tree is imported by a file +# above the tree and that file is run through `bend`, all of them at once, and +# a proof passes only when the first line bend prints is exactly `All terms +# check.` Nothing is cached: a gate CI leans on answers for the tree in front +# of it, not for one it saw before. # # The line is the verdict, never the exit status. Both # `All terms check, with N unsafe annotations.` and 2.0.18's @@ -9,7 +10,7 @@ # gate reading the status alone goes green on a claim that leans on code # nothing proved. Only the bare line means every term was proved outright. import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../ez/args.bend as Args import ../ez/env.bend as Env import ../ez/cap.bend as Cap @@ -17,6 +18,7 @@ import ./quiet.bend as Q import ./sorted.bend as Sort import ../ez/ends.bend as E import ../lock/run.bend as Run +import ../io/file.bend as F # every file of a kind in the tree, sorted, so a run's report is the same twice # over. Base has no readdir, so this is `find`. `.claude` is skipped along with @@ -52,6 +54,60 @@ def fresh.dir(+at: String) -> IO(Unit): def out.at() -> String: ".ez/run/prove" +# where a proof is started from. Bend 2.0.28 names a file from the program +# that starts it, and a start inside the tree gives one file two names. Each +# proof is imported by a file here, above the tree, and that file is what +# bend runs. +def entry.dir() -> String: + ".ez/prove-entry" + +# `./sha/PROOF.bend` without the `./` find puts on the front +def drop.dot(+path: String) -> String: + Bool.pick(String, String.starts_with(path, "./"), String.drop(path, 2n), path) + +# one character of a path, `/` written as `_` +def us.ch(slash: Bool, ch: Char) -> Char: + match slash: + case True{}: + '_' + case False{}: + ch + +# `/` written as `_`, so a path is one file name +def us.slash(text: String) -> String: + match text: + case SNil{}: + "" + case SCon{+h, t}: + SCon{us.ch(Char.is_eq(h, '/'), h), us.slash(t)} + +# the file bend starts for one proof +def shim.at(+path: String) -> String: + entry.dir() ++ "/" ++ us.slash(drop.dot(path)) + +# a program whose only import is the proof. It defines no main, so bend +# prints the check line and stops, which is the line the gate reads. +def shim.text(+path: String) -> String: + "import Base\nimport ../../" ++ drop.dot(path) ++ " as P\n" + +# that file written, and its path +def lay.one(+path: String) -> IO(String): + do IO: + +at : String <- IO.pure(String, shim.at(path)) + _w : Bool <- F.write(at, shim.text(path)) + return at + +# one start file for every proof, in the tree's order +def lay(ps: List<&2, String>) -> IO(List<&2, String>): + match ps: + case Nil{}: + IO.pure(List<&2, String>, Nil{}) + case Con{+h, t}: + do IO>: + at : String <- lay.one(h) + rest : List<&2, String> <- lay(t) + return at <> rest + # the first line of a run's output def head.of(ls: List<&2, String>) -> String: match ls: @@ -153,13 +209,15 @@ def done(+passed: Nat, +total: Nat) -> IO(Unit): # and one that never finishes is stopped by whatever runs the gate. def run() -> IO(Unit): do IO: - +cap : Bool <- Cap.ok() + +cap : Bool <- Cap.ready() Cap.warn(cap) +g : String <- Cap.gb() +at : String <- Env.lib() +jobs : String <- width() +ps : List<&2, String> <- find.proofs() fresh.dir(out.at()) - as : List<&2, String> <- R.par(cmds(ps, cap, g, at), jobs, g, out.at(), "0") + fresh.dir(entry.dir()) + +shims : List<&2, String> <- lay(ps) + as : List<&2, String> <- R.par(cmds(shims, cap, g, at), jobs, g, out.at(), "0") +passed : Nat <- report(ps, as, g, 0n) done(passed, List.length(&2, String, ps)) diff --git a/ez/say.bend b/ez/say.bend index 21dbe1c..8a7d123 100644 --- a/ez/say.bend +++ b/ez/say.bend @@ -10,7 +10,7 @@ # already has. A pipe is not a terminal: the line is printed once and left, # which is what a log wants. import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../pkg/path.bend as P # a spinner that is running, or none. An empty pid means the line was already diff --git a/ez/test.bend b/ez/test.bend index 59838cb..8be33ec 100644 --- a/ez/test.bend +++ b/ez/test.bend @@ -7,7 +7,7 @@ # # Tests are not the proof gate. `ez prove` is, and nothing here runs a proof. import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../io/file.bend as F import ../ez/env.bend as Env import ../ez/cap.bend as Cap @@ -122,7 +122,7 @@ def budget(late: Bool, +secs: String, score: Tally) -> IO(Tally): # the jobs finished in. def run() -> IO(Unit): do IO: - +cap : Bool <- Cap.ok() + +cap : Bool <- Cap.ready() Cap.warn(cap) +secs : String <- Clock.seconds() +deadline : String <- Clock.start(secs) diff --git a/fetch/LAWS.bend b/fetch/LAWS.bend index fa3d45a..bfb32f0 100644 --- a/fetch/LAWS.bend +++ b/fetch/LAWS.bend @@ -139,7 +139,7 @@ law fetch_weighs_the_checkout: # (`fetch_refusal_writes_nothing`). # EZ-FETCH-1 law fetch_refuses_unweighed: - for +fs: List<&2, K.File> + for +fs: List<&2, K.Member> for +h: String for +why: String for ls: List<&2, W.Source> diff --git a/fetch/PROOF.bend b/fetch/PROOF.bend index 0d47264..c608f07 100644 --- a/fetch/PROOF.bend +++ b/fetch/PROOF.bend @@ -280,14 +280,14 @@ def Laws.fetch_lays_the_lock(w): # LAW: the planner weighs a file the way the law vocabulary does law weighs_same: for ls: List<&2, W.Source> - {FP.weighs(ls) == W.weighs(ls) : List<&2, K.File>} + {FP.weighs(ls) == W.weighs(ls) : List<&2, K.Member>} def weighs_same(ls): match ls: case []: {==} case W.Source{at, text} <> t: - Equal.cong(List<&2, K.File>, List<&2, K.File>, ys => K.File{at, Sha.hex(text)} <> ys, + Equal.cong(List<&2, K.Member>, List<&2, K.Member>, ys => K.Member{at, Sha.hex(text)} <> ys, FP.weighs(t), W.weighs(t), weighs_same(t)) law named_seal: @@ -307,7 +307,7 @@ def named_seal(_es, o, e): # it law named_got: for b: Bool - for +fs: List<&2, K.File> + for +fs: List<&2, K.Member> for +h: String for +ls: List<&2, W.Source> for rest: List<&2, P.Effect> @@ -350,7 +350,7 @@ def named_got(b, fs, h, ls, rest, g, e): e law named_one: - for +fs: List<&2, K.File> + for +fs: List<&2, K.Member> for +h: String for p: FP.Part for rest: List<&2, P.Effect> @@ -744,7 +744,7 @@ law weighed_good: for +ss: List<&2, T.Sect> for +rs: List<&2, F.Reply> for +here: String - for +fs: List<&2, K.File> + for +fs: List<&2, K.Member> for +h: String for +ls: List<&2, W.Source> for rest: List<&2, P.Effect> @@ -768,7 +768,7 @@ law weighed_got: for +ss: List<&2, T.Sect> for +rs: List<&2, F.Reply> for +here: String - for +fs: List<&2, K.File> + for +fs: List<&2, K.Member> for +h: String for +ls: List<&2, W.Source> for rest: List<&2, P.Effect> @@ -790,7 +790,7 @@ law weighed_one: for +ss: List<&2, T.Sect> for +rs: List<&2, F.Reply> for +here: String - for +fs: List<&2, K.File> + for +fs: List<&2, K.Member> for +h: String for p: FP.Part for rest: List<&2, P.Effect> @@ -944,7 +944,7 @@ def Laws.fetch_weighs_the_checkout(ss, rs, here, h, url, rev, entry, root, nar, # LAW: a reason that is not empty stops the package with it law unweighed_stops: for k: Bool - for +fs: List<&2, K.File> + for +fs: List<&2, K.Member> for +h: String for +why: String for ls: List<&2, W.Source> diff --git a/fetch/plan.bend b/fetch/plan.bend index 7bae334..80d402a 100644 --- a/fetch/plan.bend +++ b/fetch/plan.bend @@ -74,7 +74,7 @@ type Tree is Data: Gone{why: String} # the files a manifest names, each with the text read for it -def zip(fs: List<&2, K.File>, ss: List<&2, String>) -> List<&2, K.Source>: +def zip(fs: List<&2, K.Member>, ss: List<&2, String>) -> List<&2, K.Source>: match fs ss: case Nil{} Nil{}: [] @@ -132,23 +132,23 @@ def key(+root: String, +at: String) -> String: # every file the lock names, with the text the tree has at its path. A file # the tree does not have is taken as empty, which does not match the lock # unless the lock records an empty file. -def cand(fs: List<&2, K.File>, +root: String, +tree: List<&2, K.Source>) -> List<&2, W.Source>: +def cand(fs: List<&2, K.Member>, +root: String, +tree: List<&2, K.Source>) -> List<&2, W.Source>: match fs: case []: [] - case K.File{+at, _sum} <> t: + case K.Member{+at, _sum} <> t: W.Source{at, text.or(K.look(tree, key(root, at)))} <> cand(t, root, tree) # --------------------------------------------------------------------------- # the checks # a file laid, weighed by its own text -def weigh(src: W.Source) -> K.File: +def weigh(src: W.Source) -> K.Member: W.Source{at, +text} = src - K.File{at, Sha.hex(text)} + K.Member{at, Sha.hex(text)} # every file laid, weighed by its own text -def weighs(ls: List<&2, W.Source>) -> List<&2, K.File>: +def weighs(ls: List<&2, W.Source>) -> List<&2, K.Member>: match ls: case []: [] @@ -157,14 +157,14 @@ def weighs(ls: List<&2, W.Source>) -> List<&2, K.File>: # whether one file is the one the lock names: the same path, and a text whose # digest is the sum the lock records -def fit(want: K.File, got: W.Source) -> Bool: - K.File{+at, sum} = want +def fit(want: K.Member, got: W.Source) -> Bool: + K.Member{+at, sum} = want W.Source{lat, +text} = got Bool.and(String.eq(lat, at), String.eq(Sha.hex(text), sum)) # whether every file is the one the lock names, in the lock's order. A list # longer or shorter than the lock's is not the package. -def fits(fs: List<&2, K.File>, ls: List<&2, W.Source>) -> Bool: +def fits(fs: List<&2, K.Member>, ls: List<&2, W.Source>) -> Bool: match fs ls: case Nil{} Nil{}: True{} @@ -203,7 +203,7 @@ def named(+ls: List<&2, W.Source>) -> String: # whether a package may be laid: every file is the one the lock names, no # path leaves the tree, and the files hash to the name the lock records them # under, so the tree laid under that name is that name's -def good(fs: List<&2, K.File>, +hash: String, +ls: List<&2, W.Source>) -> Bool: +def good(fs: List<&2, K.Member>, +hash: String, +ls: List<&2, W.Source>) -> Bool: +fit = fits(fs, ls) +safe = paths.safe(ls) Bool.and(fit, Bool.and(safe, String.eq(hash, named(ls)))) @@ -218,7 +218,7 @@ def unfit.pick(ok: Bool, +at: String, rest: String) -> String: at # the first path that does not fit, "" when every file does -def unfit(fs: List<&2, K.File>, ls: List<&2, W.Source>) -> String: +def unfit(fs: List<&2, K.Member>, ls: List<&2, W.Source>) -> String: match fs ls: case Nil{} Nil{}: "" @@ -231,7 +231,7 @@ def unfit(fs: List<&2, K.File>, ls: List<&2, W.Source>) -> String: unfit.pick(fit(f, l), K.file.at(f), unfit(g, m)) # why a package may not be laid, naming it -def bad.why(fs: List<&2, K.File>, +hash: String, +ls: List<&2, W.Source>) -> String: +def bad.why(fs: List<&2, K.Member>, +hash: String, +ls: List<&2, W.Source>) -> String: +at = unfit(fs, ls) Bool.pick(String, String.is_empty(at), Bool.pick(String, paths.safe(ls), @@ -253,7 +253,7 @@ type Part is Data: No{why: String} # the files that arrived for a package, or why none did -def part.tree(tree: Tree, fs: List<&2, K.File>) -> Part: +def part.tree(tree: Tree, fs: List<&2, K.Member>) -> Part: match tree: case Tree{r, files}: Got{cand(fs, r, files)} @@ -261,7 +261,7 @@ def part.tree(tree: Tree, fs: List<&2, K.File>) -> Part: No{why} # a package fetched, once it is answered -def part.fetch.heard(got: F.Heard, fs: List<&2, K.File>, +root: String) -> Part: +def part.fetch.heard(got: F.Heard, fs: List<&2, K.Member>, +root: String) -> Part: match got: case F.Open{}: AskFetch{} @@ -272,7 +272,7 @@ def part.fetch.heard(got: F.Heard, fs: List<&2, K.File>, +root: String) -> Part: def part.fetch( +rs: List<&2, F.Reply>, +src: L.Src, - fs: List<&2, K.File>, + fs: List<&2, K.Member>, +here: String, +hub: String, +hash: String @@ -284,7 +284,7 @@ def part.kept( ok: Bool, +rs: List<&2, F.Reply>, +src: L.Src, - fs: List<&2, K.File>, + fs: List<&2, K.Member>, +here: String, +hub: String, +hash: String @@ -301,7 +301,7 @@ def part.found( tree: Tree, +rs: List<&2, F.Reply>, +src: L.Src, - +fs: List<&2, K.File>, + +fs: List<&2, K.Member>, +here: String, +hub: String, +hash: String @@ -317,7 +317,7 @@ def part.laid( got: F.Heard, +rs: List<&2, F.Reply>, +src: L.Src, - +fs: List<&2, K.File>, + +fs: List<&2, K.Member>, +here: String, +hub: String, +hash: String @@ -332,7 +332,7 @@ def part.laid( def part( +rs: List<&2, F.Reply>, +src: L.Src, - +fs: List<&2, K.File>, + +fs: List<&2, K.Member>, +here: String, +hub: String, +hash: String @@ -434,7 +434,7 @@ def weigh.part(+why: String, part: Part) -> Part: # one package of the lock, and where it stands type Pt is Data: - Pt{hash: String, src: L.Src, files: List<&2, K.File>, part: Part} + Pt{hash: String, src: L.Src, files: List<&2, K.Member>, part: Part} # every package of the lock, and where each stands def parts( @@ -599,7 +599,7 @@ type Verdict is Data: Stop{why: String} # the files that arrived, laid when they pass -def judge.got(ok: Bool, fs: List<&2, K.File>, +hash: String, +ls: List<&2, W.Source>) -> Verdict: +def judge.got(ok: Bool, fs: List<&2, K.Member>, +hash: String, +ls: List<&2, W.Source>) -> Verdict: match ok: case True{}: Put{hash, ls} @@ -607,7 +607,7 @@ def judge.got(ok: Bool, fs: List<&2, K.File>, +hash: String, +ls: List<&2, W.Sou Stop{bad.why(fs, hash, ls)} # what one package comes to, where it stands -def judge(+fs: List<&2, K.File>, +hash: String, part: Part) -> Verdict: +def judge(+fs: List<&2, K.Member>, +hash: String, part: Part) -> Verdict: match part: case AskLaid{}: Stop{"ez: " ++ hash ++ " was never looked for under BEND_LIB"} @@ -829,7 +829,7 @@ def front(fs: List<&2, W.Source>) -> List<&2, W.Source>: h <> front(h2 <> t2) # the files the lock records under a hash -def locked(+ss: List<&2, T.Sect>, +hash: String) -> List<&2, K.File>: +def locked(+ss: List<&2, T.Sect>, +hash: String) -> List<&2, K.Member>: L.pack.files(L.pack_of(ss, hash)) # whether an effect that lays a tree lays the files the lock records under diff --git a/fetch/run.bend b/fetch/run.bend index 3c53687..4ddde3e 100644 --- a/fetch/run.bend +++ b/fetch/run.bend @@ -14,7 +14,7 @@ # BEND_LIB as it found it. It decides nothing; that it reads and executes # faithfully is EZ-TRUST-2. import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../io/file.bend as F import ../lock/run.bend as Run import ../lock/world.bend as W diff --git a/flake.lock b/flake.lock index 8e2d1c9..3a5e0b5 100644 --- a/flake.lock +++ b/flake.lock @@ -7,16 +7,17 @@ ] }, "locked": { - "lastModified": 1790200275, - "narHash": "sha256-huYLnKbMUukFhFLypIXx/wLVU3EmgsUEe9l67mU6CDw=", + "lastModified": 1790482124, + "narHash": "sha256-Gv309ikt48M8cISbwSo6V0md2572iieIRiyl3noF1cA=", "owner": "bendlang", "repo": "bend", - "rev": "d37909174ebd664338ae3194799a9e0899dedd51", + "rev": "af569d4826913b2ce3557e9829ccad31fcf86f94", "type": "github" }, "original": { "owner": "bendlang", "repo": "bend", + "rev": "af569d4826913b2ce3557e9829ccad31fcf86f94", "type": "github" } }, diff --git a/flake.nix b/flake.nix index 9c89b55..a6696e8 100644 --- a/flake.nix +++ b/flake.nix @@ -6,7 +6,9 @@ inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable"; inputs.bend = { - url = "github:bendlang/bend"; + # The v2.0.31 tag's flake still fetches the 2.0.30 archive. This commit + # is the flake that names 2.0.31. + url = "github:bendlang/bend/af569d4826913b2ce3557e9829ccad31fcf86f94"; inputs.nixpkgs.follows = "nixpkgs"; }; diff --git a/git/git.bend b/git/git.bend index 215565f..3cf56bc 100644 --- a/git/git.bend +++ b/git/git.bend @@ -11,7 +11,7 @@ # process effect the rest of ez uses: arguments execvp'd, no shell between. import Base import ../io/file.bend as F -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../toml/toml.bend as T import ../ledger/manifest.bend as M import ../pkg/pkg.bend as K diff --git a/hub/hub.bend b/hub/hub.bend index 9138d53..4d2c16b 100644 --- a/hub/hub.bend +++ b/hub/hub.bend @@ -2,11 +2,11 @@ # it. bend accepts any prefix of the sha256, and a package's `0x` name is the # first 32 characters of its manifest's digest, so the check is a prefix test. import Base -import 0x0a372da4a053652f70ded7d6e0d19330/main.bend as Http -import 0x0a372da4a053652f70ded7d6e0d19330/client.bend as Client -import 0x0a372da4a053652f70ded7d6e0d19330/url.bend as Url -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R -import ../io/file.bend as File +import 0x5e4e2a9db839a0214ace6923b04b685b/main.bend as Http +import 0x5e4e2a9db839a0214ace6923b04b685b/client.bend as Client +import 0x5e4e2a9db839a0214ace6923b04b685b/url.bend as Url +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R +import ../io/file.bend as Disk import ../sha/sha.bend as Sha # The GET is ezhttp's. What is kept here is the answer's shape: a status on @@ -48,7 +48,7 @@ def get.file.got(got: Maybe<&2, String>, path: String) -> String: # a file url read off the disk def get.file(+path: String) -> IO(String): do IO: - m : Maybe<&2, String> <- File.read(path) + m : Maybe<&2, String> <- Disk.read(path) return get.file.got(m, path) # a url whose scheme decides where the body comes from diff --git a/ledger/LAWS.bend b/ledger/LAWS.bend index ddeddb5..2354316 100644 --- a/ledger/LAWS.bend +++ b/ledger/LAWS.bend @@ -14,7 +14,7 @@ import ../check/str.bend as Str # written to: every ledger `R.renderable` accepts reads back, from the text # `R.show` writes, as itself. `R.show` is eztoml's `render` of the document ez # assembles (`R.text`), and `M.parse` reads through eztoml's `parse`, so this -# rests on eztoml's round trip (TOML-RT-1, pending in eztoml v0.4.0) and is +# rests on eztoml's round trip (TOML-RT-1, proved in eztoml v0.5.0) and is # trusted as EZ-TRUST-8, not proved here. A law that takes it holds of the # file's bytes wherever the round trip does. def ReadsBack() -> Type: diff --git a/lock/LAWS.bend b/lock/LAWS.bend index 19b326d..fe82930 100644 --- a/lock/LAWS.bend +++ b/lock/LAWS.bend @@ -13,7 +13,6 @@ import ../toml/toml.bend as T import ../pkg/pkg.bend as K import ../pkg/LAWS.bend as KL import ../hub/hub.bend as Web -import ../ledger/upgrade.bend as U import ../ledger/ignore.bend as I import ../ledger/LAWS.bend as ML import ../check/str.bend as Str @@ -173,10 +172,10 @@ law pack_order_free: for +ns: List<&2, Nat> for +hash: String for +src: L.Src - for +fs: List<&2, K.File> + for +fs: List<&2, K.Member> for dis: {KL.distinct(fs) == True{} : Bool} {L.pack.block(L.Pack{hash, src, KL.perm(ns, fs)}) - == L.pack.block(L.Pack{hash, src, fs}) : K.File} + == L.pack.block(L.Pack{hash, src, fs}) : K.Member} # LAW: a lock with no tools is the lock `render` writes. Packages do not # move because a tool list was empty. @@ -198,12 +197,12 @@ law path_eq_unlockable: for +src: L.Src for +at: String for +sum: String - for +fs: List<&2, K.File> + for +fs: List<&2, K.Member> for +rest: List<&2, L.Pack> for +ts: List<&2, M.Tool> for +hub: String for e: {False{} == P.path.eqless(at) : Bool} - {P.lockable(L.Pack{hash, src, K.File{at, sum} <> fs} <> rest, ts, hub) == False{} + {P.lockable(L.Pack{hash, src, K.Member{at, sum} <> fs} <> rest, ts, hub) == False{} : Bool} # LAW: and the refusal names the package and the path, so the author knows @@ -213,10 +212,10 @@ law path_eq_named: for +src: L.Src for +at: String for +sum: String - for +fs: List<&2, K.File> + for +fs: List<&2, K.Member> for +rest: List<&2, L.Pack> for +e: {False{} == P.path.eqless(at) : Bool} - {P.lockable.why(L.Pack{hash, src, K.File{at, sum} <> fs} <> rest) + {P.lockable.why(L.Pack{hash, src, K.Member{at, sum} <> fs} <> rest) == P.path.eq.why(hash, at) : String} # The planner (plan.bend) over the World (world.bend). Every law below is @@ -1045,12 +1044,12 @@ def lock.doc(nms: List<&2, L.Name>, ts: List<&2, M.Tool>, hub: String, ps: List< List.append(&2, T.Sect, L.doc(hub, ps), tail(nms, ts)) # a name as a lock gives it back, from the pair it is written as -def name.back(item: K.File) -> L.Name: - K.File{at, sum} = item +def name.back(item: K.Member) -> L.Name: + K.Member{at, sum} = item L.Name{at, sum} # every name, so -def names.back(fs: List<&2, K.File>) -> List<&2, L.Name>: +def names.back(fs: List<&2, K.Member>) -> List<&2, L.Name>: match fs: case []: [] @@ -1059,12 +1058,12 @@ def names.back(fs: List<&2, K.File>) -> List<&2, L.Name>: # a name as a file of a package: its `@` as the path and its # hash as the sum. Law vocabulary. -def name.as.file(nm: L.Name) -> K.File: +def name.as.file(nm: L.Name) -> K.Member: L.Name{nv, hash} = nm - K.File{nv, hash} + K.Member{nv, hash} # every name, so. Law vocabulary. -def names.as.files(nms: List<&2, L.Name>) -> List<&2, K.File>: +def names.as.files(nms: List<&2, L.Name>) -> List<&2, K.Member>: match nms: case []: [] @@ -1660,7 +1659,7 @@ law git_named_without_license: for +ss: List<&2, String> for unnamed: {False{} == Web.matches(L.want(hash), manifest) : Bool} {W.git.weighed("", hash, manifest, ss) - == W.git.body(List.is_empty(&2, K.File, K.bare(L.manifest.files(String.lines(manifest)))), + == W.git.body(List.is_empty(&2, K.Member, K.bare(L.manifest.files(String.lines(manifest)))), hash, K.manifest.lines(K.bare(L.manifest.files(String.lines(manifest)))), K.bare.srcs(L.manifest.files(String.lines(manifest)), ss)) : W.Verdict} diff --git a/lock/PROOF.bend b/lock/PROOF.bend index 2a86e0e..96c9088 100644 --- a/lock/PROOF.bend +++ b/lock/PROOF.bend @@ -76,7 +76,7 @@ law blocks_ins_at: for +x: L.Pack for +ps: List<&2, L.Pack> {L.pack.blocks(Laws.perm.ins_at(n, x, ps)) - == KL.perm.ins_at(n, L.pack.block(x), L.pack.blocks(ps)) : List<&2, K.File>} + == KL.perm.ins_at(n, L.pack.block(x), L.pack.blocks(ps)) : List<&2, K.Member>} def blocks_ins_at(n, x, ps): match n ps: @@ -85,7 +85,7 @@ def blocks_ins_at(n, x, ps): case 1n+p Nil{}: {==} case 1n+p Con{+h, +t}: - Equal.cong(List<&2, K.File>, List<&2, K.File>, + Equal.cong(List<&2, K.Member>, List<&2, K.Member>, bs => L.pack.block(h) <> bs, L.pack.blocks(Laws.perm.ins_at(p, x, t)), KL.perm.ins_at(p, L.pack.block(x), L.pack.blocks(t)), @@ -96,7 +96,7 @@ law blocks_perm: for +ns: List<&2, Nat> for +ps: List<&2, L.Pack> {L.pack.blocks(Laws.perm(ns, ps)) == KL.perm(ns, L.pack.blocks(ps)) - : List<&2, K.File>} + : List<&2, K.Member>} def blocks_perm(ns, ps): match ns ps: @@ -107,12 +107,12 @@ def blocks_perm(ns, ps): case Con{n, ms} Nil{}: {==} case Con{+n, +ms} Con{+h, +t}: - Equal.trans(List<&2, K.File>, + Equal.trans(List<&2, K.Member>, L.pack.blocks(Laws.perm.ins_at(n, h, Laws.perm(ms, t))), KL.perm.ins_at(n, L.pack.block(h), L.pack.blocks(Laws.perm(ms, t))), KL.perm.ins_at(n, L.pack.block(h), KL.perm(ms, L.pack.blocks(t))), blocks_ins_at(n, h, Laws.perm(ms, t)), - Equal.cong(List<&2, K.File>, List<&2, K.File>, + Equal.cong(List<&2, K.Member>, List<&2, K.Member>, bs => KL.perm.ins_at(n, L.pack.block(h), bs), L.pack.blocks(Laws.perm(ms, t)), KL.perm(ms, L.pack.blocks(t)), blocks_perm(ms, t))) @@ -123,7 +123,7 @@ law fresh_blocks: for +x: String for +s: String for +ps: List<&2, L.Pack> - {Laws.hash.fresh(x, ps) == KL.fresh(K.File{x, s}, L.pack.blocks(ps)) : Bool} + {Laws.hash.fresh(x, ps) == KL.fresh(K.Member{x, s}, L.pack.blocks(ps)) : Bool} def fresh_blocks(x, s, ps): match ps: @@ -131,7 +131,7 @@ def fresh_blocks(x, s, ps): {==} case L.Pack{+h, _src, _fs} <> +t: Equal.cong(Bool, Bool, b => Bool.and(Bool.not(String.eq(x, h)), b), - Laws.hash.fresh(x, t), KL.fresh(K.File{x, s}, L.pack.blocks(t)), + Laws.hash.fresh(x, t), KL.fresh(K.Member{x, s}, L.pack.blocks(t)), fresh_blocks(x, s, t)) # LAW: so distinct hashes are distinct block paths @@ -166,14 +166,14 @@ law blocks_sort_perm: for +ps: List<&2, L.Pack> for dis: {Laws.distinct(ps) == True{} : Bool} {K.file.sort(L.pack.blocks(Laws.perm(ns, ps))) == K.file.sort(L.pack.blocks(ps)) - : List<&2, K.File>} + : List<&2, K.Member>} def blocks_sort_perm(ns, ps, dis): - Equal.trans(List<&2, K.File>, + Equal.trans(List<&2, K.Member>, K.file.sort(L.pack.blocks(Laws.perm(ns, ps))), K.file.sort(KL.perm(ns, L.pack.blocks(ps))), K.file.sort(L.pack.blocks(ps)), - Equal.cong(List<&2, K.File>, List<&2, K.File>, bs => K.file.sort(bs), + Equal.cong(List<&2, K.Member>, List<&2, K.Member>, bs => K.file.sort(bs), L.pack.blocks(Laws.perm(ns, ps)), KL.perm(ns, L.pack.blocks(ps)), blocks_perm(ns, ps)), KL.sort_perm(ns, L.pack.blocks(ps), @@ -185,15 +185,15 @@ def blocks_sort_perm(ns, ps, dis): # The text is the sorted blocks under the `[lock]` table and before the # tools, so it follows. def Laws.lock_order_free(ns, nms, ps, ts, hub, dis): - Equal.cong(List<&2, K.File>, String, + Equal.cong(List<&2, K.Member>, String, bs => L.text.of(hub, bs, T.render.all(Laws.tail(nms, ts))), K.file.sort(L.pack.blocks(Laws.perm(ns, ps))), K.file.sort(L.pack.blocks(ps)), blocks_sort_perm(ns, ps, dis)) # A block renders its files sorted, so this is `sort_perm` under the block. def Laws.pack_order_free(ns, hash, src, fs, dis): - Equal.cong(List<&2, K.File>, K.File, - ys => K.File{hash, T.render(L.pack.sects.of(hash, src, K.dedup(ys)))}, + Equal.cong(List<&2, K.Member>, K.Member, + ys => K.Member{hash, T.render(L.pack.sects.of(hash, src, K.dedup(ys)))}, K.file.sort(KL.perm(ns, fs)), K.file.sort(fs), KL.sort_perm(ns, fs, dis)) # LAW: one character before the slash, with the separator test given as @@ -2289,7 +2289,7 @@ def and_false(a): def Laws.path_eq_unlockable(hash, src, at, sum, fs, rest, ts, hub, e): %e : {Bool.and(P.clean(hub), Bool.and(Bool.and(Bool.and(Bool.and(_, P.paths.ok(fs)), Bool.and(P.clean.all(P.pack.values(L.Pack{hash, src, - K.File{at, sum} <> fs})), Bool.not(L.has(rest, hash)))), P.packs.ok(rest)), + K.Member{at, sum} <> fs})), Bool.not(L.has(rest, hash)))), P.packs.ok(rest)), P.tools.ok(ts))) == False{} : Bool} and_false(P.clean(hub)) @@ -2348,25 +2348,25 @@ def eqless_clear(s, e): law blocks_ins.step: for +hp: String for +sp: L.Src - for +fp: List<&2, K.File> + for +fp: List<&2, K.Member> for +hh: String for +sh: L.Src - for +fh: List<&2, K.File> + for +fh: List<&2, K.Member> for +t: List<&2, L.Pack> for b: Bool for ih: {K.file.ins(L.pack.blocks(t), L.pack.block(L.Pack{hp, sp, fp})) - == L.pack.blocks(L.pack.ins(t, L.Pack{hp, sp, fp})) : List<&2, K.File>} + == L.pack.blocks(L.pack.ins(t, L.Pack{hp, sp, fp})) : List<&2, K.Member>} {K.file.ins.put(b, L.pack.block(L.Pack{hp, sp, fp}), L.pack.block(L.Pack{hh, sh, fh}), L.pack.blocks(t), K.file.ins(L.pack.blocks(t), L.pack.block(L.Pack{hp, sp, fp}))) == L.pack.blocks(L.pack.ins.put(b, L.Pack{hp, sp, fp}, L.Pack{hh, sh, fh}, t, - L.pack.ins(t, L.Pack{hp, sp, fp}))) : List<&2, K.File>} + L.pack.ins(t, L.Pack{hp, sp, fp}))) : List<&2, K.Member>} def blocks_ins.step(hp, sp, fp, hh, sh, fh, t, b, ih): match b: case True{}: {==} case False{}: - Equal.cong(List<&2, K.File>, List<&2, K.File>, r => L.pack.block(L.Pack{hh, sh, fh}) <> r, + Equal.cong(List<&2, K.Member>, List<&2, K.Member>, r => L.pack.block(L.Pack{hh, sh, fh}) <> r, K.file.ins(L.pack.blocks(t), L.pack.block(L.Pack{hp, sp, fp})), L.pack.blocks(L.pack.ins(t, L.Pack{hp, sp, fp})), ih) @@ -2376,9 +2376,9 @@ law blocks_ins.cons: for +t: List<&2, L.Pack> for +p: L.Pack for ih: {K.file.ins(L.pack.blocks(t), L.pack.block(p)) - == L.pack.blocks(L.pack.ins(t, p)) : List<&2, K.File>} + == L.pack.blocks(L.pack.ins(t, p)) : List<&2, K.Member>} {K.file.ins(L.pack.blocks(h <> t), L.pack.block(p)) - == L.pack.blocks(L.pack.ins(h <> t, p)) : List<&2, K.File>} + == L.pack.blocks(L.pack.ins(h <> t, p)) : List<&2, K.Member>} def blocks_ins.cons(h, t, p, ih): match h p: @@ -2391,7 +2391,7 @@ law blocks_ins: for +qs: List<&2, L.Pack> for +p: L.Pack {K.file.ins(L.pack.blocks(qs), L.pack.block(p)) == L.pack.blocks(L.pack.ins(qs, p)) - : List<&2, K.File>} + : List<&2, K.Member>} def blocks_ins(qs, p): match qs: @@ -2403,17 +2403,17 @@ def blocks_ins(qs, p): # LAW: the blocks sorted are the blocks of the packages sorted law blocks_sort: for +ps: List<&2, L.Pack> - {K.file.sort(L.pack.blocks(ps)) == L.pack.blocks(L.pack.sort(ps)) : List<&2, K.File>} + {K.file.sort(L.pack.blocks(ps)) == L.pack.blocks(L.pack.sort(ps)) : List<&2, K.Member>} def blocks_sort(ps): match ps: case []: {==} case +h <> +t: - ih = Equal.sym(List<&2, K.File>, K.file.sort(L.pack.blocks(t)), + ih = Equal.sym(List<&2, K.Member>, K.file.sort(L.pack.blocks(t)), L.pack.blocks(L.pack.sort(t)), blocks_sort(t)) %ih : {K.file.ins(_, L.pack.block(h)) == L.pack.blocks(L.pack.sort(h <> t)) - : List<&2, K.File>} + : List<&2, K.Member>} blocks_ins(L.pack.sort(t), h) # LAW: each package's block, joined among what follows, is its two tables @@ -2785,15 +2785,15 @@ def src_read(src): # LAW: a package's files read back from the pairs they are written as law pair_files: - for +fs: List<&2, K.File> - {L.pair.files(L.file.pairs(fs)) == fs : List<&2, K.File>} + for +fs: List<&2, K.Member> + {L.pair.files(L.file.pairs(fs)) == fs : List<&2, K.Member>} def pair_files(fs): match fs: case []: {==} - case K.File{+at, +sum} <> +t: - Equal.cong(List<&2, K.File>, List<&2, K.File>, r => K.File{at, sum} <> r, + case K.Member{+at, +sum} <> +t: + Equal.cong(List<&2, K.Member>, List<&2, K.Member>, r => K.Member{at, sum} <> r, L.pair.files(L.file.pairs(t)), t, pair_files(t)) # LAW: a git tool reads back from the pairs it is written as, as the lock @@ -3377,7 +3377,7 @@ def hash.all(qs: List<&2, L.Pack>) -> List<&2, String>: def pk.src(h: String, s: L.Src) -> T.Sect: T.Sect{pack.name(h, "source"), L.src.pairs(s)} -def pk.files(h: String, f: List<&2, K.File>) -> T.Sect: +def pk.files(h: String, f: List<&2, K.Member>) -> T.Sect: T.Sect{pack.name(h, "files"), L.file.pairs(K.files_of(f))} # the document from its packages' tables on. Proof vocabulary. @@ -3402,28 +3402,28 @@ def hashes_skip_names(nms, _rest): # LAW: the pairs of a names table, read as names, are the names written law pair_names_back: - for fs: List<&2, K.File> + for fs: List<&2, K.Member> {L.pair.names(L.file.pairs(fs)) == Laws.names.back(fs) : List<&2, L.Name>} def pair_names_back(fs): match fs: case []: {==} - case K.File{at, sum} <> t: + case K.Member{at, sum} <> t: Equal.cong(List<&2, L.Name>, List<&2, L.Name>, r => L.Name{at, sum} <> r, L.pair.names(L.file.pairs(t)), Laws.names.back(t), pair_names_back(t)) # LAW: the lock writes each name as the law's file of it law name_files_as: for nms: List<&2, L.Name> - {L.name.files(nms) == Laws.names.as.files(nms) : List<&2, K.File>} + {L.name.files(nms) == Laws.names.as.files(nms) : List<&2, K.Member>} def name_files_as(nms): match nms: case []: {==} case L.Name{nv, hash} <> t: - Equal.cong(List<&2, K.File>, List<&2, K.File>, x => K.File{nv, hash} <> x, + Equal.cong(List<&2, K.Member>, List<&2, K.Member>, x => K.Member{nv, hash} <> x, L.name.files(t), Laws.names.as.files(t), name_files_as(t)) # The upgrade's decisions: what it keeps (EZ-RES-4, EZ-RES-6) and what it @@ -14913,7 +14913,7 @@ def nv.all(js: List<&2, W.Judged>) -> Bool: law nv.laid: for ok: Bool for +hash: String - for +fs: List<&2, K.File> + for +fs: List<&2, K.Member> for +ss: List<&2, String> for e: {String.eq(hash, W.named(W.laid(fs, ss))) == ok : Bool} {nv(hash, W.body.laid(ok, hash, fs, ss)) == True{} : Bool} @@ -14928,7 +14928,7 @@ def nv.laid(ok, _hash, _fs, _ss, e): law nv.sums: for ok: Bool for +hash: String - for +fs: List<&2, K.File> + for +fs: List<&2, K.Member> for +ss: List<&2, String> {nv(hash, W.body.sums(ok, hash, fs, ss)) == True{} : Bool} @@ -14943,7 +14943,7 @@ law nv.escape: for clean: Bool for +bad: String for +hash: String - for +fs: List<&2, K.File> + for +fs: List<&2, K.Member> for +ss: List<&2, String> {nv(hash, W.body.escape.go(clean, bad, hash, fs, ss)) == True{} : Bool} @@ -15003,10 +15003,10 @@ law nv.rule: def nv.rule(named, hash, manifest, ss): match named: case True{}: - nv.git.body(List.is_empty(&2, K.File, L.manifest.files(String.lines(manifest))), + nv.git.body(List.is_empty(&2, K.Member, L.manifest.files(String.lines(manifest))), hash, manifest, ss) case False{}: - nv.git.body(List.is_empty(&2, K.File, K.bare(L.manifest.files(String.lines(manifest)))), + nv.git.body(List.is_empty(&2, K.Member, K.bare(L.manifest.files(String.lines(manifest)))), hash, K.manifest.lines(K.bare(L.manifest.files(String.lines(manifest)))), K.bare.srcs(L.manifest.files(String.lines(manifest)), ss)) @@ -17144,7 +17144,7 @@ def Laws.upgrade_origins_skip_tools(_nx, _n, _e, _b, _h, _hpa, _hpv, ds, _ts, g) def Laws.git_named_without_license(hash, manifest, ss, unnamed): %unnamed : {W.git.rule(_, hash, manifest, ss) - == W.git.body(List.is_empty(&2, K.File, K.bare(L.manifest.files(String.lines(manifest)))), + == W.git.body(List.is_empty(&2, K.Member, K.bare(L.manifest.files(String.lines(manifest)))), hash, K.manifest.lines(K.bare(L.manifest.files(String.lines(manifest)))), K.bare.srcs(L.manifest.files(String.lines(manifest)), ss)) : W.Verdict} {==} diff --git a/lock/lock.bend b/lock/lock.bend index 9ecc55d..e5cc5f4 100644 --- a/lock/lock.bend +++ b/lock/lock.bend @@ -25,7 +25,7 @@ type Src is Data: # a package the lock records type Pack is Data: - Pack{hash: String, src: Src, files: List<&2, K.File>} + Pack{hash: String, src: Src, files: List<&2, K.Member>} # a package's origin, as ez.toml records it type Origin is Data: @@ -302,17 +302,17 @@ def origin.hash(known: Origin) -> String: n # one ` ` line of a manifest -def line.put(+ws: List<&2, String>) -> List<&2, K.File>: - Bool.pick(List<&2, K.File>, Nat.is_eq(List.length(&2, String, ws), 2n), - [K.File{K.word(ws, 1n), K.word(ws, 0n)}], []) +def line.put(+ws: List<&2, String>) -> List<&2, K.Member>: + Bool.pick(List<&2, K.Member>, Nat.is_eq(List.length(&2, String, ws), 2n), + [K.Member{K.word(ws, 1n), K.word(ws, 0n)}], []) # every file a manifest names -def manifest.files(ls: List<&2, String>) -> List<&2, K.File>: +def manifest.files(ls: List<&2, String>) -> List<&2, K.Member>: match ls: case []: [] case h <> t: - List.append(&2, K.File, line.put(K.words(h)), manifest.files(t)) + List.append(&2, K.Member, line.put(K.words(h)), manifest.files(t)) # a url under the hub def url_of(+hub: String, +hash: String, at: String) -> String: @@ -412,12 +412,12 @@ def src.pairs(source: Src) -> List<&2, T.Kv>: kv("root", root), kv("narHash", nar), kv("tag", tag)]) # a file of a package as a `"" = ""` pair -def file.pair(item: K.File) -> T.Kv: - K.File{at, sum} = item +def file.pair(item: K.Member) -> T.Kv: + K.Member{at, sum} = item T.Kv{at, sum} # every file of a package, in path order -def file.pairs(fs: List<&2, K.File>) -> List<&2, T.Kv>: +def file.pairs(fs: List<&2, K.Member>) -> List<&2, T.Kv>: match fs: case []: [] @@ -426,7 +426,7 @@ def file.pairs(fs: List<&2, K.File>) -> List<&2, T.Kv>: # the two tables a package is written as, from its files already in path # order and each one once -def pack.sects.of(hash: String, src: Src, fs: List<&2, K.File>) -> List<&2, T.Sect>: +def pack.sects.of(hash: String, src: Src, fs: List<&2, K.Member>) -> List<&2, T.Sect>: +at = "packages." ++ T.quote(hash) [T.Sect{at ++ ".source", src.pairs(src)}, T.Sect{at ++ ".files", file.pairs(fs)}] @@ -498,12 +498,12 @@ def doc(hub: String, ps: List<&2, Pack>) -> List<&2, T.Sect>: # that proof again, and Bend's function values are linear, so one sort by a # key function applied at every comparison cannot be written. A block's path # is its package's hash, so distinct hashes are distinct paths. -def pack.block(package: Pack) -> K.File: +def pack.block(package: Pack) -> K.Member: Pack{+hash, src, files} = package - K.File{hash, T.render(pack.sects.of(hash, src, K.files_of(files)))} + K.Member{hash, T.render(pack.sects.of(hash, src, K.files_of(files)))} # every package, as its block -def pack.blocks(ps: List<&2, Pack>) -> List<&2, K.File>: +def pack.blocks(ps: List<&2, Pack>) -> List<&2, K.Member>: match ps: case []: [] @@ -511,18 +511,18 @@ def pack.blocks(ps: List<&2, Pack>) -> List<&2, K.File>: pack.block(h) <> pack.blocks(t) # the text of every block, in the order given -def block.texts(bs: List<&2, K.File>) -> List<&2, String>: +def block.texts(bs: List<&2, K.Member>) -> List<&2, String>: match bs: case []: [] - case K.File{_hash, text} <> t: + case K.Member{_hash, text} <> t: text <> block.texts(t) # the lock's text: the `[lock]` table, each block in the order given, then the # rest, assembled as ez's document text (`T.render`) and written as eztoml # writes it (`T.normal`). Every part of it is fixed by the blocks' order, so # the order the walk found packages in does not reach the file (EZ-DOC-2). -def text.of(hub: String, bs: List<&2, K.File>, rest: List<&2, String>) -> String: +def text.of(hub: String, bs: List<&2, K.Member>, rest: List<&2, String>) -> String: T.normal(String.join(T.render.sect(lock.sect(hub)) <> List.append(&2, String, block.texts(bs), rest), "\n")) @@ -562,12 +562,12 @@ def render.tools(ts: List<&2, M.Tool>, hub: String, ps: List<&2, Pack>) -> Strin # a name as the pair the `[names]` table writes it as, which is the shape a # file of a package is written in: its `@` as a quoted key and # its hash as the value -def name.file(name: Name) -> K.File: +def name.file(name: Name) -> K.Member: Name{nv, hash} = name - K.File{nv, hash} + K.Member{nv, hash} # every name, so -def name.files(ns: List<&2, Name>) -> List<&2, K.File>: +def name.files(ns: List<&2, Name>) -> List<&2, K.Member>: match ns: case []: [] @@ -658,12 +658,12 @@ def hashes(ss: List<&2, T.Sect>) -> List<&2, String>: hash.put(named3(segs(h), "packages", "files"), h, hashes(t)) # a pair of a files table as a file -def pair.file(kv: T.Kv) -> K.File: +def pair.file(kv: T.Kv) -> K.Member: T.Kv{k, v} = kv - K.File{k, v} + K.Member{k, v} # every pair of a files table, as files -def pair.files(ps: List<&2, T.Kv>) -> List<&2, K.File>: +def pair.files(ps: List<&2, T.Kv>) -> List<&2, K.Member>: match ps: case []: [] @@ -693,7 +693,7 @@ def pack.src(package: Pack) -> Src: s # a package's files -def pack.files(package: Pack) -> List<&2, K.File>: +def pack.files(package: Pack) -> List<&2, K.Member>: Pack{_h, _s, f} = package f diff --git a/lock/plan.bend b/lock/plan.bend index f3cf820..a1dd2c4 100644 --- a/lock/plan.bend +++ b/lock/plan.bend @@ -322,11 +322,11 @@ def src.values(source: L.Src) -> List<&2, String>: [url, rev, entry, root, nar, tag] # every path and sum a package's files write -def file.values(fs: List<&2, K.File>) -> List<&2, String>: +def file.values(fs: List<&2, K.Member>) -> List<&2, String>: match fs: case []: [] - case K.File{at, sum} <> t: + case K.Member{at, sum} <> t: at <> (sum <> file.values(t)) # every hash, key and value a package writes @@ -348,11 +348,11 @@ def path.eqless(text: String) -> Bool: Bool.and(Bool.not(Char.is_eq(h, '=')), rest) # whether no file path of a package holds `=` -def paths.ok(fs: List<&2, K.File>) -> Bool: +def paths.ok(fs: List<&2, K.Member>) -> Bool: match fs: case []: True{} - case K.File{at, _sum} <> t: + case K.Member{at, _sum} <> t: +rest = paths.ok(t) Bool.and(path.eqless(at), rest) @@ -401,11 +401,11 @@ def path.eq.pick(ok: Bool, at: String, rest: String) -> String: case False{}: at -def path.eq.first(fs: List<&2, K.File>) -> String: +def path.eq.first(fs: List<&2, K.Member>) -> String: match fs: case []: "" - case K.File{+at, _sum} <> t: + case K.Member{+at, _sum} <> t: path.eq.pick(path.eqless(at), at, path.eq.first(t)) # why a package with such a path cannot be locked, naming it and the path diff --git a/lock/run.bend b/lock/run.bend index 6734b95..cbf155f 100644 --- a/lock/run.bend +++ b/lock/run.bend @@ -13,7 +13,7 @@ # from its entry here, by `K.pkg_of`, which is interpreter code under # EZ-TRUST-2 until `ez add` is converted. import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../io/file.bend as F import ../hub/hub.bend as Web import ../git/git.bend as Git @@ -106,7 +106,7 @@ def gots(+how: W.How, +manifest: String, gs: List<&2, Web.Got>, acc: List<&2, St gots(how, manifest, t, body <> acc) # every file of a hub package, fetched and checked against its sum -def hub.all(+hub: String, +hash: String, fs: List<&2, K.File>) -> IO(List<&2, Web.Got>): +def hub.all(+hub: String, +hash: String, fs: List<&2, K.Member>) -> IO(List<&2, Web.Got>): match fs: case []: IO.pure(List<&2, Web.Got>, []) @@ -137,7 +137,7 @@ def answer.hub(+hub: String, +hash: String) -> IO(W.Answer): # every file a tree's manifest names, read from beside it. A file that is not # there reads as "", which does not hash to its sum. -def disk.all(+dir: String, fs: List<&2, K.File>) -> IO(List<&2, String>): +def disk.all(+dir: String, fs: List<&2, K.Member>) -> IO(List<&2, String>): match fs: case []: IO.pure(List<&2, String>, []) @@ -179,7 +179,7 @@ def clone.run(+work: String, what: String, args: List<&2, String>, go: Unit -> I def clone.walk(+work: String, +entry: String, +nar: String) -> IO(W.Answer): do IO: +p : K.Pkg <- K.pkg_in(work, entry) - +fs : List<&2, K.File> <- IO.pure(List<&2, K.File>, K.pkg.files(p)) + +fs : List<&2, K.Member> <- IO.pure(List<&2, K.Member>, K.pkg.files(p)) ss : List<&2, String> <- disk.all(K.pkg.root(p), fs) _rm : String <- R.exec(["rm", "-rf", work]) return W.Got{W.Clone{nar}, K.manifest_of(fs), ss} @@ -332,7 +332,7 @@ def answer.above(+lib: String, +url: String, +pin: String, +tip: String) -> IO(U def tree.walk(+work: String, +at: String, +nar: String) -> IO(Up.Answer): do IO: +p : K.Pkg <- K.pkg_in(work, at) - +fs : List<&2, K.File> <- IO.pure(List<&2, K.File>, K.pkg.files(p)) + +fs : List<&2, K.Member> <- IO.pure(List<&2, K.Member>, K.pkg.files(p)) ss : List<&2, String> <- disk.all(K.pkg.root(p), fs) +rt : String <- IO.pure(String, Git.root.rel(P.join(work, at), K.pkg.root(p), at)) _rm : String <- R.exec(["rm", "-rf", work]) diff --git a/lock/world.bend b/lock/world.bend index 1231028..5db38ab 100644 --- a/lock/world.bend +++ b/lock/world.bend @@ -85,7 +85,7 @@ type World is Data: # check passed, or why it refused them; or, for a name or the lock, the names # it resolves, each to its hash type Verdict is Data: - Ok{files: List<&2, K.File>, srcs: List<&2, String>} + Ok{files: List<&2, K.Member>, srcs: List<&2, String>} No{why: String} Named{names: List<&2, L.Name>} @@ -150,7 +150,7 @@ def ask.hash(ask: Ask) -> String: # whether every text hashes to the sum its file is recorded with. A list of # texts that is longer or shorter than the files is not the package. -def sums.ok(fs: List<&2, K.File>, ss: List<&2, String>) -> Bool: +def sums.ok(fs: List<&2, K.Member>, ss: List<&2, String>) -> Bool: match fs ss: case Nil{} Nil{}: True{} @@ -163,7 +163,7 @@ def sums.ok(fs: List<&2, K.File>, ss: List<&2, String>) -> Bool: Bool.and(String.eq(Sha.hex(s), K.file.sum(f)), rest) # each file with its text, as it is laid -def laid(fs: List<&2, K.File>, ss: List<&2, String>) -> List<&2, Source>: +def laid(fs: List<&2, K.Member>, ss: List<&2, String>) -> List<&2, Source>: match fs ss: case Nil{} Nil{}: [] @@ -175,12 +175,12 @@ def laid(fs: List<&2, K.File>, ss: List<&2, String>) -> List<&2, Source>: Source{K.file.at(f), s} <> laid(g, t) # a laid file weighed by its own text -def weigh(src: Source) -> K.File: +def weigh(src: Source) -> K.Member: Source{at, +text} = src - K.File{at, Sha.hex(text)} + K.Member{at, Sha.hex(text)} # every laid file weighed by its own text -def weighs(ls: List<&2, Source>) -> List<&2, K.File>: +def weighs(ls: List<&2, Source>) -> List<&2, K.Member>: match ls: case []: [] @@ -202,7 +202,7 @@ def named(+ls: List<&2, Source>) -> String: # manifest is not written the way ez writes one (a line per file, in path # order, each file once) is refused here rather than laid under a name its # laid manifest does not hash to. -def body.laid(ok: Bool, +hash: String, fs: List<&2, K.File>, ss: List<&2, String>) -> Verdict: +def body.laid(ok: Bool, +hash: String, fs: List<&2, K.Member>, ss: List<&2, String>) -> Verdict: match ok: case True{}: Ok{fs, ss} @@ -211,7 +211,7 @@ def body.laid(ok: Bool, +hash: String, fs: List<&2, K.File>, ss: List<&2, String " (one line per file, in path order, each file once)"} # the verdict once the texts were weighed against the manifest -def body.sums(ok: Bool, +hash: String, +fs: List<&2, K.File>, +ss: List<&2, String>) -> Verdict: +def body.sums(ok: Bool, +hash: String, +fs: List<&2, K.Member>, +ss: List<&2, String>) -> Verdict: match ok: case True{}: body.laid(String.eq(hash, named(laid(fs, ss))), hash, fs, ss) @@ -219,7 +219,7 @@ def body.sums(ok: Bool, +hash: String, +fs: List<&2, K.File>, +ss: List<&2, Stri No{"ez: " ++ hash ++ ": a file does not match its manifest"} # the verdict once each path was asked whether it escapes the package -def body.escape.go(clean: Bool, +bad: String, +hash: String, +fs: List<&2, K.File>, +ss: List<&2, String>) -> Verdict: +def body.escape.go(clean: Bool, +bad: String, +hash: String, +fs: List<&2, K.Member>, +ss: List<&2, String>) -> Verdict: match clean: case True{}: body.sums(sums.ok(fs, ss), hash, fs, ss) @@ -227,7 +227,7 @@ def body.escape.go(clean: Bool, +bad: String, +hash: String, +fs: List<&2, K.Fil No{"ez: " ++ hash ++ ": its manifest escapes the package (" ++ bad ++ ")"} # the verdict once no path was found to escape the package -def body.escape(+bad: String, +hash: String, +fs: List<&2, K.File>, +ss: List<&2, String>) -> Verdict: +def body.escape(+bad: String, +hash: String, +fs: List<&2, K.Member>, +ss: List<&2, String>) -> Verdict: body.escape.go(String.is_empty(bad), bad, hash, fs, ss) # the verdict once the manifest was known to be the one the hash names @@ -266,12 +266,12 @@ def git.body(empty: Bool, +hash: String, +manifest: String, +ss: List<&2, String def git.rule(named: Bool, +hash: String, +manifest: String, +ss: List<&2, String>) -> Verdict: match named: case True{}: - git.body(List.is_empty(&2, K.File, L.manifest.files(String.lines(manifest))), + git.body(List.is_empty(&2, K.Member, L.manifest.files(String.lines(manifest))), hash, manifest, ss) case False{}: +fs = L.manifest.files(String.lines(manifest)) +bs = K.bare(fs) - git.body(List.is_empty(&2, K.File, bs), hash, K.manifest.lines(bs), + git.body(List.is_empty(&2, K.Member, bs), hash, K.manifest.lines(bs), K.bare.srcs(fs, ss)) # a git package's bytes once its checkout was weighed. A tree read from diff --git a/pkg/LAWS.bend b/pkg/LAWS.bend index 7fea663..5bdf358 100644 --- a/pkg/LAWS.bend +++ b/pkg/LAWS.bend @@ -12,7 +12,7 @@ import ../sha/sha.bend as Sha # and `perm` below are the vocabulary the order-independence law needs and # nothing else uses: ez never calls them, and they say here what a rearranged # file list is in a form Bend can walk. -def perm.ins_at(place: Nat, file: P.File, xs: List<&2, P.File>) -> List<&2, P.File>: +def perm.ins_at(place: Nat, file: P.Member, xs: List<&2, P.Member>) -> List<&2, P.Member>: match place xs: case 0n _: file <> xs @@ -28,7 +28,7 @@ def perm.ins_at(place: Nat, file: P.File, xs: List<&2, P.File>) -> List<&2, P.Fi # the numbers reach every rearrangement of a list and nothing but its # rearrangements — that is a fact about this encoding and is argued, not # proved, since the laws below quantify over the numbers and never need it. -def perm(ns: List<&2, Nat>, xs: List<&2, P.File>) -> List<&2, P.File>: +def perm(ns: List<&2, Nat>, xs: List<&2, P.Member>) -> List<&2, P.Member>: match ns xs: case Nil{} Nil{}: [] @@ -40,7 +40,7 @@ def perm(ns: List<&2, Nat>, xs: List<&2, P.File>) -> List<&2, P.File>: perm.ins_at(n, h, perm(ms, t)) # whether a file's path is none of the paths a list holds -def fresh(+file: P.File, xs: List<&2, P.File>) -> Bool: +def fresh(+file: P.Member, xs: List<&2, P.Member>) -> Bool: match xs: case []: True{} @@ -53,7 +53,7 @@ def fresh(+file: P.File, xs: List<&2, P.File>) -> Bool: # say nothing about such a list, because there is nothing true to say: `dedup` # keeps the last of a run, so which of the two survives is the order's to # decide. -def distinct(xs: List<&2, P.File>) -> Bool: +def distinct(xs: List<&2, P.Member>) -> Bool: match xs: case []: True{} @@ -67,16 +67,16 @@ def distinct(xs: List<&2, P.File>) -> Bool: # of this file. It moved here from Base's List.sort, which no proof could # reach, and what it wanted was a permutation lemma over file.ins. law dedup_dup: - for +f: P.File - for t: List<&2, P.File> - {P.dedup(f <> (f <> t)) == P.dedup(f <> t) : List<&2, P.File>} + for +f: P.Member + for t: List<&2, P.Member> + {P.dedup(f <> (f <> t)) == P.dedup(f <> t) : List<&2, P.Member>} # LAW: a package that found a file publishes a file. Deduplication drops # repeats and never the last of them. law dedup_keeps: - for +h: P.File - for t: List<&2, P.File> - {List.is_empty(&2, P.File, P.dedup(h <> t)) == False{} : Bool} + for +h: P.Member + for t: List<&2, P.Member> + {List.is_empty(&2, P.Member, P.dedup(h <> t)) == False{} : Bool} # LAW: the base of a path is its last component, whatever comes before it. # The walk keeps the one it is carrying only when nothing follows. @@ -91,16 +91,16 @@ law base_last: # business and not the file system's. law sort_perm: for +ns: List<&2, Nat> - for +xs: List<&2, P.File> + for +xs: List<&2, P.Member> for +dis: {distinct(xs) == True{} : Bool} - {P.file.sort(perm(ns, xs)) == P.file.sort(xs) : List<&2, P.File>} + {P.file.sort(perm(ns, xs)) == P.file.sort(xs) : List<&2, P.Member>} # LAW: and so the manifest a package renders is the same text whatever order # its files were found in. `manifest_of` sorts before it renders, so this # follows from the law above. law manifest_perm: for +ns: List<&2, Nat> - for +xs: List<&2, P.File> + for +xs: List<&2, P.Member> for +dis: {distinct(xs) == True{} : Bool} {P.manifest_of(perm(ns, xs)) == P.manifest_of(xs) : String} @@ -110,7 +110,7 @@ law manifest_perm: # EZ-HASH-1 law hash_perm: for +ns: List<&2, Nat> - for +xs: List<&2, P.File> + for +xs: List<&2, P.Member> for +dis: {distinct(xs) == True{} : Bool} {P.hash_of(perm(ns, xs)) == P.hash_of(xs) : String} @@ -420,7 +420,7 @@ law foreign_keeps_head: # thirty-two hex characters of the manifest's digest. A lock that pins # `0x` pins this prefix, and nothing else of the digest. law hash_is_prefix: - for xs: List<&2, P.File> + for xs: List<&2, P.Member> {P.hash_of(xs) == "0x" ++ String.take(Sha.hex(P.manifest_of(xs)), 32n) : String} @@ -596,14 +596,14 @@ law license_dir_passes: # LAW: a package as bend named it before 2.0.27 leaves a LICENSE out law bare_drops_license: - for +h: P.File - for t: List<&2, P.File> + for +h: P.Member + for t: List<&2, P.Member> for lic: {True{} == P.file.lic(h) : Bool} - {P.bare(h <> t) == P.bare(t) : List<&2, P.File>} + {P.bare(h <> t) == P.bare(t) : List<&2, P.Member>} # LAW: and keeps every other file, in its place law bare_keeps_sources: - for +h: P.File - for t: List<&2, P.File> + for +h: P.Member + for t: List<&2, P.Member> for src: {False{} == P.file.lic(h) : Bool} - {P.bare(h <> t) == h <> P.bare(t) : List<&2, P.File>} + {P.bare(h <> t) == h <> P.bare(t) : List<&2, P.Member>} diff --git a/pkg/PROOF.bend b/pkg/PROOF.bend index 5180c04..962a085 100644 --- a/pkg/PROOF.bend +++ b/pkg/PROOF.bend @@ -22,36 +22,36 @@ import ./LAWS.bend as Laws # a parameter and the equation that put it there given alongside, since a # match may not scrutinise a computed value law dedup_dup.arm: - for +f: P.File - for b: P.File - for t: List<&2, P.File> + for +f: P.Member + for b: P.Member + for t: List<&2, P.Member> for bb: Bool for eb: {String.eq(P.file.at(f), P.file.at(b)) == bb : Bool} {P.dedup.head(f, P.dedup.pick(bb, f, b <> t)) == P.dedup.pick(bb, f, b <> t) - : List<&2, P.File>} + : List<&2, P.Member>} def dedup_dup.arm(f, b, t, bb, eb): match bb: case True{}: - Equal.cong(Bool, List<&2, P.File>, x => P.dedup.pick(x, f, b <> t), + Equal.cong(Bool, List<&2, P.Member>, x => P.dedup.pick(x, f, b <> t), String.eq(P.file.at(f), P.file.at(b)), True{}, eb) case False{}: - Equal.cong(Bool, List<&2, P.File>, + Equal.cong(Bool, List<&2, P.Member>, x => P.dedup.pick(x, f, f <> (b <> t)), String.eq(P.file.at(f), P.file.at(f)), True{}, Eq.string_eq_self(P.file.at(f))) # LAW: offering the same file to a deduplicated list twice changes nothing law dedup_dup.head: - for +f: P.File - for r: List<&2, P.File> + for +f: P.Member + for r: List<&2, P.Member> {P.dedup.head(f, P.dedup.head(f, r)) == P.dedup.head(f, r) - : List<&2, P.File>} + : List<&2, P.Member>} def dedup_dup.head(f, r): match r: case []: - Equal.cong(Bool, List<&2, P.File>, x => P.dedup.pick(x, f, [f]), + Equal.cong(Bool, List<&2, P.Member>, x => P.dedup.pick(x, f, [f]), String.eq(P.file.at(f), P.file.at(f)), True{}, Eq.string_eq_self(P.file.at(f))) case +b <> t: @@ -62,11 +62,11 @@ def Laws.dedup_dup(f, t): # LAW: whichever branch the pick takes, what comes back is a file and a rest law dedup_keeps.arm: - for -f: P.File - for -b: P.File - for -t: List<&2, P.File> + for -f: P.Member + for -b: P.Member + for -t: List<&2, P.Member> for bb: Bool - {List.is_empty(&2, P.File, P.dedup.pick(bb, f, b <> t)) == False{} : Bool} + {List.is_empty(&2, P.Member, P.dedup.pick(bb, f, b <> t)) == False{} : Bool} def dedup_keeps.arm(_f, _b, _t, bb): match bb: @@ -77,9 +77,9 @@ def dedup_keeps.arm(_f, _b, _t, bb): # LAW: a file offered to any deduplicated list comes back with it law dedup_keeps.head: - for +h: P.File - for r: List<&2, P.File> - {List.is_empty(&2, P.File, P.dedup.head(h, r)) == False{} : Bool} + for +h: P.Member + for r: List<&2, P.Member> + {List.is_empty(&2, P.Member, P.dedup.head(h, r)) == False{} : Bool} def dedup_keeps.head(h, r): match r: @@ -724,9 +724,9 @@ def le.trans.go(u, v, w, ok, eu, ev): # LAW: the order files are written in is transitive, as a total order is law le.trans: - for +x: P.File - for +y: P.File - for +z: P.File + for +x: P.Member + for +y: P.Member + for +z: P.Member for exy: {P.file.le(x, y) == True{} : Bool} for eyz: {P.file.le(y, z) == True{} : Bool} {P.file.le(x, z) == True{} : Bool} @@ -776,8 +776,8 @@ def le.excl.go(u, eu): # both and never neither. This is what the order of a package's files rests # on: a package holds each path once, so no two of its files tie. law le.excl: - for +a: P.File - for +b: P.File + for +a: P.Member + for +b: P.Member for ne: {String.eq(P.file.at(a), P.file.at(b)) == False{} : Bool} {P.file.le(a, b) == Bool.not(P.file.le(b, a)) : Bool} @@ -804,50 +804,50 @@ def le.excl(a, b, ne): # LAW: two files inserted into an empty list in either order land the same way law ins.swap.nil: - for +a: P.File - for +b: P.File + for +a: P.Member + for +b: P.Member for ba: Bool for eba: {P.file.le(b, a) == ba : Bool} for eab: {P.file.le(a, b) == Bool.not(ba) : Bool} {P.file.ins(P.file.ins([], a), b) == P.file.ins(P.file.ins([], b), a) - : List<&2, P.File>} + : List<&2, P.Member>} def ins.swap.nil(a, b, ba, eba, eab): match ba: case True{}: - Equal.trans(List<&2, P.File>, + Equal.trans(List<&2, P.Member>, P.file.ins(P.file.ins([], a), b), b <> (a <> []), P.file.ins(P.file.ins([], b), a), - Equal.cong(Bool, List<&2, P.File>, + Equal.cong(Bool, List<&2, P.Member>, y => P.file.ins.put(y, b, a, [], [b]), P.file.le(b, a), True{}, eba), - Equal.sym(List<&2, P.File>, + Equal.sym(List<&2, P.Member>, P.file.ins(P.file.ins([], b), a), b <> (a <> []), - Equal.cong(Bool, List<&2, P.File>, + Equal.cong(Bool, List<&2, P.Member>, y => P.file.ins.put(y, a, b, [], [a]), P.file.le(a, b), False{}, eab))) case False{}: - Equal.trans(List<&2, P.File>, + Equal.trans(List<&2, P.Member>, P.file.ins(P.file.ins([], a), b), a <> (b <> []), P.file.ins(P.file.ins([], b), a), - Equal.cong(Bool, List<&2, P.File>, + Equal.cong(Bool, List<&2, P.Member>, y => P.file.ins.put(y, b, a, [], [b]), P.file.le(b, a), False{}, eba), - Equal.sym(List<&2, P.File>, + Equal.sym(List<&2, P.Member>, P.file.ins(P.file.ins([], b), a), a <> (b <> []), - Equal.cong(Bool, List<&2, P.File>, + Equal.cong(Bool, List<&2, P.Member>, y => P.file.ins.put(y, a, b, [], [a]), P.file.le(a, b), True{}, eab))) # LAW: both files belong before the head, so both end up in front of it, in # the order their own comparison puts them law ins.swap.tt: - for +h: P.File - for +t: List<&2, P.File> - for +a: P.File - for +b: P.File + for +h: P.Member + for +t: List<&2, P.Member> + for +a: P.Member + for +b: P.Member for ba: Bool for eba: {P.file.le(b, a) == ba : Bool} for eab: {P.file.le(a, b) == Bool.not(ba) : Bool} @@ -855,76 +855,76 @@ law ins.swap.tt: for eB: {P.file.le(b, h) == True{} : Bool} {P.file.ins(P.file.ins.put(True{}, a, h, t, P.file.ins(t, a)), b) == P.file.ins(P.file.ins.put(True{}, b, h, t, P.file.ins(t, b)), a) - : List<&2, P.File>} + : List<&2, P.Member>} def ins.swap.tt(h, t, a, b, ba, eba, eab, eA, eB): match ba: case True{}: - Equal.trans(List<&2, P.File>, + Equal.trans(List<&2, P.Member>, P.file.ins(P.file.ins.put(True{}, a, h, t, P.file.ins(t, a)), b), b <> (a <> (h <> t)), P.file.ins(P.file.ins.put(True{}, b, h, t, P.file.ins(t, b)), a), - Equal.trans(List<&2, P.File>, + Equal.trans(List<&2, P.Member>, P.file.ins(P.file.ins.put(True{}, a, h, t, P.file.ins(t, a)), b), P.file.ins.put(P.file.le(b, a), b, a, h <> t, b <> (h <> t)), b <> (a <> (h <> t)), - Equal.cong(List<&2, P.File>, List<&2, P.File>, + Equal.cong(List<&2, P.Member>, List<&2, P.Member>, r => P.file.ins.put(P.file.le(b, a), b, a, h <> t, r), P.file.ins(h <> t, b), b <> (h <> t), - Equal.cong(Bool, List<&2, P.File>, + Equal.cong(Bool, List<&2, P.Member>, y => P.file.ins.put(y, b, h, t, P.file.ins(t, b)), P.file.le(b, h), True{}, eB)), - Equal.cong(Bool, List<&2, P.File>, + Equal.cong(Bool, List<&2, P.Member>, y => P.file.ins.put(y, b, a, h <> t, b <> (h <> t)), P.file.le(b, a), True{}, eba)), - Equal.sym(List<&2, P.File>, + Equal.sym(List<&2, P.Member>, P.file.ins(P.file.ins.put(True{}, b, h, t, P.file.ins(t, b)), a), b <> (a <> (h <> t)), - Equal.trans(List<&2, P.File>, + Equal.trans(List<&2, P.Member>, P.file.ins(P.file.ins.put(True{}, b, h, t, P.file.ins(t, b)), a), P.file.ins.put(P.file.le(a, b), a, b, h <> t, a <> (h <> t)), b <> (a <> (h <> t)), - Equal.cong(List<&2, P.File>, List<&2, P.File>, + Equal.cong(List<&2, P.Member>, List<&2, P.Member>, r => P.file.ins.put(P.file.le(a, b), a, b, h <> t, r), P.file.ins(h <> t, a), a <> (h <> t), - Equal.cong(Bool, List<&2, P.File>, + Equal.cong(Bool, List<&2, P.Member>, y => P.file.ins.put(y, a, h, t, P.file.ins(t, a)), P.file.le(a, h), True{}, eA)), - Equal.cong(Bool, List<&2, P.File>, + Equal.cong(Bool, List<&2, P.Member>, y => P.file.ins.put(y, a, b, h <> t, a <> (h <> t)), P.file.le(a, b), False{}, eab)))) case False{}: - Equal.trans(List<&2, P.File>, + Equal.trans(List<&2, P.Member>, P.file.ins(P.file.ins.put(True{}, a, h, t, P.file.ins(t, a)), b), a <> (b <> (h <> t)), P.file.ins(P.file.ins.put(True{}, b, h, t, P.file.ins(t, b)), a), - Equal.trans(List<&2, P.File>, + Equal.trans(List<&2, P.Member>, P.file.ins(P.file.ins.put(True{}, a, h, t, P.file.ins(t, a)), b), P.file.ins.put(P.file.le(b, a), b, a, h <> t, b <> (h <> t)), a <> (b <> (h <> t)), - Equal.cong(List<&2, P.File>, List<&2, P.File>, + Equal.cong(List<&2, P.Member>, List<&2, P.Member>, r => P.file.ins.put(P.file.le(b, a), b, a, h <> t, r), P.file.ins(h <> t, b), b <> (h <> t), - Equal.cong(Bool, List<&2, P.File>, + Equal.cong(Bool, List<&2, P.Member>, y => P.file.ins.put(y, b, h, t, P.file.ins(t, b)), P.file.le(b, h), True{}, eB)), - Equal.cong(Bool, List<&2, P.File>, + Equal.cong(Bool, List<&2, P.Member>, y => P.file.ins.put(y, b, a, h <> t, b <> (h <> t)), P.file.le(b, a), False{}, eba)), - Equal.sym(List<&2, P.File>, + Equal.sym(List<&2, P.Member>, P.file.ins(P.file.ins.put(True{}, b, h, t, P.file.ins(t, b)), a), a <> (b <> (h <> t)), - Equal.trans(List<&2, P.File>, + Equal.trans(List<&2, P.Member>, P.file.ins(P.file.ins.put(True{}, b, h, t, P.file.ins(t, b)), a), P.file.ins.put(P.file.le(a, b), a, b, h <> t, a <> (h <> t)), a <> (b <> (h <> t)), - Equal.cong(List<&2, P.File>, List<&2, P.File>, + Equal.cong(List<&2, P.Member>, List<&2, P.Member>, r => P.file.ins.put(P.file.le(a, b), a, b, h <> t, r), P.file.ins(h <> t, a), a <> (h <> t), - Equal.cong(Bool, List<&2, P.File>, + Equal.cong(Bool, List<&2, P.Member>, y => P.file.ins.put(y, a, h, t, P.file.ins(t, a)), P.file.le(a, h), True{}, eA)), - Equal.cong(Bool, List<&2, P.File>, + Equal.cong(Bool, List<&2, P.Member>, y => P.file.ins.put(y, a, b, h <> t, a <> (h <> t)), P.file.le(a, b), True{}, eab)))) @@ -933,17 +933,17 @@ def ins.swap.tt(h, t, a, b, ba, eba, eab, eA, eB): # two were offered. A file that came before the first would come before the # head too, so the branch where one does is no branch at all. law ins.swap.tf: - for +h: P.File - for +t: List<&2, P.File> - for +a: P.File - for +b: P.File + for +h: P.Member + for +t: List<&2, P.Member> + for +a: P.Member + for +b: P.Member for ba: Bool for eba: {P.file.le(b, a) == ba : Bool} for eA: {P.file.le(a, h) == True{} : Bool} for eB: {P.file.le(b, h) == False{} : Bool} {P.file.ins(P.file.ins.put(True{}, a, h, t, P.file.ins(t, a)), b) == P.file.ins(P.file.ins.put(False{}, b, h, t, P.file.ins(t, b)), a) - : List<&2, P.File>} + : List<&2, P.Member>} def ins.swap.tf(h, t, a, b, ba, eba, eA, eB): match ba: @@ -951,50 +951,50 @@ def ins.swap.tf(h, t, a, b, ba, eba, eA, eB): Eq.bit.absurd2(&2, {P.file.ins(P.file.ins.put(True{}, a, h, t, P.file.ins(t, a)), b) == P.file.ins(P.file.ins.put(False{}, b, h, t, P.file.ins(t, b)), a) - : List<&2, P.File>}, + : List<&2, P.Member>}, Equal.trans(Bool, True{}, P.file.le(b, h), False{}, Equal.sym(Bool, P.file.le(b, h), True{}, le.trans(b, a, h, eba, eA)), eB)) case False{}: - Equal.trans(List<&2, P.File>, + Equal.trans(List<&2, P.Member>, P.file.ins(P.file.ins.put(True{}, a, h, t, P.file.ins(t, a)), b), a <> (h <> P.file.ins(t, b)), P.file.ins(P.file.ins.put(False{}, b, h, t, P.file.ins(t, b)), a), - Equal.trans(List<&2, P.File>, + Equal.trans(List<&2, P.Member>, P.file.ins(P.file.ins.put(True{}, a, h, t, P.file.ins(t, a)), b), P.file.ins.put(P.file.le(b, a), b, a, h <> t, h <> P.file.ins(t, b)), a <> (h <> P.file.ins(t, b)), - Equal.cong(List<&2, P.File>, List<&2, P.File>, + Equal.cong(List<&2, P.Member>, List<&2, P.Member>, r => P.file.ins.put(P.file.le(b, a), b, a, h <> t, r), P.file.ins(h <> t, b), h <> P.file.ins(t, b), - Equal.cong(Bool, List<&2, P.File>, + Equal.cong(Bool, List<&2, P.Member>, y => P.file.ins.put(y, b, h, t, P.file.ins(t, b)), P.file.le(b, h), False{}, eB)), - Equal.cong(Bool, List<&2, P.File>, + Equal.cong(Bool, List<&2, P.Member>, y => P.file.ins.put(y, b, a, h <> t, h <> P.file.ins(t, b)), P.file.le(b, a), False{}, eba)), - Equal.sym(List<&2, P.File>, + Equal.sym(List<&2, P.Member>, P.file.ins(P.file.ins.put(False{}, b, h, t, P.file.ins(t, b)), a), a <> (h <> P.file.ins(t, b)), - Equal.cong(Bool, List<&2, P.File>, + Equal.cong(Bool, List<&2, P.Member>, y => P.file.ins.put(y, a, h, P.file.ins(t, b), P.file.ins(P.file.ins(t, b), a)), P.file.le(a, h), True{}, eA))) # LAW: the mirror of the one above, with the two files the other way round law ins.swap.ft: - for +h: P.File - for +t: List<&2, P.File> - for +a: P.File - for +b: P.File + for +h: P.Member + for +t: List<&2, P.Member> + for +a: P.Member + for +b: P.Member for ab: Bool for eab: {P.file.le(a, b) == ab : Bool} for eA: {P.file.le(a, h) == False{} : Bool} for eB: {P.file.le(b, h) == True{} : Bool} {P.file.ins(P.file.ins.put(False{}, a, h, t, P.file.ins(t, a)), b) == P.file.ins(P.file.ins.put(True{}, b, h, t, P.file.ins(t, b)), a) - : List<&2, P.File>} + : List<&2, P.Member>} def ins.swap.ft(h, t, a, b, ab, eab, eA, eB): match ab: @@ -1002,72 +1002,72 @@ def ins.swap.ft(h, t, a, b, ab, eab, eA, eB): Eq.bit.absurd2(&2, {P.file.ins(P.file.ins.put(False{}, a, h, t, P.file.ins(t, a)), b) == P.file.ins(P.file.ins.put(True{}, b, h, t, P.file.ins(t, b)), a) - : List<&2, P.File>}, + : List<&2, P.Member>}, Equal.trans(Bool, True{}, P.file.le(a, h), False{}, Equal.sym(Bool, P.file.le(a, h), True{}, le.trans(a, b, h, eab, eB)), eA)) case False{}: - Equal.trans(List<&2, P.File>, + Equal.trans(List<&2, P.Member>, P.file.ins(P.file.ins.put(False{}, a, h, t, P.file.ins(t, a)), b), b <> (h <> P.file.ins(t, a)), P.file.ins(P.file.ins.put(True{}, b, h, t, P.file.ins(t, b)), a), - Equal.cong(Bool, List<&2, P.File>, + Equal.cong(Bool, List<&2, P.Member>, y => P.file.ins.put(y, b, h, P.file.ins(t, a), P.file.ins(P.file.ins(t, a), b)), P.file.le(b, h), True{}, eB), - Equal.sym(List<&2, P.File>, + Equal.sym(List<&2, P.Member>, P.file.ins(P.file.ins.put(True{}, b, h, t, P.file.ins(t, b)), a), b <> (h <> P.file.ins(t, a)), - Equal.trans(List<&2, P.File>, + Equal.trans(List<&2, P.Member>, P.file.ins(P.file.ins.put(True{}, b, h, t, P.file.ins(t, b)), a), P.file.ins.put(P.file.le(a, b), a, b, h <> t, h <> P.file.ins(t, a)), b <> (h <> P.file.ins(t, a)), - Equal.cong(List<&2, P.File>, List<&2, P.File>, + Equal.cong(List<&2, P.Member>, List<&2, P.Member>, r => P.file.ins.put(P.file.le(a, b), a, b, h <> t, r), P.file.ins(h <> t, a), h <> P.file.ins(t, a), - Equal.cong(Bool, List<&2, P.File>, + Equal.cong(Bool, List<&2, P.Member>, y => P.file.ins.put(y, a, h, t, P.file.ins(t, a)), P.file.le(a, h), False{}, eA)), - Equal.cong(Bool, List<&2, P.File>, + Equal.cong(Bool, List<&2, P.Member>, y => P.file.ins.put(y, a, b, h <> t, h <> P.file.ins(t, a)), P.file.le(a, b), False{}, eab)))) # LAW: neither file belongs before the head, so both go past it and the swap # is the one the shorter list already answered for law ins.swap.ff: - for +h: P.File - for +t: List<&2, P.File> - for +a: P.File - for +b: P.File + for +h: P.Member + for +t: List<&2, P.Member> + for +a: P.Member + for +b: P.Member for eA: {P.file.le(a, h) == False{} : Bool} for eB: {P.file.le(b, h) == False{} : Bool} for ih: {P.file.ins(P.file.ins(t, a), b) == P.file.ins(P.file.ins(t, b), a) - : List<&2, P.File>} + : List<&2, P.Member>} {P.file.ins(P.file.ins.put(False{}, a, h, t, P.file.ins(t, a)), b) == P.file.ins(P.file.ins.put(False{}, b, h, t, P.file.ins(t, b)), a) - : List<&2, P.File>} + : List<&2, P.Member>} def ins.swap.ff(h, t, a, b, eA, eB, ih): - Equal.trans(List<&2, P.File>, + Equal.trans(List<&2, P.Member>, P.file.ins(P.file.ins.put(False{}, a, h, t, P.file.ins(t, a)), b), h <> P.file.ins(P.file.ins(t, a), b), P.file.ins(P.file.ins.put(False{}, b, h, t, P.file.ins(t, b)), a), - Equal.cong(Bool, List<&2, P.File>, + Equal.cong(Bool, List<&2, P.Member>, y => P.file.ins.put(y, b, h, P.file.ins(t, a), P.file.ins(P.file.ins(t, a), b)), P.file.le(b, h), False{}, eB), - Equal.trans(List<&2, P.File>, + Equal.trans(List<&2, P.Member>, h <> P.file.ins(P.file.ins(t, a), b), h <> P.file.ins(P.file.ins(t, b), a), P.file.ins(P.file.ins.put(False{}, b, h, t, P.file.ins(t, b)), a), - Equal.cong(List<&2, P.File>, List<&2, P.File>, r => h <> r, + Equal.cong(List<&2, P.Member>, List<&2, P.Member>, r => h <> r, P.file.ins(P.file.ins(t, a), b), P.file.ins(P.file.ins(t, b), a), ih), - Equal.sym(List<&2, P.File>, + Equal.sym(List<&2, P.Member>, P.file.ins(P.file.ins.put(False{}, b, h, t, P.file.ins(t, b)), a), h <> P.file.ins(P.file.ins(t, b), a), - Equal.cong(Bool, List<&2, P.File>, + Equal.cong(Bool, List<&2, P.Member>, y => P.file.ins.put(y, a, h, P.file.ins(t, b), P.file.ins(P.file.ins(t, b), a)), P.file.le(a, h), False{}, eA)))) @@ -1075,20 +1075,20 @@ def ins.swap.ff(h, t, a, b, eA, eB, ih): # LAW: one step of the swap, with the two comparisons against the head given # as parameters and the equations that put them there given alongside law ins.swap.arm: - for +h: P.File - for +t: List<&2, P.File> - for +a: P.File - for +b: P.File + for +h: P.Member + for +t: List<&2, P.Member> + for +a: P.Member + for +b: P.Member for A: Bool for eA: {P.file.le(a, h) == A : Bool} for B: Bool for eB: {P.file.le(b, h) == B : Bool} for exc: {P.file.le(a, b) == Bool.not(P.file.le(b, a)) : Bool} for ih: {P.file.ins(P.file.ins(t, a), b) == P.file.ins(P.file.ins(t, b), a) - : List<&2, P.File>} + : List<&2, P.Member>} {P.file.ins(P.file.ins.put(A, a, h, t, P.file.ins(t, a)), b) == P.file.ins(P.file.ins.put(B, b, h, t, P.file.ins(t, b)), a) - : List<&2, P.File>} + : List<&2, P.Member>} def ins.swap.arm(h, t, a, b, A, eA, B, eB, exc, ih): match A B: @@ -1105,12 +1105,12 @@ def ins.swap.arm(h, t, a, b, A, eA, B, eB, exc, ih): # give the same list. The list is any list: the sort's accumulator is in order # already, but the induction never needs to say so. law ins.swap: - for xs: List<&2, P.File> - for +a: P.File - for +b: P.File + for xs: List<&2, P.Member> + for +a: P.Member + for +b: P.Member for +ne: {String.eq(P.file.at(a), P.file.at(b)) == False{} : Bool} {P.file.ins(P.file.ins(xs, a), b) == P.file.ins(P.file.ins(xs, b), a) - : List<&2, P.File>} + : List<&2, P.Member>} def ins.swap(xs, a, b, ne): match xs: @@ -1124,9 +1124,9 @@ def ins.swap(xs, a, b, ne): # list with one more file put in it, as long as it is not that file's either law fresh.ins_at: for +n: Nat - for +x: P.File - for +y: P.File - for +xs: List<&2, P.File> + for +x: P.Member + for +y: P.Member + for +xs: List<&2, P.Member> for nxy: {String.eq(P.file.at(x), P.file.at(y)) == False{} : Bool} for +fx: {Laws.fresh(x, xs) == True{} : Bool} {Laws.fresh(x, Laws.perm.ins_at(n, y, xs)) == True{} : Bool} @@ -1163,9 +1163,9 @@ def fresh.ins_at(n, x, y, xs, nxy, fx): # LAW: rearranging a list does not put a path in it that was not there law fresh.perm: - for +x: P.File + for +x: P.Member for +ns: List<&2, Nat> - for +xs: List<&2, P.File> + for +xs: List<&2, P.Member> for +fx: {Laws.fresh(x, xs) == True{} : Bool} {Laws.fresh(x, Laws.perm(ns, xs)) == True{} : Bool} @@ -1191,11 +1191,11 @@ def fresh.perm(x, ns, xs, fx): # which is the whole of the order-independence, said one file at a time. law sort.ins_at: for +n: Nat - for +x: P.File - for +xs: List<&2, P.File> + for +x: P.Member + for +xs: List<&2, P.Member> for +fr: {Laws.fresh(x, xs) == True{} : Bool} {P.file.sort(Laws.perm.ins_at(n, x, xs)) == P.file.ins(P.file.sort(xs), x) - : List<&2, P.File>} + : List<&2, P.Member>} def sort.ins_at(n, x, xs, fr): match n xs: @@ -1204,11 +1204,11 @@ def sort.ins_at(n, x, xs, fr): case 1n+p Nil{}: {==} case 1n+p Con{+h, +t}: - Equal.trans(List<&2, P.File>, + Equal.trans(List<&2, P.Member>, P.file.sort(h <> Laws.perm.ins_at(p, x, t)), P.file.ins(P.file.ins(P.file.sort(t), x), h), P.file.ins(P.file.ins(P.file.sort(t), h), x), - Equal.cong(List<&2, P.File>, List<&2, P.File>, + Equal.cong(List<&2, P.Member>, List<&2, P.Member>, r => P.file.ins(r, h), P.file.sort(Laws.perm.ins_at(p, x, t)), P.file.ins(P.file.sort(t), x), @@ -1229,21 +1229,21 @@ def Laws.sort_perm(ns, xs, dis): case Con{n, ms} Nil{}: {==} case Con{+n, +ms} Con{+h, +t}: - Equal.trans(List<&2, P.File>, + Equal.trans(List<&2, P.Member>, P.file.sort(Laws.perm.ins_at(n, h, Laws.perm(ms, t))), P.file.ins(P.file.sort(Laws.perm(ms, t)), h), P.file.ins(P.file.sort(t), h), sort.ins_at(n, h, Laws.perm(ms, t), fresh.perm(h, ms, t, Eq.and.left(Laws.fresh(h, t), Laws.distinct(t), dis))), - Equal.cong(List<&2, P.File>, List<&2, P.File>, + Equal.cong(List<&2, P.Member>, List<&2, P.Member>, r => P.file.ins(r, h), P.file.sort(Laws.perm(ms, t)), P.file.sort(t), Laws.sort_perm(ms, t, Eq.and.right(Laws.fresh(h, t), Laws.distinct(t), dis)))) def Laws.manifest_perm(ns, xs, dis): - Equal.cong(List<&2, P.File>, String, + Equal.cong(List<&2, P.Member>, String, ys => P.manifest.lines(P.dedup(ys)), P.file.sort(Laws.perm(ns, xs)), P.file.sort(xs), Laws.sort_perm(ns, xs, dis)) @@ -2323,25 +2323,25 @@ def Laws.escaping_import_refused(f, entry, tree, eb, seen, out, file, ns, rest, law placed_is_laid: for +pre: String for +out: List<&2, P.Hit> - {P.placed(pre, P.hit.sums(out)) == P.laid.sums(P.laid(pre, out)) : List<&2, P.File>} + {P.placed(pre, P.hit.sums(out)) == P.laid.sums(P.laid(pre, out)) : List<&2, P.Member>} def placed_is_laid(pre, out): match out: case []: {==} case P.Hit{+raw, +text} <> t: - Equal.cong(List<&2, P.File>, List<&2, P.File>, - xs => P.File{Path.join(pre, raw), Sha.hex(text)} <> xs, + Equal.cong(List<&2, P.Member>, List<&2, P.Member>, + xs => P.Member{Path.join(pre, raw), Sha.hex(text)} <> xs, P.placed(pre, P.hit.sums(t)), P.laid.sums(P.laid(pre, t)), placed_is_laid(pre, t)) def Laws.walked_named_by_texts(pre, out): - Equal.cong(List<&2, P.File>, String, fs => P.hash_of(fs), + Equal.cong(List<&2, P.Member>, String, fs => P.hash_of(fs), P.placed(pre, P.hit.sums(out)), P.laid.sums(P.laid(pre, out)), placed_is_laid(pre, out)) def Laws.walked_manifest_of_texts(pre, out): - Equal.cong(List<&2, P.File>, String, fs => P.manifest_of(fs), + Equal.cong(List<&2, P.Member>, String, fs => P.manifest_of(fs), P.placed(pre, P.hit.sums(out)), P.laid.sums(P.laid(pre, out)), placed_is_laid(pre, out)) @@ -2410,11 +2410,11 @@ def Laws.license_dir_passes(root, pre, out, none): {==} def Laws.bare_drops_license(h, t, lic): - %lic : {P.bare.pick(_, h, P.bare(t)) == P.bare(t) : List<&2, P.File>} + %lic : {P.bare.pick(_, h, P.bare(t)) == P.bare(t) : List<&2, P.Member>} {==} def Laws.bare_keeps_sources(h, t, src): - %src : {P.bare.pick(_, h, P.bare(t)) == h <> P.bare(t) : List<&2, P.File>} + %src : {P.bare.pick(_, h, P.bare(t)) == h <> P.bare(t) : List<&2, P.Member>} {==} # --------------------------------------------------------------------------- diff --git a/pkg/pkg.bend b/pkg/pkg.bend index f8952f0..3a7d89a 100644 --- a/pkg/pkg.bend +++ b/pkg/pkg.bend @@ -16,8 +16,8 @@ import ../sha/sha.bend as Sha import ./path.bend as P # a file of a package: the path it takes inside the package, and its sha256 -type File is Data: - File{at: String, sum: String} +type Member is Data: + Member{at: String, sum: String} # a package: the files it holds, the hash that names them, and the directory # their paths are written from. The root is the entry's own directory until a @@ -25,7 +25,7 @@ type File is Data: # copying the files out joins them against this and never against the entry's # directory. type Pkg is Data: - Pkg{hash: String, root: String, files: List<&2, File>} + Pkg{hash: String, root: String, files: List<&2, Member>} # what a source file's header imports: modules by the path they were reached # through, and the foreign C and JS bodies bend uploads alongside the sources @@ -503,12 +503,12 @@ def seen.has(xs: List<&2, String>, +want: String) -> Bool: seen.has.step(String.eq(h, want), _u => seen.has(t, want)) # a found file, placed under whatever the package re-rooted at -def file_of(+pre: String, hit: Found) -> File: +def file_of(+pre: String, hit: Found) -> Member: Found{raw, sum} = hit - File{P.join(pre, raw), sum} + Member{P.join(pre, raw), sum} # every found file, placed -def placed(+pre: String, fs: List<&2, Found>) -> List<&2, File>: +def placed(+pre: String, fs: List<&2, Found>) -> List<&2, Member>: match fs: case []: [] @@ -516,17 +516,17 @@ def placed(+pre: String, fs: List<&2, Found>) -> List<&2, File>: file_of(pre, h) <> placed(pre, t) # where a file sits inside its package -def file.at(item: File) -> String: - File{at, _sum} = item +def file.at(item: Member) -> String: + Member{at, _sum} = item at # a package's files are written in path order, so the manifest of a package is # the same text whoever computes it -def file.le(left: File, right: File) -> Bool: +def file.le(left: Member, right: Member) -> Bool: String.is_le(file.at(left), file.at(right)) # the same path twice is the same file twice, and a package holds it once -def dedup.pick(same: Bool, head: File, rest: List<&2, File>) -> List<&2, File>: +def dedup.pick(same: Bool, head: Member, rest: List<&2, Member>) -> List<&2, Member>: match same: case True{}: rest @@ -534,7 +534,7 @@ def dedup.pick(same: Bool, head: File, rest: List<&2, File>) -> List<&2, File>: head <> rest # a file against the deduplicated files that follow it -def dedup.head(+head: File, rest: List<&2, File>) -> List<&2, File>: +def dedup.head(+head: Member, rest: List<&2, Member>) -> List<&2, Member>: match rest: case []: [head] @@ -542,7 +542,7 @@ def dedup.head(+head: File, rest: List<&2, File>) -> List<&2, File>: dedup.pick(String.eq(file.at(head), file.at(b)), head, b <> t) # a sorted file list with the repeats dropped -def dedup(fs: List<&2, File>) -> List<&2, File>: +def dedup(fs: List<&2, Member>) -> List<&2, Member>: match fs: case []: [] @@ -552,7 +552,13 @@ def dedup(fs: List<&2, File>) -> List<&2, File>: # where a file goes among the files already in order: before the one it is not # after, otherwise behind it. The rest of the insertion is a parameter, because # two defs that call each other are not allowed. -def file.ins.put(le: Bool, item: File, head: File, tail: List<&2, File>, rest: List<&2, File>) -> List<&2, File>: +def file.ins.put( + le: Bool, + item: Member, + head: Member, + tail: List<&2, Member>, + rest: List<&2, Member> +) -> List<&2, Member>: match le: case True{}: item <> (head <> tail) @@ -560,7 +566,7 @@ def file.ins.put(le: Bool, item: File, head: File, tail: List<&2, File>, rest: L head <> rest # a file inserted into a list already in path order -def file.ins(fs: List<&2, File>, +item: File) -> List<&2, File>: +def file.ins(fs: List<&2, Member>, +item: Member) -> List<&2, Member>: match fs: case []: [item] @@ -572,7 +578,7 @@ def file.ins(fs: List<&2, File>, +item: File) -> List<&2, File>: # is reported as unsafe and every proof downstream of it inherits the report. # An insertion sort shrinks its list at every step, so Bend checks it, and a # package's file set is small enough that the cost is not felt. -def file.sort(fs: List<&2, File>) -> List<&2, File>: +def file.sort(fs: List<&2, Member>) -> List<&2, Member>: match fs: case []: [] @@ -580,7 +586,7 @@ def file.sort(fs: List<&2, File>) -> List<&2, File>: file.ins(file.sort(t), h) # the files of a package, in path order and each one once -def files_of(fs: List<&2, File>) -> List<&2, File>: +def files_of(fs: List<&2, Member>) -> List<&2, Member>: dedup(file.sort(fs)) # a path that leaves the package behind, which no package may hold @@ -599,7 +605,7 @@ def escaped.step(here: Bool, at: String, rest: Unit -> String) -> String: rest(Unit{}) # the first file whose path leaves the package, or "" when none does -def escaped(fs: List<&2, File>) -> String: +def escaped(fs: List<&2, Member>) -> String: match fs: case []: "" @@ -608,12 +614,12 @@ def escaped(fs: List<&2, File>) -> String: escaped.step(escapes(at), at, _u => escaped(t)) # one ` ` line -def manifest.line(item: File) -> String: - File{at, sum} = item +def manifest.line(item: Member) -> String: + Member{at, sum} = item sum ++ " " ++ at ++ "\n" # every line of a manifest -def manifest.lines(fs: List<&2, File>) -> String: +def manifest.lines(fs: List<&2, Member>) -> String: match fs: case []: "" @@ -622,21 +628,21 @@ def manifest.lines(fs: List<&2, File>) -> String: # the manifest text is the package's identity, and bend checks a fetched # manifest against the first 32 hex characters of its sha256 -def manifest_of(fs: List<&2, File>) -> String: +def manifest_of(fs: List<&2, Member>) -> String: manifest.lines(files_of(fs)) # the `0x` name a file set is published under -def hash_of(fs: List<&2, File>) -> String: +def hash_of(fs: List<&2, Member>) -> String: "0x" ++ String.take(Sha.hex(manifest_of(fs)), 32n) # whether a file of a package is a LICENSE bend took along. A module ends in # `.bend` and a foreign body in `.c` or `.js`, so a file named LICENSE is one # the walk took along beside them. -def file.lic(item: File) -> Bool: - File{at, _sum} = item +def file.lic(item: Member) -> Bool: + Member{at, _sum} = item String.eq(P.base(at), "LICENSE") -def bare.pick(lic: Bool, head: File, rest: List<&2, File>) -> List<&2, File>: +def bare.pick(lic: Bool, head: Member, rest: List<&2, Member>) -> List<&2, Member>: match lic: case True{}: rest @@ -645,7 +651,7 @@ def bare.pick(lic: Bool, head: File, rest: List<&2, File>) -> List<&2, File>: # a package's files as bend named them before 2.0.27: without the LICENSE # files it now takes along, in the order they were given -def bare(fs: List<&2, File>) -> List<&2, File>: +def bare(fs: List<&2, Member>) -> List<&2, Member>: match fs: case []: [] @@ -661,7 +667,7 @@ def bare.srcs.pick(lic: Bool, text: String, rest: List<&2, String>) -> List<&2, # the texts that go with those files: the texts of a file list, one per file # in the same order, with the LICENSE files' texts left out -def bare.srcs(fs: List<&2, File>, ss: List<&2, String>) -> List<&2, String>: +def bare.srcs(fs: List<&2, Member>, ss: List<&2, String>) -> List<&2, String>: match fs ss: case Nil{} _: ss @@ -717,7 +723,7 @@ type State is Data: # written from, the files it lays with their texts, and those files weighed, # in path order, which is what its manifest lists. type Walked is Data: - Walked{hash: String, root: String, files: List<&2, Source>, sums: List<&2, File>} + Walked{hash: String, root: String, files: List<&2, Source>, sums: List<&2, Member>} Asks{at: String} Refused{why: String} @@ -1101,12 +1107,12 @@ def laid(+pre: String, fs: List<&2, Hit>) -> List<&2, Source>: # a laid file weighed: its path and the sha256 of its text. This is what a # plan's reader would compute from the files a `Lay` writes. -def laid.sum(src: Source) -> File: +def laid.sum(src: Source) -> Member: Source{at, +text} = src - File{at, Sha.hex(text)} + Member{at, Sha.hex(text)} # every laid file weighed -def laid.sums(fs: List<&2, Source>) -> List<&2, File>: +def laid.sums(fs: List<&2, Source>) -> List<&2, Member>: match fs: case []: [] @@ -1132,7 +1138,7 @@ def made.judge( +bad: String, +root: String, +pre: String, - +fs: List<&2, File>, + +fs: List<&2, Member>, out: List<&2, Hit> ) -> Walked: match ok: @@ -1386,11 +1392,11 @@ def pkg.root(package: Pkg) -> String: root # the files a package holds -def pkg.files(package: Pkg) -> List<&2, File>: +def pkg.files(package: Pkg) -> List<&2, Member>: Pkg{_h, _root, fs} = package fs # the sha256 recorded for a file -def file.sum(item: File) -> String: - File{_at, sum} = item +def file.sum(item: Member) -> String: + Member{_at, sum} = item sum diff --git a/pub/run.bend b/pub/run.bend index 10b07c0..67c9f74 100644 --- a/pub/run.bend +++ b/pub/run.bend @@ -19,7 +19,7 @@ # the text: whether the hub answered 200, and the body or why not. # It decides nothing; that it reads and executes faithfully is EZ-TRUST-2. import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../io/file.bend as F import ../lock/run.bend as Run import ../tool/run.bend as ToolRun diff --git a/run/bend.bend b/run/bend.bend index c713c49..df87288 100644 --- a/run/bend.bend +++ b/run/bend.bend @@ -9,7 +9,7 @@ # report and the toolchain part of a cache key. # Asking both ways, current spelling first, is the whole of this module. import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R # the older spelling, tried only when the current one was not understood def version.older(ok: Bool, out: String) -> IO(String): diff --git a/sha/LAWS.bend b/sha/LAWS.bend index 218da6d..a3c25c1 100644 --- a/sha/LAWS.bend +++ b/sha/LAWS.bend @@ -21,14 +21,14 @@ law utf8_append: # listed in, so long as no name is listed twice, which a directory never does. # `find` lists a directory in whatever order the filesystem keeps it, and two # machines may keep it differently; this is why their narHash still agrees. -# `perm` and `distinct` are pkg's: an entry is a `K.File` holding its name and +# `perm` and `distinct` are pkg's: an entry is a `K.Member` holding its name and # its node's serial, so a rearranged directory is a rearranged file list. # Every directory the walk serializes goes through `Nar.dir`, children and # root alike, so the law at one level is the law for the whole tree. # EZ-HASH-2 law nar_dir_order_free: for +ns: List<&2, Nat> - for +es: List<&2, K.File> + for +es: List<&2, K.Member> for +dis: {PL.distinct(es) == True{} : Bool} {Nar.dir(PL.perm(ns, es)) == Nar.dir(es) : String} diff --git a/sha/PROOF.bend b/sha/PROOF.bend index 2d681fb..ac609bb 100644 --- a/sha/PROOF.bend +++ b/sha/PROOF.bend @@ -35,7 +35,7 @@ def Laws.utf8_append(a, b): # `Nar.dir` sorts before it serializes, so this is pkg's `sort_perm` carried # under `Nar.directory` def Laws.nar_dir_order_free(ns, es, dis): - Equal.cong(List<&2, K.File>, String, ys => Nar.directory(ys), + Equal.cong(List<&2, K.Member>, String, ys => Nar.directory(ys), K.file.sort(PL.perm(ns, es)), K.file.sort(es), PL.sort_perm(ns, es, dis)) diff --git a/sha/nar.bend b/sha/nar.bend index fecc03c..9f2fdff 100644 --- a/sha/nar.bend +++ b/sha/nar.bend @@ -9,12 +9,12 @@ # of a path is what nix's dumper takes: the owner's exec bit of the mode, # every name and link target as it is, and a file's bytes. import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../io/file.bend as F import ../pkg/pkg.bend as K import ../sha/sha.bend as Sha -# A directory child is a `K.File`: its name in `at` and the NAR serial of its +# A directory child is a `K.Member`: its name in `at` and the NAR serial of its # node in `sum`. That is a package file's shape, a name and the text that # stands for it, so the walk sorts children with the same `K.file.sort` a # package sorts its files with, and what is proved of that sort is proved of @@ -72,13 +72,13 @@ def symlink(+target: String) -> String: ++ str(Sha.utf8(target)) ++ str(")") # one directory entry: its name and its node -def entry(+ent: K.File) -> String: - K.File{name, node} = ent +def entry(+ent: K.Member) -> String: + K.Member{name, node} = ent str("entry") ++ str("(") ++ str("name") ++ str(Sha.utf8(name)) ++ str("node") ++ node ++ str(")") # a directory's entries, in the order given -def entries(es: List<&2, K.File>) -> String: +def entries(es: List<&2, K.Member>) -> String: match es: case []: "" @@ -86,7 +86,7 @@ def entries(es: List<&2, K.File>) -> String: entry(h) ++ entries(t) # a directory's node, its entries in the order given -def directory(es: List<&2, K.File>) -> String: +def directory(es: List<&2, K.Member>) -> String: str("(") ++ str("type") ++ str("directory") ++ entries(es) ++ str(")") # a directory's node as NAR writes it: its entries sorted by name, whatever @@ -94,7 +94,7 @@ def directory(es: List<&2, K.File>) -> String: # byte order for the UTF-8 of valid names. Every directory the walk serializes # goes through here, so the order `find` printed its names in never reaches # the NAR. -def dir(es: List<&2, K.File>) -> String: +def dir(es: List<&2, K.Member>) -> String: directory(K.file.sort(es)) # a whole NAR: the magic, then the root node @@ -320,7 +320,7 @@ type Ent is Data: # a directory still open: its path from the top, its name, and the entries # found in it so far type Frame is Data: - Frame{at: String, name: String, kids: List<&2, K.File>} + Frame{at: String, name: String, kids: List<&2, K.Member>} # where the build stands: the paths still to place, the directory they are # being placed in, and the directories around it @@ -330,7 +330,7 @@ type State is Data: # a step of the build: another state, or the finished node of the top type Move is Data: Next{st: State} - Done{node: String} + Built{node: String} def leaf.of(link: Bool, ex: Bool, +body: String) -> String: match link: @@ -354,9 +354,9 @@ def close(top: Frame, up: List<&2, Frame>, es: List<&2, Ent>) -> Move: Frame{_at, +name, kids} = top match up: case []: - Done{dir(kids)} + Built{dir(kids)} case Frame{pat, pname, pkids} <> rest: - Next{State{es, Frame{pat, pname, K.File{name, dir(kids)} <> pkids}, rest}} + Next{State{es, Frame{pat, pname, K.Member{name, dir(kids)} <> pkids}, rest}} # an entry's type, name and path, and an open directory's path def ent.kind(entry: Ent) -> String: @@ -394,7 +394,7 @@ def place( Next{State{more, Frame{at, name, []}, top <> up}} case False{}: Frame{a, n, ks} = top - Next{State{more, Frame{a, n, K.File{name, node} <> ks}, up}} + Next{State{more, Frame{a, n, K.Member{name, node} <> ks}, up}} # the next path: placed when it is inside the directory on top, which closes # otherwise @@ -429,7 +429,7 @@ def build.go(fuel: Nat, mv: Move) -> Maybe<&2, String>: match mv: case Next{st}: build.go(f, step(st)) - case Done{node}: + case Built{node}: Some{node} # the node of a directory, from its paths in the order `find` lists them. Each diff --git a/sha/sha.bend b/sha/sha.bend index 0fbdc74..3ac3f2e 100644 --- a/sha/sha.bend +++ b/sha/sha.bend @@ -1,10 +1,10 @@ # sha/sha: the sha256 a package hash is built from. The digest itself comes from -# Giulio2002/bend-sha256, which proves its output equal to an executable FIPS +# noah-emp/bend-sha256, which proves its output equal to an executable FIPS # 180-4 specification; this file is only the string-in, hex-out shape ez uses. # The dependency hashes packed big-endian words and returns eight of them, or # nothing when the declared length does not fit the array. import Base -import 0xda83506fb9f059ead7afcfa2f498df5f/sha256.bend as S +import 0xa17f0215fb4dd22e26fd007661489402/sha256.bend as S # four big-endian bytes in one word, each kept to eight bits def pack(first: U32, second: U32, third: U32, fourth: U32) -> U32: @@ -86,44 +86,44 @@ def raw(+text: String) -> String: def utf8.byte(+code: U32) -> Char: Chr{(code .&. 255 : U32)} -def utf8.1(+code: U32) -> String: +def utf8.one(+code: U32) -> String: SCon{utf8.byte(code), SNil{}} -def utf8.2(+code: U32) -> String: +def utf8.two(+code: U32) -> String: SCon{utf8.byte((192 .|. U32.shrn(code, 6n) : U32)), SCon{utf8.byte((128 .|. (code .&. 63 : U32) : U32)), SNil{}}} -def utf8.3(+code: U32) -> String: +def utf8.three(+code: U32) -> String: SCon{utf8.byte((224 .|. U32.shrn(code, 12n) : U32)), SCon{utf8.byte((128 .|. (U32.shrn(code, 6n) .&. 63 : U32) : U32)), SCon{utf8.byte((128 .|. (code .&. 63 : U32) : U32)), SNil{}}}} -def utf8.4(+code: U32) -> String: +def utf8.four(+code: U32) -> String: SCon{utf8.byte((240 .|. U32.shrn(code, 18n) : U32)), SCon{utf8.byte((128 .|. (U32.shrn(code, 12n) .&. 63 : U32) : U32)), SCon{utf8.byte((128 .|. (U32.shrn(code, 6n) .&. 63 : U32) : U32)), SCon{utf8.byte((128 .|. (code .&. 63 : U32) : U32)), SNil{}}}}} -def utf8.put.3(three: Bool, +code: U32) -> String: +def utf8.put.three(three: Bool, +code: U32) -> String: match three: case True{}: - utf8.3(code) + utf8.three(code) case False{}: - utf8.4(code) + utf8.four(code) -def utf8.put.2(two: Bool, +code: U32) -> String: +def utf8.put.two(two: Bool, +code: U32) -> String: match two: case True{}: - utf8.2(code) + utf8.two(code) case False{}: - utf8.put.3(U32.is_lt(code, 65536), code) + utf8.put.three(U32.is_lt(code, 65536), code) def utf8.put.ascii(ascii: Bool, +code: U32) -> String: match ascii: case True{}: - utf8.1(code) + utf8.one(code) case False{}: - utf8.put.2(U32.is_lt(code, 2048), code) + utf8.put.two(U32.is_lt(code, 2048), code) def utf8.put(+code: U32) -> String: utf8.put.ascii(U32.is_lt(code, 128), code) diff --git a/tests/check.bend b/tests/check.bend index 57eb7bb..f4c408c 100644 --- a/tests/check.bend +++ b/tests/check.bend @@ -2,7 +2,7 @@ # entry, so this is also the "no main to run" case: bend checks the file clean # and then exits 1 from the emit, and ez has to read that as a pass. import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../ez/quiet.bend as Q import ../check/kit.bend as Check diff --git a/tests/cli.bend b/tests/cli.bend index a1538ee..6cad227 100644 --- a/tests/cli.bend +++ b/tests/cli.bend @@ -3,7 +3,7 @@ # checked, run, tested, and removed again. The remote is taken away before the # check, so nothing here can quietly be falling back to the network. import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../io/file.bend as F import ../ez/quiet.bend as Q import ../check/kit.bend as Check diff --git a/tests/fetch.bend b/tests/fetch.bend index e7b3d1d..7dd9883 100644 --- a/tests/fetch.bend +++ b/tests/fetch.bend @@ -6,7 +6,7 @@ # unit tests beside the code are about what can be said without one. import Base import ../hub/hub.bend as Hub -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../check/kit.bend as Check import ../check/world.bend as W diff --git a/tests/fresh.bend b/tests/fresh.bend index b5a765f..d10ff44 100644 --- a/tests/fresh.bend +++ b/tests/fresh.bend @@ -52,7 +52,7 @@ # was not needed, and is not allowed to pass a binary from a toolchain that is # gone. import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../io/file.bend as F import ../ez/cache.bend as C import ../check/kit.bend as Check diff --git a/tests/git.bend b/tests/git.bend index aefd500..9b5fb3e 100644 --- a/tests/git.bend +++ b/tests/git.bend @@ -4,7 +4,7 @@ # are compared file by file, because the claim is that they are the same # package and not merely two packages that both work. import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../io/file.bend as F import ../ez/quiet.bend as Q import ../check/kit.bend as Check diff --git a/tests/hub.bend b/tests/hub.bend index ef05e7c..b803390 100644 --- a/tests/hub.bend +++ b/tests/hub.bend @@ -3,7 +3,7 @@ # the whole point of ez: bend resolves a hub import during the check, and a nix # sandbox has no network to do it with. import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../io/file.bend as F import ../sha/sha.bend as Sha import ../doctor/plan.bend as DP diff --git a/tests/init.bend b/tests/init.bend index bc55ba2..a68ebe5 100644 --- a/tests/init.bend +++ b/tests/init.bend @@ -2,7 +2,7 @@ # checks and runs, and the library under `src/` it imports. A second run is # refused and leaves everything it found. import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../io/file.bend as F import ../ez/quiet.bend as Q import ../check/kit.bend as Check diff --git a/tests/nix.bend b/tests/nix.bend index 322a596..957f9a1 100644 --- a/tests/nix.bend +++ b/tests/nix.bend @@ -3,7 +3,7 @@ # fixed-output fetches. This is the gap ez exists to close — bend resolves a # hub import during the check, inside `book_load`, and a nix build cannot. import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../io/file.bend as F import ../sha/sha.bend as Sha import ../ez/quiet.bend as Q diff --git a/tests/publish.bend b/tests/publish.bend index 9869b21..77f416f 100644 --- a/tests/publish.bend +++ b/tests/publish.bend @@ -6,7 +6,7 @@ # The hub is check/oracle.bend, never the real one. `bend --publish` uploads, # and uploading someone's tree to a public hub is not a thing a test does. import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../io/file.bend as F import ../ez/quiet.bend as Q import ../check/kit.bend as Check diff --git a/tests/publishing.bend b/tests/publishing.bend index 2259017..0ac2826 100644 --- a/tests/publishing.bend +++ b/tests/publishing.bend @@ -8,7 +8,7 @@ # since a dirty tree is refused before anything is sent, or reach # check/liar.bend, a `bend` that uploads nothing. import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../io/file.bend as F import ../ez/quiet.bend as Q import ../pub/plan.bend as P diff --git a/tests/relock.bend b/tests/relock.bend index 4edd744..edc8839 100644 --- a/tests/relock.bend +++ b/tests/relock.bend @@ -7,7 +7,7 @@ # tree away and asks again: the lock fetches it at the ledger's rev and # checks it. import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../io/file.bend as F import ../ez/quiet.bend as Q import ../check/kit.bend as Check diff --git a/toml/toml.bend b/toml/toml.bend index 7467daa..18e01be 100644 --- a/toml/toml.bend +++ b/toml/toml.bend @@ -12,7 +12,7 @@ # eztoml writes it (`render`). That form is the TOML ez wrote before eztoml # 0.4, so an old ledger or lock and a new one read to the same sections. import Base -import 0xb652b3fca73c8a28ae49abaa395bb530/main.bend as E +import 0xd79254973edee82bcf56616220876efe/main.bend as E # a key and the string written for it type Kv is Data: diff --git a/tool/PROOF.bend b/tool/PROOF.bend index fa63485..7eac2c2 100644 --- a/tool/PROOF.bend +++ b/tool/PROOF.bend @@ -228,14 +228,14 @@ def Laws.tool_builds_on_miss(w, ok, miss): # LAW: a record with no commit reuses nothing, whatever is on record law no_rev: - for was: Key.Key + for was: Key.Stamp for +f: String for +b: String - {Key.reuse(was, Key.Key{"", f, b}) == False{} : Bool} + {Key.reuse(was, Key.Stamp{"", f, b}) == False{} : Bool} def no_rev(was, _f, _b): match was: - case Key.Key{_r0, _f0, _b0}: + case Key.Stamp{_r0, _f0, _b0}: {==} # LAW: an `and` with a False right half is False @@ -258,9 +258,9 @@ law unrevved_miss: def unrevved_miss(w, none): %Equal.sym(String, TP.rev(w), "", none) - : {Bool.and(TP.there(w), Key.reuse(TP.was(w), Key.Key{_, TP.file(w), TW.bend(w)})) + : {Bool.and(TP.there(w), Key.reuse(TP.was(w), Key.Stamp{_, TP.file(w), TW.bend(w)})) == False{} : Bool} - %Equal.sym(Bool, Key.reuse(TP.was(w), Key.Key{"", TP.file(w), TW.bend(w)}), False{}, + %Equal.sym(Bool, Key.reuse(TP.was(w), Key.Stamp{"", TP.file(w), TW.bend(w)}), False{}, no_rev(TP.was(w), TP.file(w), TW.bend(w))) : {Bool.and(TP.there(w), _) == False{} : Bool} and_false(TP.there(w)) diff --git a/tool/plan.bend b/tool/plan.bend index f270fa5..29ea95a 100644 --- a/tool/plan.bend +++ b/tool/plan.bend @@ -705,11 +705,11 @@ def name(+world: TW.World) -> String: Tgt.out.name(name.raw(world)) # what the binary is made from: the commit, the file and the bend (EZ-TOOL-2) -def key(+world: TW.World) -> Key.Key: - Key.Key{rev(world), file(world), TW.bend(world)} +def key(+world: TW.World) -> Key.Stamp: + Key.Stamp{rev(world), file(world), TW.bend(world)} # the directory a record's binary lives in, named by the record -def stamp.of(key: Key.Key) -> String: +def stamp.of(key: Key.Stamp) -> String: String.take(Sha.hex(Key.show(key)), 16n) # the directory of this record's binary @@ -724,7 +724,7 @@ def key.at(+world: TW.World) -> String: bdir(world) ++ "/key" # the binary's record as it was written, none when there is none -def was(+world: TW.World) -> Key.Key: +def was(+world: TW.World) -> Key.Stamp: Key.read(String.trim(TW.text.or(read.got(world, key.at(world))))) # whether the binary is there diff --git a/tool/run.bend b/tool/run.bend index 29949db..8462636 100644 --- a/tool/run.bend +++ b/tool/run.bend @@ -19,7 +19,7 @@ # `sync` asks the planner which pins to install (`TP.sync`) and installs # each in turn as `ez tool install ` would. import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R import ../io/file.bend as F import ../lock/run.bend as Run import ../lock/plan.bend as LP @@ -178,7 +178,7 @@ def compile.said(ok: Bool, +why: String, +text: String) -> IO(Unit): # `bend -o ` under the memory cap, with the checkout's library def compile(+lib: String, +file: String, +out: String) -> IO(Unit): do IO: - +on : Bool <- Cap.ok() + +on : Bool <- Cap.ready() Cap.warn.err(on) +g : String <- Cap.gb() _mk : String <- R.exec(["mkdir", "-p", P.dir(out)])