diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index aac17c1..404d485 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -32,5 +32,5 @@ jobs: echo "$RUNNER_TEMP/bend/bin" >> "$GITHUB_PATH" - run: sh bootstrap.sh - run: mkdir -p bin - - run: BEND_LIB=$PWD/.ez/lib bend ez/main.bend -o bin/ez.bin + - run: BEND_LIB=$PWD/.ez/lib bend main.bend -o bin/ez.bin - run: bin/ez.bin prove diff --git a/AGENTS.md b/AGENTS.md index db650d1..91be4d1 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -4,14 +4,16 @@ How to work in this repository. It is written for coding agents, and it holds fo ## What ez is -ez is a project manager for Bend 2, written in Bend. Each command is a pure planner (`/plan.bend`) over a World (`/world.bend`), run by a thin interpreter (`/run.bend`). What ez guarantees is listed in `SPEC.md`. The design and its history are in `docs/rfc/ez-spec.md`. The user guide is `docs/guide.md`. +ez is a project manager for Bend 2, written in Bend. Each command is a pure planner (`src//plan.bend`) over a World (`src//world.bend`), run by a thin interpreter (`src//run.bend`). What ez guarantees is listed in `SPEC.md`. The design and its history are in `docs/rfc/ez-spec.md`. The user guide is `docs/guide.md`. + +The top-level `main.bend` is ez's program and the entry the hub publishes as `ezx`; it calls `src/ez/main.bend`. Every module lives under `src/`, so the package bend publishes is `main.bend`, the LICENSE beside it and what it imports under `src/`, and `main.bend`'s first line is the hub's description. No file the program reaches may import a `LAWS.bend`, a `PROOF.bend`, `src/check/` or `tests/`. ## Build and check ```bash sh bootstrap.sh mkdir -p bin -BEND_LIB=$PWD/.ez/lib bend ez/main.bend -o bin/ez.bin +BEND_LIB=$PWD/.ez/lib bend main.bend -o bin/ez.bin bin/ez.bin prove # the proof gate: every PROOF.bend must pass bin/ez.bin tool run bolt -- --gpu off # lint: 0 errors bin/ez.bin lock # must leave ez.lock.toml unchanged unless you meant to change it diff --git a/README.md b/README.md index b661a10..a592a50 100644 --- a/README.md +++ b/README.md @@ -10,29 +10,49 @@ tools for a whole project. ## Install -ez needs Bend 2.0.32 or later; the fleet is built and checked on Bend 2.0.34. +ez needs Bend 2.0.32 or later; it is built and checked on Bend 2.0.34, the +version `flake.lock` pins. Building ez needs clang as well, since ez is one +native binary. Every subcommand runs the `bend` and `git` on your PATH. -### The ledger library, from the hub +### From the hub -ez's ledger library, which reads `ez.toml`, is on the Bend hub as `ezx`. A -plain Bend program imports it by name, at v1.3.0: +With an installed `bend` and nothing else, build ez v1.4.0 from the Bend hub, +where the whole program is published as `ezx@1.4.0.0`. Put this in `t.bend`: ```bend -import ezx@1.3.0.0/main.bend as Ledger +import ezx@1.4.0.0/main.bend as Ez + +def main() -> IO(Unit): + Ez.main() +``` + +and build it: + +```bash +curl -fsSL https://bend-lang.com/install.sh | sh +bend t.bend -o ez # fetches ez and its libraries from the hub +./ez --help +``` + +There is no install step: `bend` fetches the package and the libraries it +imports by hash (shake, snap, ezhttp, eztoml and sha256) on the first build, +into `~/.bend/lib`. `import 0x/main.bend`, with the hash the hub names +for `ezx@1.4.0.0`, pins it by content. + +ez's ledger library, which reads `ez.toml`, comes in the same package, at +`src/ledger/manifest.bend`: + +```bend +import ezx@1.4.0.0/src/ledger/manifest.bend as Ledger def main() -> String: Ledger.show(Ledger.parse("[package]\nname = \"app\"\nentry = \"main.bend\"\n")) ``` -`bend` fetches it from the hub on first run; there is no install step. -`ezx@1.3.0.0` resolves to `0x046551eff0d59a82cf10d858b17b0c84`, and -`import 0x046551eff0d59a82cf10d858b17b0c84/main.bend` pins it by content. In -an ez project, `ez add Emerging-Patterns/ez` records it in the ledger. - -The hub package is the library only. The `ez` command is built from a clone, -or installed with nix, as below. +In an ez project, `ez add Emerging-Patterns/ez` records the package in the +ledger. -### The ez command +### From a clone Install Bend, then fetch the packages ez builds itself with, and build it: @@ -42,16 +62,18 @@ git clone https://github.com/Emerging-Patterns/ez cd ez sh bootstrap.sh mkdir -p bin -BEND_LIB=$PWD/.ez/lib bend ez/main.bend -o bin/ez.bin +BEND_LIB=$PWD/.ez/lib bend main.bend -o bin/ez.bin ``` -ez's own 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 -into `.ez/lib`, and checks every file's sha256 and the package's `0x` name -against the lock. It needs `git` and `sha256sum` (or `shasum`), and nothing -comes from the hub. `bend` then only needs telling where the packages are, -since it looks in `~/.bend/lib` otherwise. +The top-level `main.bend` is ez's program; the modules it imports are under +`src/`. ez's own 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 into `.ez/lib`, and checks every +file's sha256 and the package's `0x` name against the lock. It needs `git` +and `sha256sum` (or `shasum`), and nothing comes from the hub. `bend` then +only needs telling where the packages are, since it looks in `~/.bend/lib` +otherwise. Put `bin/ez.bin` on your PATH as `ez`. ez is Bend and nothing else, so the binary is all there is: no runtime, no helper scripts beside it, nothing to diff --git a/SPEC.md b/SPEC.md index dbf1101..c1e39d2 100644 --- a/SPEC.md +++ b/SPEC.md @@ -27,157 +27,157 @@ Untagged quantified laws are allowed. They pass the proof gate like any law, but | ID | Requirement | Level | Status | Law | | :---- | :---- | :---- | :---- | :---- | -| EZ-HASH-1 | The 0x hash of a file list with distinct paths depends only on its (path, sum) pairs, not on the order they were found in. | Proved | proved | pkg/LAWS.bend hash_perm | -| EZ-HASH-2 | The NAR serialization of a directory does not depend on the order its entries are listed in. | Proved | proved | sha/LAWS.bend nar_dir_order_free | -| EZ-HASH-3 | When ez writes a package under `/`, `h` is the 0x hash of the file list whose manifest it writes beside the files. | Proved | proved | pkg/LAWS.bend walked_named_by_texts; pkg/LAWS.bend walked_manifest_of_texts; add/LAWS.bend add_lays_named; fetch/LAWS.bend fetch_lays_named; lock/LAWS.bend lock_lays_named; add/LAWS.bend add_named_lays_named | +| EZ-HASH-1 | The 0x hash of a file list with distinct paths depends only on its (path, sum) pairs, not on the order they were found in. | Proved | proved | src/pkg/LAWS.bend hash_perm | +| EZ-HASH-2 | The NAR serialization of a directory does not depend on the order its entries are listed in. | Proved | proved | src/sha/LAWS.bend nar_dir_order_free | +| EZ-HASH-3 | When ez writes a package under `/`, `h` is the 0x hash of the file list whose manifest it writes beside the files. | Proved | proved | src/pkg/LAWS.bend walked_named_by_texts; src/pkg/LAWS.bend walked_manifest_of_texts; src/add/LAWS.bend add_lays_named; src/fetch/LAWS.bend fetch_lays_named; src/lock/LAWS.bend lock_lays_named; src/add/LAWS.bend add_named_lays_named | | EZ-HASH-4 | ez's 0x hash for an entry equals the hash `bend --publish` assigns to it. | Trusted | | | | EZ-HASH-5 | ez's narHash equals `nix hash path --type sha256 --sri` of the same tree. | Trusted | | | | EZ-HASH-6 | `Sha.hex(s)` is the SHA-256 of the UTF-8 bytes of `s`. For a file's text that is SHA-256 of the file's bytes, which is what `bend --publish` and the hub compute. | Trusted | | | -| EZ-HASH-7 | The NAR walk reads every name and symlink target as the tree listing prints it: nothing is trimmed, and a newline stays inside the name that holds it. | Proved | proved | sha/LAWS.bend nar_field_verbatim; sha/LAWS.bend nar_listing_verbatim | +| EZ-HASH-7 | The NAR walk reads every name and symlink target as the tree listing prints it: nothing is trimmed, and a newline stays inside the name that holds it. | Proved | proved | src/sha/LAWS.bend nar_field_verbatim; src/sha/LAWS.bend nar_listing_verbatim | ### Ledger (EZ-LED) | ID | Requirement | Level | Status | Law | | :---- | :---- | :---- | :---- | :---- | -| EZ-LED-1 | A ledger that does not parse is never read into a model, and renders as nothing, so no command writes a guess over it. | Proved | proved | ledger/LAWS.bend read_refuses_a_problem; ledger/LAWS.bend render_of_unread_is_blank; remove/LAWS.bend remove_refuses_unread; add/LAWS.bend add_refuses_unread; lock/LAWS.bend lock_refuses_unread | -| EZ-LED-2 | Adding a dependency to a ledger model twice is adding it once. | Proved | proved | ledger/LAWS.bend add_keep_idem; add/LAWS.bend add_edits_ledger; add/LAWS.bend add_named_edits_ledger | -| EZ-LED-3 | Removing a dependency from a ledger model twice is removing it once. | Proved | proved | ledger/LAWS.bend remove_idem; remove/LAWS.bend remove_edits_ledger | -| EZ-LED-4 | Every ledger ez writes is one `Rend.renderable` accepts, and so reads back to the model it was rendered from wherever eztoml's round trip holds (EZ-TRUST-8). | Proved | proved | init/LAWS.bend init_ledger_reads_back; add/LAWS.bend add_ledger_reads_back; remove/LAWS.bend remove_ledger_reads_back; add/LAWS.bend add_named_reads_back; add/LAWS.bend add_named_refuses_unrenderable | -| EZ-LED-5 | A `[tools.*]` section is a tool, never a dependency, and needs no `hash`. | Proved | proved | ledger/LAWS.bend tool_section_not_dep; ledger/LAWS.bend tool_section_is_tool; ledger/LAWS.bend tool_needs_no_hash; lock/LAWS.bend lock_origins_skip_tools; lock/LAWS.bend upgrade_origins_skip_tools; add/LAWS.bend add_keeps_tools; remove/LAWS.bend remove_keeps_tools; remove/LAWS.bend remove_refuses_tool; doctor/LAWS.bend doctor_ignores_tools | -| EZ-LED-6 | `ez init` writes nothing when a ledger exists, and `ez add`, `ez remove`, `ez fetch` and `ez lock`, with or without `--upgrade`, refuse and write nothing when there is none. | Proved | proved | init/LAWS.bend init_keeps_ledger; remove/LAWS.bend remove_needs_ledger; add/LAWS.bend add_needs_ledger; add/LAWS.bend add_needs_ledger_asks_nothing; lock/LAWS.bend lock_needs_ledger; fetch/LAWS.bend fetch_needs_ledger; fetch/LAWS.bend fetch_needs_ledger_asks_nothing | -| EZ-LED-7 | A dependency's ledger name is `--rename` when given, which must be a TOML bare key; otherwise the name the ledger already records for that source; otherwise the target's `[package] name` when it is a TOML bare key; otherwise the repository's name; otherwise the directory's name. A hub package added by its `@` is named by `--rename` when given; otherwise by the name the ledger already records for a dependency added by the same name part, so another version replaces it; otherwise by the name part. A name the ledger gives a different source is refused, and so is a `--rename` of a source the ledger records under another name. | Proved | proved | ez/LAWS.bend rename_wins; ez/LAWS.bend rename_dotted; ez/LAWS.bend rename_moved; ez/LAWS.bend rename_clash; ez/LAWS.bend name_keeps; ez/LAWS.bend own_package; ez/LAWS.bend own_invalid; ez/LAWS.bend leaf_is_last; ez/LAWS.bend clash_same; ez/LAWS.bend clash_other; ez/LAWS.bend clash_hub; add/LAWS.bend add_records_named; add/LAWS.bend add_refuses_named; ez/LAWS.bend hub_rename_wins; ez/LAWS.bend hub_key_keeps; ez/LAWS.bend hub_key_fresh; ez/LAWS.bend hub_clash_git; add/LAWS.bend add_named_key; add/LAWS.bend add_named_refuses_clash | -| EZ-LED-8 | A path target is recorded in the ledger as it was given, with a leading `~/` expanded, and a relative path resolves against the project root wherever git reads it: `ez add`, `ez lock`, `ez fetch` and `ez lock --upgrade`. | Proved | proved | ez/LAWS.bend anchor_url; ez/LAWS.bend anchor_absolute; ez/LAWS.bend anchor_relative; add/LAWS.bend add_records_as_given; add/LAWS.bend add_path_as_given; add/LAWS.bend add_asks_anchored; fetch/LAWS.bend fetch_asks_anchored; fetch/LAWS.bend fetch_keeps_records; lock/LAWS.bend lock_asks_anchored; lock/LAWS.bend upgrade_asks_its_questions; lock/LAWS.bend upgrade_asks_anchored; lock/LAWS.bend lock_records_as_given; lock/LAWS.bend upgrade_records_as_given; lock/LAWS.bend upgrade_records_tools_as_given | +| EZ-LED-1 | A ledger that does not parse is never read into a model, and renders as nothing, so no command writes a guess over it. | Proved | proved | src/ledger/LAWS.bend read_refuses_a_problem; src/ledger/LAWS.bend render_of_unread_is_blank; src/remove/LAWS.bend remove_refuses_unread; src/add/LAWS.bend add_refuses_unread; src/lock/LAWS.bend lock_refuses_unread | +| EZ-LED-2 | Adding a dependency to a ledger model twice is adding it once. | Proved | proved | src/ledger/LAWS.bend add_keep_idem; src/add/LAWS.bend add_edits_ledger; src/add/LAWS.bend add_named_edits_ledger | +| EZ-LED-3 | Removing a dependency from a ledger model twice is removing it once. | Proved | proved | src/ledger/LAWS.bend remove_idem; src/remove/LAWS.bend remove_edits_ledger | +| EZ-LED-4 | Every ledger ez writes is one `Rend.renderable` accepts, and so reads back to the model it was rendered from wherever eztoml's round trip holds (EZ-TRUST-8). | Proved | proved | src/init/LAWS.bend init_ledger_reads_back; src/add/LAWS.bend add_ledger_reads_back; src/remove/LAWS.bend remove_ledger_reads_back; src/add/LAWS.bend add_named_reads_back; src/add/LAWS.bend add_named_refuses_unrenderable | +| EZ-LED-5 | A `[tools.*]` section is a tool, never a dependency, and needs no `hash`. | Proved | proved | src/ledger/LAWS.bend tool_section_not_dep; src/ledger/LAWS.bend tool_section_is_tool; src/ledger/LAWS.bend tool_needs_no_hash; src/lock/LAWS.bend lock_origins_skip_tools; src/lock/LAWS.bend upgrade_origins_skip_tools; src/add/LAWS.bend add_keeps_tools; src/remove/LAWS.bend remove_keeps_tools; src/remove/LAWS.bend remove_refuses_tool; src/doctor/LAWS.bend doctor_ignores_tools | +| EZ-LED-6 | `ez init` writes nothing when a ledger exists, and `ez add`, `ez remove`, `ez fetch` and `ez lock`, with or without `--upgrade`, refuse and write nothing when there is none. | Proved | proved | src/init/LAWS.bend init_keeps_ledger; src/remove/LAWS.bend remove_needs_ledger; src/add/LAWS.bend add_needs_ledger; src/add/LAWS.bend add_needs_ledger_asks_nothing; src/lock/LAWS.bend lock_needs_ledger; src/fetch/LAWS.bend fetch_needs_ledger; src/fetch/LAWS.bend fetch_needs_ledger_asks_nothing | +| EZ-LED-7 | A dependency's ledger name is `--rename` when given, which must be a TOML bare key; otherwise the name the ledger already records for that source; otherwise the target's `[package] name` when it is a TOML bare key; otherwise the repository's name; otherwise the directory's name. A hub package added by its `@` is named by `--rename` when given; otherwise by the name the ledger already records for a dependency added by the same name part, so another version replaces it; otherwise by the name part. A name the ledger gives a different source is refused, and so is a `--rename` of a source the ledger records under another name. | Proved | proved | src/ez/LAWS.bend rename_wins; src/ez/LAWS.bend rename_dotted; src/ez/LAWS.bend rename_moved; src/ez/LAWS.bend rename_clash; src/ez/LAWS.bend name_keeps; src/ez/LAWS.bend own_package; src/ez/LAWS.bend own_invalid; src/ez/LAWS.bend leaf_is_last; src/ez/LAWS.bend clash_same; src/ez/LAWS.bend clash_other; src/ez/LAWS.bend clash_hub; src/add/LAWS.bend add_records_named; src/add/LAWS.bend add_refuses_named; src/ez/LAWS.bend hub_rename_wins; src/ez/LAWS.bend hub_key_keeps; src/ez/LAWS.bend hub_key_fresh; src/ez/LAWS.bend hub_clash_git; src/add/LAWS.bend add_named_key; src/add/LAWS.bend add_named_refuses_clash | +| EZ-LED-8 | A path target is recorded in the ledger as it was given, with a leading `~/` expanded, and a relative path resolves against the project root wherever git reads it: `ez add`, `ez lock`, `ez fetch` and `ez lock --upgrade`. | Proved | proved | src/ez/LAWS.bend anchor_url; src/ez/LAWS.bend anchor_absolute; src/ez/LAWS.bend anchor_relative; src/add/LAWS.bend add_records_as_given; src/add/LAWS.bend add_path_as_given; src/add/LAWS.bend add_asks_anchored; src/fetch/LAWS.bend fetch_asks_anchored; src/fetch/LAWS.bend fetch_keeps_records; src/lock/LAWS.bend lock_asks_anchored; src/lock/LAWS.bend upgrade_asks_its_questions; src/lock/LAWS.bend upgrade_asks_anchored; src/lock/LAWS.bend lock_records_as_given; src/lock/LAWS.bend upgrade_records_as_given; src/lock/LAWS.bend upgrade_records_tools_as_given | ### New projects (EZ-INIT) | ID | Requirement | Level | Status | Law | | :---- | :---- | :---- | :---- | :---- | -| EZ-INIT-1 | The entry `ez init` writes opens with the line `# : `, the description `--description` gives, or `TODO describe ` when none is given, so that line is what the hub describes the package by. A description holding a newline is refused, and nothing is written. | Proved | proved | init/LAWS.bend init_stub_heads; init/LAWS.bend init_header_given; init/LAWS.bend init_header_placeholder; init/LAWS.bend init_one_line | -| EZ-INIT-2 | With nothing at the entry, the entry at the project's top and nothing at `src/lib.bend`, `ez init` writes `src/lib.bend` and an entry that imports it; an entry in a directory of its own is written alone. It never writes over an entry or a `src/lib.bend` that is already there. | Proved | proved | init/LAWS.bend init_lays_src; init/LAWS.bend init_lays_main; init/LAWS.bend init_keeps_src; init/LAWS.bend init_keeps_entry | +| EZ-INIT-1 | The entry `ez init` writes opens with the line `# : `, the description `--description` gives, or `TODO describe ` when none is given, so that line is what the hub describes the package by. A description holding a newline is refused, and nothing is written. | Proved | proved | src/init/LAWS.bend init_stub_heads; src/init/LAWS.bend init_header_given; src/init/LAWS.bend init_header_placeholder; src/init/LAWS.bend init_one_line | +| EZ-INIT-2 | With nothing at the entry, the entry at the project's top and nothing at `src/lib.bend`, `ez init` writes `src/lib.bend` and an entry that imports it; an entry in a directory of its own is written alone. It never writes over an entry or a `src/lib.bend` that is already there. | Proved | proved | src/init/LAWS.bend init_lays_src; src/init/LAWS.bend init_lays_main; src/init/LAWS.bend init_keeps_src; src/init/LAWS.bend init_keeps_entry | ### Lock document (EZ-DOC) | ID | Requirement | Level | Status | Law | | :---- | :---- | :---- | :---- | :---- | | EZ-DOC-1 | Parsing a rendered lock yields the packages, hub, names and tools that were rendered. | Trusted | | | -| EZ-DOC-2 | Packages are written in hash order and each package's files in path order, so the lock's text does not depend on the order the walk found them in. | Proved | proved | lock/LAWS.bend lock_order_free; lock/LAWS.bend pack_order_free; lock/LAWS.bend plain_lock_hashes_distinct | -| EZ-DOC-3 | `ez lock` output is a function of the ledger and the committed tree. A fresh clone reproduces the lock byte for byte. | Proved | proved | lock/LAWS.bend lock_reproducible; lock/LAWS.bend clone_reproduces; lock/LAWS.bend root_reads_as_bend | -| EZ-DOC-4 | `ez lock` is idempotent: run on the world it just produced, it writes the same bytes. | Proved | proved | lock/LAWS.bend lock_idempotent; lock/LAWS.bend relock_lays_nothing; lock/LAWS.bend upgrade_idempotent; lock/LAWS.bend reupgrade_moves_nothing; lock/LAWS.bend upgrade_settles; lock/LAWS.bend reupgrade_lays_nothing; lock/LAWS.bend reupgrade_writes_only_lock | -| EZ-DOC-5 | `ez lock` without `--upgrade` never writes ez.toml, and records every dependency's and tool's pin exactly as ez.toml has it. | Proved | proved | lock/LAWS.bend plain_lock_keeps_ledger; lock/LAWS.bend plain_lock_pins_ledger_sources | +| EZ-DOC-2 | Packages are written in hash order and each package's files in path order, so the lock's text does not depend on the order the walk found them in. | Proved | proved | src/lock/LAWS.bend lock_order_free; src/lock/LAWS.bend pack_order_free; src/lock/LAWS.bend plain_lock_hashes_distinct | +| EZ-DOC-3 | `ez lock` output is a function of the ledger and the committed tree. A fresh clone reproduces the lock byte for byte. | Proved | proved | src/lock/LAWS.bend lock_reproducible; src/lock/LAWS.bend clone_reproduces; src/lock/LAWS.bend root_reads_as_bend | +| EZ-DOC-4 | `ez lock` is idempotent: run on the world it just produced, it writes the same bytes. | Proved | proved | src/lock/LAWS.bend lock_idempotent; src/lock/LAWS.bend relock_lays_nothing; src/lock/LAWS.bend upgrade_idempotent; src/lock/LAWS.bend reupgrade_moves_nothing; src/lock/LAWS.bend upgrade_settles; src/lock/LAWS.bend reupgrade_lays_nothing; src/lock/LAWS.bend reupgrade_writes_only_lock | +| EZ-DOC-5 | `ez lock` without `--upgrade` never writes ez.toml, and records every dependency's and tool's pin exactly as ez.toml has it. | Proved | proved | src/lock/LAWS.bend plain_lock_keeps_ledger; src/lock/LAWS.bend plain_lock_pins_ledger_sources | ### Resolution (EZ-RES) | ID | Requirement | Level | Status | Law | | :---- | :---- | :---- | :---- | :---- | -| EZ-RES-1 | `ez add` with no ref pins the greatest semver-ish release tag on the remote; with no release, the greatest pre-release; with no semver-ish tag, the remote's default branch as its `HEAD` symref names it. A named ref resolves exactly, as `refs/tags/` and then `refs/heads/`. A 40-hex ref is used as a commit without asking the remote. | Proved | proved | git/LAWS.bend is_rev_needs_40; git/LAWS.bend is_rev_needs_hex; git/LAWS.bend is_rev_hex40; git/LAWS.bend choose_release; git/LAWS.bend choose_prerelease; git/LAWS.bend branch_of_symref; git/LAWS.bend branch_skips_other; git/LAWS.bend branch_skips_commit; git/LAWS.bend exact_skips; git/LAWS.bend exact_tag_first; git/LAWS.bend exact_branch; git/LAWS.bend latest_greatest; git/LAWS.bend latest_rel_greatest; git/LAWS.bend choose_greatest_release; git/LAWS.bend choose_greatest_prerelease; git/LAWS.bend choose_is_a_tag; add/LAWS.bend add_pins_chosen; add/LAWS.bend add_pins_chosen_rev; add/LAWS.bend add_pins_head_rev; add/LAWS.bend add_pins_named; add/LAWS.bend add_pins_commit; add/LAWS.bend add_commit_asks_nothing | -| EZ-RES-2 | `ez add` with no entry uses the revision's `[package] entry`, then `[package] bin`, then `main.bend`, and refuses if that file is not in the revision. An add that succeeds prints the import line for that entry's path inside the package, the line `ez publish` prints. `ez add @` with no entry uses the package's `main.bend`, then its first top-level `.bend` file, and records none when it has neither; it refuses an entry given that the package does not hold, and prints the import line with the name in place of the hash. | Proved | proved | pkg/LAWS.bend absent_entry_refused; git/LAWS.bend entry_pick_entry; git/LAWS.bend entry_pick_bin; git/LAWS.bend entry_pick_main; add/LAWS.bend add_entry_default; add/LAWS.bend add_entry_absent; add/LAWS.bend add_says_import; add/LAWS.bend add_named_entry_default; add/LAWS.bend add_named_entry_absent; add/LAWS.bend add_named_says_import | -| EZ-RES-3 | A target containing `://` or starting `git@` is a git URL. A target starting `/`, `./`, `../` or `~/` is a path. A target of exactly two segments of letters, digits, `-`, `_` and `.`, neither of them `.` or `..`, is `https://github.com/`, unless its second segment ends in `.bend`, which makes it a path. Anything else is a path, except the empty word, which is refused. For `ez add`, a path bend reads as a hub package's `@` names that package on the hub; a git URL, `owner/repo` or other path never does. | Proved | proved | ez/LAWS.bend classify_url; ez/LAWS.bend classify_scp; ez/LAWS.bend classify_abs; ez/LAWS.bend classify_here; ez/LAWS.bend classify_up; ez/LAWS.bend classify_home; ez/LAWS.bend classify_github; ez/LAWS.bend classify_else; ez/LAWS.bend aim_named; ez/LAWS.bend aim_path; ez/LAWS.bend aim_remote; ez/LAWS.bend aim_bad; ez/LAWS.bend aim_scp | -| EZ-RES-4 | `ez lock --upgrade` never moves a hub dependency. | Proved | proved | lock/LAWS.bend upgrade_holds_hub | -| EZ-RES-5 | An upgraded rev-only dependency moves to the default branch tip only when its pin is an ancestor of that tip, and stays a commit pin. Otherwise the upgrade refuses with exit 1. | Proved | proved | lock/LAWS.bend upgrade_forward_moves_onward; lock/LAWS.bend upgrade_forward_refuses_off; lock/LAWS.bend upgrade_forward_reaches_tip; git/LAWS.bend tip_of_head; git/LAWS.bend tip_skips_other; git/LAWS.bend tip_skips_symref | -| EZ-RES-6 | `--package NAME` asks the remote to resolve only the named dependency or tool, and every other ledger entry keeps its rev, tag and hash. Resolving is asking for refs, the default branch, ancestry, or a checkout at a new rev. | Proved | proved | lock/LAWS.bend upgrade_one_frames_deps; lock/LAWS.bend upgrade_one_frames_tools; lock/LAWS.bend upgrade_one_asks_alone | +| EZ-RES-1 | `ez add` with no ref pins the greatest semver-ish release tag on the remote; with no release, the greatest pre-release; with no semver-ish tag, the remote's default branch as its `HEAD` symref names it. A named ref resolves exactly, as `refs/tags/` and then `refs/heads/`. A 40-hex ref is used as a commit without asking the remote. | Proved | proved | src/git/LAWS.bend is_rev_needs_40; src/git/LAWS.bend is_rev_needs_hex; src/git/LAWS.bend is_rev_hex40; src/git/LAWS.bend choose_release; src/git/LAWS.bend choose_prerelease; src/git/LAWS.bend branch_of_symref; src/git/LAWS.bend branch_skips_other; src/git/LAWS.bend branch_skips_commit; src/git/LAWS.bend exact_skips; src/git/LAWS.bend exact_tag_first; src/git/LAWS.bend exact_branch; src/git/LAWS.bend latest_greatest; src/git/LAWS.bend latest_rel_greatest; src/git/LAWS.bend choose_greatest_release; src/git/LAWS.bend choose_greatest_prerelease; src/git/LAWS.bend choose_is_a_tag; src/add/LAWS.bend add_pins_chosen; src/add/LAWS.bend add_pins_chosen_rev; src/add/LAWS.bend add_pins_head_rev; src/add/LAWS.bend add_pins_named; src/add/LAWS.bend add_pins_commit; src/add/LAWS.bend add_commit_asks_nothing | +| EZ-RES-2 | `ez add` with no entry uses the revision's `[package] entry`, then `[package] bin`, then `main.bend`, and refuses if that file is not in the revision. An add that succeeds prints the import line for that entry's path inside the package, the line `ez publish` prints. `ez add @` with no entry uses the package's `main.bend`, then its first top-level `.bend` file, and records none when it has neither; it refuses an entry given that the package does not hold, and prints the import line with the name in place of the hash. | Proved | proved | src/pkg/LAWS.bend absent_entry_refused; src/git/LAWS.bend entry_pick_entry; src/git/LAWS.bend entry_pick_bin; src/git/LAWS.bend entry_pick_main; src/add/LAWS.bend add_entry_default; src/add/LAWS.bend add_entry_absent; src/add/LAWS.bend add_says_import; src/add/LAWS.bend add_named_entry_default; src/add/LAWS.bend add_named_entry_absent; src/add/LAWS.bend add_named_says_import | +| EZ-RES-3 | A target containing `://` or starting `git@` is a git URL. A target starting `/`, `./`, `../` or `~/` is a path. A target of exactly two segments of letters, digits, `-`, `_` and `.`, neither of them `.` or `..`, is `https://github.com/`, unless its second segment ends in `.bend`, which makes it a path. Anything else is a path, except the empty word, which is refused. For `ez add`, a path bend reads as a hub package's `@` names that package on the hub; a git URL, `owner/repo` or other path never does. | Proved | proved | src/ez/LAWS.bend classify_url; src/ez/LAWS.bend classify_scp; src/ez/LAWS.bend classify_abs; src/ez/LAWS.bend classify_here; src/ez/LAWS.bend classify_up; src/ez/LAWS.bend classify_home; src/ez/LAWS.bend classify_github; src/ez/LAWS.bend classify_else; src/ez/LAWS.bend aim_named; src/ez/LAWS.bend aim_path; src/ez/LAWS.bend aim_remote; src/ez/LAWS.bend aim_bad; src/ez/LAWS.bend aim_scp | +| EZ-RES-4 | `ez lock --upgrade` never moves a hub dependency. | Proved | proved | src/lock/LAWS.bend upgrade_holds_hub | +| EZ-RES-5 | An upgraded rev-only dependency moves to the default branch tip only when its pin is an ancestor of that tip, and stays a commit pin. Otherwise the upgrade refuses with exit 1. | Proved | proved | src/lock/LAWS.bend upgrade_forward_moves_onward; src/lock/LAWS.bend upgrade_forward_refuses_off; src/lock/LAWS.bend upgrade_forward_reaches_tip; src/git/LAWS.bend tip_of_head; src/git/LAWS.bend tip_skips_other; src/git/LAWS.bend tip_skips_symref | +| EZ-RES-6 | `--package NAME` asks the remote to resolve only the named dependency or tool, and every other ledger entry keeps its rev, tag and hash. Resolving is asking for refs, the default branch, ancestry, or a checkout at a new rev. | Proved | proved | src/lock/LAWS.bend upgrade_one_frames_deps; src/lock/LAWS.bend upgrade_one_frames_tools; src/lock/LAWS.bend upgrade_one_asks_alone | | EZ-RES-7 | Tags, refs, and ancestry reported by git are accurate. | Trusted | | | -| EZ-RES-8 | An upgraded tagged dependency re-resolves its tag. A tag that now names a commit the pin does not descend to, or a pinned commit whose tree no longer hashes to the pin, stops the upgrade with exit 1. | Proved | proved | lock/LAWS.bend upgrade_tag_follows; lock/LAWS.bend upgrade_tag_resolves; lock/LAWS.bend upgrade_tag_refuses_off; lock/LAWS.bend upgrade_tag_refuses_drift | +| EZ-RES-8 | An upgraded tagged dependency re-resolves its tag. A tag that now names a commit the pin does not descend to, or a pinned commit whose tree no longer hashes to the pin, stops the upgrade with exit 1. | Proved | proved | src/lock/LAWS.bend upgrade_tag_follows; src/lock/LAWS.bend upgrade_tag_resolves; src/lock/LAWS.bend upgrade_tag_refuses_off; src/lock/LAWS.bend upgrade_tag_refuses_drift | ### Vendoring and source rewriting (EZ-VEN) | ID | Requirement | Level | Status | Law | | :---- | :---- | :---- | :---- | :---- | -| EZ-VEN-1 | After `ez add`, `ez remove` or `ez lock --upgrade`, the `.gitignore` allowlist names exactly the hashes of dependencies marked `vendor = true`, and every other line of `.gitignore` is unchanged. | Proved | proved | ledger/LAWS.bend allowlist_is_the_ledger; ledger/LAWS.bend allowlist_keeps_other_lines; ledger/LAWS.bend sync_allowlist_is_the_ledger; ledger/LAWS.bend sync_keeps_other_lines; ledger/LAWS.bend sync_idempotent; ledger/LAWS.bend vended_once; remove/LAWS.bend remove_syncs_allowlist; lock/LAWS.bend upgrade_allowlist_is_the_ledger; lock/LAWS.bend upgrade_allowlist_keeps_other_lines; lock/LAWS.bend upgrade_vends_the_ledger; add/LAWS.bend add_syncs_allowlist; lock/LAWS.bend upgrade_allowlist_kept_in_sync; lock/LAWS.bend upgrade_unmoved_vends_the_ledger | -| EZ-VEN-2 | When an upgrade moves a hash, every line of a `.bend` file outside `.ez` and `.git` that starts `import /` names `` afterwards. | Proved | proved | ledger/LAWS.bend rewrite_names_new; lock/LAWS.bend upgrade_rewrites_imports | -| EZ-VEN-3 | Import rewriting leaves every other line of every file byte-identical, and does not write a file with no matching line. | Proved | proved | ledger/LAWS.bend rewrite_keeps_other_lines; ledger/LAWS.bend rewrite_keeps_line_count; ledger/LAWS.bend rewrite_nothing_named; lock/LAWS.bend upgrade_leaves_other_lines; lock/LAWS.bend upgrade_keeps_line_count; lock/LAWS.bend upgrade_writes_only_hits | -| EZ-VEN-4 | `ez doctor` never writes to the project's source files. | Proved | proved | doctor/LAWS.bend doctor_writes_nothing | -| EZ-VEN-5 | `ez doctor` reports every hash an import line names that the ledger does not, and every ledger dependency no import line names, and exits 1 when it reports any. | Proved | proved | doctor/LAWS.bend doctor_reports_unrecorded; doctor/LAWS.bend doctor_reports_unused; doctor/LAWS.bend doctor_drift_fails | -| EZ-VEN-6 | `ez doctor` reports a lock that `ez lock` would not write as it stands, judged without the network from the ledger, the committed sources and the trees under `BEND_LIB`, and exits 1 when it reports one or cannot judge it. | Proved | proved | doctor/LAWS.bend doctor_passes_fresh_lock; doctor/LAWS.bend doctor_says_fresh_lock; doctor/LAWS.bend doctor_reports_stale_lock; doctor/LAWS.bend doctor_stale_lock_fails; doctor/LAWS.bend doctor_unchecked_lock_fails; doctor/LAWS.bend doctor_unchecked_names_fail | +| EZ-VEN-1 | After `ez add`, `ez remove` or `ez lock --upgrade`, the `.gitignore` allowlist names exactly the hashes of dependencies marked `vendor = true`, and every other line of `.gitignore` is unchanged. | Proved | proved | src/ledger/LAWS.bend allowlist_is_the_ledger; src/ledger/LAWS.bend allowlist_keeps_other_lines; src/ledger/LAWS.bend sync_allowlist_is_the_ledger; src/ledger/LAWS.bend sync_keeps_other_lines; src/ledger/LAWS.bend sync_idempotent; src/ledger/LAWS.bend vended_once; src/remove/LAWS.bend remove_syncs_allowlist; src/lock/LAWS.bend upgrade_allowlist_is_the_ledger; src/lock/LAWS.bend upgrade_allowlist_keeps_other_lines; src/lock/LAWS.bend upgrade_vends_the_ledger; src/add/LAWS.bend add_syncs_allowlist; src/lock/LAWS.bend upgrade_allowlist_kept_in_sync; src/lock/LAWS.bend upgrade_unmoved_vends_the_ledger | +| EZ-VEN-2 | When an upgrade moves a hash, every line of a `.bend` file outside `.ez` and `.git` that starts `import /` names `` afterwards. | Proved | proved | src/ledger/LAWS.bend rewrite_names_new; src/lock/LAWS.bend upgrade_rewrites_imports | +| EZ-VEN-3 | Import rewriting leaves every other line of every file byte-identical, and does not write a file with no matching line. | Proved | proved | src/ledger/LAWS.bend rewrite_keeps_other_lines; src/ledger/LAWS.bend rewrite_keeps_line_count; src/ledger/LAWS.bend rewrite_nothing_named; src/lock/LAWS.bend upgrade_leaves_other_lines; src/lock/LAWS.bend upgrade_keeps_line_count; src/lock/LAWS.bend upgrade_writes_only_hits | +| EZ-VEN-4 | `ez doctor` never writes to the project's source files. | Proved | proved | src/doctor/LAWS.bend doctor_writes_nothing | +| EZ-VEN-5 | `ez doctor` reports every hash an import line names that the ledger does not, and every ledger dependency no import line names, and exits 1 when it reports any. | Proved | proved | src/doctor/LAWS.bend doctor_reports_unrecorded; src/doctor/LAWS.bend doctor_reports_unused; src/doctor/LAWS.bend doctor_drift_fails | +| EZ-VEN-6 | `ez doctor` reports a lock that `ez lock` would not write as it stands, judged without the network from the ledger, the committed sources and the trees under `BEND_LIB`, and exits 1 when it reports one or cannot judge it. | Proved | proved | src/doctor/LAWS.bend doctor_passes_fresh_lock; src/doctor/LAWS.bend doctor_says_fresh_lock; src/doctor/LAWS.bend doctor_reports_stale_lock; src/doctor/LAWS.bend doctor_stale_lock_fails; src/doctor/LAWS.bend doctor_unchecked_lock_fails; src/doctor/LAWS.bend doctor_unchecked_names_fail | ### Fetch (EZ-FETCH) | ID | Requirement | Level | Status | Law | | :---- | :---- | :---- | :---- | :---- | -| EZ-FETCH-1 | `ez fetch` writes a package file under `BEND_LIB` only when its digest matches the lock: a hub body's digest starts with the lock's sum, a git file's digest equals it, and a git package's checkout weighs to the narHash the lock records. | Proved | proved | fetch/LAWS.bend fetch_lays_the_lock; fetch/LAWS.bend fetch_lays_weighed; fetch/LAWS.bend fetch_weighs_the_checkout; fetch/LAWS.bend fetch_refuses_unweighed | +| EZ-FETCH-1 | `ez fetch` writes a package file under `BEND_LIB` only when its digest matches the lock: a hub body's digest starts with the lock's sum, a git file's digest equals it, and a git package's checkout weighs to the narHash the lock records. | Proved | proved | src/fetch/LAWS.bend fetch_lays_the_lock; src/fetch/LAWS.bend fetch_lays_weighed; src/fetch/LAWS.bend fetch_weighs_the_checkout; src/fetch/LAWS.bend fetch_refuses_unweighed | ### Hub names (EZ-HUB) | ID | Requirement | Level | Status | Law | | :---- | :---- | :---- | :---- | :---- | -| EZ-HUB-1 | A named import `@/...` resolves to one hash: the one ez.toml records for that name, else the one the lock being rewritten records, else the one the hub answers. The lock walks that package, records the pair under `[names]`, and `ez fetch` lays that hash in the name's file. `ez add @` asks the hub the ledger names, and records the name with the hash the hub answers. | Proved | proved | lock/LAWS.bend named_kid_queued; lock/LAWS.bend lock_names_agree; lock/LAWS.bend ledger_names_first; fetch/LAWS.bend fetch_names_the_lock; add/LAWS.bend add_named_records_name; add/LAWS.bend add_named_asks_hub | -| EZ-HUB-2 | `ez lock` asks the hub what a name names only when neither ez.toml nor the lock being rewritten records it. | Proved | proved | lock/LAWS.bend lock_answer_names; lock/LAWS.bend resolved_not_asked | -| EZ-HUB-3 | An import whose first path segment holds `@` is a hub dependency and never a file of the project. A name bend would refuse is refused, in bend's words, before any package is hashed around it. | Proved | proved | pkg/LAWS.bend named_is_no_module; pkg/LAWS.bend unnamed_stops; pkg/LAWS.bend unnamed_refused; lock/LAWS.bend lock_reads_named | -| EZ-HUB-4 | `ez lock` and `ez fetch` lay `BEND_LIB/names/@` holding the hash the lock records, for every name it records, and `ez add @` lays the file of the name it adds. `ez fetch` rewrites a file that names another hash, and says so. `ez doctor` fails when a file is missing or names another hash. | Proved | proved | lock/LAWS.bend lock_lays_its_names; fetch/LAWS.bend fetch_lays_missing_name; fetch/LAWS.bend fetch_rewrites_name; fetch/LAWS.bend fetch_refuses_unread_name; fetch/LAWS.bend fetch_lays_the_names; doctor/LAWS.bend doctor_wrong_name_fails; add/LAWS.bend add_named_lays_name | +| EZ-HUB-1 | A named import `@/...` resolves to one hash: the one ez.toml records for that name, else the one the lock being rewritten records, else the one the hub answers. The lock walks that package, records the pair under `[names]`, and `ez fetch` lays that hash in the name's file. `ez add @` asks the hub the ledger names, and records the name with the hash the hub answers. | Proved | proved | src/lock/LAWS.bend named_kid_queued; src/lock/LAWS.bend lock_names_agree; src/lock/LAWS.bend ledger_names_first; src/fetch/LAWS.bend fetch_names_the_lock; src/add/LAWS.bend add_named_records_name; src/add/LAWS.bend add_named_asks_hub | +| EZ-HUB-2 | `ez lock` asks the hub what a name names only when neither ez.toml nor the lock being rewritten records it. | Proved | proved | src/lock/LAWS.bend lock_answer_names; src/lock/LAWS.bend resolved_not_asked | +| EZ-HUB-3 | An import whose first path segment holds `@` is a hub dependency and never a file of the project. A name bend would refuse is refused, in bend's words, before any package is hashed around it. | Proved | proved | src/pkg/LAWS.bend named_is_no_module; src/pkg/LAWS.bend unnamed_stops; src/pkg/LAWS.bend unnamed_refused; src/lock/LAWS.bend lock_reads_named | +| EZ-HUB-4 | `ez lock` and `ez fetch` lay `BEND_LIB/names/@` holding the hash the lock records, for every name it records, and `ez add @` lays the file of the name it adds. `ez fetch` rewrites a file that names another hash, and says so. `ez doctor` fails when a file is missing or names another hash. | Proved | proved | src/lock/LAWS.bend lock_lays_its_names; src/fetch/LAWS.bend fetch_lays_missing_name; src/fetch/LAWS.bend fetch_rewrites_name; src/fetch/LAWS.bend fetch_refuses_unread_name; src/fetch/LAWS.bend fetch_lays_the_names; src/doctor/LAWS.bend doctor_wrong_name_fails; src/add/LAWS.bend add_named_lays_name | ### Tools (EZ-TOOL) | ID | Requirement | Level | Status | Law | | :---- | :---- | :---- | :---- | :---- | -| EZ-TOOL-1 | The link directory is `$EZ_TOOL_BIN`, else `$XDG_BIN_HOME`, else `$HOME/.local/bin`, an empty value counting as unset. `ez tool install` and `ez tool upgrade` link there, and refuse before anything is built when all three are empty. | Proved | proved | tool/LAWS.bend bin_dir_ez; tool/LAWS.bend bin_dir_xdg; tool/LAWS.bend bin_dir_home; tool/LAWS.bend bin_dir_none; tool/LAWS.bend tool_links_in_bin_dir; tool/LAWS.bend tool_needs_bin_dir | -| EZ-TOOL-2 | A cached binary is reused only when the recorded commit, built file and bend version all equal the resolved ones, and never when the resolved commit is empty. A cached checkout is reused only when its recorded commit equals the resolved one. | Proved | proved | ez/LAWS.bend key_rev_differs; ez/LAWS.bend key_file_differs; ez/LAWS.bend key_bend_differs; ez/LAWS.bend key_no_rev; ez/LAWS.bend key_same_reuses; ez/LAWS.bend checkout_differs; ez/LAWS.bend checkout_same; tool/LAWS.bend tool_reuses_record; tool/LAWS.bend tool_builds_on_miss | -| EZ-TOOL-3 | A local target with uncommitted or untracked changes, whatever the repository's own settings hide, or a path that is not the top of a checkout, resolves to no commit and is rebuilt on every run. | Proved | proved | tool/LAWS.bend local_rev_dirty; tool/LAWS.bend local_rev_unchecked; tool/LAWS.bend local_rev_elsewhere; tool/LAWS.bend tool_unrevved_builds | -| EZ-TOOL-4 | A target naming a `[tools.*]` pin in ez.toml builds the lock's rev, url, entry and bin. An `owner/repo` or URL target builds the commit `git ls-remote HEAD` names. A path builds its clean `HEAD`. A checkout with no ez.toml is a plain Bend repository: it is built with no lock fetched and with BEND_LIB at a library of its own under the cache, where bend fetches its hub imports. A checkout with an ez.toml and no ez.lock.toml is refused when its binary is to be built. | Proved | proved | tool/LAWS.bend tool_pin_src; tool/LAWS.bend tool_pin_rev; tool/LAWS.bend tool_pin_url; tool/LAWS.bend tool_pin_over; tool/LAWS.bend tool_free_src; tool/LAWS.bend tool_free_rev; tool/LAWS.bend tool_path_rev; tool/LAWS.bend local_rev_clean; tool/LAWS.bend tool_plain_no_lock; tool/LAWS.bend tool_plain_lib; tool/LAWS.bend tool_ledger_needs_lock | -| EZ-TOOL-5 | `ez tool run` exits with the built program's status; any failure before the program runs exits 1. | Proved | proved | tool/LAWS.bend tool_run_exits_with_program; tool/LAWS.bend tool_refusal_exits_one | -| EZ-TOOL-6 | `ez tool install` and `ez tool upgrade` never run the built binary. | Proved | proved | tool/LAWS.bend tool_link_never_runs | -| EZ-TOOL-7 | The built file is the pin's `bin`, then the pin's `entry`, then the file `--entry` names, then the checkout's `bin`, then its `entry`, then `main.bend`, and a built file that is not in the checkout is refused. The link is named after the checkout's package name, or `app`; a plain repository's is the built file's name without `.bend`, or the repository's name when that is `main`; and a name that is not a TOML bare key is refused. | Proved | proved | tool/LAWS.bend file_pin_bin; tool/LAWS.bend file_pin_entry; tool/LAWS.bend file_bin; tool/LAWS.bend file_entry; tool/LAWS.bend file_main; tool/LAWS.bend file_flag_over_ledger; tool/LAWS.bend file_pin_over_flag; tool/LAWS.bend tool_builds_file; tool/LAWS.bend tool_plain_builds_main; tool/LAWS.bend tool_plain_builds_entry; tool/LAWS.bend tool_refuses_missing_entry; tool/LAWS.bend out_name_own; tool/LAWS.bend out_name_app; tool/LAWS.bend plain_name_stem; tool/LAWS.bend plain_name_repo; tool/LAWS.bend tool_plain_named; tool/LAWS.bend tool_links_named; tool/LAWS.bend tool_refuses_unsafe_name | -| EZ-TOOL-8 | A remote target whose cache slug is empty, absolute, or climbs with `..` is refused. | Proved | proved | tool/LAWS.bend remote_refuses_slug; tool/LAWS.bend tool_refuses_bad_slug; tool/LAWS.bend tool_refuses_nowhere | -| EZ-TOOL-9 | `ez tool run [--entry ] ` passes every word after the target to the program, dropping one leading `--`. `ez run` passes every word after `run` to the entry ez.toml names, or `main.bend` when it names none. | Proved | proved | tool/LAWS.bend tool_rest_dash; tool/LAWS.bend tool_rest_word; tool/LAWS.bend tool_rest_none; tool/LAWS.bend tool_rest_entry; tool/LAWS.bend tool_run_passes_words; tool/LAWS.bend run_line_rest; ez/LAWS.bend run_starts_entry; ez/LAWS.bend run_starts_main | +| EZ-TOOL-1 | The link directory is `$EZ_TOOL_BIN`, else `$XDG_BIN_HOME`, else `$HOME/.local/bin`, an empty value counting as unset. `ez tool install` and `ez tool upgrade` link there, and refuse before anything is built when all three are empty. | Proved | proved | src/tool/LAWS.bend bin_dir_ez; src/tool/LAWS.bend bin_dir_xdg; src/tool/LAWS.bend bin_dir_home; src/tool/LAWS.bend bin_dir_none; src/tool/LAWS.bend tool_links_in_bin_dir; src/tool/LAWS.bend tool_needs_bin_dir | +| EZ-TOOL-2 | A cached binary is reused only when the recorded commit, built file and bend version all equal the resolved ones, and never when the resolved commit is empty. A cached checkout is reused only when its recorded commit equals the resolved one. | Proved | proved | src/ez/LAWS.bend key_rev_differs; src/ez/LAWS.bend key_file_differs; src/ez/LAWS.bend key_bend_differs; src/ez/LAWS.bend key_no_rev; src/ez/LAWS.bend key_same_reuses; src/ez/LAWS.bend checkout_differs; src/ez/LAWS.bend checkout_same; src/tool/LAWS.bend tool_reuses_record; src/tool/LAWS.bend tool_builds_on_miss | +| EZ-TOOL-3 | A local target with uncommitted or untracked changes, whatever the repository's own settings hide, or a path that is not the top of a checkout, resolves to no commit and is rebuilt on every run. | Proved | proved | src/tool/LAWS.bend local_rev_dirty; src/tool/LAWS.bend local_rev_unchecked; src/tool/LAWS.bend local_rev_elsewhere; src/tool/LAWS.bend tool_unrevved_builds | +| EZ-TOOL-4 | A target naming a `[tools.*]` pin in ez.toml builds the lock's rev, url, entry and bin. An `owner/repo` or URL target builds the commit `git ls-remote HEAD` names. A path builds its clean `HEAD`. A checkout with no ez.toml is a plain Bend repository: it is built with no lock fetched and with BEND_LIB at a library of its own under the cache, where bend fetches its hub imports. A checkout with an ez.toml and no ez.lock.toml is refused when its binary is to be built. | Proved | proved | src/tool/LAWS.bend tool_pin_src; src/tool/LAWS.bend tool_pin_rev; src/tool/LAWS.bend tool_pin_url; src/tool/LAWS.bend tool_pin_over; src/tool/LAWS.bend tool_free_src; src/tool/LAWS.bend tool_free_rev; src/tool/LAWS.bend tool_path_rev; src/tool/LAWS.bend local_rev_clean; src/tool/LAWS.bend tool_plain_no_lock; src/tool/LAWS.bend tool_plain_lib; src/tool/LAWS.bend tool_ledger_needs_lock | +| EZ-TOOL-5 | `ez tool run` exits with the built program's status; any failure before the program runs exits 1. | Proved | proved | src/tool/LAWS.bend tool_run_exits_with_program; src/tool/LAWS.bend tool_refusal_exits_one | +| EZ-TOOL-6 | `ez tool install` and `ez tool upgrade` never run the built binary. | Proved | proved | src/tool/LAWS.bend tool_link_never_runs | +| EZ-TOOL-7 | The built file is the pin's `bin`, then the pin's `entry`, then the file `--entry` names, then the checkout's `bin`, then its `entry`, then `main.bend`, and a built file that is not in the checkout is refused. The link is named after the checkout's package name, or `app`; a plain repository's is the built file's name without `.bend`, or the repository's name when that is `main`; and a name that is not a TOML bare key is refused. | Proved | proved | src/tool/LAWS.bend file_pin_bin; src/tool/LAWS.bend file_pin_entry; src/tool/LAWS.bend file_bin; src/tool/LAWS.bend file_entry; src/tool/LAWS.bend file_main; src/tool/LAWS.bend file_flag_over_ledger; src/tool/LAWS.bend file_pin_over_flag; src/tool/LAWS.bend tool_builds_file; src/tool/LAWS.bend tool_plain_builds_main; src/tool/LAWS.bend tool_plain_builds_entry; src/tool/LAWS.bend tool_refuses_missing_entry; src/tool/LAWS.bend out_name_own; src/tool/LAWS.bend out_name_app; src/tool/LAWS.bend plain_name_stem; src/tool/LAWS.bend plain_name_repo; src/tool/LAWS.bend tool_plain_named; src/tool/LAWS.bend tool_links_named; src/tool/LAWS.bend tool_refuses_unsafe_name | +| EZ-TOOL-8 | A remote target whose cache slug is empty, absolute, or climbs with `..` is refused. | Proved | proved | src/tool/LAWS.bend remote_refuses_slug; src/tool/LAWS.bend tool_refuses_bad_slug; src/tool/LAWS.bend tool_refuses_nowhere | +| EZ-TOOL-9 | `ez tool run [--entry ] ` passes every word after the target to the program, dropping one leading `--`. `ez run` passes every word after `run` to the entry ez.toml names, or `main.bend` when it names none. | Proved | proved | src/tool/LAWS.bend tool_rest_dash; src/tool/LAWS.bend tool_rest_word; src/tool/LAWS.bend tool_rest_none; src/tool/LAWS.bend tool_rest_entry; src/tool/LAWS.bend tool_run_passes_words; src/tool/LAWS.bend run_line_rest; src/ez/LAWS.bend run_starts_entry; src/ez/LAWS.bend run_starts_main | ### Publish (EZ-PUB) | ID | Requirement | Level | Status | Law | | :---- | :---- | :---- | :---- | :---- | -| EZ-PUB-1 | `ez publish` refuses, and sends nothing, when `git status --porcelain --untracked-files=normal` names any path, when git cannot answer it, or when a file of the package is one git does not track as unchanged (`git ls-files -v` tag `H`), an ignored file included. | Proved | proved | pub/LAWS.bend clean_is_all_blank; pub/LAWS.bend untracked_is_dirty; pub/LAWS.bend modified_is_dirty; pub/LAWS.bend staged_is_dirty; pub/LAWS.bend assumed_is_untracked; pub/LAWS.bend skipped_is_untracked; pub/LAWS.bend pub_dirty_refuses; pub/LAWS.bend pub_gitless_refuses; pub/LAWS.bend pub_stray_sends_nothing; pub/LAWS.bend pub_stop_sends_nothing; pub/LAWS.bend pub_unsent_refuses | -| EZ-PUB-2 | `ez publish` succeeds only when bend exits 0, a line of its output is exactly a `0x` name, and every such line equals ez's own hash; it then prints that hash and the import line for the entry's path inside the package, by the package's name when EZ-PUB-3 gives it one and by that hash otherwise. Any other answer exits 1. | Proved | proved | pub/LAWS.bend unread_never_agrees; pub/LAWS.bend differs_never_agrees; pub/LAWS.bend ours_agrees; pub/LAWS.bend progress_is_not_an_answer; pub/LAWS.bend import_is_not_an_answer; pub/LAWS.bend is_name_needs_0x; pub/LAWS.bend is_name_needs_length; pub/LAWS.bend is_name_needs_hex; pub/LAWS.bend is_name_hex34; pub/LAWS.bend pub_needs_agreement; pub/LAWS.bend pub_reports_ours; pub/LAWS.bend pub_reports_hash | -| EZ-PUB-3 | `ez publish` publishes under a name when the ledger's `[package]` table gives both `publish-as` and `version`: it runs `bend --publish @.0` and, on success, prints the hash and the import line by that name. `publish-as` must be a hub name as bend's NAMED rule reads one, and `version` MAJOR.MINOR.PATCH with no leading zeros and no pre-release or build suffix. With only one of the two keys, or with either one malformed, it refuses before it asks git anything or sends anything. With neither it publishes by hash as before. | Proved | proved | pub/LAWS.bend semver_needs_digits; pub/LAWS.bend prerelease_refused; pub/LAWS.bend build_refused; pub/LAWS.bend neither_is_hash; pub/LAWS.bend name_needs_version; pub/LAWS.bend version_needs_name; pub/LAWS.bend bad_name_refused; pub/LAWS.bend bad_version_refused; pub/LAWS.bend named_is_four_part; pub/LAWS.bend upload_by_hash; pub/LAWS.bend upload_by_name; pub/LAWS.bend pub_misnamed_stops; pub/LAWS.bend pub_named_uploads_named; pub/LAWS.bend pub_unnamed_uploads_by_hash; pub/LAWS.bend pub_reports_name; init/LAWS.bend init_publishes_by_hash | -| EZ-PUB-4 | Once every check before the upload has passed, and just before the upload runs, `ez publish` prints `hub description: ` on stderr, the line the hub will describe the package by: the first line of the package's first file by path, in plain string order, passing over every file named `LICENSE`. A publish refused before the upload prints only why. | Proved | proved | pub/LAWS.bend line_first_cut; pub/LAWS.bend hub_license_named; pub/LAWS.bend hub_skips_license; pub/LAWS.bend hub_first_by_path; pub/LAWS.bend pub_upload_says_description | -| EZ-PUB-5 | `ez publish` uploads only when every hub package the package imports is on the hub the ledger names: for each `0x/...` import in the package's files the hub serves a manifest that hashes to that name, and for each `@/...` import the hub resolves the name to a `0x` name, the one the lock or the ledger resolved it to when either records one. Before the upload it asks the hub about each; a package the hub does not have, and a hub that could not be asked, refuse with exit 1, naming each such import and the dependency key and origin the ledger records for it, and nothing is sent. | Proved | proved | pub/LAWS.bend pub_sends_only_on_hub; pub/LAWS.bend pub_offhub_sends_nothing; pub/LAWS.bend pub_offhub_refuses; pub/LAWS.bend hub_one_off_is_off; pub/LAWS.bend hub_404_is_absent; pub/LAWS.bend hub_unreachable_is_off; pub/LAWS.bend hub_name_elsewhere_is_off; pub/LAWS.bend hub_name_there | +| EZ-PUB-1 | `ez publish` refuses, and sends nothing, when `git status --porcelain --untracked-files=normal` names any path, when git cannot answer it, or when a file of the package is one git does not track as unchanged (`git ls-files -v` tag `H`), an ignored file included. | Proved | proved | src/pub/LAWS.bend clean_is_all_blank; src/pub/LAWS.bend untracked_is_dirty; src/pub/LAWS.bend modified_is_dirty; src/pub/LAWS.bend staged_is_dirty; src/pub/LAWS.bend assumed_is_untracked; src/pub/LAWS.bend skipped_is_untracked; src/pub/LAWS.bend pub_dirty_refuses; src/pub/LAWS.bend pub_gitless_refuses; src/pub/LAWS.bend pub_stray_sends_nothing; src/pub/LAWS.bend pub_stop_sends_nothing; src/pub/LAWS.bend pub_unsent_refuses | +| EZ-PUB-2 | `ez publish` succeeds only when bend exits 0, a line of its output is exactly a `0x` name, and every such line equals ez's own hash; it then prints that hash and the import line for the entry's path inside the package, by the package's name when EZ-PUB-3 gives it one and by that hash otherwise. Any other answer exits 1. | Proved | proved | src/pub/LAWS.bend unread_never_agrees; src/pub/LAWS.bend differs_never_agrees; src/pub/LAWS.bend ours_agrees; src/pub/LAWS.bend progress_is_not_an_answer; src/pub/LAWS.bend import_is_not_an_answer; src/pub/LAWS.bend is_name_needs_0x; src/pub/LAWS.bend is_name_needs_length; src/pub/LAWS.bend is_name_needs_hex; src/pub/LAWS.bend is_name_hex34; src/pub/LAWS.bend pub_needs_agreement; src/pub/LAWS.bend pub_reports_ours; src/pub/LAWS.bend pub_reports_hash | +| EZ-PUB-3 | `ez publish` publishes under a name when the ledger's `[package]` table gives both `publish-as` and `version`: it runs `bend --publish @.0` and, on success, prints the hash and the import line by that name. `publish-as` must be a hub name as bend's NAMED rule reads one, and `version` MAJOR.MINOR.PATCH with no leading zeros and no pre-release or build suffix. With only one of the two keys, or with either one malformed, it refuses before it asks git anything or sends anything. With neither it publishes by hash as before. | Proved | proved | src/pub/LAWS.bend semver_needs_digits; src/pub/LAWS.bend prerelease_refused; src/pub/LAWS.bend build_refused; src/pub/LAWS.bend neither_is_hash; src/pub/LAWS.bend name_needs_version; src/pub/LAWS.bend version_needs_name; src/pub/LAWS.bend bad_name_refused; src/pub/LAWS.bend bad_version_refused; src/pub/LAWS.bend named_is_four_part; src/pub/LAWS.bend upload_by_hash; src/pub/LAWS.bend upload_by_name; src/pub/LAWS.bend pub_misnamed_stops; src/pub/LAWS.bend pub_named_uploads_named; src/pub/LAWS.bend pub_unnamed_uploads_by_hash; src/pub/LAWS.bend pub_reports_name; src/init/LAWS.bend init_publishes_by_hash | +| EZ-PUB-4 | Once every check before the upload has passed, and just before the upload runs, `ez publish` prints `hub description: ` on stderr, the line the hub will describe the package by: the first line of the package's first file by path, in plain string order, passing over every file named `LICENSE`. A publish refused before the upload prints only why. | Proved | proved | src/pub/LAWS.bend line_first_cut; src/pub/LAWS.bend hub_license_named; src/pub/LAWS.bend hub_skips_license; src/pub/LAWS.bend hub_first_by_path; src/pub/LAWS.bend pub_upload_says_description | +| EZ-PUB-5 | `ez publish` uploads only when every hub package the package imports is on the hub the ledger names: for each `0x/...` import in the package's files the hub serves a manifest that hashes to that name, and for each `@/...` import the hub resolves the name to a `0x` name, the one the lock or the ledger resolved it to when either records one. Before the upload it asks the hub about each; a package the hub does not have, and a hub that could not be asked, refuse with exit 1, naming each such import and the dependency key and origin the ledger records for it, and nothing is sent. | Proved | proved | src/pub/LAWS.bend pub_sends_only_on_hub; src/pub/LAWS.bend pub_offhub_sends_nothing; src/pub/LAWS.bend pub_offhub_refuses; src/pub/LAWS.bend hub_one_off_is_off; src/pub/LAWS.bend hub_404_is_absent; src/pub/LAWS.bend hub_unreachable_is_off; src/pub/LAWS.bend hub_name_elsewhere_is_off; src/pub/LAWS.bend hub_name_there | ### Exit status (EZ-OUT) | ID | Requirement | Level | Status | Law | | :---- | :---- | :---- | :---- | :---- | -| EZ-OUT-1 | Every command exits 0 on success and 1 on any failure ez detects, except `ez run` and `ez tool run`, which exit with the program's status. | Proved | proved | init/LAWS.bend init_exits_as_it_refuses; lock/LAWS.bend lock_exits_as_it_refuses; remove/LAWS.bend remove_exits_as_it_refuses; add/LAWS.bend add_exits_as_it_refuses; fetch/LAWS.bend fetch_exits_as_it_refuses; tool/LAWS.bend tool_refusal_status_one; tool/LAWS.bend tool_run_status_is_program; tool/LAWS.bend tool_link_status_zero; tool/LAWS.bend sync_exits_as_it_refuses; tool/LAWS.bend sync_needs_ledger; pub/LAWS.bend pub_exits_as_it_refuses; doctor/LAWS.bend doctor_exits_as_it_fails; ez/LAWS.bend build_exits_as_bend; ez/LAWS.bend check_exits_as_it_passes; ez/LAWS.bend gate_exits_as_it_counts; ez/LAWS.bend package_needs_upgrade; ez/LAWS.bend start_needs_ledger; ez/LAWS.bend start_needs_parse; ez/LAWS.bend run_refusal_exits_one; ez/LAWS.bend run_exits_with_program; ez/LAWS.bend help_exits_zero; ez/LAWS.bend usage_error_exits_one; ez/LAWS.bend bare_exits_zero; ez/LAWS.bend group_exits_one; ez/LAWS.bend command_runs; ez/LAWS.bend command_ends_its_own | -| EZ-OUT-2 | A command that refuses writes nothing: every file it would otherwise write or remove is left as it found it. | Proved | proved | init/LAWS.bend init_refusal_writes_nothing; lock/LAWS.bend lock_refusal_writes_nothing; remove/LAWS.bend remove_refusal_writes_nothing; add/LAWS.bend add_refusal_writes_nothing; fetch/LAWS.bend fetch_refusal_writes_nothing; tool/LAWS.bend tool_refusal_writes_nothing; tool/LAWS.bend tool_missing_entry_writes_nothing; tool/LAWS.bend sync_refusal_installs_nothing; pub/LAWS.bend pub_refusal_writes_nothing; pub/LAWS.bend pub_misnamed_writes_nothing; pub/LAWS.bend pub_offhub_writes_nothing; add/LAWS.bend add_named_refusal_writes_nothing; add/LAWS.bend add_named_refuses_unknown; add/LAWS.bend add_named_refuses_unhashed; add/LAWS.bend add_named_refuses_manifest | +| EZ-OUT-1 | Every command exits 0 on success and 1 on any failure ez detects, except `ez run` and `ez tool run`, which exit with the program's status. | Proved | proved | src/init/LAWS.bend init_exits_as_it_refuses; src/lock/LAWS.bend lock_exits_as_it_refuses; src/remove/LAWS.bend remove_exits_as_it_refuses; src/add/LAWS.bend add_exits_as_it_refuses; src/fetch/LAWS.bend fetch_exits_as_it_refuses; src/tool/LAWS.bend tool_refusal_status_one; src/tool/LAWS.bend tool_run_status_is_program; src/tool/LAWS.bend tool_link_status_zero; src/tool/LAWS.bend sync_exits_as_it_refuses; src/tool/LAWS.bend sync_needs_ledger; src/pub/LAWS.bend pub_exits_as_it_refuses; src/doctor/LAWS.bend doctor_exits_as_it_fails; src/ez/LAWS.bend build_exits_as_bend; src/ez/LAWS.bend check_exits_as_it_passes; src/ez/LAWS.bend gate_exits_as_it_counts; src/ez/LAWS.bend package_needs_upgrade; src/ez/LAWS.bend start_needs_ledger; src/ez/LAWS.bend start_needs_parse; src/ez/LAWS.bend run_refusal_exits_one; src/ez/LAWS.bend run_exits_with_program; src/ez/LAWS.bend help_exits_zero; src/ez/LAWS.bend usage_error_exits_one; src/ez/LAWS.bend bare_exits_zero; src/ez/LAWS.bend group_exits_one; src/ez/LAWS.bend command_runs; src/ez/LAWS.bend command_ends_its_own | +| EZ-OUT-2 | A command that refuses writes nothing: every file it would otherwise write or remove is left as it found it. | Proved | proved | src/init/LAWS.bend init_refusal_writes_nothing; src/lock/LAWS.bend lock_refusal_writes_nothing; src/remove/LAWS.bend remove_refusal_writes_nothing; src/add/LAWS.bend add_refusal_writes_nothing; src/fetch/LAWS.bend fetch_refusal_writes_nothing; src/tool/LAWS.bend tool_refusal_writes_nothing; src/tool/LAWS.bend tool_missing_entry_writes_nothing; src/tool/LAWS.bend sync_refusal_installs_nothing; src/pub/LAWS.bend pub_refusal_writes_nothing; src/pub/LAWS.bend pub_misnamed_writes_nothing; src/pub/LAWS.bend pub_offhub_writes_nothing; src/add/LAWS.bend add_named_refusal_writes_nothing; src/add/LAWS.bend add_named_refuses_unknown; src/add/LAWS.bend add_named_refuses_unhashed; src/add/LAWS.bend add_named_refuses_manifest | ## Left to prove No requirement is pending. The paragraphs below record how each proved requirement that took more than one command was closed, and what its laws rest on. -EZ-HASH-3 is proved of every command that lays a tree. Over the package walk (`pkg/pkg.bend`), the `0x` name of the files it found, and their manifest, are the name and the manifest of the files it lays, each weighed by its own text. `ez add`, `ez fetch` and `ez lock`, plain or `--upgrade`: every tree the plan lays has the manifest of the texts it lays as its last file, each weighed by its own text, and is named by that manifest's `0x` hash (`add_lays_named`, `add_named_lays_named`, `fetch_lays_named`, `lock_lays_named`, all over `P.lays.named`). `ez add @` judges the package the hub serves as `ez lock` judges a hub package, so one whose manifest does not hash to the name the hub answered is refused, never laid (`add_named_refuses_manifest`). The lock checks, besides the manifest's digest and each file's sum, that the files it lays hash to the name, and lays the manifest of those files, so a package whose manifest hashes to its name but is not written the way the name is taken is refused, not locked (see docs/rfc/ez-spec.md, "Decided behavior changes"). +EZ-HASH-3 is proved of every command that lays a tree. Over the package walk (`src/pkg/pkg.bend`), the `0x` name of the files it found, and their manifest, are the name and the manifest of the files it lays, each weighed by its own text. `ez add`, `ez fetch` and `ez lock`, plain or `--upgrade`: every tree the plan lays has the manifest of the texts it lays as its last file, each weighed by its own text, and is named by that manifest's `0x` hash (`add_lays_named`, `add_named_lays_named`, `fetch_lays_named`, `lock_lays_named`, all over `P.lays.named`). `ez add @` judges the package the hub serves as `ez lock` judges a hub package, so one whose manifest does not hash to the name the hub answered is refused, never laid (`add_named_refuses_manifest`). The lock checks, besides the manifest's digest and each file's sum, that the files it lays hash to the name, and lays the manifest of those files, so a package whose manifest hashes to its name but is not written the way the name is taken is refused, not locked (see docs/rfc/ez-spec.md, "Decided behavior changes"). EZ-HASH-4 stays Trusted, since bend is another program, but the walk's side of it is stated in laws. bend 2.0.27 publishes every file named exactly `LICENSE` beside a file of the package, at the same path, and refuses a file under a directory named license in any case. The walk takes such a LICENSE along beside a module (`license_goes_along`) and beside a foreign body (`foreign_license_goes_along`), asks for one it was not given rather than hashing without it (`license_asked`), finds a file whose directory holds none as it always did (`no_license_as_before`), and refuses a package with a file under a license directory, naming it (`licensed_names`, `license_dir_refused`, `license_dir_passes`). A ledger written before names a git package without its LICENSE files, and the name decides: `ez lock` judges a checkout whose walked manifest is not the one its name is the digest of without them (`bare_drops_license`, `bare_keeps_sources`, `git_named_without_license`), and `ez lock --upgrade` weighs a pinned commit the same way (`upgrade_named_without_license`). -EZ-HASH-7 is proved of the reading the NAR walk (`sha/nar.bend`) makes of its listing: every field is cut at the NUL that ends it and nowhere else (`nar_field_verbatim`), so a listing is read back as the fields it was printed from (`nar_listing_verbatim`), whatever spaces or newlines a name or target holds. That the listing is what the filesystem holds, and that the walk builds the NAR from it as nix's dumper does, is EZ-HASH-5. +EZ-HASH-7 is proved of the reading the NAR walk (`src/sha/nar.bend`) makes of its listing: every field is cut at the NUL that ends it and nowhere else (`nar_field_verbatim`), so a listing is read back as the fields it was printed from (`nar_listing_verbatim`), whatever spaces or newlines a name or target holds. That the listing is what the filesystem holds, and that the walk builds the NAR from it as nix's dumper does, is EZ-HASH-5. EZ-LED-8 is proved for every command that reads a source. `P.anchor` keeps a URL and an absolute path and joins a relative path to the project root. `ez add` records the target as given, a path with only `~` expanded against HOME (`add_records_as_given`, `add_path_as_given`). `ez fetch` writes no file (`fetch_keeps_records`). `ez lock`, plain or `--upgrade`, records in the lock the source the ledger it is made from records for each package (`lock_records_as_given`), and `ez lock --upgrade` renders a model whose dependencies and tool pins record ez.toml's sources in ez.toml's order (`upgrade_records_as_given`, `upgrade_records_tools_as_given`), which is what ez.toml's bytes read back as (EZ-LED-4). Every question git is asked names the source anchored at the project, as the planner computes it: `ez add`'s (`add_asks_anchored`), `ez fetch`'s checkouts (`fetch_asks_anchored`), `ez lock`'s package questions (`lock_asks_anchored`), and the upgrade's, each put to git as `Up.anchor` of the question the upgrade looks its answer up by, which are exactly `P.wants.up` (`upgrade_asks_anchored`, `upgrade_asks_its_questions`). That the interpreter hands git the source a question names is EZ-TRUST-2. EZ-DOC-3 reads the committed tree as bend reads it. A hub import line is a root of the lock whatever run of spaces and tabs stands between `import`, the path, `as` and the name, however the line is indented and whatever blanks trail it, so long as the lines above it leave the header open (`root_reads_as_bend`). The scan trims a line and cuts it at the white space bend's loader splits on, JavaScript's `\s`, so spaces and tabs are the case the law states and not the only one the scan reads. `ez doctor` reads the same roots (`P.roots`), so EZ-VEN-5's import lines are these too. -EZ-VEN-1 is proved for `ez add`, `ez remove` and `ez lock --upgrade`. Over the line-level function `I.lines` (ledger/ignore.bend), its allowlist lines are exactly the vendored hashes, each once, in the order the ledger first names them, and every other line is kept in order; the file `I.sync` writes reads back (`I.file.lines`) as those lines, whatever the file it read ended with, and applying it twice is applying it once; each for a ledger whose vendored hashes hold no newline. `ez remove` and `ez add` leave `.gitignore` holding exactly `I.sync`'s text over the ledger they leave (`remove_syncs_allowlist`, `add_syncs_allowlist`). `ez lock --upgrade`: every `.gitignore` its plan writes has the allowlist of the hashes the upgrade commits and keeps every other line of the file it read, when no source it read is at `.gitignore`; an upgrade that does not refuse and leaves `.gitignore` unwritten read one whose allowlist is already those hashes (`upgrade_allowlist_kept_in_sync`); and the hashes it commits are the vendored hashes of the model it renders when it writes ez.toml (`upgrade_vends_the_ledger`) and of ez.toml as it is when it does not (`upgrade_unmoved_vends_the_ledger`). `ez add`'s half and the upgrade's hold of ez.toml's bytes, since the ledger they leave reads back as the model they render (EZ-LED-4). +EZ-VEN-1 is proved for `ez add`, `ez remove` and `ez lock --upgrade`. Over the line-level function `I.lines` (src/ledger/ignore.bend), its allowlist lines are exactly the vendored hashes, each once, in the order the ledger first names them, and every other line is kept in order; the file `I.sync` writes reads back (`I.file.lines`) as those lines, whatever the file it read ended with, and applying it twice is applying it once; each for a ledger whose vendored hashes hold no newline. `ez remove` and `ez add` leave `.gitignore` holding exactly `I.sync`'s text over the ledger they leave (`remove_syncs_allowlist`, `add_syncs_allowlist`). `ez lock --upgrade`: every `.gitignore` its plan writes has the allowlist of the hashes the upgrade commits and keeps every other line of the file it read, when no source it read is at `.gitignore`; an upgrade that does not refuse and leaves `.gitignore` unwritten read one whose allowlist is already those hashes (`upgrade_allowlist_kept_in_sync`); and the hashes it commits are the vendored hashes of the model it renders when it writes ez.toml (`upgrade_vends_the_ledger`) and of ez.toml as it is when it does not (`upgrade_unmoved_vends_the_ledger`). `ez add`'s half and the upgrade's hold of ez.toml's bytes, since the ledger they leave reads back as the model they render (EZ-LED-4). -EZ-DOC-1 is trusted, not proved: the lock is written as eztoml's `render` of the document ez assembles (`T.normal`, `toml/toml.bend`) and read through eztoml's `parse`, so it reads back when eztoml's round trip holds, which is EZ-TRUST-8, proved in eztoml v0.8.0. ez still writes no lock that `lockable.named` refuses: `lockable` refuses a hash, key or value holding `"`, `\` or a newline, a hash written twice, and a file path holding `=`. eztoml escapes strings and reads a quoted key whole, so these refusals are no longer needed for eztoml; they are kept for `bootstrap.sh`, whose awk cuts a pair at its first `=` and reads no escape. What the lock records is the packages in hash order with each one's files in path order and each once, each tool pin without `vendor`, and the names in name order and each once. Until ez moved to eztoml 0.4 this row was proved against the v0.1.0 reader (`lock_reads_back` and its tools, names and hub laws); the maintainer chose to move ahead of eztoml's proofs, and those laws went with the reader they unfolded. +EZ-DOC-1 is trusted, not proved: the lock is written as eztoml's `render` of the document ez assembles (`T.normal`, `src/toml/toml.bend`) and read through eztoml's `parse`, so it reads back when eztoml's round trip holds, which is EZ-TRUST-8, proved in eztoml v0.8.0. ez still writes no lock that `lockable.named` refuses: `lockable` refuses a hash, key or value holding `"`, `\` or a newline, a hash written twice, and a file path holding `=`. eztoml escapes strings and reads a quoted key whole, so these refusals are no longer needed for eztoml; they are kept for `bootstrap.sh`, whose awk cuts a pair at its first `=` and reads no escape. What the lock records is the packages in hash order with each one's files in path order and each once, each tool pin without `vendor`, and the names in name order and each once. Until ez moved to eztoml 0.4 this row was proved against the v0.1.0 reader (`lock_reads_back` and its tools, names and hub laws); the maintainer chose to move ahead of eztoml's proofs, and those laws went with the reader they unfolded. -EZ-LED-4 is proved relative to EZ-TRUST-8. `ledger/LAWS.bend` states the read-back as a premise, `ReadsBack`: every ledger `Rend.renderable` accepts reads back, from the text `Rend.show` writes, as itself. `Rend.show` is eztoml's `render` of the document ez assembles (`Rend.text`) and `M.parse` reads through eztoml's `parse`, so the premise is eztoml's round trip, proved in eztoml v0.8.0, and ez's gate does not re-check it. What ez proves is the rest: every command that writes ez.toml refuses a ledger that is not renderable, with no effect (EZ-OUT-2), and writes one that reads back, given the premise, as the model its laws are stated over: `ez init` the package and entry it was given (`init_ledger_reads_back`), `ez add` the ledger with the dependency added (`add_ledger_reads_back`, `add_named_reads_back`), and `ez remove` the ledger with it dropped (`remove_ledger_reads_back`). `renderable` refuses a name or value holding `"`, `\` or a newline, a dependency with no hash, and a git source that names no repo or no root. A ledger written before ez used eztoml 0.4 reads to the same model: `toml/toml.bend` passes over the tables a dotted header implies, and `tests/toml.bend` reads an old ledger and lock and their new forms to the same sections. +EZ-LED-4 is proved relative to EZ-TRUST-8. `src/ledger/LAWS.bend` states the read-back as a premise, `ReadsBack`: every ledger `Rend.renderable` accepts reads back, from the text `Rend.show` writes, as itself. `Rend.show` is eztoml's `render` of the document ez assembles (`Rend.text`) and `M.parse` reads through eztoml's `parse`, so the premise is eztoml's round trip, proved in eztoml v0.8.0, and ez's gate does not re-check it. What ez proves is the rest: every command that writes ez.toml refuses a ledger that is not renderable, with no effect (EZ-OUT-2), and writes one that reads back, given the premise, as the model its laws are stated over: `ez init` the package and entry it was given (`init_ledger_reads_back`), `ez add` the ledger with the dependency added (`add_ledger_reads_back`, `add_named_reads_back`), and `ez remove` the ledger with it dropped (`remove_ledger_reads_back`). `renderable` refuses a name or value holding `"`, `\` or a newline, a dependency with no hash, and a git source that names no repo or no root. A ledger written before ez used eztoml 0.4 reads to the same model: `src/toml/toml.bend` passes over the tables a dotted header implies, and `tests/toml.bend` reads an old ledger and lock and their new forms to the same sections. -The upgrade laws of phase three, for EZ-RES-4, EZ-RES-5, EZ-RES-6, EZ-RES-8 and the `ez lock --upgrade` half of EZ-VEN-1, are stated over the ledger model the upgrade renders into ez.toml, and hold of the file's bytes because those bytes read back as that model (EZ-LED-4). The design is in [docs/rfc/ez-lock-planner.md](docs/rfc/ez-lock-planner.md). EZ-RES-4 and EZ-RES-6 are proved so: their laws (`lock/LAWS.bend`) are over `P.ledger.next`, the model an upgrade renders, and over `P.wants.up`, the questions it asks, and what they say of ez.toml's bytes, and of the lock made from those bytes read back, holds by EZ-LED-4. EZ-RES-6's `NAME` is a nonempty `--package`; an empty one is no filter, as `ez lock --upgrade` alone. +The upgrade laws of phase three, for EZ-RES-4, EZ-RES-5, EZ-RES-6, EZ-RES-8 and the `ez lock --upgrade` half of EZ-VEN-1, are stated over the ledger model the upgrade renders into ez.toml, and hold of the file's bytes because those bytes read back as that model (EZ-LED-4). The design is in [docs/rfc/ez-lock-planner.md](docs/rfc/ez-lock-planner.md). EZ-RES-4 and EZ-RES-6 are proved so: their laws (`src/lock/LAWS.bend`) are over `P.ledger.next`, the model an upgrade renders, and over `P.wants.up`, the questions it asks, and what they say of ez.toml's bytes, and of the lock made from those bytes read back, holds by EZ-LED-4. EZ-RES-6's `NAME` is a nonempty `--package`; an empty one is no filter, as `ez lock --upgrade` alone. EZ-RES-5 and EZ-RES-8 are proved in the same way. Their laws are over `P.ledger.next`, the model `ez lock --upgrade` renders into ez.toml: a pin by its commit alone moves only to the default branch tip the remote named, when the remote said the tip descends from it, keeps no tag, and, when the upgrade asks about it and does not refuse, is at that tip; a pin through a tag keeps its tag, moves only to the commit the remote names for the tag along its history, and is at that commit when the upgrade does not refuse; and a tip off the pin's history, or a pinned commit whose checkout no longer agrees with the pin, makes `P.refuses` true, which is a plan with no effect (EZ-OUT-2) that the interpreter ends with exit 1 (EZ-TRUST-2). That the bytes of ez.toml read back as that model is EZ-LED-4, and that the remote's refs and ancestry are true of the repository is EZ-RES-7. -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-DOC-4 is proved for a plain lock and for `ez lock --upgrade`. `after` (`src/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 (`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()` with the program's own name, which bend 2.0.32 and later put first, dropped by `Args.all`), 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 takes `--threads` and `--gpu` with the value after each, and answers `--gpu-build` and `--bend-help` itself, anywhere on the line before a `--`, before ez sees it. `--help` reaches ez, and Shake reads it as it reads `help`: before any positional of the command is bound, `ez --help` and `ez add --help` are requests for help, exiting 0 by `help_exits_zero`, while `ez add owner/repo --help` is a usage error (shake's SHAKE-PARSE-8, trusted as EZ-TRUST-7). A `--help` after a `--` is a word like any other, and one among the words `ez run` and `ez tool run` forward is the program's. -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. +EZ-FETCH-1 is proved over the plan `ez fetch` runs (`src/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 (`src/tool/plan.bend`), over what it resolves a target to, and over the words `ez tool run` and `ez run` hand on (`src/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 `src/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()` with the program's own name, which bend 2.0.32 and later put first, dropped by `Args.all`), 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 (`src/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 `src/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, `src/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 `src/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 takes `--threads` and `--gpu` with the value after each, and answers `--gpu-build` and `--bend-help` itself, anywhere on the line before a `--`, before ez sees it. `--help` reaches ez, and Shake reads it as it reads `help`: before any positional of the command is bound, `ez --help` and `ez add --help` are requests for help, exiting 0 by `help_exits_zero`, while `ez add owner/repo --help` is a usage error (shake's SHAKE-PARSE-8, trusted as EZ-TRUST-7). A `--help` after a `--` is a word like any other, and one among the words `ez run` and `ez tool run` forward is the program's. +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` (src/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 (`src/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. EZ-PUB-3 is proved over the same plan. `PP.naming` reads the two `[package]` keys the ledger model carries: neither is a publish by hash (`neither_is_hash`), one without the other is refused naming the key that is missing (`name_needs_version`, `version_needs_name`), a `publish-as` that `K.name.part` refuses, the NAMED name rule the package walk already reads imports by, is refused (`bad_name_refused`), and so is a `version` that `PP.semver` refuses: one with a character other than a digit or a dot anywhere (`semver_needs_digits`, `prerelease_refused`, `build_refused`), or one that is not three numbers each as `K.ver.num` reads one (`bad_version_refused`). Both good are `@.0` (`named_is_four_part`). Over a World whose ledger text parses to a model with those keys, a refusal stops before git is asked (`pub_misnamed_stops`) and its plan is the refusal alone (`pub_misnamed_writes_nothing`); a name is asked for in the upload question (`pub_named_uploads_named`), and no name asks for the upload by hash (`pub_unnamed_uploads_by_hash`); the words the upload runs are `upload_by_name` and `upload_by_hash`. A named publish that succeeds prints the import line by the name (`pub_reports_name`), and one by hash by the hash (`pub_reports_hash`). The two keys read back from the ledger ez writes under EZ-LED-4, since `Rend.renderable` checks them and `ReadsBack` covers the whole model, and the ledger `ez init` writes names neither (`init_publishes_by_hash`). What the laws take from the interpreter is EZ-TRUST-2: that it runs the words `PP.upload.line` makes of the question. -EZ-PUB-4 is proved over the same plan and `pub/blurb.bend`. The upload question carries the line (`pub_upload_says_description`), `B.blurb` of the files the walk made, which are the files bend sends: the entry, what it imports, and since bend 2.0.27 the LICENSE beside each (EZ-HASH-4). A LICENSE never gives the line (`hub_license_named`, `hub_skips_license`), and a file that is not one, whose path comes no later than any other file's, does, with its first line (`hub_first_by_path`), which is what comes before its first newline (`line_first_cut`). Paths are compared by `String.is_le`, the order the manifest is written in, which is JavaScript's for every path whose characters are in the Basic Multilingual Plane. The upload is the last question the planner asks, so a World the planner refuses before it never carries the line (`pub_stop_sends_nothing`, `pub_stray_sends_nothing`). That the hub picks the line this way is the hub's, not ez's: ez says what it expects the hub to show. What the laws take from the interpreter is EZ-TRUST-2: that it prints the line the question carries just before it runs the upload, and at no other time. +EZ-PUB-4 is proved over the same plan and `src/pub/blurb.bend`. The upload question carries the line (`pub_upload_says_description`), `B.blurb` of the files the walk made, which are the files bend sends: the entry, what it imports, and since bend 2.0.27 the LICENSE beside each (EZ-HASH-4). A LICENSE never gives the line (`hub_license_named`, `hub_skips_license`), and a file that is not one, whose path comes no later than any other file's, does, with its first line (`hub_first_by_path`), which is what comes before its first newline (`line_first_cut`). Paths are compared by `String.is_le`, the order the manifest is written in, which is JavaScript's for every path whose characters are in the Basic Multilingual Plane. The upload is the last question the planner asks, so a World the planner refuses before it never carries the line (`pub_stop_sends_nothing`, `pub_stray_sends_nothing`). That the hub picks the line this way is the hub's, not ez's: ez says what it expects the hub to show. What the laws take from the interpreter is EZ-TRUST-2: that it prints the line the question carries just before it runs the upload, and at no other time. EZ-PUB-5 is proved over the same plan. Past the check that git tracks every file, the planner collects the hub imports of the files the walk made, each `0x` name and each `@` once, reads the lock when there is a name among them, and asks the ledger's hub about each (`PP.hubbed`). A World gets as far as the upload only when every one is on the hub (`pub_sends_only_on_hub`), so one that is off it sends nothing (`pub_offhub_sends_nothing`) and refuses (`pub_offhub_refuses`), and one import off the hub is enough wherever it stands among them (`hub_one_off_is_off`). What counts as off is stated over the answer: a 404 is a package the hub does not have (`hub_404_is_absent`), any other answer that is not a 200, the hub unreachable among them, is a hub that could not be asked, which refuses too (`hub_unreachable_is_off`), and a name the hub resolves to a hash other than the one the lock records is not the package imported (`hub_name_elsewhere_is_off`), while one it resolves to that hash is (`hub_name_there`). A manifest the hub serves for a `0x` name counts only when it hashes to that name, as `ez lock` checks it. What the laws take from the interpreter is EZ-TRUST-2: that it GETs the url each question names under the ledger's hub, as `ez lock` does, and reads the lock from ez.lock.toml. EZ-INIT-1 and EZ-INIT-2 are proved over the plan `ez init` runs. The stub is its line for the hub, a newline, and the program, so its first line is that line whenever the line is one line (`init_stub_heads`, with `line_first_cut`), and the planner refuses, with no effect, a project whose line is not (`init_one_line`, `init_refusal_writes_nothing`). The line is the description given (`init_header_given`) or the placeholder (`init_header_placeholder`). A fresh project that fits writes `src/lib.bend` and a `main.bend` that imports it (`init_lays_src`, `init_lays_main`); in the package that entry makes, `main.bend` comes before `src/lib.bend`, so the hub shows the entry's first line. A `src/lib.bend` or an entry that is there is left as it was, whatever else the World holds (`init_keeps_src`, `init_keeps_entry`); the law for `src/lib.bend` excepts an entry asked for at that path, which the entry's own text decides, and the one for the entry excepts ez.toml and `.gitignore`, which the plan writes itself. What the laws take from the interpreter is EZ-TRUST-2: that it reads the entry and `src/lib.bend` from the paths the planner names. -EZ-RES-2's import line is proved over the plan `ez add` runs (`add/plan.bend`): an add that does not refuse ends what it says with `Git.import.line` of the hash its walk made and the entry's path inside the package, `K.inside` of the walk's root and the entry (`add_says_import`). `ez publish` prints the same function of the same two, so both commands name a package's entry where the hub serves it: by its name alone, or, for a package whose imports climb out of the entry's directory, under the directories the package re-rooted above it. `ez add @` prints the same function with the name in place of the hash, for the entry it records (`add_named_says_import`). +EZ-RES-2's import line is proved over the plan `ez add` runs (`src/add/plan.bend`): an add that does not refuse ends what it says with `Git.import.line` of the hash its walk made and the entry's path inside the package, `K.inside` of the walk's root and the entry (`add_says_import`). `ez publish` prints the same function of the same two, so both commands name a package's entry where the hub serves it: by its name alone, or, for a package whose imports climb out of the entry's directory, under the directories the package re-rooted above it. `ez add @` prints the same function with the name in place of the hash, for the entry it records (`add_named_says_import`). -EZ-VEN-4 and EZ-VEN-5 are proved over the plan `ez doctor` runs (`doctor/plan.bend`). Its plan is lines said and how the command ends, so it writes, lays and removes nothing (`doctor_writes_nothing`). An import line names a hash when `ez lock` reads it so: the header imports of a `.bend` file git tracks outside `.ez/`, as the package walk scans them (`P.roots`). Over a ledger that reads, every such hash the ledger's dependencies lack has its line (`doctor_reports_unrecorded`), every dependency whose hash no such line names has its line (`doctor_reports_unused`), and a report with any line fails the command (`doctor_drift_fails`). A ledger that is not there or does not read fails the command before any comparison. That the interpreter hands doctor the tracked files as git lists them and their texts as they are on disk is EZ-TRUST-2. +EZ-VEN-4 and EZ-VEN-5 are proved over the plan `ez doctor` runs (`src/doctor/plan.bend`). Its plan is lines said and how the command ends, so it writes, lays and removes nothing (`doctor_writes_nothing`). An import line names a hash when `ez lock` reads it so: the header imports of a `.bend` file git tracks outside `.ez/`, as the package walk scans them (`P.roots`). Over a ledger that reads, every such hash the ledger's dependencies lack has its line (`doctor_reports_unrecorded`), every dependency whose hash no such line names has its line (`doctor_reports_unused`), and a report with any line fails the command (`doctor_drift_fails`). A ledger that is not there or does not read fails the command before any comparison. That the interpreter hands doctor the tracked files as git lists them and their texts as they are on disk is EZ-TRUST-2. EZ-VEN-6 is proved over the same plan. `DP.relock(w, fs)` is the World doctor puts to the lock planner: a plain `ez lock` over the ledger's text, the sources `fs` git listed, and every tree doctor read from `BEND_LIB`, a hub package's judged as the hub's bytes and a git package's as `ez lock` judges one it finds there. When a lock is there and the lock planner asks nothing more, a lock whose text is the one `P.decide` makes is said to be up to date, and that line is not a problem (`doctor_passes_fresh_lock`, `doctor_says_fresh_lock`); a lock whose text differs by any byte is said to be out of date and fails the command (`doctor_reports_stale_lock`, `doctor_stale_lock_fails`). When the lock planner still asks about a package, which doctor asks `BEND_LIB` for and never the network, the lock is not checked and the command fails (`doctor_unchecked_lock_fails`). The lock planner answers the names it asks about from the lock and the names files under `BEND_LIB`, never the hub, and when it still asks about one the lock is not checked either (`doctor_unchecked_names_fail`); the laws before it hold when it asks nothing more about names. What the laws take from the interpreter is EZ-TRUST-2: that a tree's answer is its manifest and files as they are under `BEND_LIB`, and that a tree it reports absent has no manifest there. @@ -195,15 +195,15 @@ These assumptions sit outside the proofs. They are the complete list of Trusted | EZ-TRUST-2 | The interpreter reads the World and executes plans faithfully. | It makes no decisions and is kept small enough to review line by line. | | EZ-TRUST-3 | The hub serves, for a hash, what was published under it. | ez checks every hub body against the hash it asked for (EZ-FETCH-1), so this reduces to availability and EZ-HASH-6. | | EZ-TRUST-4 | `ez prove` runs `bend` on every PROOF.bend in the tree and passes only on an exact `ALL PROOFS CHECK` first line. | It is ez code run by `mkProofs`, not a law. CI builds from a clean tree, so nothing is cached. | -| EZ-TRUST-5 | HTTP framing and URL parsing are correct. | Proved in ezhttp v0.8.0, the rev ez.toml pins; ez's gate does not re-check it. ez imports its interface, `main.bend`, and `src/client.bend` and `src/url.bend` for the two types whose constructors `hub/get.bend` matches, which `main.bend` names but does not define. | +| EZ-TRUST-5 | HTTP framing and URL parsing are correct. | Proved in ezhttp v0.8.0, the rev ez.toml pins; ez's gate does not re-check it. ez imports its interface, `main.bend`, and `src/client.bend` and `src/url.bend` for the two types whose constructors `src/hub/get.bend` matches, which `main.bend` names but does not define. | | EZ-TRUST-6 | A `@` the hub answered once names the same hash forever. | The hub never moves a name once it is taken, so a name is resolved once and pinned in the lock. The package it names is still checked against its hash (EZ-FETCH-1). | | EZ-TRUST-7 | Command-line parsing is correct: `parse` binds a line as shake's spec says, `help_path` names a request for help and only one, `path_of` and `at` follow the selected path, and `get`, `on` and `help` read and render it. | Proved in shake v0.4.0, the rev ez.toml pins (SHAKE-PARSE-1 to SHAKE-PARSE-10, SHAKE-GET-1, SHAKE-GET-2, SHAKE-HELP-1, SHAKE-ERR-1, SHAKE-ERR-2); ez imports only its interface, `main.bend`, and its gate does not re-check it. In particular `ez help ` with a word that names no command there fails as `Unexpected`, not as a request for help, and a bare `--help` before any positional of the command is a request for help as `help` is (SHAKE-PARSE-8). | -| EZ-TRUST-8 | A document eztoml renders reads back as itself, and a text it reads without error renders back as the same document: its TOML-RT-1, TOML-RT-2 and TOML-RT-3. | Proved in eztoml v0.8.0, the rev ez.toml pins; ez imports only its interface, `main.bend`, and its gate does not re-check it. ez relies on them for EZ-DOC-1 and EZ-LED-4. ez's step between its sections and eztoml's document (`toml/toml.bend`) is ez code with no law: `tests/toml.bend` checks it on an old and a new ledger and lock. | -| EZ-TRUST-9 | A law may read snap's answers, `code`, `text` and `ok`, from `src/answer.bend`, the pure module snap's `main.bend` returns them from unchanged. | ez imports that module deliberately, in `ez/ends.bend`, `ez/LAWS.bend` and `ez/PROOF.bend`: bend 2.0.32's verdict fails every proof whose imports reach snap's foreign effects, which `main.bend` holds, so no law may import `main.bend`. That `main.bend`'s `code`, `text` and `ok` are `src/answer.bend`'s is snap's SNAP-TRUST-5, a one-line delegate each in snap v1.1.0, the rev ez.toml pins; the interpreters read the same answers through `main.bend`. | +| EZ-TRUST-8 | A document eztoml renders reads back as itself, and a text it reads without error renders back as the same document: its TOML-RT-1, TOML-RT-2 and TOML-RT-3. | Proved in eztoml v0.8.0, the rev ez.toml pins; ez imports only its interface, `main.bend`, and its gate does not re-check it. ez relies on them for EZ-DOC-1 and EZ-LED-4. ez's step between its sections and eztoml's document (`src/toml/toml.bend`) is ez code with no law: `tests/toml.bend` checks it on an old and a new ledger and lock. | +| EZ-TRUST-9 | A law may read snap's answers, `code`, `text` and `ok`, from `src/answer.bend`, the pure module snap's `main.bend` returns them from unchanged. | ez imports that module deliberately, in `src/ez/ends.bend`, `src/ez/LAWS.bend` and `src/ez/PROOF.bend`: bend 2.0.32's verdict fails every proof whose imports reach snap's foreign effects, which `main.bend` holds, so no law may import `main.bend`. That `main.bend`'s `code`, `text` and `ok` are `src/answer.bend`'s is snap's SNAP-TRUST-5, a one-line delegate each in snap v1.1.0, the rev ez.toml pins; the interpreters read the same answers through `main.bend`. | | EZ-DOC-1 | Parsing a rendered lock yields the packages, hub, names and tools that were rendered. | It is EZ-TRUST-8 for the document ez assembles for the lock. | | EZ-RES-7 | git reports refs, tags, and ancestry accurately. | The World model takes git's answers as given. | | EZ-HASH-4 | ez's 0x hash matches `bend --publish`. | The publisher is a separate program. | | EZ-HASH-5 | ez's narHash matches nix. | nix is a separate program. What ez trusts of its own walk is GNU `find`'s listing of the tree, each path's type, `%M` mode, name and link target, and the file effect's read of each file's bytes. The walk takes the executable bit from the owner's exec bit of that mode, as nix's dumper does, and reads names and targets as listed (EZ-HASH-7). Submodules are not part of the tree: ez weighs a checkout without them, and its nix side asks `fetchgit` for the same. | | EZ-HASH-6 | `Sha.raw` computes the SHA-256 digest of its bytes, and `Sha.hex` of its text's UTF-8. | Proved in 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. +EZ-VEN-2 and EZ-VEN-3 are proved for the moves an upgrade makes (`src/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/docs/guide.md b/docs/guide.md index 4d9b8c1..6f6cc23 100644 --- a/docs/guide.md +++ b/docs/guide.md @@ -755,7 +755,7 @@ at once, and passes a proof only when the first line bend prints is exactly main. A proof that reaches an `@unsafe` def or foreign code, imports included, is `SOME PROOFS FAIL`, so a PROOF.bend imports only modules that run nothing. ez keeps the half of a module that runs programs or fetches over the network -in a sibling module no law imports (`git/exec.bend` beside `git/git.bend`, for +in a sibling module no law imports (`src/git/exec.bend` beside `src/git/git.bend`, for one). The gate reads the line rather than the exit status. It prints a line for each proof and then the count, and exits 1 when any diff --git a/docs/rfc/ez-add-planner.md b/docs/rfc/ez-add-planner.md index 75dfb2f..b8f15d0 100644 --- a/docs/rfc/ez-add-planner.md +++ b/docs/rfc/ez-add-planner.md @@ -2,6 +2,8 @@ ## Draft Status +Module paths here are the ones the code had when this was written, at the top of the repository. Since ez's WP34 every module lives under `src/`, so `lock/plan.bend` is now `src/lock/plan.bend`; see [ez-spec.md](ez-spec.md). + State: Accepted. Nothing here changes `ez add` or `ez remove` yet; the work packages below do. This is the design for the phase after [ez-lock-planner.md](ez-lock-planner.md): converting `ez add` and `ez remove` to pure planners and thin interpreters, then proving the pending rows they touch. It follows the lock design's pattern (a World, a planner that asks or plans, an interpreter that answers and executes) and does not repeat it; read that design's "Summary", "Laziness without losing purity" and "The Plan and the outcome" first. It was written from the code at `0f8f179`, where WP1 of the lock design has landed, and it builds on the shapes WP1 built (see that design's "Update" note) rather than on its sketches. A spike in `pkg/tree/` makes the package walk pure; nothing imports it, so `ez add` behaves exactly as before. `SPEC.md` does not change until a requirement's law lands; how the work went is summarized in [ez-spec.md](ez-spec.md) under "How we got here". diff --git a/docs/rfc/ez-lock-planner.md b/docs/rfc/ez-lock-planner.md index 71eccae..cb2a5d1 100644 --- a/docs/rfc/ez-lock-planner.md +++ b/docs/rfc/ez-lock-planner.md @@ -2,6 +2,8 @@ ## Draft Status +Module paths here are the ones the code had when this was written, at the top of the repository. Since ez's WP34 every module lives under `src/`, so `lock/plan.bend` is now `src/lock/plan.bend`; see [ez-spec.md](ez-spec.md). + State: Accepted. Nothing here changes `ez lock` yet; the work packages below do. **Update:** WP1 has landed. Plain `ez lock` runs the planner in `lock/world.bend`, `lock/plan.bend` and `lock/run.bend`, the spike in `lock/world/` is deleted, and its laws are restated over that planner in `lock/LAWS.bend`. Where the code differs from the sketches below: an `Ask` carries the hub a hub package is served from, so the interpreter never parses the ledger; the World's ledger is `Maybe<&2, String>`, so a missing ez.toml is refused by the planner (EZ-LED-6); `Outcome`'s success is `Success{}`, since Base owns `Done`; a refused plan has no effect at all and its reason is in `Refused{why}`; and a `Lay` is built from the planner's verdict, so only a checked tree is laid, and only by a lock that succeeds. What each work package proved is in [ez-spec.md](ez-spec.md) under "How we got here", and the laws behind each row are in the Law column of [SPEC.md](../../SPEC.md). diff --git a/docs/rfc/ez-spec.md b/docs/rfc/ez-spec.md index 1f62da1..dc0f67f 100644 --- a/docs/rfc/ez-spec.md +++ b/docs/rfc/ez-spec.md @@ -105,7 +105,7 @@ We are not proving Bend itself, git, the hub, nix, or the host filesystem correc ### Scope -ez is a project manager first: it keeps a Bend project's ledger, lock, vendored packages and publishing honest. The tools area, `[tools.*]`, the `ez tool` commands and `ezx`, exists so that a project can pin the tools it runs, such as bolt, and after 1.0.0 it is frozen except for fixes. Installing a tool by its hub name is paused until the Bend ecosystem needs it: a bend package is an import closure, not a directory, so the hub carries libraries, and tools install from git. ez itself is published to the hub by hash (from 1.2.0). Its library directory was `manifest/` until then; the hub serves every package's own manifest at `/manifest`, so it refuses a package with a top-level `manifest/` (EISDIR), and the directory became `ledger/`, its entry `ledger/manifest.bend`. +ez is a project manager first: it keeps a Bend project's ledger, lock, vendored packages and publishing honest. The tools area, `[tools.*]`, the `ez tool` commands and `ezx`, exists so that a project can pin the tools it runs, such as bolt, and after 1.0.0 it is frozen except for fixes. Installing a tool by its hub name is paused until the Bend ecosystem needs it: a bend package is an import closure, not a directory, so the hub carries libraries, and tools install from git. ez itself is published to the hub by hash (from 1.2.0). Its library directory was `manifest/` until then; the hub serves every package's own manifest at `/manifest`, so it refuses a package with a top-level `manifest/` (EISDIR), and the directory became `ledger/`, its entry `ledger/manifest.bend`. From 1.4.0 (WP34) the package the hub serves as ezx is the whole ez program, and the ledger library is a file inside it, `src/ledger/manifest.bend`. ## Proposal @@ -208,6 +208,8 @@ The price of the loop is small. Measured on this repository's own lock when WP1 The law sketches below use these names. Where no definition exists, the sketch introduces one. +Module paths in this document, here and elsewhere, are written from `src/`, where every module has lived since WP34; before WP34 they sat at the top of the repository, and a line number is the one the module had when the sentence was written. + | Name in a sketch | Real definition | | :---- | :---- | | `K.hash_of` | `pkg/pkg.bend:381`. The 0x name of a file list. | @@ -585,6 +587,8 @@ Moving to eztoml v0.4.0 (WP32) changes the layout of ez.toml and ez.lock.toml, a Moving to bend 2.0.34 (WP33) changes what a user sees in a few ways, and needs bend 2.0.32 or later. The proof gate reads 2.0.32's verdict, `ALL PROOFS CHECK`, and since bend now fails a proof whose imports reach foreign code, every module that runs a program or opens a socket keeps that half in a sibling no law imports: `git/exec.bend` beside `git/git.bend`, `hub/get.bend` beside `hub/hub.bend`, `sha/dump.bend` beside `sha/nar.bend`, `share/spin.bend` beside `share/say.bend`, `share/exec.bend` beside `share/env.bend` and `ez/timer.bend` beside `ez/clock.bend`, and a law reads snap's answers from `src/answer.bend`, the pure file snap's `main.bend` re-exports them from. `IO.args()` now starts with the program's own name, which `Args.all` drops, and a compiled binary hands `--help` to the program, so `ez --help` and `ez --help` print ez's help, which shake v0.4.0 reads as it reads `help`, rather than failing as an unknown flag; the runtime's own usage is `--bend-help`. A hub name is 1 to 64 characters, bend's NAMED rule, where ez asked for 12 to 64: which names a Bender may take is the hub's to decide, not the name's shape. And the lock walk's fuel, a fixed 100000 steps, is now worked out from its inputs, as the add walk's is: one step for each hash the queue starts with and one for each import a hub verdict can queue, since a hash is resolved at most once. 2.0.33 and 2.0.34 compare a walk the lock laws unfold at a fixed fuel one stack frame a step, and overflowed the checker's stack past about 10000 steps where 2.0.31 did not; a fuel the laws leave unevaluated is never unrolled. The package ez publishes to the hub, ezx, takes a top-level `main.bend` as its entry, which names ledger/manifest.bend's reading, so the LICENSE beside it goes along, and the hub describes it by the first line of ledger/manifest.bend, now `# ezx: ...`. ez moves with it to shake v0.4.0, which reads a bare `--help` as `help` and so replaces a rewrite ez carried for a while, to ezhttp v0.8.0, whose entry is now its top-level `main.bend`, and to eztoml v0.8.0, which proves the round trip EZ-TRUST-8 had been waiting on. A law reading snap's answers from `src/answer.bend` is recorded as EZ-TRUST-9, resting on snap's SNAP-TRUST-5. +Publishing ez itself as ezx (WP34) changes what the hub package is, and the maintainer decided it. Up to 1.3.0 ezx was the ledger library: a top-level `main.bend` that named `ledger/manifest.bend`'s reading, and the program was a separate `bin`, `ez/main.bend`, which only a clone or nix could build. From 1.4.0 the top-level `main.bend` is ez's program, and the package entry: it calls `src/ez/main.bend`'s `main`, so a plain Bend user builds the `ez` binary from the hub as bolt's users build bolt, with a file that imports `ezx@.0/main.bend` and calls `main`, and no clone, lock or nix. Every module moved under `src/`, as `ez init` lays a project out, so the relative imports between modules kept working, only the LICENSE sorts before `main.bend` in the files bend publishes, and the hub describes the package by `main.bend`'s first line, `# ezx: ez, the package manager for Bend 2.` `[package] bin` is gone from ez.toml, since the entry is the program; `ez build`, `ez run` and the nix package build it. The ledger library is still in the package, now at `src/ledger/manifest.bend`, and a program that imported ezx's `main.bend` for `parse` and `show` imports that file instead. No law, proof, test or `src/check/` file is reached from `main.bend`, so none is published. The hub imports the program reaches, shake, snap, ezhttp, eztoml and sha256, are all on the hub, so bend fetches them on a plain user's first build. + Reading the code also turned up behavior that looked accidental and is not a requirement. Besides the ledger changes above, two such fixes were worth making, and both have landed. Every command, `ez help` included, created `.ez` and `bin` in the current directory, because `Env.make()` ran before the line was parsed; `Env.dirs` now names only the directories a command writes into, and nothing for most commands (`dirs_other`, `dirs_check`, `dirs_build`, `dirs_build_out`). And `ez doctor` failed a project with no dependencies, because it counted a lock that names no package as a problem even when the ledger needed none. The rest of what looked accidental was either covered by a decided change above or left alone as incidental, and what remains open is under "Known gaps". ### Known gaps @@ -698,6 +702,7 @@ The rollout above ran as planned, with the command conversions split into work p | WP31 | shake v0.2.0 through its interface alone, snap v1.0.0, sha256 by its published walk, and ezhttp v0.5.0; the line laws restated over shake's `help_path`, `path_of` and `at`, resting on shake's proofs (EZ-TRUST-7). | EZ-OUT-1 | | WP32 | eztoml v0.4.0 through its interface alone: ez.toml and ez.lock.toml written by eztoml's `render`, in its layout, and read by its `parse`, old layouts included. EZ-DOC-1 becomes Trusted, and the EZ-LED-4 and upgrade laws take the ledger's read-back as a premise (EZ-TRUST-8). | EZ-LED-4, EZ-DOC-4 | | WP33 | bend 2.0.34: the proof gate reads `ALL PROOFS CHECK`, the foreign half of each module a law imports moved to a sibling, `IO.args()` read past the program's name, `--help` read as `help` (shake v0.4.0), hub names of 1 to 64 characters, the lock walk's fuel worked out from its inputs, and ezx's entry a top-level `main.bend`. | EZ-OUT-1, EZ-PUB-3, EZ-HUB-3 | +| WP34 | ezx is the whole ez program: the top-level `main.bend` is the entry and calls `src/ez/main.bend`, every module moved under `src/`, `[package] bin` dropped, and the ledger library imported from `src/ledger/manifest.bend`. | EZ-PUB-4 | Proving also found bugs that reading the code had missed, and each was fixed where it was found: WP6 found that WP2's upgrade read an empty refusal reason as no refusal (a case the interpreter never built, so the binary did not change), WP5b found that a tool pin with a rev and no narHash moved on the next upgrade, WP7 found the allowlist written twice for a shared tree, and WP10 found a lock that accepted a manifest `ez fetch` would then refuse. The proofs are long, as the risks below expected: `lock/PROOF.bend` grew by about 4,800 lines in WP5b alone, most of them one lemma per step of the upgrade. diff --git a/ez.toml b/ez.toml index 3022071..609cba4 100644 --- a/ez.toml +++ b/ez.toml @@ -1,7 +1,6 @@ [package] name = "ez" entry = "main.bend" -bin = "ez/main.bend" [deps] [deps.sha256] hash = "0x3bdc0c9f5265bb49f7fc76b61f529f24" diff --git a/flake.nix b/flake.nix index 3272355..358f50d 100644 --- a/flake.nix +++ b/flake.nix @@ -24,11 +24,13 @@ # network in the sandbox beyond the lock's own fixed-output fetches bendLib = ez.bendLib ./ez.lock.toml; - # the `ez` binary, with everything it shells out to on its PATH. curl is - # not among them: ezhttp speaks HTTP and HTTPS itself, and what it needs - # instead is libssl by name (it opens it at run time, and no search path - # reaches a Nix store path) and a CA bundle, which OpenSSL takes from - # SSL_CERT_FILE. git stays, because `ez add` vendors a repo. + # the `ez` binary, built from ez.toml's entry, the top-level main.bend + # (the program; its modules are under src/), with everything it shells + # out to on its PATH. curl is not among them: ezhttp speaks HTTP and + # HTTPS itself, and what it needs instead is libssl by name (it opens it + # at run time, and no search path reaches a Nix store path) and a CA + # bundle, which OpenSSL takes from SSL_CERT_FILE. git stays, because + # `ez add` vendors a repo. ezBin = ez.mkPackage { inherit bend; src = self; diff --git a/main.bend b/main.bend index ed29b28..16a786d 100644 --- a/main.bend +++ b/main.bend @@ -1,79 +1,16 @@ -# ezx: ez's ledger library for Bend 2: it parses an ez.toml into its package, dependencies and pinned tools. +# ezx: ez, the package manager for Bend 2. # -# main: the library's entry, which the hub publishes as ezx. It names the -# reading ledger/manifest.bend does, one def each, so a program can read a -# ledger by importing this file alone; the types the answers come in are -# ledger/manifest.bend's, and a program that takes one apart imports that -# file too. It sits at the top of the repo so the LICENSE beside it goes -# along with the package. The ez binary is ez/main.bend, which ez.toml names -# as `bin`. +# main: ez's program, and the entry the hub publishes as ezx. Building this +# file builds the `ez` binary (`bend main.bend -o ez`), and a plain Bend file +# that imports it and calls `main` builds the same binary. The program itself +# is src/ez/main.bend; every module it reaches lives under src/, so the +# LICENSE beside this file goes along with the package and nothing else sorts +# before it. ez's ledger library, which reads an ez.toml, is +# src/ledger/manifest.bend, importable from the package at that path. import Base -import ./ledger/manifest.bend as M +import ./src/ez/main.bend as App -# an ez.toml's text read as a ledger, or why it could not be -def parse(text: String) -> M.Read: - M.parse(text) - -# a ledger, or the error, on one line -def show(ledger: M.Read) -> String: - M.show(ledger) - -# the named dependency of a ledger, or one with empty fields -def dep(ledger: M.Read, name: String) -> M.Dep: - M.dep(ledger, name) - -# a dependency's own name -def dep.name(dependency: M.Dep) -> String: - M.dep.name(dependency) - -# a dependency's hash, the `0x` name its import line carries -def dep.hash(dependency: M.Dep) -> String: - M.dep.hash(dependency) - -# the file inside the package a dependency was added by -def dep.entry(dependency: M.Dep) -> String: - M.dep.entry(dependency) - -# where a dependency's bytes come from -def dep.source(dependency: M.Dep) -> M.Source: - M.source.dep(dependency) - -# the commit a source is pinned to, or "" for a hub package -def source.rev(src: M.Source) -> String: - M.source.rev(src) - -# the tag a source was asked for, or "" when it was pinned by commit -def source.tag(src: M.Source) -> String: - M.source.tag(src) - -# the repo a source is taken from, or "" for a hub package -def source.url(src: M.Source) -> String: - M.source.url(src) - -# the `@` a hub source was added by, or "" -def source.nv(src: M.Source) -> String: - M.source.nv(src) - -# whether a source names a repo rather than the hub -def source.is_git(src: M.Source) -> Bool: - M.source.is_git(src) - -# the commit the named dependency is pinned to -def rev_of(ledger: M.Read, name: String) -> String: - M.rev_of(ledger, name) - -# the tag the named dependency was asked for -def tag_of(ledger: M.Read, name: String) -> String: - M.tag_of(ledger, name) - -# the hub a ledger's packages come from -def hub_of(ledger: M.Read) -> String: - M.hub_of(ledger) - -# the pinned CLIs of a ledger -def tools_of(ledger: M.Read) -> List<&2, M.Tool>: - M.tools_of(ledger) - -# a tool's own name -def tool.name(pin: M.Tool) -> String: - M.tool.name(pin) +# the ez command line: read the words, run the command they name, and exit +# as it ends +def main() -> IO(Unit): + App.main() diff --git a/add/LAWS.bend b/src/add/LAWS.bend similarity index 100% rename from add/LAWS.bend rename to src/add/LAWS.bend diff --git a/add/PROOF.bend b/src/add/PROOF.bend similarity index 100% rename from add/PROOF.bend rename to src/add/PROOF.bend diff --git a/add/hub.bend b/src/add/hub.bend similarity index 100% rename from add/hub.bend rename to src/add/hub.bend diff --git a/add/plan.bend b/src/add/plan.bend similarity index 100% rename from add/plan.bend rename to src/add/plan.bend diff --git a/add/run.bend b/src/add/run.bend similarity index 100% rename from add/run.bend rename to src/add/run.bend diff --git a/add/world.bend b/src/add/world.bend similarity index 100% rename from add/world.bend rename to src/add/world.bend diff --git a/check/PROOF.bend b/src/check/PROOF.bend similarity index 100% rename from check/PROOF.bend rename to src/check/PROOF.bend diff --git a/check/eq.bend b/src/check/eq.bend similarity index 100% rename from check/eq.bend rename to src/check/eq.bend diff --git a/check/framing.bend b/src/check/framing.bend similarity index 100% rename from check/framing.bend rename to src/check/framing.bend diff --git a/check/kit.bend b/src/check/kit.bend similarity index 100% rename from check/kit.bend rename to src/check/kit.bend diff --git a/check/liar.bend b/src/check/liar.bend similarity index 100% rename from check/liar.bend rename to src/check/liar.bend diff --git a/check/oracle.bend b/src/check/oracle.bend similarity index 100% rename from check/oracle.bend rename to src/check/oracle.bend diff --git a/check/serve.bend b/src/check/serve.bend similarity index 100% rename from check/serve.bend rename to src/check/serve.bend diff --git a/check/str.bend b/src/check/str.bend similarity index 100% rename from check/str.bend rename to src/check/str.bend diff --git a/check/world.bend b/src/check/world.bend similarity index 100% rename from check/world.bend rename to src/check/world.bend diff --git a/doctor/LAWS.bend b/src/doctor/LAWS.bend similarity index 100% rename from doctor/LAWS.bend rename to src/doctor/LAWS.bend diff --git a/doctor/PROOF.bend b/src/doctor/PROOF.bend similarity index 100% rename from doctor/PROOF.bend rename to src/doctor/PROOF.bend diff --git a/doctor/plan.bend b/src/doctor/plan.bend similarity index 100% rename from doctor/plan.bend rename to src/doctor/plan.bend diff --git a/doctor/run.bend b/src/doctor/run.bend similarity index 100% rename from doctor/run.bend rename to src/doctor/run.bend diff --git a/doctor/world.bend b/src/doctor/world.bend similarity index 100% rename from doctor/world.bend rename to src/doctor/world.bend diff --git a/ez/LAWS.bend b/src/ez/LAWS.bend similarity index 100% rename from ez/LAWS.bend rename to src/ez/LAWS.bend diff --git a/ez/PROOF.bend b/src/ez/PROOF.bend similarity index 100% rename from ez/PROOF.bend rename to src/ez/PROOF.bend diff --git a/ez/cache.bend b/src/ez/cache.bend similarity index 100% rename from ez/cache.bend rename to src/ez/cache.bend diff --git a/ez/clock.bend b/src/ez/clock.bend similarity index 100% rename from ez/clock.bend rename to src/ez/clock.bend diff --git a/ez/cmd.bend b/src/ez/cmd.bend similarity index 100% rename from ez/cmd.bend rename to src/ez/cmd.bend diff --git a/ez/ends.bend b/src/ez/ends.bend similarity index 100% rename from ez/ends.bend rename to src/ez/ends.bend diff --git a/ez/gate.bend b/src/ez/gate.bend similarity index 100% rename from ez/gate.bend rename to src/ez/gate.bend diff --git a/ez/key.bend b/src/ez/key.bend similarity index 100% rename from ez/key.bend rename to src/ez/key.bend diff --git a/ez/line.bend b/src/ez/line.bend similarity index 100% rename from ez/line.bend rename to src/ez/line.bend diff --git a/ez/main.bend b/src/ez/main.bend similarity index 95% rename from ez/main.bend rename to src/ez/main.bend index 02f810d..eff5c22 100644 --- a/ez/main.bend +++ b/src/ez/main.bend @@ -4,9 +4,9 @@ # shown and the line exits 0, or the line is misused and exits 1. This file # prints and exits as they say and runs the command, which is trusted under # EZ-TRUST-2. `IO.args()` is copied so each word can be read more than once. -# Build it -# native (`bend ez/main.bend -o bin/ez.bin`); interpreted, bend's own CLI -# would take the flags meant for ez. +# The repo's top-level main.bend calls this `main`, and is the file that gets +# built. Build it native (`bend main.bend -o bin/ez.bin`); interpreted, bend's +# own CLI would take the flags meant for ez. import Base import 0xcab8a7a189cec2b51e8db0484f69c593/main.bend as Shake import ../share/args.bend as Args diff --git a/ez/named.bend b/src/ez/named.bend similarity index 100% rename from ez/named.bend rename to src/ez/named.bend diff --git a/ez/prove.bend b/src/ez/prove.bend similarity index 100% rename from ez/prove.bend rename to src/ez/prove.bend diff --git a/ez/quiet.bend b/src/ez/quiet.bend similarity index 100% rename from ez/quiet.bend rename to src/ez/quiet.bend diff --git a/ez/sorted.bend b/src/ez/sorted.bend similarity index 100% rename from ez/sorted.bend rename to src/ez/sorted.bend diff --git a/ez/start.bend b/src/ez/start.bend similarity index 100% rename from ez/start.bend rename to src/ez/start.bend diff --git a/ez/target.bend b/src/ez/target.bend similarity index 100% rename from ez/target.bend rename to src/ez/target.bend diff --git a/ez/test.bend b/src/ez/test.bend similarity index 100% rename from ez/test.bend rename to src/ez/test.bend diff --git a/ez/timer.bend b/src/ez/timer.bend similarity index 100% rename from ez/timer.bend rename to src/ez/timer.bend diff --git a/fetch/LAWS.bend b/src/fetch/LAWS.bend similarity index 100% rename from fetch/LAWS.bend rename to src/fetch/LAWS.bend diff --git a/fetch/PROOF.bend b/src/fetch/PROOF.bend similarity index 100% rename from fetch/PROOF.bend rename to src/fetch/PROOF.bend diff --git a/fetch/plan.bend b/src/fetch/plan.bend similarity index 100% rename from fetch/plan.bend rename to src/fetch/plan.bend diff --git a/fetch/run.bend b/src/fetch/run.bend similarity index 100% rename from fetch/run.bend rename to src/fetch/run.bend diff --git a/fetch/world.bend b/src/fetch/world.bend similarity index 100% rename from fetch/world.bend rename to src/fetch/world.bend diff --git a/git/LAWS.bend b/src/git/LAWS.bend similarity index 100% rename from git/LAWS.bend rename to src/git/LAWS.bend diff --git a/git/PROOF.bend b/src/git/PROOF.bend similarity index 100% rename from git/PROOF.bend rename to src/git/PROOF.bend diff --git a/git/exec.bend b/src/git/exec.bend similarity index 100% rename from git/exec.bend rename to src/git/exec.bend diff --git a/git/git.bend b/src/git/git.bend similarity index 100% rename from git/git.bend rename to src/git/git.bend diff --git a/hub/LAWS.bend b/src/hub/LAWS.bend similarity index 100% rename from hub/LAWS.bend rename to src/hub/LAWS.bend diff --git a/hub/PROOF.bend b/src/hub/PROOF.bend similarity index 100% rename from hub/PROOF.bend rename to src/hub/PROOF.bend diff --git a/hub/get.bend b/src/hub/get.bend similarity index 100% rename from hub/get.bend rename to src/hub/get.bend diff --git a/hub/hub.bend b/src/hub/hub.bend similarity index 100% rename from hub/hub.bend rename to src/hub/hub.bend diff --git a/init/LAWS.bend b/src/init/LAWS.bend similarity index 100% rename from init/LAWS.bend rename to src/init/LAWS.bend diff --git a/init/PROOF.bend b/src/init/PROOF.bend similarity index 100% rename from init/PROOF.bend rename to src/init/PROOF.bend diff --git a/init/plan.bend b/src/init/plan.bend similarity index 100% rename from init/plan.bend rename to src/init/plan.bend diff --git a/init/run.bend b/src/init/run.bend similarity index 100% rename from init/run.bend rename to src/init/run.bend diff --git a/io/LAWS.bend b/src/io/LAWS.bend similarity index 100% rename from io/LAWS.bend rename to src/io/LAWS.bend diff --git a/io/PROOF.bend b/src/io/PROOF.bend similarity index 100% rename from io/PROOF.bend rename to src/io/PROOF.bend diff --git a/io/file.bend b/src/io/file.bend similarity index 100% rename from io/file.bend rename to src/io/file.bend diff --git a/ledger/LAWS.bend b/src/ledger/LAWS.bend similarity index 100% rename from ledger/LAWS.bend rename to src/ledger/LAWS.bend diff --git a/ledger/PROOF.bend b/src/ledger/PROOF.bend similarity index 100% rename from ledger/PROOF.bend rename to src/ledger/PROOF.bend diff --git a/ledger/ignore.bend b/src/ledger/ignore.bend similarity index 100% rename from ledger/ignore.bend rename to src/ledger/ignore.bend diff --git a/ledger/manifest.bend b/src/ledger/manifest.bend similarity index 97% rename from ledger/manifest.bend rename to src/ledger/manifest.bend index aa65b3b..09d372f 100644 --- a/ledger/manifest.bend +++ b/src/ledger/manifest.bend @@ -1,9 +1,8 @@ -# ezx: ez's ledger library for Bend 2: it parses an ez.toml into its package, dependencies and pinned tools. -# -# ledger/manifest: the dependency ledger. Bend's import lines carry a bare -# `0x`, which says nothing about what the package is or where it came -# from, and nothing in a repo lists them. ez.toml is that list: every package -# the repo imports, by name, with its hash and its origin. +# ledger/manifest: the dependency ledger, and ez's ledger library. Bend's +# import lines carry a bare `0x`, which says nothing about what the +# package is or where it came from, and nothing in a repo lists them. +# ez.toml is that list: every package the repo imports, by name, with its +# hash and its origin. import Base import ../toml/toml.bend as T diff --git a/ledger/render.bend b/src/ledger/render.bend similarity index 100% rename from ledger/render.bend rename to src/ledger/render.bend diff --git a/ledger/upgrade.bend b/src/ledger/upgrade.bend similarity index 100% rename from ledger/upgrade.bend rename to src/ledger/upgrade.bend diff --git a/lock/LAWS.bend b/src/lock/LAWS.bend similarity index 100% rename from lock/LAWS.bend rename to src/lock/LAWS.bend diff --git a/lock/PROOF.bend b/src/lock/PROOF.bend similarity index 100% rename from lock/PROOF.bend rename to src/lock/PROOF.bend diff --git a/lock/lock.bend b/src/lock/lock.bend similarity index 100% rename from lock/lock.bend rename to src/lock/lock.bend diff --git a/lock/plan.bend b/src/lock/plan.bend similarity index 100% rename from lock/plan.bend rename to src/lock/plan.bend diff --git a/lock/run.bend b/src/lock/run.bend similarity index 100% rename from lock/run.bend rename to src/lock/run.bend diff --git a/lock/up.bend b/src/lock/up.bend similarity index 100% rename from lock/up.bend rename to src/lock/up.bend diff --git a/lock/world.bend b/src/lock/world.bend similarity index 100% rename from lock/world.bend rename to src/lock/world.bend diff --git a/pkg/LAWS.bend b/src/pkg/LAWS.bend similarity index 100% rename from pkg/LAWS.bend rename to src/pkg/LAWS.bend diff --git a/pkg/PROOF.bend b/src/pkg/PROOF.bend similarity index 100% rename from pkg/PROOF.bend rename to src/pkg/PROOF.bend diff --git a/pkg/bench/scan.bend b/src/pkg/bench/scan.bend similarity index 100% rename from pkg/bench/scan.bend rename to src/pkg/bench/scan.bend diff --git a/pkg/main.bend b/src/pkg/main.bend similarity index 89% rename from pkg/main.bend rename to src/pkg/main.bend index f34c7f1..59392c1 100644 --- a/pkg/main.bend +++ b/src/pkg/main.bend @@ -3,7 +3,7 @@ # written from on the second, then the manifest. The entry arrives in EZ_ENTRY, # since a native Bend binary takes no arguments of its own. # -# EZ_ENTRY=src/lib.bend bend pkg/main.bend +# EZ_ENTRY=src/lib.bend bend src/pkg/main.bend import Base import ./pkg.bend as K @@ -28,7 +28,7 @@ def report(+at: String) -> IO(Unit): # nothing to weigh is an error, not an empty package def go(+at: String) -> IO(Unit): Bool.pick(IO(Unit), String.is_empty(at), - IO.die(Unit, 1, "usage: EZ_ENTRY= bend pkg/main.bend"), + IO.die(Unit, 1, "usage: EZ_ENTRY= bend src/pkg/main.bend"), report(at)) def main() -> IO(Unit): diff --git a/pkg/path.bend b/src/pkg/path.bend similarity index 100% rename from pkg/path.bend rename to src/pkg/path.bend diff --git a/pkg/pkg.bend b/src/pkg/pkg.bend similarity index 100% rename from pkg/pkg.bend rename to src/pkg/pkg.bend diff --git a/pub/LAWS.bend b/src/pub/LAWS.bend similarity index 100% rename from pub/LAWS.bend rename to src/pub/LAWS.bend diff --git a/pub/PROOF.bend b/src/pub/PROOF.bend similarity index 100% rename from pub/PROOF.bend rename to src/pub/PROOF.bend diff --git a/pub/blurb.bend b/src/pub/blurb.bend similarity index 100% rename from pub/blurb.bend rename to src/pub/blurb.bend diff --git a/pub/plan.bend b/src/pub/plan.bend similarity index 100% rename from pub/plan.bend rename to src/pub/plan.bend diff --git a/pub/run.bend b/src/pub/run.bend similarity index 100% rename from pub/run.bend rename to src/pub/run.bend diff --git a/pub/world.bend b/src/pub/world.bend similarity index 100% rename from pub/world.bend rename to src/pub/world.bend diff --git a/remove/LAWS.bend b/src/remove/LAWS.bend similarity index 100% rename from remove/LAWS.bend rename to src/remove/LAWS.bend diff --git a/remove/PROOF.bend b/src/remove/PROOF.bend similarity index 100% rename from remove/PROOF.bend rename to src/remove/PROOF.bend diff --git a/remove/plan.bend b/src/remove/plan.bend similarity index 100% rename from remove/plan.bend rename to src/remove/plan.bend diff --git a/remove/run.bend b/src/remove/run.bend similarity index 100% rename from remove/run.bend rename to src/remove/run.bend diff --git a/run/bend.bend b/src/run/bend.bend similarity index 100% rename from run/bend.bend rename to src/run/bend.bend diff --git a/sha/LAWS.bend b/src/sha/LAWS.bend similarity index 100% rename from sha/LAWS.bend rename to src/sha/LAWS.bend diff --git a/sha/PROOF.bend b/src/sha/PROOF.bend similarity index 100% rename from sha/PROOF.bend rename to src/sha/PROOF.bend diff --git a/sha/dump.bend b/src/sha/dump.bend similarity index 100% rename from sha/dump.bend rename to src/sha/dump.bend diff --git a/sha/nar.bend b/src/sha/nar.bend similarity index 100% rename from sha/nar.bend rename to src/sha/nar.bend diff --git a/share/args.bend b/src/share/args.bend similarity index 100% rename from share/args.bend rename to src/share/args.bend diff --git a/share/cap.bend b/src/share/cap.bend similarity index 100% rename from share/cap.bend rename to src/share/cap.bend diff --git a/share/env.bend b/src/share/env.bend similarity index 100% rename from share/env.bend rename to src/share/env.bend diff --git a/share/exec.bend b/src/share/exec.bend similarity index 100% rename from share/exec.bend rename to src/share/exec.bend diff --git a/share/pass.bend b/src/share/pass.bend similarity index 100% rename from share/pass.bend rename to src/share/pass.bend diff --git a/share/pass.c b/src/share/pass.c similarity index 100% rename from share/pass.c rename to src/share/pass.c diff --git a/share/pass.js b/src/share/pass.js similarity index 100% rename from share/pass.js rename to src/share/pass.js diff --git a/share/pin.bend b/src/share/pin.bend similarity index 100% rename from share/pin.bend rename to src/share/pin.bend diff --git a/share/say.bend b/src/share/say.bend similarity index 100% rename from share/say.bend rename to src/share/say.bend diff --git a/share/sha.bend b/src/share/sha.bend similarity index 100% rename from share/sha.bend rename to src/share/sha.bend diff --git a/share/spin.bend b/src/share/spin.bend similarity index 100% rename from share/spin.bend rename to src/share/spin.bend diff --git a/toml/toml.bend b/src/toml/toml.bend similarity index 100% rename from toml/toml.bend rename to src/toml/toml.bend diff --git a/tool/LAWS.bend b/src/tool/LAWS.bend similarity index 100% rename from tool/LAWS.bend rename to src/tool/LAWS.bend diff --git a/tool/PROOF.bend b/src/tool/PROOF.bend similarity index 100% rename from tool/PROOF.bend rename to src/tool/PROOF.bend diff --git a/tool/plan.bend b/src/tool/plan.bend similarity index 100% rename from tool/plan.bend rename to src/tool/plan.bend diff --git a/tool/run.bend b/src/tool/run.bend similarity index 100% rename from tool/run.bend rename to src/tool/run.bend diff --git a/tool/world.bend b/src/tool/world.bend similarity index 100% rename from tool/world.bend rename to src/tool/world.bend diff --git a/tests/check.bend b/tests/check.bend index f4c408c..b265e2b 100644 --- a/tests/check.bend +++ b/tests/check.bend @@ -1,15 +1,14 @@ -# ez, run against the repo it is built from. The ledger here names a library -# 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. +# ez, run against the repo it is built from. The ledger here names ez's own +# program as its entry, and `ez check` checks it without running it. import Base import 0xabe575924687afad4cee1a2c1194d639/main.bend as R -import ../ez/quiet.bend as Q -import ../check/kit.bend as Check +import ../src/ez/quiet.bend as Q +import ../src/check/kit.bend as Check def main() -> IO(Unit): do IO: +out : String <- R.exec(["bin/ez.bin", "check"]) Check.eq_str("ez checks the repo's own ledger", Q.chomp(R.text(out)), - "ok ledger/manifest.bend") + "ok main.bend") #|ok ez checks the repo's own ledger diff --git a/tests/cli.bend b/tests/cli.bend index 4bb3ff3..7bd028e 100644 --- a/tests/cli.bend +++ b/tests/cli.bend @@ -4,10 +4,10 @@ # check, so nothing here can quietly be falling back to the network. import Base import 0xabe575924687afad4cee1a2c1194d639/main.bend as R -import ../io/file.bend as F -import ../ez/quiet.bend as Q -import ../check/kit.bend as Check -import ../check/world.bend as W +import ../src/io/file.bend as F +import ../src/ez/quiet.bend as Q +import ../src/check/kit.bend as Check +import ../src/check/world.bend as W # a check whose answer is a yes or a no def yes(name: String, ok: Bool) -> IO(Unit): diff --git a/tests/fetch.bend b/tests/fetch.bend index 082c3b2..1f13b15 100644 --- a/tests/fetch.bend +++ b/tests/fetch.bend @@ -5,11 +5,11 @@ # It is under tests/ rather than hub/tests/ because it drives a socket, and the # unit tests beside the code are about what can be said without one. import Base -import ../hub/hub.bend as Hub -import ../hub/get.bend as Net +import ../src/hub/hub.bend as Hub +import ../src/hub/get.bend as Net import 0xabe575924687afad4cee1a2c1194d639/main.bend as R -import ../check/kit.bend as Check -import ../check/world.bend as W +import ../src/check/kit.bend as Check +import ../src/check/world.bend as W # a url on that server def at(+port: String, path: String) -> String: diff --git a/tests/fresh.bend b/tests/fresh.bend index d10ff44..5673507 100644 --- a/tests/fresh.bend +++ b/tests/fresh.bend @@ -53,12 +53,12 @@ # gone. import Base import 0xabe575924687afad4cee1a2c1194d639/main.bend as R -import ../io/file.bend as F -import ../ez/cache.bend as C -import ../check/kit.bend as Check +import ../src/io/file.bend as F +import ../src/ez/cache.bend as C +import ../src/check/kit.bend as Check # every source the binary is compiled from that is newer than the binary. -# `check` and the `tests` directories are left out because `ez/main.bend` does +# `check` and the `tests` directories are left out because `main.bend` does # not reach them: they are what grades ez, not what ez is made of. A missing # binary is caught by the same walk, since `find` has nothing to compare against # and says so. @@ -67,7 +67,7 @@ def newer() -> IO(String): +out : String <- R.exec(["find", ".", "-name", "*.bend", "-newer", "bin/ez.bin", "-not", "-path", "./.ez/*", "-not", "-path", "./.git/*", - "-not", "-path", "./.claude/*", "-not", "-path", "./check/*", + "-not", "-path", "./.claude/*", "-not", "-path", "./src/check/*", "-not", "-path", "*/tests/*"]) return String.trim(R.text(out)) diff --git a/tests/git.bend b/tests/git.bend index 330a25a..1ef3431 100644 --- a/tests/git.bend +++ b/tests/git.bend @@ -5,10 +5,10 @@ # package and not merely two packages that both work. import Base import 0xabe575924687afad4cee1a2c1194d639/main.bend as R -import ../io/file.bend as F -import ../ez/quiet.bend as Q -import ../check/kit.bend as Check -import ../check/world.bend as W +import ../src/io/file.bend as F +import ../src/ez/quiet.bend as Q +import ../src/check/kit.bend as Check +import ../src/check/world.bend as W # a check whose answer is a yes or a no def yes(name: String, ok: Bool) -> IO(Unit): diff --git a/tests/hub.bend b/tests/hub.bend index 0bac715..4a12eae 100644 --- a/tests/hub.bend +++ b/tests/hub.bend @@ -4,12 +4,12 @@ # sandbox has no network to do it with. import Base import 0xabe575924687afad4cee1a2c1194d639/main.bend as R -import ../io/file.bend as F -import ../share/sha.bend as Sha -import ../doctor/plan.bend as DP -import ../ez/quiet.bend as Q -import ../check/kit.bend as Check -import ../check/world.bend as W +import ../src/io/file.bend as F +import ../src/share/sha.bend as Sha +import ../src/doctor/plan.bend as DP +import ../src/ez/quiet.bend as Q +import ../src/check/kit.bend as Check +import ../src/check/world.bend as W # a check whose answer is a yes or a no def yes(name: String, ok: Bool) -> IO(Unit): diff --git a/tests/init.bend b/tests/init.bend index a68ebe5..19e8e2b 100644 --- a/tests/init.bend +++ b/tests/init.bend @@ -3,10 +3,10 @@ # refused and leaves everything it found. import Base import 0xabe575924687afad4cee1a2c1194d639/main.bend as R -import ../io/file.bend as F -import ../ez/quiet.bend as Q -import ../check/kit.bend as Check -import ../check/world.bend as W +import ../src/io/file.bend as F +import ../src/ez/quiet.bend as Q +import ../src/check/kit.bend as Check +import ../src/check/world.bend as W # a check whose answer is a yes or a no def yes(name: String, ok: Bool) -> IO(Unit): diff --git a/tests/nix.bend b/tests/nix.bend index a379e19..5e5227e 100644 --- a/tests/nix.bend +++ b/tests/nix.bend @@ -4,11 +4,11 @@ # hub import during the check, inside `book_load`, and a nix build cannot. import Base import 0xabe575924687afad4cee1a2c1194d639/main.bend as R -import ../io/file.bend as F -import ../share/sha.bend as Sha -import ../ez/quiet.bend as Q -import ../check/kit.bend as Check -import ../check/world.bend as W +import ../src/io/file.bend as F +import ../src/share/sha.bend as Sha +import ../src/ez/quiet.bend as Q +import ../src/check/kit.bend as Check +import ../src/check/world.bend as W # a check whose answer is a yes or a no def yes(name: String, ok: Bool) -> IO(Unit): diff --git a/tests/publish.bend b/tests/publish.bend index 77f416f..209c1ad 100644 --- a/tests/publish.bend +++ b/tests/publish.bend @@ -7,10 +7,10 @@ # and uploading someone's tree to a public hub is not a thing a test does. import Base import 0xabe575924687afad4cee1a2c1194d639/main.bend as R -import ../io/file.bend as F -import ../ez/quiet.bend as Q -import ../check/kit.bend as Check -import ../check/world.bend as W +import ../src/io/file.bend as F +import ../src/ez/quiet.bend as Q +import ../src/check/kit.bend as Check +import ../src/check/world.bend as W # the repo being published: a nested layout with an import across it, which is # the shape that makes the file walk worth checking. One comment is not ASCII, @@ -39,11 +39,11 @@ def repo(+at: String) -> IO(Unit): # what ez says a file's package would be, without publishing it: the hash on # the first line, the directory its paths are written from on the second, then # the manifest. One run answers both questions, because a second `bend` over -# `pkg/main.bend` would cost a whole check to learn nothing new. The check +# `src/pkg/main.bend` would cost a whole check to learn nothing new. The check # report shares the stream with the answer, so the caller takes it back out. def ours(+here: String, +entry: String) -> IO(String): R.exec(["env", "BEND_LIB=" ++ here ++ "/.ez/lib", "EZ_ENTRY=" ++ entry, - "bend", here ++ "/pkg/main.bend"]) + "bend", here ++ "/src/pkg/main.bend"]) # the hash `bend --publish` mined, which is the line of its output that names a # package: the proof of work reports as it goes, on the same stream. diff --git a/tests/publishing.bend b/tests/publishing.bend index ecdae53..c8b5b0f 100644 --- a/tests/publishing.bend +++ b/tests/publishing.bend @@ -9,11 +9,11 @@ # check/liar.bend, a `bend` that uploads nothing. import Base import 0xabe575924687afad4cee1a2c1194d639/main.bend as R -import ../io/file.bend as F -import ../ez/quiet.bend as Q -import ../pub/plan.bend as P -import ../check/kit.bend as Check -import ../check/world.bend as W +import ../src/io/file.bend as F +import ../src/ez/quiet.bend as Q +import ../src/pub/plan.bend as P +import ../src/check/kit.bend as Check +import ../src/check/world.bend as W # a check whose answer is a yes or a no def yes(name: String, ok: Bool) -> IO(Unit): diff --git a/tests/relock.bend b/tests/relock.bend index edc8839..56f24ef 100644 --- a/tests/relock.bend +++ b/tests/relock.bend @@ -8,10 +8,10 @@ # checks it. import Base import 0xabe575924687afad4cee1a2c1194d639/main.bend as R -import ../io/file.bend as F -import ../ez/quiet.bend as Q -import ../check/kit.bend as Check -import ../check/world.bend as W +import ../src/io/file.bend as F +import ../src/ez/quiet.bend as Q +import ../src/check/kit.bend as Check +import ../src/check/world.bend as W # a check whose answer is a yes or a no def yes(name: String, ok: Bool) -> IO(Unit): diff --git a/tests/toml.bend b/tests/toml.bend index 7512e46..c18c75c 100644 --- a/tests/toml.bend +++ b/tests/toml.bend @@ -5,10 +5,10 @@ # one layout. The step checked is `toml/toml.bend`'s, between eztoml's # document and ez's sections, which no law covers (EZ-TRUST-8). import Base -import ../toml/toml.bend as T -import ../ledger/manifest.bend as M -import ../ledger/render.bend as Rend -import ../check/kit.bend as Check +import ../src/toml/toml.bend as T +import ../src/ledger/manifest.bend as M +import ../src/ledger/render.bend as Rend +import ../src/check/kit.bend as Check # a ledger as ez wrote it before: quoted strings, a bare `vendor = true`, and # a blank line before each table