From 9c61a3ea5a15b029e1cffc2008fc3a835e389926 Mon Sep 17 00:00:00 2001 From: Noah Gardner Date: Fri, 25 Sep 2026 15:19:42 -0400 Subject: [PATCH] fix: move the library from manifest/ to ledger/ so ez can go on the hub The hub serves every package's own manifest at /manifest, and it refuses a package with a top-level manifest/ directory (EISDIR on its staging file), so ez could not be published. The directory is now ledger/ (ez calls ez.toml the ledger); the entry is ledger/manifest.bend. Only paths moved: every import, SPEC Law cell and doc reference follows, and the RFC now records ez as published to the hub by hash. Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_01Vp3SCG5bcKMF4fUytZTwPj --- SPEC.md | 20 ++++++++++---------- add/LAWS.bend | 8 ++++---- add/PROOF.bend | 10 +++++----- add/hub.bend | 6 +++--- add/plan.bend | 6 +++--- add/world.bend | 2 +- docs/rfc/ez-add-planner.md | 4 ++-- docs/rfc/ez-lock-planner.md | 16 ++++++++-------- docs/rfc/ez-spec.md | 16 ++++++++-------- doctor/LAWS.bend | 2 +- doctor/PROOF.bend | 2 +- doctor/plan.bend | 2 +- doctor/world.bend | 2 +- ez.toml | 2 +- ez/LAWS.bend | 2 +- ez/PROOF.bend | 2 +- ez/named.bend | 2 +- ez/pin.bend | 2 +- ez/start.bend | 2 +- git/git.bend | 2 +- init/LAWS.bend | 4 ++-- init/PROOF.bend | 8 ++++---- init/plan.bend | 4 ++-- {manifest => ledger}/LAWS.bend | 0 {manifest => ledger}/PROOF.bend | 0 {manifest => ledger}/ignore.bend | 2 +- {manifest => ledger}/manifest.bend | 2 +- {manifest => ledger}/render.bend | 2 +- {manifest => ledger}/upgrade.bend | 4 ++-- lock/LAWS.bend | 14 +++++++------- lock/PROOF.bend | 12 ++++++------ lock/lock.bend | 2 +- lock/plan.bend | 2 +- lock/up.bend | 8 ++++---- lock/world.bend | 4 ++-- pub/LAWS.bend | 2 +- pub/PROOF.bend | 2 +- pub/plan.bend | 2 +- remove/LAWS.bend | 8 ++++---- remove/PROOF.bend | 10 +++++----- remove/plan.bend | 6 +++--- tests/check.bend | 2 +- tests/toml.bend | 4 ++-- tool/LAWS.bend | 2 +- tool/PROOF.bend | 2 +- tool/plan.bend | 2 +- tool/world.bend | 2 +- 47 files changed, 111 insertions(+), 111 deletions(-) rename {manifest => ledger}/LAWS.bend (100%) rename {manifest => ledger}/PROOF.bend (100%) rename {manifest => ledger}/ignore.bend (99%) rename {manifest => ledger}/manifest.bend (99%) rename {manifest => ledger}/render.bend (99%) rename {manifest => ledger}/upgrade.bend (97%) diff --git a/SPEC.md b/SPEC.md index 5eecc62..b319e7e 100644 --- a/SPEC.md +++ b/SPEC.md @@ -39,11 +39,11 @@ Untagged quantified laws are allowed. They pass the proof gate like any law, but | 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 | manifest/LAWS.bend read_refuses_a_problem; manifest/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 | manifest/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 | manifest/LAWS.bend remove_idem; remove/LAWS.bend remove_edits_ledger | +| 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 | manifest/LAWS.bend tool_section_not_dep; manifest/LAWS.bend tool_section_is_tool; manifest/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-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 | @@ -82,9 +82,9 @@ Untagged quantified laws are allowed. They pass the proof gate like any law, but | 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 | manifest/LAWS.bend allowlist_is_the_ledger; manifest/LAWS.bend allowlist_keeps_other_lines; manifest/LAWS.bend sync_allowlist_is_the_ledger; manifest/LAWS.bend sync_keeps_other_lines; manifest/LAWS.bend sync_idempotent; manifest/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 | manifest/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 | manifest/LAWS.bend rewrite_keeps_other_lines; manifest/LAWS.bend rewrite_keeps_line_count; manifest/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-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 | @@ -149,11 +149,11 @@ EZ-LED-8 is proved for every command that reads a source. `P.anchor` keeps a URL 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` (manifest/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` (ledger/ignore.bend), its allowlist lines are exactly the vendored hashes, each once, in the order the ledger first names them, and every other line is kept in order; the file `I.sync` writes reads back (`I.file.lines`) as those lines, whatever the file it read ended with, and applying it twice is applying it once; each for a ledger whose vendored hashes hold no newline. `ez remove` and `ez add` leave `.gitignore` holding exactly `I.sync`'s text over the ledger they leave (`remove_syncs_allowlist`, `add_syncs_allowlist`). `ez lock --upgrade`: every `.gitignore` its plan writes has the allowlist of the hashes the upgrade commits and keeps every other line of the file it read, when no source it read is at `.gitignore`; an upgrade that does not refuse and leaves `.gitignore` unwritten read one whose allowlist is already those hashes (`upgrade_allowlist_kept_in_sync`); and the hashes it commits are the vendored hashes of the model it renders when it writes ez.toml (`upgrade_vends_the_ledger`) and of ez.toml as it is when it does not (`upgrade_unmoved_vends_the_ledger`). `ez add`'s half and the upgrade's hold of ez.toml's bytes, since the ledger they leave reads back as the model they render (EZ-LED-4). EZ-DOC-1 is trusted, not proved: the lock is written as eztoml's `render` of the document ez assembles (`T.normal`, `toml/toml.bend`) and read through eztoml's `parse`, so it reads back when eztoml's round trip holds, which is EZ-TRUST-8, pending in eztoml v0.4.0. ez still writes no lock that `lockable.named` refuses: `lockable` refuses a hash, key or value holding `"`, `\` or a newline, a hash written twice, and a file path holding `=`. eztoml v0.4.0 escapes strings and reads a quoted key whole, so these refusals are no longer needed for eztoml; they are kept for `bootstrap.sh`, whose awk cuts a pair at its first `=` and reads no escape. What the lock records is the packages in hash order with each one's files in path order and each once, each tool pin without `vendor`, and the names in name order and each once. Until ez moved to eztoml 0.4 this row was proved against the v0.1.0 reader (`lock_reads_back` and its tools, names and hub laws); the maintainer chose to move ahead of eztoml's proofs, and those laws went with the reader they unfolded. -EZ-LED-4 is proved relative to EZ-TRUST-8. `manifest/LAWS.bend` states the read-back as a premise, `ReadsBack`: every ledger `Rend.renderable` accepts reads back, from the text `Rend.show` writes, as itself. `Rend.show` is eztoml's `render` of the document ez assembles (`Rend.text`) and `M.parse` reads through eztoml's `parse`, so the premise is eztoml's round trip, pending in eztoml v0.4.0, and ez does not prove it. What ez proves is the rest: every command that writes ez.toml refuses a ledger that is not renderable, with no effect (EZ-OUT-2), and writes one that reads back, given the premise, as the model its laws are stated over: `ez init` the package and entry it was given (`init_ledger_reads_back`), `ez add` the ledger with the dependency added (`add_ledger_reads_back`, `add_named_reads_back`), and `ez remove` the ledger with it dropped (`remove_ledger_reads_back`). `renderable` refuses a name or value holding `"`, `\` or a newline, a dependency with no hash, and a git source that names no repo or no root. A ledger written before ez used eztoml 0.4 reads to the same model: `toml/toml.bend` passes over the tables a dotted header implies, and `tests/toml.bend` reads an old ledger and lock and their new forms to the same sections. +EZ-LED-4 is proved relative to EZ-TRUST-8. `ledger/LAWS.bend` states the read-back as a premise, `ReadsBack`: every ledger `Rend.renderable` accepts reads back, from the text `Rend.show` writes, as itself. `Rend.show` is eztoml's `render` of the document ez assembles (`Rend.text`) and `M.parse` reads through eztoml's `parse`, so the premise is eztoml's round trip, pending in eztoml v0.4.0, and ez does not prove it. What ez proves is the rest: every command that writes ez.toml refuses a ledger that is not renderable, with no effect (EZ-OUT-2), and writes one that reads back, given the premise, as the model its laws are stated over: `ez init` the package and entry it was given (`init_ledger_reads_back`), `ez add` the ledger with the dependency added (`add_ledger_reads_back`, `add_named_reads_back`), and `ez remove` the ledger with it dropped (`remove_ledger_reads_back`). `renderable` refuses a name or value holding `"`, `\` or a newline, a dependency with no hash, and a git source that names no repo or no root. A ledger written before ez used eztoml 0.4 reads to the same model: `toml/toml.bend` passes over the tables a dotted header implies, and `tests/toml.bend` reads an old ledger and lock and their new forms to the same sections. 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. @@ -205,4 +205,4 @@ These assumptions sit outside the proofs. They are the complete list of Trusted | EZ-HASH-5 | ez's narHash matches nix. | nix is a separate program. What ez trusts of its own walk is GNU `find`'s listing of the tree, each path's type, `%M` mode, name and link target, and the file effect's read of each file's bytes. The walk takes the executable bit from the owner's exec bit of that mode, as nix's dumper does, and reads names and targets as listed (EZ-HASH-7). Submodules are not part of the tree: ez weighs a checkout without them, and its nix side asks `fetchgit` for the same. | | EZ-HASH-6 | `Sha.raw` computes the SHA-256 digest of its bytes, and `Sha.hex` of its text's UTF-8. | Proved in Giulio2002/bend-sha256 against an executable FIPS 180-4 specification, at the hash ez vendors; ez's gate does not re-check it. Collision resistance is also assumed. | -EZ-VEN-2 and EZ-VEN-3 are proved for the moves an upgrade makes (`manifest/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 (`ledger/LAWS.bend` `moves.ok`): each old hash names something, no hash holds `/` or a newline, as a `0x` name never does, and no move's new hash is the old hash of a move after it. That last is the premise the spec's notes call for: swaps apply one after another, so a new hash that is a later move's old one would be moved again. The text laws are over `U.reimport.many`, and the plan laws carry them to what `ez lock --upgrade` leaves at a `.bend` source it read and the World names once (`found`, with `pre` and `post` around it), when the lock does not refuse; that the sources the upgrade reads are the `.bend` files outside `.ez` and `.git` is the interpreter's (EZ-TRUST-2). A line names a hash when it starts `import /` at column 0; the new hash a line names is the one the first move of its old hash sends it to. diff --git a/add/LAWS.bend b/add/LAWS.bend index 97ac0f2..80dcf1a 100644 --- a/add/LAWS.bend +++ b/add/LAWS.bend @@ -22,10 +22,10 @@ import ../lock/up.bend as Up import ../lock/world.bend as W import ../lock/lock.bend as L import ../hub/hub.bend as Web -import ../manifest/manifest.bend as M -import ../manifest/LAWS.bend as ML -import ../manifest/render.bend as Rend -import ../manifest/ignore.bend as I +import ../ledger/manifest.bend as M +import ../ledger/LAWS.bend as ML +import ../ledger/render.bend as Rend +import ../ledger/ignore.bend as I import ../pkg/pkg.bend as K import ../pkg/path.bend as Path import ../git/git.bend as Git diff --git a/add/PROOF.bend b/add/PROOF.bend index 139b6ab..ce2b1f8 100644 --- a/add/PROOF.bend +++ b/add/PROOF.bend @@ -17,9 +17,9 @@ import ../lock/world.bend as W import ../lock/up.bend as Up import ../lock/lock.bend as L import ../hub/hub.bend as Web -import ../manifest/manifest.bend as M -import ../manifest/render.bend as Rend -import ../manifest/ignore.bend as I +import ../ledger/manifest.bend as M +import ../ledger/render.bend as Rend +import ../ledger/ignore.bend as I import ../pkg/pkg.bend as K import ../pkg/path.bend as Path import ../git/git.bend as Git @@ -29,8 +29,8 @@ import ../sha/sha.bend as Sha import ../check/eq.bend as Eq import ../check/str.bend as Str import ../pkg/PROOF.bend as Pk -import ../manifest/LAWS.bend as ML -import ../manifest/PROOF.bend as MP +import ../ledger/LAWS.bend as ML +import ../ledger/PROOF.bend as MP import ./LAWS.bend as Laws # --------------------------------------------------------------------------- diff --git a/add/hub.bend b/add/hub.bend index e290aff..3a64409 100644 --- a/add/hub.bend +++ b/add/hub.bend @@ -31,9 +31,9 @@ import ./world.bend as A import ../lock/plan.bend as P import ../lock/world.bend as W import ../lock/lock.bend as L -import ../manifest/manifest.bend as M -import ../manifest/render.bend as Rend -import ../manifest/ignore.bend as I +import ../ledger/manifest.bend as M +import ../ledger/render.bend as Rend +import ../ledger/ignore.bend as I import ../pkg/pkg.bend as K import ../pkg/path.bend as Path import ../git/git.bend as Git diff --git a/add/plan.bend b/add/plan.bend index d0d6489..af37444 100644 --- a/add/plan.bend +++ b/add/plan.bend @@ -44,9 +44,9 @@ import ./hub.bend as H import ../lock/plan.bend as P import ../lock/world.bend as W import ../lock/up.bend as Up -import ../manifest/manifest.bend as M -import ../manifest/render.bend as Rend -import ../manifest/ignore.bend as I +import ../ledger/manifest.bend as M +import ../ledger/render.bend as Rend +import ../ledger/ignore.bend as I import ../pkg/pkg.bend as K import ../pkg/path.bend as Path import ../git/git.bend as Git diff --git a/add/world.bend b/add/world.bend index fb03f6e..bd24739 100644 --- a/add/world.bend +++ b/add/world.bend @@ -17,7 +17,7 @@ import Base import ../lock/up.bend as Up import ../lock/world.bend as W -import ../manifest/manifest.bend as M +import ../ledger/manifest.bend as M import ../pkg/path.bend as P import ../ez/target.bend as Tgt import ../ez/named.bend as Named diff --git a/docs/rfc/ez-add-planner.md b/docs/rfc/ez-add-planner.md index 07f296a..df3bba3 100644 --- a/docs/rfc/ez-add-planner.md +++ b/docs/rfc/ez-add-planner.md @@ -368,7 +368,7 @@ pkg/pkg.bend io 0xa7168d2397b53aa3f11f3d0b949e4a1a root=. 4 fil pure 0xa7168d2397b53aa3f11f3d0b949e4a1a root=. 4 files lock/lock.bend io 0xe7b933bda3ab04d49220a988a598e7ee root=. 10 files pure 0xe7b933bda3ab04d49220a988a598e7ee root=. 10 files -manifest/LAWS.bend io 0xacce45a1ad6a67a1a363b7219cf1dc13 root=manifest 5 files +ledger/LAWS.bend io 0xacce45a1ad6a67a1a363b7219cf1dc13 root=manifest 5 files pure 0xacce45a1ad6a67a1a363b7219cf1dc13 root=manifest 5 files tests/cli.bend io 0x6336eb2017dddccca7c2cdde7560dede root=. 5 files pure 0x6336eb2017dddccca7c2cdde7560dede root=. 5 files @@ -456,7 +456,7 @@ The rewritten `K.pkg_of`, and `K.of` over every tracked file, give the hash, roo - Three questions of its own: `Probe{name}`, a program asked for its version (bend through `run/bend`), and `Lib{dir}`, the names `ls` gives for the library, both answered with what the program printed; and `Sources`, the lock's own listing (`W.Listing`, answered by `Run.read.listing`), every `.bend` file git tracks with its text. Every question depends only on what the World read, so doctor asks in one round. The library is looked in only when the lock records a package, and the sources are read only when the ledger reads. - The import lines are the lock's roots (`P.roots`), so doctor and `ez lock` agree on what the source imports, and the lock's packages are read by `L.hashes`, not grepped. The ledger is seen without its tools (`ledger.seen`) before anything is decided. - The plan is the lock's `Plan`: one `Say` per line and `Refused{""}` when any line is a problem, so it prints what it found and exits 1, as before. -- The laws, all in `doctor/LAWS.bend` unless named otherwise: `doctor_writes_nothing` (EZ-VEN-4); `doctor_reports_unrecorded`, `doctor_reports_unused`, `doctor_drift_fails` (EZ-VEN-5); `doctor_ignores_tools`, with `manifest/tool_section_not_dep`, `tool_section_is_tool`, `tool_needs_no_hash`, `lock/lock_origins_skip_tools`, `upgrade_origins_skip_tools`, `add/add_keeps_tools`, `remove/remove_keeps_tools` and `remove_refuses_tool` (EZ-LED-5); and the untagged `doctor_needs_ledger`, `doctor_refuses_unread`, `lock_needless`, `lock_needed`, `lock_names`. EZ-VEN-4, EZ-VEN-5 and EZ-LED-5 are proved. +- The laws, all in `doctor/LAWS.bend` unless named otherwise: `doctor_writes_nothing` (EZ-VEN-4); `doctor_reports_unrecorded`, `doctor_reports_unused`, `doctor_drift_fails` (EZ-VEN-5); `doctor_ignores_tools`, with `ledger/tool_section_not_dep`, `tool_section_is_tool`, `tool_needs_no_hash`, `lock/lock_origins_skip_tools`, `upgrade_origins_skip_tools`, `add/add_keeps_tools`, `remove/remove_keeps_tools` and `remove_refuses_tool` (EZ-LED-5); and the untagged `doctor_needs_ledger`, `doctor_refuses_unread`, `lock_needless`, `lock_needed`, `lock_names`. EZ-VEN-4, EZ-VEN-5 and EZ-LED-5 are proved. - Choices made with the maintainer away, as `cargo check` would: the sources are the tracked files, as the lock's are; no ez.toml, or one that does not read, fails the command and compares nothing; a lock that does not parse fails it whatever the ledger holds; and a lock that is missing fails it only when the ledger has dependencies, which keeps #67. ## Work packages diff --git a/docs/rfc/ez-lock-planner.md b/docs/rfc/ez-lock-planner.md index 9c5deb8..71eccae 100644 --- a/docs/rfc/ez-lock-planner.md +++ b/docs/rfc/ez-lock-planner.md @@ -248,7 +248,7 @@ How much of today's code moves unchanged: | :---- | ----: | :---- | | `lock/lock.bend` pure half: `Src`, `Pack`, `Origin`, `ledger.read`, `origin`, `known`, `has`, `specs`, `kids`, `manifest.files`, `nar.why`, `render.tools`, `doc`, `pack.sort`, and the readers `packs`, `pack_of`, `lock.hub` | about 465 of 929 | unchanged; the planner and `restore.bend` both use it | | `lock/lock.bend` IO half: `files.judge`, `fetch.*`, `disk.*`, `read.*`, `resolve.*`, `root.*`, `roots`, `lib`, `lock.at` | about 460 | the checks become `accept` (planner); the reads become `answer` (interpreter); the two continuation-passing walks become one pure walk | -| `manifest/upgrade.bend` (`U.aim`, `U.judge`, `U.agree`, `U.retarget`, `U.reimport.many`) and `manifest/ignore.bend` (`I.sync`) | 576 | unchanged; the upgrade planner calls them | +| `ledger/upgrade.bend` (`U.aim`, `U.judge`, `U.agree`, `U.retarget`, `U.reimport.many`) and `ledger/ignore.bend` (`I.sync`) | 576 | unchanged; the upgrade planner calls them | | `ez/upgrade.bend` | 532 | `Done`, `Out`, `join`, `swap.of`, `swap.hash` move to `lock/up.bend` unchanged; `walk`, `one`, `follow`, `forward`, `ask`, `judged`, `confirm`, `advanced` become pure functions of replies; `go.out` and the writers become effects | | `ez/pin.bend` | 424 | `set`, `join`, `gap`, `gaps` move unchanged; the IO walk becomes pure, like the dependency walk | | `git/git.bend` pure parsers `rows`, `exact`, `tip.rev`, `tip.branch`, `choose` | | unchanged; the planner reads `Printed` answers with them | @@ -361,7 +361,7 @@ law upgrade_settles: For a plain lock this is a corollary of `clone_reproduces` read backwards: the only thing a plain plan changes that the lock reads is which trees are under BEND_LIB. Under `--upgrade` the second run asks each moved pin's remote again, gets the same tip, finds the pin equal to it, confirms the checkout with `U.agree` against the hash, narHash and root the first run wrote, and so keeps it (`U.Keep`), and a ledger with nothing moved is not rewritten. -Reuses `clone_reproduces`, `check/eq.bend string_eq_self`. Replaces `manifest/LAWS.bend same_rev_keeps` (toward EZ-DOC-4). Effort: small for the plain lock, medium to large for the upgrade, whose key lemma is that a dependency's verdict on its own tip is `Keep` with agreement. +Reuses `clone_reproduces`, `check/eq.bend string_eq_self`. Replaces `ledger/LAWS.bend same_rev_keeps` (toward EZ-DOC-4). Effort: small for the plain lock, medium to large for the upgrade, whose key lemma is that a dependency's verdict on its own tip is `Keep` with agreement. **Update:** WP5a has landed the plain half as `lock/LAWS.bend lock_idempotent` and `relock_lays_nothing`. Where it differs from the sketch: `after` is law vocabulary in `lock/LAWS.bend`, not `P.after`, and a refused lock leaves the World it read, so `lock_idempotent` needs no premise. The second law is about BEND_LIB rather than ez.toml, which a plain lock never writes (EZ-DOC-5): after a lock that succeeded, no tree arrives by a clone that passes, so none is laid again. `upgrade_settles` is WP5b's. @@ -436,9 +436,9 @@ These are pointwise facts about a walk over the ledger's dependencies, so each p | Law | Reuses | Replaces | Effort | | :---- | :---- | :---- | :---- | -| EZ-RES-4 | `U.aim` of a hub source is `Hold` | `manifest/LAWS.bend hub_holds` | small | +| EZ-RES-4 | `U.aim` of a hub source is `Hold` | `ledger/LAWS.bend hub_holds` | small | | EZ-RES-5 | `U.judge`, `U.retarget`, `Git.tip.*` | `sha256_aims_forward`, `sha256_advances`, `sha256_retarget` (manifest); `sha256_remote_tip`, `sha256_remote_branch` (git), once a quantified `tip.rev` law is in | medium; key lemma: a `Forward` pin's verdict is `Advance` exactly when the tip differs and is onward | -| EZ-RES-6 | `U.chosen`, `U.aim(False, _) == Hold` | `manifest/LAWS.bend unselected_holds` | small for the frame, medium for the asks, whose key lemma is that `wants` only asks resolution questions about a selected entry | +| EZ-RES-6 | `U.chosen`, `U.aim(False, _) == Hold` | `ledger/LAWS.bend unselected_holds` | small for the frame, medium for the asks, whose key lemma is that `wants` only asks resolution questions about a selected entry | | EZ-RES-8 | `U.judge` with its agreement bit live, `U.agree` | `tag_follows`, `same_rev_drifts`, `tag_moved_off` (manifest) | medium | **Update:** WP6's second half has landed EZ-RES-5 and EZ-RES-8, proved relative to EZ-LED-4 and EZ-RES-7. Where the laws differ from the sketches above: @@ -492,12 +492,12 @@ law upgrade_writes_only_hits: `ignore.lines(w)` is the lines of the `.gitignore` the plan leaves (written or not), `source.next(w, at)` the text of source `at` after the plan, and `swapped(w, at, i, s)` says line `i` of the old text named `s.old` at column 0. Only `ez lock --upgrade` is in this phase; `ez add` and `ez remove` meet EZ-VEN-1 when they are converted. -EZ-VEN-1's line-level half is proved (`manifest/LAWS.bend allowlist_is_the_ledger`, `allowlist_keeps_other_lines`). What is left is the text layer of `I.sync`, which is "Left to prove" in `SPEC.md`: that `String.lines` of `String.join(ls, "\n")` is `ls` when no line holds a newline, which is the dual of the spike's `join_split`, and that a file left unwritten is the file `I.sync` would have made, which needs string equality reflected. EZ-VEN-2 and EZ-VEN-3 need the same `lines` after `join` lemma to go from `reimport` to its lines, then a lemma about one rewritten line, then an induction over the swaps with their old and new hashes disjoint, which is the premise the RFC already calls for. +EZ-VEN-1's line-level half is proved (`ledger/LAWS.bend allowlist_is_the_ledger`, `allowlist_keeps_other_lines`). What is left is the text layer of `I.sync`, which is "Left to prove" in `SPEC.md`: that `String.lines` of `String.join(ls, "\n")` is `ls` when no line holds a newline, which is the dual of the spike's `join_split`, and that a file left unwritten is the file `I.sync` would have made, which needs string equality reflected. EZ-VEN-2 and EZ-VEN-3 need the same `lines` after `join` lemma to go from `reimport` to its lines, then a lemma about one rewritten line, then an induction over the swaps with their old and new hashes disjoint, which is the premise the RFC already calls for. | Law | Reuses | Replaces | Effort | | :---- | :---- | :---- | :---- | | EZ-VEN-1 | `allowlist_is_the_ledger`, `allowlist_keeps_other_lines`, the spike's `join_split` | nothing; its laws are already tagged | medium | -| EZ-VEN-2 | the spike's `char_eq_true`, lifted to strings | `manifest/LAWS.bend imports_follow_hash` | medium to large; key lemma: `reimport.hash` of a rewritten line is the new hash | +| EZ-VEN-2 | the spike's `char_eq_true`, lifted to strings | `ledger/LAWS.bend imports_follow_hash` | medium to large; key lemma: `reimport.hash` of a rewritten line is the new hash | | EZ-VEN-3 | `join_split` with `\n`, `string_eq_self` | shares `imports_follow_hash` with EZ-VEN-2 | medium | ### EZ-HASH-2: NAR order @@ -517,7 +517,7 @@ Reuses `sort_perm`, `perm`, `distinct`. Replaces no trail. Effort: small. It doe ### Trails this phase deletes -`lock/LAWS.bend`: `hashes_sorted`, `lock_roundtrip`, `tool_pin_reads_back`. `manifest/LAWS.bend`: `sha256_aims_forward`, `hub_holds`, `tag_follows`, `unselected_holds`, `sha256_advances`, `same_rev_keeps`, `same_rev_drifts`, `tag_moved_off`, `sha256_retarget`, `imports_follow_hash`. `git/LAWS.bend`: `sha256_remote_tip`, `sha256_remote_branch`. Each goes in the change that lands the law naming it above. The trails toward EZ-LED-4, EZ-LED-5, EZ-VEN-5, EZ-TOOL-* and EZ-FETCH-1 stay. +`lock/LAWS.bend`: `hashes_sorted`, `lock_roundtrip`, `tool_pin_reads_back`. `ledger/LAWS.bend`: `sha256_aims_forward`, `hub_holds`, `tag_follows`, `unselected_holds`, `sha256_advances`, `same_rev_keeps`, `same_rev_drifts`, `tag_moved_off`, `sha256_retarget`, `imports_follow_hash`. `git/LAWS.bend`: `sha256_remote_tip`, `sha256_remote_branch`. Each goes in the change that lands the law naming it above. The trails toward EZ-LED-4, EZ-LED-5, EZ-VEN-5, EZ-TOOL-* and EZ-FETCH-1 stay. **Update:** these trails, and every other trail, are already gone. We deleted all 40 remaining `# toward` laws in one change, ahead of the laws that were to replace them, so that ez could move to the bolt whose strict `closed` and `trace` rules check `SPEC.md` (see the RFC's "Retiring closed laws"). Where a WP above says it replaces a closed law, there is nothing left to delete: the WP lands its quantified law and tags it. @@ -554,7 +554,7 @@ $ bolt.bin --gpu off We also ran the planner, outside the gate, on a two-package sample in which the project imports `0xb` and `0xb` imports `0xa`: with no replies it asked for `0xb`; with `0xb` answered it asked for `0xa`; with both answered it returned the lock, both packages in hash order; and with one file's text changed by a byte it refused. -What the spike tells us. The World and the planner are total pure terms with no `unsafe` def; the checker needed no fuel tricks beyond the walk's own. EZ-DOC-3 and the walk half of EZ-DOC-5 are small once the planner is shaped for them. The string layer of EZ-DOC-1, which we expected to be the hardest part of the phase, went through at about the rate `lock/PROOF.bend` and `manifest/PROOF.bend` were written: every failure was linearity (`+` on a binder used twice), definition order, or a def that matched on a value it had not been given as a parameter, and each was fixed in one edit. +What the spike tells us. The World and the planner are total pure terms with no `unsafe` def; the checker needed no fuel tricks beyond the walk's own. EZ-DOC-3 and the walk half of EZ-DOC-5 are small once the planner is shaped for them. The string layer of EZ-DOC-1, which we expected to be the hardest part of the phase, went through at about the rate `lock/PROOF.bend` and `ledger/PROOF.bend` were written: every failure was linearity (`+` on a binder used twice), definition order, or a def that matched on a value it had not been given as a parameter, and each was fixed in one edit. What it does not tell us. It has no upgrade, no interpreter, and no performance measurement. The upgrade laws are pointwise over dependencies and look like the walk invariant it did prove, but they read `Printed` answers through git's parsers, which the spike did not exercise. The re-verification cost of the demand loop is an estimate from the round count, not a measurement. diff --git a/docs/rfc/ez-spec.md b/docs/rfc/ez-spec.md index ed926e7..37fb727 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. Two things are paused until the Bend ecosystem needs them: publishing ez itself to the hub, and installing a tool by its hub name. A bend package is an import closure, not a directory, so the hub carries libraries, and tools install from git. ez's own layout, with its entry at `manifest/manifest.bend`, stays as it is. +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`. ## Proposal @@ -184,7 +184,7 @@ We do not need to convert every command before the spec is useful. The spec is w ### How far ez lock is from planner form -This is how the code stood at `b28ca2c`, before any conversion. Much of the pure half already existed. `origin` and `origins.all` choose where a package comes from (`lock/lock.bend:137-195`). `U.aim`, `U.judge`, `U.retarget`, `U.reallow.many` and `U.reimport.many` decide upgrades and compute the rewritten ledger, gitignore and sources (`manifest/upgrade.bend`). `Lock.render.tools` turns packages and tools into the lock's text. `K.hash_of` and `K.manifest_of` are pure. +This is how the code stood at `b28ca2c`, before any conversion. Much of the pure half already existed. `origin` and `origins.all` choose where a package comes from (`lock/lock.bend:137-195`). `U.aim`, `U.judge`, `U.retarget`, `U.reallow.many` and `U.reimport.many` decide upgrades and compute the rewritten ledger, gitignore and sources (`ledger/upgrade.bend`). `Lock.render.tools` turns packages and tools into the lock's text. `K.hash_of` and `K.manifest_of` are pure. What is not pure is the control flow between them, spread across roughly forty IO functions. Three places matter most. The package set grows from IO results: `resolve` reads or fetches a package, scans its text for imports, and queues what it finds, dying on the first bad package in walk order. A decision is made inside IO: `read.git` turns a missing manifest into an empty file list (`lock/lock.bend:287-293`), which is the bug that breaks EZ-DOC-3. And `--upgrade` runs three phases (`Up.run`, `Pin.upgrade`, `lock.now`) that communicate by writing ez.toml and `.ez/lib` and reading them back, so the final lock depends on the order of writes, and a failure in a later phase leaves earlier writes in place. @@ -217,11 +217,11 @@ The law sketches below use these names. Where no definition exists, the sketch i | `Lock.render.tools` | `lock/lock.bend:630`. The text of `ez.lock.toml`. | | `Lock.lock.at` | `lock/lock.bend:817`. The whole lock computation for a ledger and `BEND_LIB` (IO). Called from `Cmd.lock.now`, `ez/cmd.bend:193`. | | `Lock.pack_of` | `lock/lock.bend:681`. A package of a parsed lock, by hash. | -| `M.find`, `M.tool.find` | `manifest/manifest.bend:274, 381`. A ledger entry by name. | +| `M.find`, `M.tool.find` | `ledger/manifest.bend:274, 381`. A ledger entry by name. | | `Up.one`, `Pin.up.one` | `ez/upgrade.bend:261`, `ez/pin.bend:272`. The per-dependency and per-tool upgrade (IO). | -| `U.aim`, `U.judge` | `manifest/upgrade.bend`. Whether a pin is asked of the remote, and what the answer means. | -| `U.reallow.many`, `U.reimport.many` | `manifest/upgrade.bend:213, 274`. The rewritten `.gitignore` and source text. | -| `M.parse`, `M.dep` | `manifest/manifest.bend`. A ledger read from text, and a dependency of a read ledger by name. | +| `U.aim`, `U.judge` | `ledger/upgrade.bend`. Whether a pin is asked of the remote, and what the answer means. | +| `U.reallow.many`, `U.reimport.many` | `ledger/upgrade.bend:213, 274`. The rewritten `.gitignore` and source text. | +| `M.parse`, `M.dep` | `ledger/manifest.bend`. A ledger read from text, and a dependency of a read ledger by name. | | `World`, `Effect`, `LockArgs`, `Inputs`, `lock_plan`, `upgrade_plan`, `doctor_plan`, `inputs` | None. Introduced by this RFC. `upgrade_plan.ledger` is the ledger an upgrade plan writes, as a read ledger. | ### Requirements @@ -371,7 +371,7 @@ EZ-RES-5 and EZ-RES-8 are proved relative to EZ-RES-7. The law says ez moves a p | 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 | | 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 | -EZ-VEN-1 was not true when we wrote it: only `ez lock --upgrade` wrote the allowlist, `ez add` never wrote it, `ez remove` never removed a line, and `ez init` wrote `.ez/`, under which git ignores every allowlist line. The decided change derives the allowlist from the ledger with one pure function, `I.sync` in `manifest/ignore.bend`, which the three commands call, and changes `ez init` to write `.ez/*`, `!.ez/lib` and `.ez/lib/*`. The laws are stated over that function and over each command's plan, and the row is proved. +EZ-VEN-1 was not true when we wrote it: only `ez lock --upgrade` wrote the allowlist, `ez add` never wrote it, `ez remove` never removed a line, and `ez init` wrote `.ez/`, under which git ignores every allowlist line. The decided change derives the allowlist from the ledger with one pure function, `I.sync` in `ledger/ignore.bend`, which the three commands call, and changes `ez init` to write `.ez/*`, `!.ez/lib` and `.ez/lib/*`. The laws are stated over that function and over each command's plan, and the row is proved. EZ-VEN-2 and EZ-VEN-3 together specify rewriting completely: the first says what changes, the second says nothing else does. The match is exact at column 0, so an indented import (which the package walk accepts) is not rewritten; the requirement states the column-0 rule so that a change to it is a behavior change. Swaps apply one after another, so the law quantifies over swap lists in which no move's new hash is a later move's old one (`moves.ok`; `SPEC.md` spells out the premise). A single closed example, `imports_follow_hash`, covered both requirements on one file until the trails were deleted; WP7 proved both rows over the text and over the upgrade's plan. @@ -573,7 +573,7 @@ Adding a named hub dependency (WP24) adds one, shown on the binary first against Publishing by name (WP25) adds one, shown on the binary first with a stand-in `bend` that logs its arguments and uploads nothing. `ez publish` ran `bend --publish` whatever the ledger said, so a package could go on the hub by name only through bend by hand. The ledger's `[package]` table now takes two keys, `publish-as`, the hub name, and `version`, and with both `ez publish` runs `bend --publish @.0` and prints the import line by that name after the hash (EZ-PUB-3). We took a new key for the name rather than `name`, which a ledger may already hold as anything and which `ez add` reads as a dependency's key, and rather than `hub`, which is the hub's URL, as cargo keeps a registry's name apart from the package's. The version is `MAJOR.MINOR.PATCH`, as cargo and uv write one, and ez adds bend's fourth number as `.0`; a pre-release or build suffix is refused, since bend's four numbers have no way to write one, and we would rather refuse than drop it. One key without the other is refused before git is asked or bend is run, naming the key that is missing, as `cargo publish` refuses a package with no version; with neither, `ez publish` publishes by hash as before. `ez init` writes neither key. Both keys are in the ledger model, so `ez add`, `ez remove` and `ez lock --upgrade` keep them when they rewrite ez.toml, since a rewrite keeps the keys the model holds and drops any other, and `Rend.renderable` checks them so the ledger still reads back (EZ-LED-4). -Laying out a new project and showing its hub description (WP26) adds two, shown on the binary first, the upload with a stand-in `bend` that logs its arguments and uploads nothing. `ez init` wrote ez.toml, `.gitignore` and a `main.bend` that opened with `import Base`, and the hub describes a package by the first line of its first file by path, in plain string order and passing over `LICENSE`, so it listed every such package as `import Base`. `ez init` now takes `--description`, and the entry it writes opens with `# : `, or with `# : TODO describe ` when none is given, a placeholder that says what is missing where the author will see it. A description holding a newline is refused, since it would spill into the program. cargo writes no description into a new Cargo.toml and asks for one only when a package is published; the hub has no field for one, so ours goes where the hub reads it. `ez init` also lays the project out as `cargo new` does, the program at the top and a library under `src/`: `src/lib.bend` holds `greeting`, which the entry imports and prints, so `ez run` on a fresh project prints `hello` as it did. git keeps no empty directory, so `src/` holds a file rather than a `.gitkeep`, and we named it `lib.bend`, as cargo names `src/lib.rs`, rather than after the package, since a package name need not be a name bend's import line can carry. In the package that entry makes, `main.bend` comes before `src/lib.bend`, so the hub shows the entry's first line. The library is laid out only with a stub at the project's top, where `./src/lib.bend` finds it; an entry asked for in a directory of its own is written alone, and an entry or a `src/lib.bend` that is already there is never written over. The layout is only what `ez init` writes for a new project: other layouts, such as ez's own `manifest/manifest.bend` entry, keep working, and `ez doctor` does not check it. `ez publish`, once every check before the upload has passed and just before bend runs, prints `hub description: `, the line the hub will show, picked as the hub picks it from the files the walk made, which are the files bend sends. It goes to stderr, where bend's own notices go, so stdout stays the hash and the import line, and a publish refused before the upload prints only why. bend cannot be stopped between that line and the upload, so the line is for the author to read while bend mines its proof of work, not a question it waits on. +Laying out a new project and showing its hub description (WP26) adds two, shown on the binary first, the upload with a stand-in `bend` that logs its arguments and uploads nothing. `ez init` wrote ez.toml, `.gitignore` and a `main.bend` that opened with `import Base`, and the hub describes a package by the first line of its first file by path, in plain string order and passing over `LICENSE`, so it listed every such package as `import Base`. `ez init` now takes `--description`, and the entry it writes opens with `# : `, or with `# : TODO describe ` when none is given, a placeholder that says what is missing where the author will see it. A description holding a newline is refused, since it would spill into the program. cargo writes no description into a new Cargo.toml and asks for one only when a package is published; the hub has no field for one, so ours goes where the hub reads it. `ez init` also lays the project out as `cargo new` does, the program at the top and a library under `src/`: `src/lib.bend` holds `greeting`, which the entry imports and prints, so `ez run` on a fresh project prints `hello` as it did. git keeps no empty directory, so `src/` holds a file rather than a `.gitkeep`, and we named it `lib.bend`, as cargo names `src/lib.rs`, rather than after the package, since a package name need not be a name bend's import line can carry. In the package that entry makes, `main.bend` comes before `src/lib.bend`, so the hub shows the entry's first line. The library is laid out only with a stub at the project's top, where `./src/lib.bend` finds it; an entry asked for in a directory of its own is written alone, and an entry or a `src/lib.bend` that is already there is never written over. The layout is only what `ez init` writes for a new project: other layouts, such as ez's own `ledger/manifest.bend` entry, keep working, and `ez doctor` does not check it. `ez publish`, once every check before the upload has passed and just before bend runs, prints `hub description: `, the line the hub will show, picked as the hub picks it from the files the walk made, which are the files bend sends. It goes to stderr, where bend's own notices go, so stdout stays the hash and the import line, and a publish refused before the upload prints only why. bend cannot be stopped between that line and the upload, so the line is for the author to read while bend mines its proof of work, not a question it waits on. Running a plain Bend repository as `uvx` runs any package (WP28) adds five, each shown on the binary first against a local repository with no ez.toml and a local ez project, and each decided as uv and cargo would. A checkout with no ez.toml is a plain Bend repository, which `ez tool run`, `install` and `upgrade` refused (` has no ez.toml`): it now builds `main.bend`, or the file a new `--entry ` names, with no lock fetched and with BEND_LIB at `/lib` under the cache, beside the binaries, so bend fetches the program's hub imports itself and checks each against its name, as `uvx` runs a package that is not a uv project. `--entry` wins over a checkout's `bin` and `entry`, as cargo's `--bin` does, and not over a `[tools.*]` pin's, which the project decided; on `ez tool run` it comes before the target, as uvx takes its own options before the command, so every word after the target is still the program's. A plain repository is linked under the built file's name without `.bend`, or, when that is `main`, under the repository's name, the last segment of its URL or path with `.git` dropped. A built file that is not in the checkout is refused before anything is written, with a message that names it and suggests `--entry`, where a missing entry reached bend and failed there. And a cached remote checkout is reused whenever its record names the commit, where it was also asked to hold an ez.toml. A checkout with an ez.toml and no ez.lock.toml is still refused, now saying that its author runs `ez lock`, since a project built without its lock would take its git dependencies as they are today. diff --git a/doctor/LAWS.bend b/doctor/LAWS.bend index 59d3561..02a0357 100644 --- a/doctor/LAWS.bend +++ b/doctor/LAWS.bend @@ -23,7 +23,7 @@ import ./world.bend as DW import ./plan.bend as DP import ../lock/plan.bend as P import ../lock/world.bend as W -import ../manifest/manifest.bend as M +import ../ledger/manifest.bend as M # LAW: `ez doctor` writes, lays and removes nothing, whatever it found: its # plan is lines said and how the command ends, so no source file, ledger, diff --git a/doctor/PROOF.bend b/doctor/PROOF.bend index 9568d18..cf87092 100644 --- a/doctor/PROOF.bend +++ b/doctor/PROOF.bend @@ -18,7 +18,7 @@ import ./plan.bend as DP import ../lock/plan.bend as P import ../lock/world.bend as W import ../lock/lock.bend as L -import ../manifest/manifest.bend as M +import ../ledger/manifest.bend as M import ../check/eq.bend as Eq import ../check/str.bend as Str import ./LAWS.bend as Laws diff --git a/doctor/plan.bend b/doctor/plan.bend index a25ffab..ada6165 100644 --- a/doctor/plan.bend +++ b/doctor/plan.bend @@ -55,7 +55,7 @@ import ./world.bend as DW import ../lock/plan.bend as P import ../lock/world.bend as W import ../lock/lock.bend as L -import ../manifest/manifest.bend as M +import ../ledger/manifest.bend as M import ../ez/args.bend as Args # one thing doctor looked at: what to print, and whether it is a problem diff --git a/doctor/world.bend b/doctor/world.bend index 0975bfe..3501bd2 100644 --- a/doctor/world.bend +++ b/doctor/world.bend @@ -17,7 +17,7 @@ # `$BEND_LIB/names/`, as it is. import Base import ../lock/world.bend as W -import ../manifest/manifest.bend as M +import ../ledger/manifest.bend as M # a question the planner asks type Ask is Data: diff --git a/ez.toml b/ez.toml index 6dca74f..037c181 100644 --- a/ez.toml +++ b/ez.toml @@ -1,6 +1,6 @@ [package] name = "ez" -entry = "manifest/manifest.bend" +entry = "ledger/manifest.bend" bin = "ez/main.bend" [deps] [deps.sha256] diff --git a/ez/LAWS.bend b/ez/LAWS.bend index e2e2cf2..dc6236a 100644 --- a/ez/LAWS.bend +++ b/ez/LAWS.bend @@ -12,7 +12,7 @@ import ./gate.bend as G import ./clock.bend as Clock import ../ez/target.bend as Tgt import ./key.bend as K -import ../manifest/manifest.bend as M +import ../ledger/manifest.bend as M import ../ez/pin.bend as Pin import ../ez/env.bend as Env import ../pkg/path.bend as P diff --git a/ez/PROOF.bend b/ez/PROOF.bend index 2900d44..aa5fdbc 100644 --- a/ez/PROOF.bend +++ b/ez/PROOF.bend @@ -13,7 +13,7 @@ import ../ez/named.bend as Named import ../pkg/pkg.bend as Pkg import ../ez/env.bend as Env import ../pkg/path.bend as P -import ../manifest/manifest.bend as M +import ../ledger/manifest.bend as M import ./key.bend as K import 0x085b03c84ca37125e38dddede7b91e55/main.bend as Shake import ../ez/line.bend as L diff --git a/ez/named.bend b/ez/named.bend index 30b07c1..53d2e77 100644 --- a/ez/named.bend +++ b/ez/named.bend @@ -7,7 +7,7 @@ # one `[deps.main]`. A name the ledger gives to another source is refused # rather than written over. import Base -import ../manifest/manifest.bend as M +import ../ledger/manifest.bend as M import ../ez/target.bend as Tgt import ../pkg/pkg.bend as K diff --git a/ez/pin.bend b/ez/pin.bend index edff8d9..df2c6d8 100644 --- a/ez/pin.bend +++ b/ez/pin.bend @@ -3,7 +3,7 @@ # with no commit or no NAR hash stops it, naming the upgrade that fills the # pin. Filling and moving a pin is `ez lock --upgrade`'s, in lock/up.bend. import Base -import ../manifest/manifest.bend as M +import ../ledger/manifest.bend as M # why a plain lock cannot copy a git pin as it stands, or "" when it can. The # lock copies `rev` and `narHash` out of the ledger and never asks a remote diff --git a/ez/start.bend b/ez/start.bend index ea854ca..92998d0 100644 --- a/ez/start.bend +++ b/ez/start.bend @@ -6,7 +6,7 @@ # project's BEND_LIB in front of the line (`Env.line`), runs it and exits; # that it does so faithfully is EZ-TRUST-2. import Base -import ../manifest/manifest.bend as M +import ../ledger/manifest.bend as M import ../ez/args.bend as Args # which of the three commands is asking, with what it was told: where a diff --git a/git/git.bend b/git/git.bend index d088c5c..215565f 100644 --- a/git/git.bend +++ b/git/git.bend @@ -13,7 +13,7 @@ import Base import ../io/file.bend as F import 0x103d0af04de36ab98b311e537366ec67/main.bend as R import ../toml/toml.bend as T -import ../manifest/manifest.bend as M +import ../ledger/manifest.bend as M import ../pkg/pkg.bend as K import ../pkg/path.bend as P import ../sha/nar.bend as Nar diff --git a/init/LAWS.bend b/init/LAWS.bend index 12a594c..c1a2501 100644 --- a/init/LAWS.bend +++ b/init/LAWS.bend @@ -5,8 +5,8 @@ import Base import ./plan.bend as IP import ../lock/plan.bend as P -import ../manifest/manifest.bend as M -import ../manifest/LAWS.bend as ML +import ../ledger/manifest.bend as M +import ../ledger/LAWS.bend as ML import ../pub/blurb.bend as B # LAW: `ez init` that refuses writes nothing: not ez.toml, not `.gitignore`, diff --git a/init/PROOF.bend b/init/PROOF.bend index 24240e8..cd6276b 100644 --- a/init/PROOF.bend +++ b/init/PROOF.bend @@ -2,10 +2,10 @@ import Base import ./plan.bend as IP import ../lock/plan.bend as P -import ../manifest/manifest.bend as M -import ../manifest/render.bend as Rend -import ../manifest/LAWS.bend as ML -import ../manifest/PROOF.bend as MP +import ../ledger/manifest.bend as M +import ../ledger/render.bend as Rend +import ../ledger/LAWS.bend as ML +import ../ledger/PROOF.bend as MP import ../pub/blurb.bend as B import ../pub/LAWS.bend as PL import ../pub/PROOF.bend as PPr diff --git a/init/plan.bend b/init/plan.bend index 00caf28..3e82d01 100644 --- a/init/plan.bend +++ b/init/plan.bend @@ -23,8 +23,8 @@ # A4)" in docs/rfc/ez-add-planner.md. import Base import ../lock/plan.bend as P -import ../manifest/manifest.bend as M -import ../manifest/render.bend as Rend +import ../ledger/manifest.bend as M +import ../ledger/render.bend as Rend import ../pub/blurb.bend as B # what `ez init` reads: the name, entry file and description asked for ("" diff --git a/manifest/LAWS.bend b/ledger/LAWS.bend similarity index 100% rename from manifest/LAWS.bend rename to ledger/LAWS.bend diff --git a/manifest/PROOF.bend b/ledger/PROOF.bend similarity index 100% rename from manifest/PROOF.bend rename to ledger/PROOF.bend diff --git a/manifest/ignore.bend b/ledger/ignore.bend similarity index 99% rename from manifest/ignore.bend rename to ledger/ignore.bend index c8b3f4f..1606bdc 100644 --- a/manifest/ignore.bend +++ b/ledger/ignore.bend @@ -1,4 +1,4 @@ -# manifest/ignore: the gitignore allowlist, derived from the ledger. A +# ledger/ignore: the gitignore allowlist, derived from the ledger. A # dependency marked `vendor = true` has its tree committed under # `.ez/lib/`, and git only keeps it when `.gitignore` says so with a # `!.ez/lib/` line. That line has to follow the ledger exactly: a hash diff --git a/manifest/manifest.bend b/ledger/manifest.bend similarity index 99% rename from manifest/manifest.bend rename to ledger/manifest.bend index f24a0a9..832aa24 100644 --- a/manifest/manifest.bend +++ b/ledger/manifest.bend @@ -1,4 +1,4 @@ -# manifest/manifest: the dependency ledger. Bend's import lines carry a bare +# 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. diff --git a/manifest/render.bend b/ledger/render.bend similarity index 99% rename from manifest/render.bend rename to ledger/render.bend index 56e449d..015ca36 100644 --- a/manifest/render.bend +++ b/ledger/render.bend @@ -1,4 +1,4 @@ -# manifest/render: a ledger written back out as ez.toml, and the two edits the +# ledger/render: a ledger written back out as ez.toml, and the two edits the # command line makes to it. Rendering is from the model, so the file it writes # is the file it would read back. import Base diff --git a/manifest/upgrade.bend b/ledger/upgrade.bend similarity index 97% rename from manifest/upgrade.bend rename to ledger/upgrade.bend index 5b1a87d..cad64ad 100644 --- a/manifest/upgrade.bend +++ b/ledger/upgrade.bend @@ -1,10 +1,10 @@ -# manifest/upgrade: what `ez lock --upgrade` may do to one dependency, before +# ledger/upgrade: what `ez lock --upgrade` may do to one dependency, before # it talks to a remote. The ledger pins exact commits. A tag is the only # floating name a person wrote down, so that is what gets re-resolved. A pin # with no tag fast-forwards to the default branch tip when the commit is an # ancestor of it, and stays a commit pin. A hub package is the hash itself. # `vend` says the tree under `.ez/lib/` is committed, so a move lays the -# new tree there; the allowlist that names it is `manifest/ignore.bend`'s, +# new tree there; the allowlist that names it is `ledger/ignore.bend`'s, # derived from the ledger the move writes. A move also rewrites an # `import 0x/` line that names the old hash. import Base diff --git a/lock/LAWS.bend b/lock/LAWS.bend index 4541792..19b326d 100644 --- a/lock/LAWS.bend +++ b/lock/LAWS.bend @@ -7,15 +7,15 @@ import ./lock.bend as L import ./world.bend as W import ./plan.bend as P import ./up.bend as Up -import ../manifest/upgrade.bend as U -import ../manifest/manifest.bend as M +import ../ledger/upgrade.bend as U +import ../ledger/manifest.bend as M import ../toml/toml.bend as T import ../pkg/pkg.bend as K import ../pkg/LAWS.bend as KL import ../hub/hub.bend as Web -import ../manifest/upgrade.bend as U -import ../manifest/ignore.bend as I -import ../manifest/LAWS.bend as ML +import ../ledger/upgrade.bend as U +import ../ledger/ignore.bend as I +import ../ledger/LAWS.bend as ML import ../check/str.bend as Str # LAW: a package resolves to the origin recorded for it, whatever origins @@ -830,7 +830,7 @@ law relock_lays_nothing: # makes it from the file it read over the dependencies it leaves, and each # source it read with every moved hash rewritten (`U.reimport.many`), when # that changes it. The laws below say so of the plan, `P.put`, and the laws -# of `manifest/LAWS.bend` say what `I.sync` and `U.reimport.many` do to a +# of `ledger/LAWS.bend` say what `I.sync` and `U.reimport.many` do to a # text. A source is one the interpreter listed, a `.bend` file outside `.ez` # and `.git`; the laws take the ones the upgrade read, and a path the World # names once, as the interpreter lists each file once. @@ -932,7 +932,7 @@ law upgrade_vends_the_ledger: # LAW: a `.bend` source the upgrade read, once, holds afterwards its text # with every moved hash rewritten, when `ez lock --upgrade` does not refuse. -# The laws of `manifest/LAWS.bend` say what that rewriting does to the text. +# The laws of `ledger/LAWS.bend` say what that rewriting does to the text. law upgrade_rewrites_sources: for +w: W.World for +at: String diff --git a/lock/PROOF.bend b/lock/PROOF.bend index a73ed4c..2a86e0e 100644 --- a/lock/PROOF.bend +++ b/lock/PROOF.bend @@ -4,8 +4,8 @@ import ./lock.bend as L import ./world.bend as W import ./plan.bend as P import ./up.bend as Up -import ../manifest/manifest.bend as M -import ../manifest/upgrade.bend as U +import ../ledger/manifest.bend as M +import ../ledger/upgrade.bend as U import ../toml/toml.bend as T import ../check/eq.bend as Eq import ../check/str.bend as Str @@ -13,10 +13,10 @@ import ../pkg/pkg.bend as K import ../hub/hub.bend as Web import ../pkg/LAWS.bend as KL import ../pkg/PROOF.bend as KP -import ../manifest/ignore.bend as I -import ../manifest/render.bend as Rend -import ../manifest/LAWS.bend as ML -import ../manifest/PROOF.bend as MP +import ../ledger/ignore.bend as I +import ../ledger/render.bend as Rend +import ../ledger/LAWS.bend as ML +import ../ledger/PROOF.bend as MP import ../git/git.bend as Git import ./LAWS.bend as Laws diff --git a/lock/lock.bend b/lock/lock.bend index 8888ccb..9ecc55d 100644 --- a/lock/lock.bend +++ b/lock/lock.bend @@ -13,7 +13,7 @@ # lock/run.bend's. `ez fetch` reads a lock back in fetch/plan.bend. import Base import ../toml/toml.bend as T -import ../manifest/manifest.bend as M +import ../ledger/manifest.bend as M import ../pkg/pkg.bend as K # where a package's bytes come from. A hub package needs nothing else; a git diff --git a/lock/plan.bend b/lock/plan.bend index e6ef95c..f3cf820 100644 --- a/lock/plan.bend +++ b/lock/plan.bend @@ -34,7 +34,7 @@ import Base import ./world.bend as W import ./up.bend as Up import ./lock.bend as L -import ../manifest/manifest.bend as M +import ../ledger/manifest.bend as M import ../pkg/pkg.bend as K import ../pkg/path.bend as Path import ../ez/pin.bend as Pin diff --git a/lock/up.bend b/lock/up.bend index 3e11ae3..724c195 100644 --- a/lock/up.bend +++ b/lock/up.bend @@ -21,10 +21,10 @@ # hashes to the pin is `Drift` and refused. import Base import ./lock.bend as L -import ../manifest/manifest.bend as M -import ../manifest/render.bend as Rend -import ../manifest/upgrade.bend as U -import ../manifest/ignore.bend as I +import ../ledger/manifest.bend as M +import ../ledger/render.bend as Rend +import ../ledger/upgrade.bend as U +import ../ledger/ignore.bend as I import ../git/git.bend as Git import ../pkg/pkg.bend as K import ../pkg/path.bend as Path diff --git a/lock/world.bend b/lock/world.bend index 51f7096..1231028 100644 --- a/lock/world.bend +++ b/lock/world.bend @@ -17,8 +17,8 @@ import Base import ./lock.bend as L import ./up.bend as Up -import ../manifest/upgrade.bend as U -import ../manifest/manifest.bend as M +import ../ledger/upgrade.bend as U +import ../ledger/manifest.bend as M import ../pkg/pkg.bend as K import ../hub/hub.bend as Web import ../sha/sha.bend as Sha diff --git a/pub/LAWS.bend b/pub/LAWS.bend index cd119c1..8729df3 100644 --- a/pub/LAWS.bend +++ b/pub/LAWS.bend @@ -16,7 +16,7 @@ import ./world.bend as PW import ./plan.bend as PP import ../lock/plan.bend as P import ../git/git.bend as G -import ../manifest/manifest.bend as M +import ../ledger/manifest.bend as M import ../pkg/pkg.bend as K import ./blurb.bend as B import ../lock/lock.bend as L diff --git a/pub/PROOF.bend b/pub/PROOF.bend index 7545e55..e59f334 100644 --- a/pub/PROOF.bend +++ b/pub/PROOF.bend @@ -15,7 +15,7 @@ import ../pkg/pkg.bend as K import ./blurb.bend as B import ../git/git.bend as G import ../check/eq.bend as Eq -import ../manifest/manifest.bend as M +import ../ledger/manifest.bend as M import ../lock/lock.bend as L import ./LAWS.bend as Laws diff --git a/pub/plan.bend b/pub/plan.bend index ecb0d16..4d50811 100644 --- a/pub/plan.bend +++ b/pub/plan.bend @@ -24,7 +24,7 @@ import Base import ../lock/plan.bend as P import ../tool/world.bend as TW -import ../manifest/manifest.bend as M +import ../ledger/manifest.bend as M import ../pkg/pkg.bend as K import ../pkg/path.bend as Path import ../git/git.bend as G diff --git a/remove/LAWS.bend b/remove/LAWS.bend index e0c2018..e5d436f 100644 --- a/remove/LAWS.bend +++ b/remove/LAWS.bend @@ -5,10 +5,10 @@ import Base import ./plan.bend as RP import ../lock/plan.bend as P -import ../manifest/manifest.bend as M -import ../manifest/LAWS.bend as ML -import ../manifest/render.bend as Rend -import ../manifest/ignore.bend as I +import ../ledger/manifest.bend as M +import ../ledger/LAWS.bend as ML +import ../ledger/render.bend as Rend +import ../ledger/ignore.bend as I # LAW: `ez remove` that refuses writes, lays and removes nothing: not # ez.toml, not `.gitignore`, and no committed tree. Its plan has no effect at diff --git a/remove/PROOF.bend b/remove/PROOF.bend index 42febdc..79bcd27 100644 --- a/remove/PROOF.bend +++ b/remove/PROOF.bend @@ -2,13 +2,13 @@ import Base import ./plan.bend as RP import ../lock/plan.bend as P -import ../manifest/manifest.bend as M -import ../manifest/render.bend as Rend -import ../manifest/ignore.bend as I +import ../ledger/manifest.bend as M +import ../ledger/render.bend as Rend +import ../ledger/ignore.bend as I import ../check/eq.bend as Eq import ../check/str.bend as Str -import ../manifest/LAWS.bend as ML -import ../manifest/PROOF.bend as MP +import ../ledger/LAWS.bend as ML +import ../ledger/PROOF.bend as MP import ./LAWS.bend as Laws # LAW: removing committed trees writes nothing at any path diff --git a/remove/plan.bend b/remove/plan.bend index b521e2f..311a1fa 100644 --- a/remove/plan.bend +++ b/remove/plan.bend @@ -17,9 +17,9 @@ # A4)" in docs/rfc/ez-add-planner.md. import Base import ../lock/plan.bend as P -import ../manifest/manifest.bend as M -import ../manifest/render.bend as Rend -import ../manifest/ignore.bend as I +import ../ledger/manifest.bend as M +import ../ledger/render.bend as Rend +import ../ledger/ignore.bend as I # what `ez remove` reads: the name it was given, the ledger's text or None, # and the ignore file's text, "" when there is none diff --git a/tests/check.bend b/tests/check.bend index 4c7677a..57eb7bb 100644 --- a/tests/check.bend +++ b/tests/check.bend @@ -10,6 +10,6 @@ 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 manifest/manifest.bend") + "ok ledger/manifest.bend") #|ok ez checks the repo's own ledger diff --git a/tests/toml.bend b/tests/toml.bend index 41f2c4e..7512e46 100644 --- a/tests/toml.bend +++ b/tests/toml.bend @@ -6,8 +6,8 @@ # document and ez's sections, which no law covers (EZ-TRUST-8). import Base import ../toml/toml.bend as T -import ../manifest/manifest.bend as M -import ../manifest/render.bend as Rend +import ../ledger/manifest.bend as M +import ../ledger/render.bend as Rend import ../check/kit.bend as Check # a ledger as ez wrote it before: quoted strings, a bare `vendor = true`, and diff --git a/tool/LAWS.bend b/tool/LAWS.bend index bf5210c..1785fd6 100644 --- a/tool/LAWS.bend +++ b/tool/LAWS.bend @@ -9,7 +9,7 @@ import ./world.bend as TW import ./plan.bend as TP import ../lock/plan.bend as P import ../lock/up.bend as Up -import ../manifest/manifest.bend as M +import ../ledger/manifest.bend as M import ../git/git.bend as Git import ../pkg/path.bend as Path import ../ez/target.bend as Tgt diff --git a/tool/PROOF.bend b/tool/PROOF.bend index ff01f7c..fa63485 100644 --- a/tool/PROOF.bend +++ b/tool/PROOF.bend @@ -15,7 +15,7 @@ import ./world.bend as TW import ./plan.bend as TP import ../lock/plan.bend as P import ../lock/up.bend as Up -import ../manifest/manifest.bend as M +import ../ledger/manifest.bend as M import ../git/git.bend as Git import ../pkg/path.bend as Path import ../ez/target.bend as Tgt diff --git a/tool/plan.bend b/tool/plan.bend index dc02617..f270fa5 100644 --- a/tool/plan.bend +++ b/tool/plan.bend @@ -38,7 +38,7 @@ import Base import ./world.bend as TW import ../lock/plan.bend as P import ../lock/up.bend as Up -import ../manifest/manifest.bend as M +import ../ledger/manifest.bend as M import ../toml/toml.bend as T import ../pkg/pkg.bend as K import ../pkg/path.bend as Path diff --git a/tool/world.bend b/tool/world.bend index 5334d41..5a28bce 100644 --- a/tool/world.bend +++ b/tool/world.bend @@ -16,7 +16,7 @@ # Everything else here is a projection: what a World says, read one way. import Base import ../lock/up.bend as Up -import ../manifest/manifest.bend as M +import ../ledger/manifest.bend as M import ../pkg/path.bend as P # what the command does with the binary once it is current: `Run` starts it