diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 07d855f..e52c905 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 diff --git a/README.md b/README.md index 6e6fbad..d3757e5 100644 --- a/README.md +++ b/README.md @@ -21,7 +21,7 @@ mkdir -p bin BEND_LIB=$PWD/.ez/lib bend ez/main.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..c1cb48f 100644 --- a/SPEC.md +++ b/SPEC.md @@ -162,7 +162,7 @@ EZ-RES-5 and EZ-RES-8 are proved in the same way. Their laws are over `P.ledger. EZ-DOC-4 is proved for a plain lock and for `ez lock --upgrade`. `after` (`lock/LAWS.bend`) is the World a lock leaves for the next to read: a refused lock leaves the World it read; one that succeeded leaves every tree it laid read from BEND_LIB with the bytes laid, and an upgrade also leaves the ledger it wrote, the committed sources as it rewrote them, and `.gitignore` as it left it. The remote does not change between the two runs: every question the second upgrade asks a remote is answered as the first run's answers say. Run again on that World, `ez lock --upgrade` writes the same bytes to ez.lock.toml (`upgrade_idempotent`), renders the same ledger model (`reupgrade_moves_nothing`), so writes no ez.toml (`upgrade_settles`), lays nothing new (`reupgrade_lays_nothing`), and writes no path but the lock (`reupgrade_writes_only_lock`), the last for a ledger whose vendored hashes hold no newline, as EZ-VEN-1's text layer requires. Each rests on the ez.toml the first run wrote reading back as the model it rendered, which is EZ-LED-4, and each takes that as its premise `ReadsBack` (EZ-TRUST-8). The key step is that a pin at its own tip is kept: the second run asks each selected pin the question the first asked, gets the tip it moved to, and checks the tree out again, which agrees with the hash, narHash and root the first run wrote. That a vendored tree laid under `.ez/lib` is read from BEND_LIB holds when BEND_LIB is `.ez/lib`, its default; with BEND_LIB elsewhere it is cloned again, and `clone_reproduces` says the lock is the same. EZ-FETCH-1 is proved over the plan `ez fetch` runs (`fetch/plan.bend`): every tree it lays holds the files the lock records under that hash, in the lock's order, each with a text whose digest equals the lock's sum for it (`fetch_lays_the_lock`). The law asks the same of a hub body and a git file, and a digest that equals the lock's sum starts with it, so it covers those halves of the row. A git package is laid only from a checkout that weighed to the narHash the lock records for it (`fetch_lays_weighed`), which is a lock that records one and a checkout whose narHash is that one (`fetch_weighs_the_checkout`); any other checkout stops the package with the reason (`fetch_refuses_unweighed`), and a stopped package refuses the fetch, which lays nothing (EZ-OUT-2). So a fetch pins the tree around the bytes it lays, the tree nix rebuilds the package from, and not only the bytes. A tree already under BEND_LIB is checked file by file before it is kept, and one that fails is fetched again rather than trusted; it was not fetched, so it has no checkout to weigh. That the interpreter reads what the hub served and what the checkout holds, weighs the checkout as `Nar.path` does, and lays each text as the plan says, is EZ-TRUST-2. -EZ-TOOL-1 to EZ-TOOL-9 are proved over the plan `ez tool run`, `install` and `upgrade` run (`tool/plan.bend`), over what it resolves a target to, and over the words `ez tool run` and `ez run` hand on (`ez/args.bend`). `ez run` starts bend on the entry ez.toml names, or `main.bend` when it names none, with every word after `run` (`run_starts_entry`, `run_starts_main`), a line `ez/start.bend` decides from the ledger the interpreter read and the words it was given. What the laws take from the interpreter is EZ-TRUST-2: that it asks `git status` with `--untracked-files=normal`, so an untracked file counts whatever the repository hides; that it reads the real path, the checkout's top and HEAD as git gives them; that it starts the program last and exits with its status, and exits 1 when a fetch, build or link it runs fails; and that `ez tool run` and `ez run` are handed the words the runtime passes them (`Args.tool.rest` and `Args.run.line` over `IO.args()`), and `ez run`'s line run with the project's BEND_LIB in front of it (`Env.line`); and that a build runs bend with the library the plan names as BEND_LIB, so a plain repository's hub imports are fetched there by bend, which checks each against its name. +EZ-TOOL-1 to EZ-TOOL-9 are proved over the plan `ez tool run`, `install` and `upgrade` run (`tool/plan.bend`), over what it resolves a target to, and over the words `ez tool run` and `ez run` hand on (`share/args.bend`). `ez run` starts bend on the entry ez.toml names, or `main.bend` when it names none, with every word after `run` (`run_starts_entry`, `run_starts_main`), a line `ez/start.bend` decides from the ledger the interpreter read and the words it was given. What the laws take from the interpreter is EZ-TRUST-2: that it asks `git status` with `--untracked-files=normal`, so an untracked file counts whatever the repository hides; that it reads the real path, the checkout's top and HEAD as git gives them; that it starts the program last and exits with its status, and exits 1 when a fetch, build or link it runs fails; and that `ez tool run` and `ez run` are handed the words the runtime passes them (`Args.tool.rest` and `Args.run.line` over `IO.args()`), and `ez run`'s line run with the project's BEND_LIB in front of it (`Env.line`); and that a build runs bend with the library the plan names as BEND_LIB, so a plain repository's hub imports are fetched there by bend, which checks each against its name. EZ-OUT-1 is proved for every command, each over the end its planner, or the pure half of its interpreter, gives it. A planner's plan ends with an outcome, and `P.status` is the status the interpreter exits with (`Run.end`): `ez init`, `ez add`, `ez remove`, `ez lock`, plain or `--upgrade`, `ez fetch`, `ez publish` and `ez doctor` exit 1 exactly when their planner refuses, or for doctor fails the command, and 0 when it does not (`init_exits_as_it_refuses`, `add_exits_as_it_refuses`, `remove_exits_as_it_refuses`, `lock_exits_as_it_refuses`, `fetch_exits_as_it_refuses`, `pub_exits_as_it_refuses`, `doctor_exits_as_it_fails`). `ez tool run`, `install` and `upgrade` exit with `TP.code` of the plan's end and the status of the program the plan started: a refusal exits 1 whatever a program would have said, since none is started (`tool_refusal_status_one`), `ez tool run` that goes on exits with the program's status (`tool_run_status_is_program`), and `install` and `upgrade` that go on exit 0 (`tool_link_status_zero`). `ez tool sync` exits 1 exactly when it refuses (`sync_exits_as_it_refuses`), which it does with no ez.toml (`sync_needs_ledger`); each install it runs ends as `ez tool install` does, so the first that refuses ends the sync with 1. `ez check`, `ez build`, `ez run`, `ez test` and `ez prove` are not planners. `ez check`, `ez build` and `ez run` first decide from ez.toml what to start (`ez/start.bend`): with no ez.toml, or one that does not parse, each refuses, starts nothing and exits 1 (`start_needs_ledger`, `start_needs_parse`). `ez check`, `ez build`, `ez test` and `ez prove` end with an outcome `ez/ends.bend` makes from what bend answered, and exit 1 exactly when the check did not pass, bend did not exit 0, or a file did not pass (`check_exits_as_it_passes`, `build_exits_as_bend`, `gate_exits_as_it_counts`). `ez run` exits with `S.code` of what it decided and the status of the program it started: 1 for a refusal, since none is started (`run_refusal_exits_one`), and the program's own status otherwise, as `cargo run` does (`run_exits_with_program`); a program bend could not check is bend's failure, and exits with bend's status. `ez lock --package` without `--upgrade` exits 1 before anything is read (`package_needs_upgrade`). Before any command runs, `ez/line.bend` decides how the line ends. Help exits 0: a bare `ez`, a line that selected no command, and every request for help Shake answers (`bare_exits_zero`, `help_exits_zero`). A misused line exits 1: a bare group such as `ez tool`, and every line Shake refuses, an unknown command or flag, a word too many, a missing argument or value, an option given twice, or `ez help` of a word that names no command there, which Shake refuses as `Unexpected` rather than answering as a request for help (`group_exits_one`, `usage_error_exits_one`; the last case is shake's SHAKE-PARSE-8, trusted as EZ-TRUST-7). A line that names a command runs it, with the bindings Shake made for that command, and leaves the status to it (`command_runs`, `command_ends_its_own`). What the laws take from the interpreter is EZ-TRUST-2: that it exits with the status these functions give; that it hands `TP.code` the status the program exited with, and `S.code` the status bend exited with, 128 plus the signal for one a signal ended and 127 for one that could not be started; that a failure it meets itself, a write the system rejects, a build or link that fails, a fetch inside `ez tool`, or a loop that runs out of fuel, exits 1; and that the answer `ez/ends.bend` reads is what bend printed and the status it exited with. A flag the native runtime takes is not ez's: the runtime answers `--help`, `--threads` and `--gpu` anywhere on the line before ez sees it, `--help` with its own usage and exit 0. EZ-OUT-2 is proved for every command, each over the plan its planner makes. `ez lock`, plain or `--upgrade`: a World on which the planner refuses has a plan with no write, lay or remove effect, so it writes nothing, not the lock, ez.toml, `.gitignore`, a source or a tree. The upgrade's refusals (a pin off its history, a drift, a hub digest that does not match, an answer IO could not give, an unknown `--package`, a ledger model that is not renderable) and the lock's refusals after an upgrade are all such Worlds. `ez remove` and `ez init`: the same, for every World on which their planners refuse: no ledger, one that does not parse, a name it does not have, or a ledger left that is not renderable, for `ez remove`; a ledger that is there, a name or entry a ledger cannot carry, or a description holding a newline, for `ez init`. `ez add`: the same for every World on which its planner refuses, before a question (no ledger, one that does not parse, a target that names nothing, a `--rename` that is no key or a clash the ledger decides) or after (a ref the remote does not have, an entry the checkout lacks, a walk that refuses, a name `Named.why.as` objects to, a ledger that is not renderable), so a refused add lays no tree, not even in the cache (`add_refusal_writes_nothing`). `ez add @` is planned by `H.plan` (add/hub.bend), and the same holds of it: no ledger, one that does not parse, a key `Named.hub.why` objects to, a name the hub has no package for or answers with no `0x` name, a package whose manifest does not hash to that name, an entry the package lacks, or a ledger that is not renderable, and it lays no tree and no name's file (`add_named_refusal_writes_nothing`, `add_named_refuses_unknown`, `add_named_refuses_unhashed`, `add_named_refuses_manifest`, `add_named_refuses_clash`, `add_named_entry_absent`, `add_named_refuses_unrenderable`). `ez fetch`: the same for every World on which its planner refuses (no ledger, no lock, a package that could not be fetched, one whose files do not match the lock, leave the package or do not hash to its name, or one whose checkout does not weigh to the lock's narHash), so a refused fetch lays no tree, not one of a package that checked before the one that failed, and removes none already under BEND_LIB (`fetch_refusal_writes_nothing`). `ez tool run`, `install` and `upgrade`: the same for every World on which their planner refuses (nowhere to link, no cache root, a project ledger that does not parse, a target that names nothing or whose slug could leave the cache, a name the lock does not pin or pins at no commit, a checkout git could not give, a file to build that is not in the checkout, a package name that is not a TOML bare key, an ez project's build with no lock), so a refused tool command lays no checkout under the cache, builds nothing and links nothing (`tool_refusal_writes_nothing`, and `tool_missing_entry_writes_nothing` for a missing file); and `ez tool sync`, which refuses before it installs anything when the ledger does not parse or names a pin the lock lacks (`sync_refusal_installs_nothing`). `ez publish`: its plan writes no file at all, only the two lines a publish that agreed says, so a refused publish writes nothing (`pub_refusal_writes_nothing`), and one refused because a hub import is off the hub has a plan with no effect at all (`pub_offhub_writes_nothing`); and every refusal that can be decided before the upload is decided before it, so a refused publish sends nothing unless bend's own answer is what it refuses (EZ-PUB-1, EZ-PUB-2, EZ-PUB-5). A sync that goes on runs one install per pin, each its own plan, so a later install that refuses leaves the earlier ones installed, as `cargo install a b` does. A write the interpreter attempts and the system rejects is EZ-OUT-1's, and what it leaves is EZ-TRUST-2's. EZ-PUB-1 and EZ-PUB-2 are proved over the plan `ez publish` runs (`pub/plan.bend`). A World whose git status names a path, or that git cannot answer, is refused outright: nothing more is asked and nothing is sent (`pub_dirty_refuses`, `pub_gitless_refuses`, `pub_stop_sends_nothing`). A package holding a file git does not track as unchanged never reaches the upload (`pub_stray_sends_nothing`), and a World that does not reach it refuses (`pub_unsent_refuses`). A publish succeeds only when the upload's answer agrees with the hash ez computed (`pub_needs_agreement`), and the laws over `agrees` say what agreeing is: at least one line is a `0x` name and every such line is ez's hash. It then says ez's hash, never bend's (`pub_reports_ours`). bend 2.0.27 cannot report a package's hash without uploading it, so the upload is the last question the planner asks and the check is made on its answer; EZ-PUB-2 promises that a disagreement exits 1 and prints no import line, not that nothing was sent. What the laws take from the interpreter is EZ-TRUST-2: that it asks `git status` with `--untracked-files=normal` and `git ls-files -v` in the project, and runs the upload with the entry the planner names. @@ -203,6 +203,6 @@ These assumptions sit outside the proofs. They are the complete list of Trusted | 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. 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..96a71f7 100644 --- a/add/PROOF.bend +++ b/add/PROOF.bend @@ -25,7 +25,7 @@ import ../pkg/path.bend as Path import ../git/git.bend as Git import ../ez/target.bend as Tgt import ../ez/named.bend as Named -import ../sha/sha.bend as Sha +import ../share/sha.bend as Sha import ../check/eq.bend as Eq import ../check/str.bend as Str import ../pkg/PROOF.bend as Pk @@ -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.Item>: 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.Item> 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.Item> 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.Item> 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.Item>, 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.Item>} 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.Item>, List<&2, K.Item>, ys => K.Item{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.Item>: 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.Item>, 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.Item> 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.Item> 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.Item> 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.Item> 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..fc15f1d 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.Item>, 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.Item>, +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.Item>) -> 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.Item>) -> 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.Item>) -> 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.Item>, +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.Item>, +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.Item>, +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.Item>, +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.Item>, +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.Item>: 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.Item>: verdict.files(decide(world)) # the dependency `ez add @` records on a World diff --git a/add/plan.bend b/add/plan.bend index af37444..552b19c 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.Item>, +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..923219d 100644 --- a/check/oracle.bend +++ b/check/oracle.bend @@ -17,9 +17,9 @@ # One connection is served at a time, each answer states its length and closes # the socket, and the oracle stops of its own accord after a million of them. import Base -import ../sha/sha.bend as Sha +import ../share/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-add-planner.md b/docs/rfc/ez-add-planner.md index df3bba3..75dfb2f 100644 --- a/docs/rfc/ez-add-planner.md +++ b/docs/rfc/ez-add-planner.md @@ -438,7 +438,7 @@ The rewritten `K.pkg_of`, and `K.of` over every tracked file, give the hash, roo - A remote's checkout lives at `///src` with its record at `///rev`, and every binary at `/bin//.out`, with its record beside it, where `` is `/` or `/local`. A cached checkout is read when its record names the commit and it has an ez.toml; otherwise the interpreter clones it into a scratch directory, the plan lays its texts, and the record goes last, so a checkout cut short is cloned again. The NAR hash `Clone` answers with is not used. - The laws, all in `tool/LAWS.bend`: `tool_refusal_writes_nothing`, `sync_refusal_installs_nothing` (EZ-OUT-2); `bin_dir_ez`, `bin_dir_xdg`, `bin_dir_home`, `bin_dir_none`, `tool_links_in_bin_dir`, `tool_needs_bin_dir` (EZ-TOOL-1); `tool_reuses_record`, `tool_builds_on_miss` (EZ-TOOL-2, beside the key laws in `ez/LAWS.bend`); `local_rev_dirty`, `local_rev_unchecked`, `local_rev_elsewhere`, `tool_unrevved_builds` (EZ-TOOL-3); `tool_pin_src`, `tool_pin_rev`, `tool_pin_url`, `tool_pin_over`, `tool_free_src`, `tool_free_rev`, `tool_path_rev`, `local_rev_clean` (EZ-TOOL-4); `tool_run_exits_with_program`, `tool_refusal_exits_one` (EZ-TOOL-5); `tool_link_never_runs` (EZ-TOOL-6); `file_pin_bin`, `file_pin_entry`, `file_bin`, `file_entry`, `file_main`, `tool_builds_file`, `out_name_own`, `out_name_app`, `tool_links_named`, `tool_refuses_unsafe_name` (EZ-TOOL-7); `remote_refuses_slug`, `tool_refuses_bad_slug`, `tool_refuses_nowhere` (EZ-TOOL-8); `tool_rest_dash`, `tool_rest_word`, `tool_rest_none`, `tool_run_passes_words`, `run_line_rest` (EZ-TOOL-9). EZ-TOOL-1 and EZ-TOOL-3 to EZ-TOOL-9 are proved. A law that a condition refuses walks `decide` stage by stage (`pre_*`, `co_*` in `tool/PROOF.bend`), since each stage before the one that checks it stops, waits or goes on. - `ez run` hands the entry `Args.run.line(entry, as)`, `bend ` and every word after `run`, so EZ-TOOL-9's second half is a law about that line. -- `ez/cap.bend`, `ez/env.bend` and `ez/args.bend` are imported as `../ez/…` from every file, as `ez/target.bend` is, since `tool/run.bend` reaches them by that path and bend gives a file one namespace per import closure. +- `share/cap.bend`, `share/env.bend` and `share/args.bend` live outside every entry directory. Bend 2.0.28 names a file from the importer's real path, so a file in an entry's own directory is one name from there and another from outside it. - `ez doctor` has no tool check, so there is nothing of it to convert here. **Update (WP11, `ez publish`).** `ez publish` is in planner form in the same shape: `pub/world.bend` (the World and the questions), `pub/plan.bend` (pure, with the decision functions of the old `pub/pub.bend`), and `pub/run.bend` (the interpreter), which `ez/cmd.bend` dispatches to. `pub/pub.bend` is deleted. Where it differs from the commands above: diff --git a/docs/rfc/ez-spec.md b/docs/rfc/ez-spec.md index 37fb727..1f9c3a5 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, 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 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. @@ -507,7 +507,7 @@ These assumptions sit outside the proofs. They are the complete list of Trusted | 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. 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`. diff --git a/doctor/plan.bend b/doctor/plan.bend index ada6165..7970fc8 100644 --- a/doctor/plan.bend +++ b/doctor/plan.bend @@ -56,7 +56,7 @@ import ../lock/plan.bend as P import ../lock/world.bend as W import ../lock/lock.bend as L import ../ledger/manifest.bend as M -import ../ez/args.bend as Args +import ../share/args.bend as Args # one thing doctor looked at: what to print, and whether it is a problem type Note is Data: diff --git a/doctor/run.bend b/doctor/run.bend index 5497aa9..e0679a2 100644 --- a/doctor/run.bend +++ b/doctor/run.bend @@ -14,10 +14,10 @@ # 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 +import ../share/args.bend as Args import ../lock/run.bend as Run import ../lock/world.bend as W import ../lock/lock.bend as L 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..1e80f1f 100644 --- a/ez.toml +++ b/ez.toml @@ -4,11 +4,11 @@ entry = "ledger/manifest.bend" bin = "ez/main.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..17eedee 100644 --- a/ez/LAWS.bend +++ b/ez/LAWS.bend @@ -13,8 +13,8 @@ import ./clock.bend as Clock import ../ez/target.bend as Tgt import ./key.bend as K import ../ledger/manifest.bend as M -import ../ez/pin.bend as Pin -import ../ez/env.bend as Env +import ../share/pin.bend as Pin +import ../share/env.bend as Env import ../pkg/path.bend as P import ../ez/named.bend as Named import ../pkg/pkg.bend as Pkg @@ -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..61c78e9 100644 --- a/ez/PROOF.bend +++ b/ez/PROOF.bend @@ -7,11 +7,11 @@ # computation itself. import Base import ./gate.bend as G -import ../ez/pin.bend as Pin +import ../share/pin.bend as Pin import ../ez/target.bend as Tgt import ../ez/named.bend as Named import ../pkg/pkg.bend as Pkg -import ../ez/env.bend as Env +import ../share/env.bend as Env import ../pkg/path.bend as P import ../ledger/manifest.bend as M import ./key.bend as K @@ -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..705318f 100644 --- a/ez/cache.bend +++ b/ez/cache.bend @@ -3,9 +3,9 @@ # 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 +import ../share/env.bend as Env # the toolchain: bend's version and the C compiler it would hand its C to def tool() -> IO(String): diff --git a/ez/clock.bend b/ez/clock.bend index 2a337d2..7ef275e 100644 --- a/ez/clock.bend +++ b/ez/clock.bend @@ -11,8 +11,8 @@ # programs ez already runs the way it runs `find` and `mkdir`, with no shell # between. import Base -import 0x103d0af04de36ab98b311e537366ec67/main.bend as R -import ../ez/env.bend as Env +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R +import ../share/env.bend as Env # how many seconds a whole run may take. Five minutes is what the gate is held # to; a tree that honestly needs longer says so in EZ_DEADLINE, and "0" turns diff --git a/ez/cmd.bend b/ez/cmd.bend index 573ed8c..015324f 100644 --- a/ez/cmd.bend +++ b/ez/cmd.bend @@ -1,18 +1,18 @@ # ez/cmd: what each subcommand does. Everything that touches the network or the # file system goes through a process effect, because bend links no TLS and # 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. +# ez reads, and `share/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 -import ../ez/env.bend as Env -import ../ez/cap.bend as Cap -import ../ez/args.bend as Args +import ../share/env.bend as Env +import ../share/cap.bend as Cap +import ../share/args.bend as Args import ../ez/ends.bend as E import ../ez/start.bend as S -import ../ez/pass.bend as Pass +import ../share/pass.bend as Pass import ../init/run.bend as InitRun import ../remove/run.bend as RemoveRun import ../add/run.bend as AddRun @@ -47,7 +47,7 @@ def report.capped(+why: String, +out: String) -> IO(Unit): Run.end(E.ran(out)) # `ez check` and `ez run` are not capped, and `ez build` is. The wall -# `ez/cap.bend` exists for is bend's C backend: emitting the C for a large +# `share/cap.bend` exists for is bend's C backend: emitting the C for a large # program peaked at 18.8 GB here and an uncapped one reached 35 GB. `ez check` # emits JS and `ez run` interprets, so neither reaches that backend; and what # `ez run` spends after that is the user's own program spending it, which is 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/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..82426dd 100644 --- a/ez/main.bend +++ b/ez/main.bend @@ -9,14 +9,14 @@ # would take the flags meant for ez. import Base import 0x085b03c84ca37125e38dddede7b91e55/main.bend as Shake -import ../ez/args.bend as Args +import ../share/args.bend as Args import ./cmd.bend as Cmd import ./test.bend as Test import ./prove.bend as Prove import ../doctor/run.bend as DoctorRun import ../tool/run.bend as ToolRun import ../tool/world.bend as TW -import ../ez/say.bend as Say +import ../share/say.bend as Say import ../io/file.bend as F import ../ez/line.bend as L diff --git a/ez/prove.bend b/ez/prove.bend index 665bfa0..a5665ce 100644 --- a/ez/prove.bend +++ b/ez/prove.bend @@ -9,10 +9,10 @@ # 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 ../ez/args.bend as Args -import ../ez/env.bend as Env -import ../ez/cap.bend as Cap +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R +import ../share/args.bend as Args +import ../share/env.bend as Env +import ../share/cap.bend as Cap import ./quiet.bend as Q import ./sorted.bend as Sort import ../ez/ends.bend as E diff --git a/ez/start.bend b/ez/start.bend index 92998d0..1f9a43f 100644 --- a/ez/start.bend +++ b/ez/start.bend @@ -7,7 +7,7 @@ # that it does so faithfully is EZ-TRUST-2. import Base import ../ledger/manifest.bend as M -import ../ez/args.bend as Args +import ../share/args.bend as Args # which of the three commands is asking, with what it was told: where a # build goes, and every word of the line for a run diff --git a/ez/test.bend b/ez/test.bend index 59838cb..baea27d 100644 --- a/ez/test.bend +++ b/ez/test.bend @@ -7,10 +7,10 @@ # # 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 +import ../share/env.bend as Env +import ../share/cap.bend as Cap import ./gate.bend as G import ./quiet.bend as Q import ./clock.bend as Clock diff --git a/fetch/LAWS.bend b/fetch/LAWS.bend index fa3d45a..9c6f4df 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.Item> for +h: String for +why: String for ls: List<&2, W.Source> diff --git a/fetch/PROOF.bend b/fetch/PROOF.bend index 0d47264..3c8223d 100644 --- a/fetch/PROOF.bend +++ b/fetch/PROOF.bend @@ -1,7 +1,7 @@ # fetch: the proofs. `bend PROOF.bend` is the gate. # # The plan is `plan.led(ledger, lock, w)`: no ledger, then no lock, is a plan -# with no effect, and otherwise the plan is `plan.parts` of every package of +# with no effect, and otherwise the plan is `parts.plan` of every package of # the lock, which seals the effects of the verdicts with how they end. A # sealed plan that refuses has no effect, so the refusal law is case splits. # Every law about what a fetch lays is a law about `effects.of` over the @@ -21,7 +21,7 @@ import ../lock/up.bend as Up import ../add/PROOF.bend as AddP import ../pkg/pkg.bend as K import ../pkg/path.bend as Path -import ../sha/sha.bend as Sha +import ../share/sha.bend as Sha import ../check/eq.bend as Eq import ../check/str.bend as Str import ./LAWS.bend as Laws @@ -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.Item>} 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.Item>, List<&2, K.Item>, ys => K.Item{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.Item> 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.Item> 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.Item> 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.Item> 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.Item> 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.Item> for +h: String for +why: String for ls: List<&2, W.Source> diff --git a/fetch/plan.bend b/fetch/plan.bend index 7bae334..6b5e9d5 100644 --- a/fetch/plan.bend +++ b/fetch/plan.bend @@ -49,7 +49,7 @@ import ../lock/up.bend as Up import ../lock/lock.bend as L import ../pkg/pkg.bend as K import ../pkg/path.bend as Path -import ../sha/sha.bend as Sha +import ../share/sha.bend as Sha # --------------------------------------------------------------------------- # the questions @@ -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.Item>, 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.Item>, +root: String, +tree: List<&2, K.Source>) -> List<&2, W.Source>: match fs: case []: [] - case K.File{+at, _sum} <> t: + case K.Item{+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.Item: W.Source{at, +text} = src - K.File{at, Sha.hex(text)} + K.Item{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.Item>: 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.Item, got: W.Source) -> Bool: + K.Item{+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.Item>, 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.Item>, +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.Item>, 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.Item>, +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.Item>) -> 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.Item>, +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.Item>, +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.Item>, +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.Item>, +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.Item>, +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.Item>, +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.Item>, 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.Item>, +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.Item>, +hash: String, part: Part) -> Verdict: match part: case AskLaid{}: Stop{"ez: " ++ hash ++ " was never looked for under BEND_LIB"} @@ -674,7 +674,7 @@ def seal(es: List<&2, P.Effect>, outcome: P.Outcome) -> P.Plan: # the plan once every package and every name stands somewhere: the names # files, then the trees, and how the command ends. Each verdict is made once # and read by both halves. -def plan.parts(ps: List<&2, Pt>, +ms: List<&2, Nm>) -> P.Plan: +def parts.plan(ps: List<&2, Pt>, +ms: List<&2, Nm>) -> P.Plan: +vs = judged(ps) seal(names.lay(ms, effects.of(vs)), outcome.then(outcome.of(vs), names.outcome(ms))) @@ -701,7 +701,7 @@ def plan.lock(got: Maybe<&2, String>, +world: F.World) -> P.Plan: P.Plan{[], P.Refused{need.lock()}} case Some{_text}: +ss = F.sects(world) - plan.parts(parts.of(ss, world), name.parts.of(ss, world)) + parts.plan(parts.of(ss, world), name.parts.of(ss, world)) # the plan: a missing ledger, then a missing lock, refused before the rest def plan.led(led: Bool, got: Maybe<&2, String>, +world: F.World) -> P.Plan: @@ -781,7 +781,7 @@ type Step is Data: def step.asks(asks: List<&2, F.Ask>, ps: List<&2, Pt>, ms: List<&2, Nm>) -> Step: match asks: case []: - Run{plan.parts(ps, ms)} + Run{parts.plan(ps, ms)} case h <> t: Asking{h <> t} @@ -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.Item>: 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..328b356 100644 --- a/flake.lock +++ b/flake.lock @@ -7,11 +7,11 @@ ] }, "locked": { - "lastModified": 1790200275, - "narHash": "sha256-huYLnKbMUukFhFLypIXx/wLVU3EmgsUEe9l67mU6CDw=", + "lastModified": 1790482124, + "narHash": "sha256-Gv309ikt48M8cISbwSo6V0md2572iieIRiyl3noF1cA=", "owner": "bendlang", "repo": "bend", - "rev": "d37909174ebd664338ae3194799a9e0899dedd51", + "rev": "af569d4826913b2ce3557e9829ccad31fcf86f94", "type": "github" }, "original": { diff --git a/git/git.bend b/git/git.bend index 215565f..0ed162c 100644 --- a/git/git.bend +++ b/git/git.bend @@ -11,13 +11,13 @@ # 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 import ../pkg/path.bend as P import ../sha/nar.bend as Nar -import ../ez/say.bend as Say +import ../share/say.bend as Say # one `\t` row of what `git ls-remote` printed type Row is Data: diff --git a/hub/hub.bend b/hub/hub.bend index 9138d53..49c5b6d 100644 --- a/hub/hub.bend +++ b/hub/hub.bend @@ -2,12 +2,12 @@ # 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 ../sha/sha.bend as Sha +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 F +import ../share/sha.bend as Sha # The GET is ezhttp's. What is kept here is the answer's shape: a status on # its own first line and then the text, the shape a run answers with and the @@ -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> <- F.read(path) return get.file.got(m, path) # a url whose scheme decides where the body comes from diff --git a/lock/LAWS.bend b/lock/LAWS.bend index 19b326d..32e5674 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.Item> 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.Item} # 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.Item> 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.Item{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.Item> 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.Item{at, sum} <> fs} <> rest) == P.path.eq.why(hash, at) : String} # The planner (plan.bend) over the World (world.bend). Every law below is @@ -836,22 +835,22 @@ law relock_lays_nothing: # names once, as the interpreter lists each file once. # what the upgrade decides on a World. Law vocabulary: ez never calls it. -def up.next(world: W.World) -> Up.Next: +def next.of(world: W.World) -> Up.Next: W.World{args, +ledger, _listing, _replies, ups} = world W.next(args, ledger, ups) # the hashes whose trees the upgrade commits under `.ez/lib`: the vendored # hashes of the dependencies it leaves def vends(world: W.World) -> List<&2, String>: - Up.next.vends(up.next(world)) + Up.next.vends(next.of(world)) # the hashes it moved, each with the hash that replaces it in an import def swaps(world: W.World) -> List<&2, U.Swap>: - Up.next.swaps(up.next(world)) + Up.next.swaps(next.of(world)) # the sources it read def found(world: W.World) -> List<&2, Up.Found>: - Up.next.found(up.next(world)) + Up.next.found(next.of(world)) # a file's text as the World answered it, "" when it did not def ignore.said(said: Up.Said) -> String: @@ -1041,16 +1040,16 @@ def tail(nms: List<&2, L.Name>, ts: List<&2, M.Tool>) -> List<&2, T.Sect>: # the document a lock renders: the `[lock]` table, every package's two tables # in hash order, then its names and every tool's table. Law vocabulary. -def lock.doc(nms: List<&2, L.Name>, ts: List<&2, M.Tool>, hub: String, ps: List<&2, L.Pack>) -> List<&2, T.Sect>: +def doc.lock(nms: List<&2, L.Name>, ts: List<&2, M.Tool>, hub: String, ps: List<&2, L.Pack>) -> List<&2, T.Sect>: 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.Item) -> L.Name: + K.Item{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.Item>) -> 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.Item: L.Name{nv, hash} = nm - K.File{nv, hash} + K.Item{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.Item>: match nms: case []: [] @@ -1438,7 +1437,7 @@ law lock_lays_named: # the origins of the ledger the lock is made from: ez.toml's for a plain # lock, the ledger the upgrade leaves for `--upgrade` def origins(world: W.World) -> List<&2, L.Origin>: - W.next.origins(up.next(world)) + W.next.origins(next.of(world)) # the package questions a step asks, none when it runs its plan def step.pkgs(st: P.Step) -> List<&2, W.Ask>: @@ -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.Item, 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..c4b444f 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.Item>} 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.Item>, List<&2, K.Item>, 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.Item>} 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.Item>, 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.Item>, List<&2, K.Item>, 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.Item{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.Item{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.Item>} def blocks_sort_perm(ns, ps, dis): - Equal.trans(List<&2, K.File>, + Equal.trans(List<&2, K.Item>, 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.Item>, List<&2, K.Item>, 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.Item>, 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.Item>, K.Item, + ys => K.Item{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.Item{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.Item> for +hh: String for +sh: L.Src - for +fh: List<&2, K.File> + for +fh: List<&2, K.Item> 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.Item>} {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.Item>} 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.Item>, List<&2, K.Item>, 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.Item>} {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.Item>} 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.Item>} 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.Item>} 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.Item>, 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.Item>} 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.Item> + {L.pair.files(L.file.pairs(fs)) == fs : List<&2, K.Item>} 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.Item{+at, +sum} <> +t: + Equal.cong(List<&2, K.Item>, List<&2, K.Item>, r => K.Item{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 @@ -3092,7 +3092,7 @@ law lock_hub_read: for +ts: List<&2, M.Tool> for +hub: String for +ps: List<&2, L.Pack> - {L.lock.hub(Laws.lock.doc(nms, ts, hub, ps)) == hub : String} + {L.lock.hub(Laws.doc.lock(nms, ts, hub, ps)) == hub : String} def lock_hub_read(_nms, _ts, _hub, _ps): {==} @@ -3116,7 +3116,7 @@ law lock_tools_read: for +ts: List<&2, M.Tool> for +hub: String for +ps: List<&2, L.Pack> - {M.tools(Laws.lock.doc(nms, ts, hub, ps)) == Laws.tools.canon(ts) : List<&2, M.Tool>} + {M.tools(Laws.doc.lock(nms, ts, hub, ps)) == Laws.tools.canon(ts) : List<&2, M.Tool>} def lock_tools_read(nms, ts, _hub, ps): Equal.trans(List<&2, M.Tool>, @@ -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.Item>) -> 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.Item> {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.Item{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.Item>} 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.Item>, List<&2, K.Item>, x => K.Item{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.Item> 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.Item> 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.Item> 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.Item, 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.Item, 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.Item, 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..fe8fea0 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.Item>} # 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.Item>: + Bool.pick(List<&2, K.Item>, Nat.is_eq(List.length(&2, String, ws), 2n), + [K.Item{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.Item>: match ls: case []: [] case h <> t: - List.append(&2, K.File, line.put(K.words(h)), manifest.files(t)) + List.append(&2, K.Item, 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.Item) -> T.Kv: + K.Item{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.Item>) -> 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.Item>) -> 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.Item: Pack{+hash, src, files} = package - K.File{hash, T.render(pack.sects.of(hash, src, K.files_of(files)))} + K.Item{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.Item>: 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.Item>) -> List<&2, String>: match bs: case []: [] - case K.File{_hash, text} <> t: + case K.Item{_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.Item>, 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.Item: Name{nv, hash} = name - K.File{nv, hash} + K.Item{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.Item>: 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.Item: T.Kv{k, v} = kv - K.File{k, v} + K.Item{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.Item>: 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.Item>: Pack{_h, _s, f} = package f diff --git a/lock/plan.bend b/lock/plan.bend index f3cf820..9d759c4 100644 --- a/lock/plan.bend +++ b/lock/plan.bend @@ -37,7 +37,7 @@ import ./lock.bend as L import ../ledger/manifest.bend as M import ../pkg/pkg.bend as K import ../pkg/path.bend as Path -import ../ez/pin.bend as Pin +import ../share/pin.bend as Pin # --------------------------------------------------------------------------- # the walk @@ -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.Item>) -> List<&2, String>: match fs: case []: [] - case K.File{at, sum} <> t: + case K.Item{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.Item>) -> Bool: match fs: case []: True{} - case K.File{at, _sum} <> t: + case K.Item{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.Item>) -> String: match fs: case []: "" - case K.File{+at, _sum} <> t: + case K.Item{+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..ef1a33f 100644 --- a/lock/run.bend +++ b/lock/run.bend @@ -13,13 +13,13 @@ # 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 import ../pkg/pkg.bend as K import ../pkg/path.bend as P -import ../ez/say.bend as Say +import ../share/say.bend as Say import ./lock.bend as L import ./world.bend as W import ./up.bend as Up @@ -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.Item>) -> 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.Item>) -> 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.Item> <- IO.pure(List<&2, K.Item>, 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.Item> <- IO.pure(List<&2, K.Item>, 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/up.bend b/lock/up.bend index 724c195..9e439a6 100644 --- a/lock/up.bend +++ b/lock/up.bend @@ -29,8 +29,8 @@ import ../git/git.bend as Git import ../pkg/pkg.bend as K import ../pkg/path.bend as Path import ../hub/hub.bend as Web -import ../sha/sha.bend as Sha -import ../ez/say.bend as Say +import ../share/sha.bend as Sha +import ../share/say.bend as Say # --------------------------------------------------------------------------- # questions and answers diff --git a/lock/world.bend b/lock/world.bend index 1231028..04e10cf 100644 --- a/lock/world.bend +++ b/lock/world.bend @@ -21,8 +21,8 @@ import ../ledger/upgrade.bend as U import ../ledger/manifest.bend as M import ../pkg/pkg.bend as K import ../hub/hub.bend as Web -import ../sha/sha.bend as Sha -import ../ez/say.bend as Say +import ../share/sha.bend as Sha +import ../share/say.bend as Say # the command as it was run: `--upgrade`, the name `--package` gave ("" for # none), and the directory it runs in, which is the project root. A relative @@ -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.Item>, 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.Item>, 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.Item>, 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.Item: Source{at, +text} = src - K.File{at, Sha.hex(text)} + K.Item{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.Item>: 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.Item>, 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.Item>, +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.Item>, +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.Item>, +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.Item, 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.Item, 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..8a681c2 100644 --- a/pkg/LAWS.bend +++ b/pkg/LAWS.bend @@ -5,14 +5,14 @@ import Base import ./pkg.bend as P import ./path.bend as Path -import ../sha/sha.bend as Sha +import ../share/sha.bend as Sha # a file put at a chosen place in a list: as many files pass in front of it as # the number says, and it lands at the end when the list runs out first. This # 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.Item, xs: List<&2, P.Item>) -> List<&2, P.Item>: 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.Item>) -> List<&2, P.Item>: 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.Item, xs: List<&2, P.Item>) -> 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.Item>) -> 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.Item + for t: List<&2, P.Item> + {P.dedup(f <> (f <> t)) == P.dedup(f <> t) : List<&2, P.Item>} # 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.Item + for t: List<&2, P.Item> + {List.is_empty(&2, P.Item, 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.Item> 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.Item>} # 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.Item> 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.Item> 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.Item> {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.Item + for t: List<&2, P.Item> 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.Item>} # 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.Item + for t: List<&2, P.Item> 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.Item>} diff --git a/pkg/PROOF.bend b/pkg/PROOF.bend index 5180c04..48c9070 100644 --- a/pkg/PROOF.bend +++ b/pkg/PROOF.bend @@ -15,43 +15,43 @@ import Base import ./pkg.bend as P import ../check/eq.bend as Eq import ./path.bend as Path -import ../sha/sha.bend as Sha +import ../share/sha.bend as Sha import ./LAWS.bend as Laws # LAW: one step of the deduplication, with the branch the pick takes given as # 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.Item + for b: P.Item + for t: List<&2, P.Item> 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.Item>} 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.Item>, 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.Item>, 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.Item + for r: List<&2, P.Item> {P.dedup.head(f, P.dedup.head(f, r)) == P.dedup.head(f, r) - : List<&2, P.File>} + : List<&2, P.Item>} 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.Item>, 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.Item + for -b: P.Item + for -t: List<&2, P.Item> for bb: Bool - {List.is_empty(&2, P.File, P.dedup.pick(bb, f, b <> t)) == False{} : Bool} + {List.is_empty(&2, P.Item, 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.Item + for r: List<&2, P.Item> + {List.is_empty(&2, P.Item, 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.Item + for +y: P.Item + for +z: P.Item 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.Item + for +b: P.Item 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.Item + for +b: P.Item 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.Item>} def ins.swap.nil(a, b, ba, eba, eab): match ba: case True{}: - Equal.trans(List<&2, P.File>, + Equal.trans(List<&2, P.Item>, 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.Item>, 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.Item>, P.file.ins(P.file.ins([], b), a), b <> (a <> []), - Equal.cong(Bool, List<&2, P.File>, + Equal.cong(Bool, List<&2, P.Item>, 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.Item>, 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.Item>, 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.Item>, P.file.ins(P.file.ins([], b), a), a <> (b <> []), - Equal.cong(Bool, List<&2, P.File>, + Equal.cong(Bool, List<&2, P.Item>, 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.Item + for +t: List<&2, P.Item> + for +a: P.Item + for +b: P.Item 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.Item>} 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.Item>, 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.Item>, 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.Item>, List<&2, P.Item>, 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.Item>, 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.Item>, 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.Item>, 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.Item>, 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.Item>, List<&2, P.Item>, 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.Item>, 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.Item>, 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.Item>, 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.Item>, 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.Item>, List<&2, P.Item>, 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.Item>, 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.Item>, 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.Item>, 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.Item>, 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.Item>, List<&2, P.Item>, 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.Item>, 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.Item>, 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.Item + for +t: List<&2, P.Item> + for +a: P.Item + for +b: P.Item 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.Item>} 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.Item>}, 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.Item>, 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.Item>, 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.Item>, List<&2, P.Item>, 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.Item>, 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.Item>, 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.Item>, 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.Item>, 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.Item + for +t: List<&2, P.Item> + for +a: P.Item + for +b: P.Item 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.Item>} 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.Item>}, 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.Item>, 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.Item>, 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.Item>, 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.Item>, 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.Item>, List<&2, P.Item>, 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.Item>, 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.Item>, 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.Item + for +t: List<&2, P.Item> + for +a: P.Item + for +b: P.Item 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.Item>} {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.Item>} def ins.swap.ff(h, t, a, b, eA, eB, ih): - Equal.trans(List<&2, P.File>, + Equal.trans(List<&2, P.Item>, 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.Item>, 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.Item>, 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.Item>, List<&2, P.Item>, 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.Item>, 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.Item>, 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.Item + for +t: List<&2, P.Item> + for +a: P.Item + for +b: P.Item 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.Item>} {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.Item>} 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.Item> + for +a: P.Item + for +b: P.Item 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.Item>} 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.Item + for +y: P.Item + for +xs: List<&2, P.Item> 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.Item for +ns: List<&2, Nat> - for +xs: List<&2, P.File> + for +xs: List<&2, P.Item> 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.Item + for +xs: List<&2, P.Item> 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.Item>} 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.Item>, 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.Item>, List<&2, P.Item>, 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.Item>, 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.Item>, List<&2, P.Item>, 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.Item>, 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.Item>} 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.Item>, List<&2, P.Item>, + xs => P.Item{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.Item>, 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.Item>, 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.Item>} {==} 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.Item>} {==} # --------------------------------------------------------------------------- diff --git a/pkg/pkg.bend b/pkg/pkg.bend index f8952f0..f03dd03 100644 --- a/pkg/pkg.bend +++ b/pkg/pkg.bend @@ -12,12 +12,12 @@ # its own. import Base import ../io/file.bend as F -import ../sha/sha.bend as Sha +import ../share/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 Item is Data: + Item{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, Item>} # 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) -> Item: Found{raw, sum} = hit - File{P.join(pre, raw), sum} + Item{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, Item>: 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: Item) -> String: + Item{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: Item, right: Item) -> 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: Item, rest: List<&2, Item>) -> List<&2, Item>: 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: Item, rest: List<&2, Item>) -> List<&2, Item>: 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, Item>) -> List<&2, Item>: match fs: case []: [] @@ -552,7 +552,7 @@ 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: Item, head: Item, tail: List<&2, Item>, rest: List<&2, Item>) -> List<&2, Item>: match le: case True{}: item <> (head <> tail) @@ -560,7 +560,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, Item>, +item: Item) -> List<&2, Item>: match fs: case []: [item] @@ -572,7 +572,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, Item>) -> List<&2, Item>: match fs: case []: [] @@ -580,7 +580,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, Item>) -> List<&2, Item>: dedup(file.sort(fs)) # a path that leaves the package behind, which no package may hold @@ -599,7 +599,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, Item>) -> String: match fs: case []: "" @@ -608,12 +608,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: Item) -> String: + Item{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, Item>) -> String: match fs: case []: "" @@ -622,21 +622,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, Item>) -> 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, Item>) -> 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: Item) -> Bool: + Item{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: Item, rest: List<&2, Item>) -> List<&2, Item>: match lic: case True{}: rest @@ -645,7 +645,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, Item>) -> List<&2, Item>: match fs: case []: [] @@ -661,7 +661,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, Item>, ss: List<&2, String>) -> List<&2, String>: match fs ss: case Nil{} _: ss @@ -717,7 +717,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, Item>} Asks{at: String} Refused{why: String} @@ -1101,12 +1101,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) -> Item: Source{at, +text} = src - File{at, Sha.hex(text)} + Item{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, Item>: match fs: case []: [] @@ -1132,7 +1132,7 @@ def made.judge( +bad: String, +root: String, +pre: String, - +fs: List<&2, File>, + +fs: List<&2, Item>, out: List<&2, Hit> ) -> Walked: match ok: @@ -1303,7 +1303,7 @@ def state.stop(st: State) -> Stop: # a walk's verdict as a package, with its root taken back under the checkout # it was read from -def pkg.made(+top: String, got: Walked) -> IO(Pkg): +def made.io(+top: String, got: Walked) -> IO(Pkg): match got: case Walked{hash, root, _files, sums}: IO.pure(Pkg, Pkg{hash, P.join(top, root), files_of(sums)}) @@ -1327,15 +1327,15 @@ def pkg.next( m : Maybe<&2, String> <- F.read(P.join(top, at)) go(tree.add(m, tree, at), resume(st)) case Going{}: - pkg.made(top, made(entry, st)) + made.io(top, made(entry, st)) case Missing{_at}: - pkg.made(top, made(entry, st)) + made.io(top, made(entry, st)) case Climbs{_at}: - pkg.made(top, made(entry, st)) + made.io(top, made(entry, st)) case Spent{}: - pkg.made(top, made(entry, st)) + made.io(top, made(entry, st)) case Unnamed{_nv}: - pkg.made(top, made(entry, st)) + made.io(top, made(entry, st)) # the walk over what has been read so far, and each file it asks for read # and handed back, until it no longer asks @@ -1351,22 +1351,22 @@ def pkg.ask(fuel: Nat, +top: String, +entry: String, +eb: String, +tree: Tree, s # the package an entry would be published as, walked over its checkout: the # entry and every file the walk reaches are paths from `top`, read from disk # as the walk asks for them. An import that climbs above `top` is refused. -def pkg.walk(+top: String, +entry: String) -> IO(Pkg): +def walk.io(+top: String, +entry: String) -> IO(Pkg): pkg.ask(U32.to_nat(100000), top, entry, P.base(entry), Tree{False{}, [], []}, start(entry)) # the package an entry of a checkout would be published as def pkg_in(+top: String, +entry: String) -> IO(Pkg): - pkg.walk(top, P.norm(entry)) + walk.io(top, P.norm(entry)) # an entry named from the working directory is walked over the working # directory, and one named from the root over the whole file system def pkg.from(abs: Bool, +entry: String) -> IO(Pkg): match abs: case True{}: - pkg.walk("/", String.drop(entry, 1n)) + walk.io("/", String.drop(entry, 1n)) case False{}: - pkg.walk("", entry) + walk.io("", entry) # the package an entry file would be published as: every module it reaches, # every foreign body beside them, and the hash over their manifest. A relative @@ -1386,11 +1386,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, Item>: 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: Item) -> String: + Item{_at, sum} = item sum diff --git a/pub/plan.bend b/pub/plan.bend index 4d50811..1a4e099 100644 --- a/pub/plan.bend +++ b/pub/plan.bend @@ -31,7 +31,7 @@ import ../git/git.bend as G import ./world.bend as PW import ./blurb.bend as B import ../lock/lock.bend as L -import ../sha/sha.bend as Sha +import ../share/sha.bend as Sha import ../io/file.bend as F # --------------------------------------------------------------------------- diff --git a/pub/run.bend b/pub/run.bend index 10b07c0..67df9d3 100644 --- a/pub/run.bend +++ b/pub/run.bend @@ -19,13 +19,13 @@ # 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 import ../tool/world.bend as TW import ../hub/hub.bend as Web -import ../ez/env.bend as Env +import ../share/env.bend as Env import ./world.bend as PW import ./plan.bend as PP 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..8345e45 100644 --- a/sha/LAWS.bend +++ b/sha/LAWS.bend @@ -1,9 +1,9 @@ # sha: the laws. The human states them; PROOF.bend must prove them. The digest -# itself is Giulio2002/bend-sha256's, proved there against FIPS 180-4, so what +# itself is noah-emp/bend-sha256's, proved there against FIPS 180-4, so what # is stated here is the encoding `Sha.hex` puts in front of it: a text is # hashed as its UTF-8 bytes, the way `bend --publish` and the hub hash it. import Base -import ../sha/sha.bend as Sha +import ../share/sha.bend as Sha import ../sha/nar.bend as Nar import ../pkg/pkg.bend as K import ../pkg/LAWS.bend as PL @@ -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.Item` 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.Item> 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..5668ca0 100644 --- a/sha/PROOF.bend +++ b/sha/PROOF.bend @@ -1,6 +1,6 @@ # sha: the proofs. `bend PROOF.bend` is the gate. import Base -import ../sha/sha.bend as Sha +import ../share/sha.bend as Sha import ../sha/nar.bend as Nar import ../pkg/pkg.bend as K import ../pkg/LAWS.bend as PL @@ -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.Item>, 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..307e823 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 +import ../share/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.Item`: 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.Item) -> String: + K.Item{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.Item>) -> 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.Item>) -> 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.Item>) -> 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.Item>} # 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.Item{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.Item{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/ez/args.bend b/share/args.bend similarity index 98% rename from ez/args.bend rename to share/args.bend index 1f05b7a..1dda43c 100644 --- a/ez/args.bend +++ b/share/args.bend @@ -1,4 +1,4 @@ -# ez/args: the command line, as the binary itself receives it. `IO.args()` gives +# share/args: the command line, as the binary itself receives it. `IO.args()` gives # a compiled Bend binary every argument it was started with: the first is the # subcommand and the rest are its own. The runtime keeps `--threads`, `--gpu`, # `--gpu-build` and `--help` for itself and strips them wherever they appear; diff --git a/ez/cap.bend b/share/cap.bend similarity index 95% rename from ez/cap.bend rename to share/cap.bend index 9bf4425..a5a2001 100644 --- a/ez/cap.bend +++ b/share/cap.bend @@ -1,4 +1,4 @@ -# ez/cap: every `bend` the runner starts, inside a memory cap. +# share/cap: every `bend` the runner starts, inside a memory cap. # # bend's C backend, not clang, is what costs the memory: emitting the C for a # large program peaked at 18.8 GB here while clang on that same C peaked at @@ -7,9 +7,9 @@ # 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 ../ez/env.bend as Env -import ../ez/args.bend as Args +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R +import ./env.bend as Env +import ./args.bend as Args # how many gigabytes one `bend` may have. 8 is what fits beside the rest of # this machine; a project whose closure costs more says so in EZ_CAP. diff --git a/ez/env.bend b/share/env.bend similarity index 93% rename from ez/env.bend rename to share/env.bend index e0dbbe9..9eb1f0c 100644 --- a/ez/env.bend +++ b/share/env.bend @@ -1,12 +1,12 @@ -# ez/env: the environment ez hands to the programs it runs. Vendored packages +# share/env: the environment ez hands to the programs it runs. Vendored packages # live with the project rather than in ~/.bend/lib, so every `bend` ez starts # has to be told where they are. Base has `get_env` and no `set_env`, and the # one foreign effect execvp's what it is given, so the variable rides in front # 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 ../ez/args.bend as Args +import 0xabe575924687afad4cee1a2c1194d639/main.bend as R +import ./args.bend as Args # a value, or the fallback when the variable was unset or empty def or_else(+value: String, +alt: String) -> String: diff --git a/ez/pass.bend b/share/pass.bend similarity index 86% rename from ez/pass.bend rename to share/pass.bend index c40abad..0d8b02f 100644 --- a/ez/pass.bend +++ b/share/pass.bend @@ -1,4 +1,4 @@ -# ez/pass: a program run on ez's own stdin, stdout and stderr, as `cargo run` +# share/pass: a program run on ez's own stdin, stdout and stderr, as `cargo run` # runs one. Every other program ez starts goes through snap's `exec`, which # hands the child /dev/null for stdin, holds what it prints until it exits, # and answers both at once; that is what a command that reads the answer @@ -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/share/pass.c similarity index 97% rename from ez/pass.c rename to share/pass.c index 9479043..05eef86 100644 --- a/ez/pass.c +++ b/share/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/share/pass.js similarity index 93% rename from ez/pass.js rename to share/pass.js index 710c43a..6e19b48 100644 --- a/ez/pass.js +++ b/share/pass.js @@ -13,3 +13,5 @@ function ezpass_run(cmd) { } return r.status; } + +io_eff(CID(ezpass.run), ezpass_run); diff --git a/ez/pin.bend b/share/pin.bend similarity index 96% rename from ez/pin.bend rename to share/pin.bend index df2c6d8..4cdc028 100644 --- a/ez/pin.bend +++ b/share/pin.bend @@ -1,4 +1,4 @@ -# ez/pin: a plain `ez lock` refuses a `[tools.*]` pin it would have to fill. +# share/pin: a plain `ez lock` refuses a `[tools.*]` pin it would have to fill. # It copies every pin as the ledger has it and never asks a remote, so a pin # with no commit or no NAR hash stops it, naming the upgrade that fills the # pin. Filling and moving a pin is `ez lock --upgrade`'s, in lock/up.bend. diff --git a/ez/say.bend b/share/say.bend similarity index 98% rename from ez/say.bend rename to share/say.bend index 21dbe1c..dc24329 100644 --- a/ez/say.bend +++ b/share/say.bend @@ -1,4 +1,4 @@ -# ez/say: the words a long step says, and a spinner for the wait. +# share/say: the words a long step says, and a spinner for the wait. # # A clone, a hub fetch or a native build can sit there for half a minute, and # a step that prints nothing looks stopped. The line is printed before the @@ -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/sha/sha.bend b/share/sha.bend similarity index 87% rename from sha/sha.bend rename to share/sha.bend index 0fbdc74..b44b4c7 100644 --- a/sha/sha.bend +++ b/share/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 +# share/sha: the sha256 a package hash is built from. The digest itself comes from +# 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..21d2620 100644 --- a/tests/hub.bend +++ b/tests/hub.bend @@ -3,9 +3,9 @@ # 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 ../share/sha.bend as Sha import ../doctor/plan.bend as DP import ../ez/quiet.bend as Q import ../check/kit.bend as Check 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..deeb7ad 100644 --- a/tests/nix.bend +++ b/tests/nix.bend @@ -3,9 +3,9 @@ # 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 ../share/sha.bend as Sha import ../ez/quiet.bend as Q import ../check/kit.bend as Check import ../check/world.bend as W 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/LAWS.bend b/tool/LAWS.bend index 1785fd6..792c26f 100644 --- a/tool/LAWS.bend +++ b/tool/LAWS.bend @@ -1,7 +1,7 @@ # tool: the laws. The human states them; PROOF.bend must prove them. They are # stated over the plan `ez tool run`, `install` and `upgrade` run # (tool/plan.bend), over what it resolves a target to, and over the words -# `ez tool run` and `ez run` hand on (ez/args.bend), so what they say of the +# `ez tool run` and `ez run` hand on (share/args.bend), so what they say of the # plan is what the command does, the interpreter's faithfulness being # EZ-TRUST-2. import Base @@ -13,7 +13,7 @@ import ../ledger/manifest.bend as M import ../git/git.bend as Git import ../pkg/path.bend as Path import ../ez/target.bend as Tgt -import ../ez/args.bend as Args +import ../share/args.bend as Args # --------------------------------------------------------------------------- # refusals diff --git a/tool/PROOF.bend b/tool/PROOF.bend index fa63485..e2e3b26 100644 --- a/tool/PROOF.bend +++ b/tool/PROOF.bend @@ -20,7 +20,7 @@ import ../git/git.bend as Git import ../pkg/path.bend as Path import ../ez/target.bend as Tgt import ../ez/key.bend as Key -import ../ez/args.bend as Args +import ../share/args.bend as Args import ../check/eq.bend as Eq import ./LAWS.bend as Laws @@ -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..e47fc98 100644 --- a/tool/plan.bend +++ b/tool/plan.bend @@ -46,8 +46,8 @@ import ../git/git.bend as Git import ../ez/target.bend as Tgt import ../ez/named.bend as Named import ../ez/key.bend as Key -import ../ez/say.bend as Say -import ../sha/sha.bend as Sha +import ../share/say.bend as Say +import ../share/sha.bend as Sha # --------------------------------------------------------------------------- # small pieces @@ -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..cfaaa8e 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 @@ -28,9 +28,9 @@ import ../git/git.bend as Git import ../fetch/run.bend as FetchRun import ../pkg/path.bend as P import ../run/bend.bend as Bend -import ../ez/cap.bend as Cap -import ../ez/say.bend as Say -import ../ez/pass.bend as Pass +import ../share/cap.bend as Cap +import ../share/say.bend as Say +import ../share/pass.bend as Pass import ./world.bend as TW import ./plan.bend as TP