feat!: bend 2.0.34, argv drops the program name, --help asks for help

README.md

@@ -24,8 +24,9 @@ ez add Emerging-Patterns/shake
 
 ## Usage
 
-A spec, a parse, and a read. `parse` answers `Done` with what the words
-bound, or `Fail` with why they could not be bound:
+A spec, a parse, and a read. `Shake.argv()` is the command line without
+the program name; `parse` answers `Done` with what the words bound, or
+`Fail` with why they could not be bound:
 
 ```
 import 0x085b03c84ca37125e38dddede7b91e55/main.bend as Shake
@@ -43,10 +44,21 @@ def greet(got: Result<&2, &2, Shake.ParseErr, Shake.Matched>) -> String:
     case Fail{ee}:
       Shake.err_text(spec(), ee)
 
-def main() -> String:
-  greet(Shake.parse(spec(), ["--name", "Ada"]))
+def main() -> IO(Unit):
+  do IO<Unit>:
+    av : List<&2, String> <- Shake.argv()
+    IO.print(greet(Shake.parse(spec(), av)))
 ```
 
+`bend hi.bend -- --name Ada` prints `hello Ada`, and so does a compiled
+`hi.bin --name Ada`. The same code works in an ez project, where
+`ez add` has put shake in the ledger.
+
+On bend 2.0.32 and later, `IO.args()` starts with the program as invoked
+(`hi.bin`, or `hi.bend` when interpreted), so a program that passes
+`IO.args()` straight to `parse` must drop that first word; `Shake.argv()`
+does it for you. shake needs bend 2.0.32 or later for that reason.
+
 `main.bend` is the whole interface: the types (`Shake.Cli`, `Shake.Sub`,
 `Shake.Arg`, `Shake.Matched`, `Shake.ParseErr`, `Shake.SpecErr`), the
 builders (`app`, `sub`, `flag`, `opt`, `many`, `pos`, `rest`), `check` and
@@ -62,9 +74,11 @@ that is not the last, a repeated name or spelling, a subcommand named
 optional one). `parse` does not call it; the guarantees hold for a spec it
 passes, so check yours once, at start or in your own laws.
 
-`parse` fails with a request for help on `tool help` or
-`tool help <command>`: `help_path` gives its command path, for `help` to
-print, and is `None` for every other error, which `err_text` describes.
+`parse` fails with a request for help on `tool help`, `tool help <command>`,
+`tool --help` or `tool <command> --help` (a command that declares its own
+long `help` gets `--help` as that argument instead): `help_path` gives its
+command path, for `help` to print, and is `None` for every other error,
+which `err_text` describes.
 A successful parse is read one command at a time, as clap's `ArgMatches`
 is: `get`, `get_all` and `on` read the bindings a command made, and
 `sub_name(m)` and `sub_of(m, name)` give the subcommand selected under it and
@@ -76,10 +90,11 @@ list, and `get` still reads one value. `argv` is the process's
 arguments, each word reusable.
 
 A compiled Bend program's runtime reads the command line before shake does
-(bend 2.0.27):
+(bend 2.0.34):
 
-- `--help` prints the runtime's own usage and exits, and `--gpu-build`
-  builds the GPU image and exits; neither runs `main`.
+- `--bend-help` prints the runtime's own usage and exits, and `--gpu-build`
+  builds the GPU image and exits; neither runs `main`. `--help` reaches
+  the program, and shake reads it as a request for help.
 - `--threads N` and `--gpu X` are taken, with their value, and a bad value
   stops the program.
 - The first `--` is taken too, and every word after it is passed on
@@ -94,6 +109,7 @@ cd shake
 mkdir -p bin
 bend examples/demo/main.bend -o bin/demo.bin
 bin/demo.bin help
+bin/demo.bin greet --help
 bin/demo.bin greet --name Ada -v
 bin/demo.bin add 2 3 --times 2
 ```
@@ -104,7 +120,7 @@ bin/demo.bin add 2 3 --times 2
 
 - `main.bend`: the interface.
 - `src/`: the implementation, with `src/LAWS.bend` stating the parser's laws
-  and `src/PROOF.bend` proving them. `ez prove` is the proof gate.
+  and `src/PROOF.bend` proving them. `nix flake check` runs the proof gate.
 - `examples/demo/`: a small program that uses only `main.bend`.
 - `ez.toml` and `ez.lock.toml`: the ledger and lock; bolt, the linter, is
   pinned there as `[tools.bolt]`, and `nix flake check` runs it.

SPEC.md

@@ -2,11 +2,11 @@
 
 This is the list of every behavior shake guarantees, each under a stable requirement ID. Every requirement is about the interface in `main.bend`: its types, builders, `parse`, `check`, the readers, `help`, `err_text`, `help_path`, `err_path` and `argv`. Every module under `src/` is internal and carries no promise.
 
-Every requirement has one of two levels. A **Proved** requirement holds for every input, and is backed by a quantified law (a `for` or `exs` binder) in `src/LAWS.bend` that passes the proof gate. A **Trusted** requirement is an assumption shake cannot check from inside its own gate, and it is listed in the trust boundary below. A Proved requirement whose laws have not all landed has status **pending**: we intend to prove it, and until then it is not guaranteed. The proof gate is this check: the first line `bend src/PROOF.bend` prints is exactly `All terms check.` (`ez prove`). Tests and fixtures are never evidence for a requirement.
+Every requirement has one of two levels. A **Proved** requirement holds for every input, and is backed by a quantified law (a `for` or `exs` binder) in `src/LAWS.bend` that passes the proof gate. A **Trusted** requirement is an assumption shake cannot check from inside its own gate, and it is listed in the trust boundary below. A Proved requirement whose laws have not all landed has status **pending**: we intend to prove it, and until then it is not guaranteed. The proof gate is this check: the first line `bend src/PROOF.bend` prints is exactly `ALL PROOFS CHECK`. Tests and fixtures are never evidence for a requirement.
 
 A spec is **well-formed** when `check` reports nothing for it (SHAKE-SPEC-1). The parse requirements hold for well-formed specs; a spec that contradicts itself, such as two options spelled `-n`, is its author's bug and not an input a user can give. Every error a row names but `NeedHelp` also carries `at`, the command path selected where the parse failed (SHAKE-ERR-2); rows write it only where it matters. A **plain word** is `-`, or a word that does not start with `-`. The **current command** is the command whose arguments `parse` matches words against: the root, then each subcommand it selects. The **selected path** is the names of the subcommands selected, in order. A successful parse answers the root command's **Matched**, as clap answers `ArgMatches`: the bindings that command made while it was current and, when a subcommand was selected under it, that subcommand's name and its own Matched, and so on down the selected path.
 
-The words `parse` receives are what the program passes it. In a compiled program they come from `argv`, after the runtime has taken its own flags and the first `--` (SHAKE-TRUST-2).
+The words `parse` receives are what the program passes it. In a compiled program they come from `argv`, which drops the program name `IO.args` starts with, after the runtime has taken its own flags and the first `--` (SHAKE-TRUST-2).
 
 The reasoning behind each requirement, the verdict of each against the code at `b93357a`, and the decisions that shaped them are in [docs/rfc/shake-spec.md](docs/rfc/shake-spec.md). The RFC also records the audit behind them and the rollout that proved every row.
 
@@ -36,7 +36,7 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n
 | SHAKE-TOK-4 | When a word exactly `--` reaches `parse` where an option could stand, it binds nothing and every later word is read as a plain word bound to a positional, whatever its shape. | Proved | proved | src/LAWS.bend dd_step; src/LAWS.bend raw_next; src/LAWS.bend raw_binds; src/LAWS.bend raw_no_pos; src/LAWS.bend raw_refused |
 | SHAKE-TOK-5 | A flag given a value (`--verbose=x`, or `-v=x` in a cluster) is refused as `Unexpected{word}`. | Proved | proved | src/LAWS.bend flag_long_valued; src/LAWS.bend letter_flag_eq |
 | SHAKE-TOK-6 | An option given no value in its own word takes the next word as its value, unless that word starts with `-` and is not `-`, or there is none; then the parse fails with `NoValue{name}`. | Proved | proved | src/LAWS.bend value_flag_shaped; src/LAWS.bend value_absent; src/LAWS.bend value_binds |
-| SHAKE-TOK-7 | A long or short spelling that no argument of the current command has is refused as `UnknownFlag{word}`. Arguments of a parent command are not matched after a subcommand is selected. | Proved | proved | src/LAWS.bend unknown_long; src/LAWS.bend unknown_short; src/LAWS.bend enter_step; src/LAWS.bend letter_unknown |
+| SHAKE-TOK-7 | A long or short spelling that no argument of the current command has is refused as `UnknownFlag{word}`, except a word `--help` that SHAKE-PARSE-8 reads as a request for help. Arguments of a parent command are not matched after a subcommand is selected. | Proved | proved | src/LAWS.bend unknown_long; src/LAWS.bend unknown_short; src/LAWS.bend enter_step; src/LAWS.bend letter_unknown |
 
 ### What a parse binds (SHAKE-PARSE)
 
@@ -49,7 +49,7 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n
 | SHAKE-PARSE-5 | A value given to an argument with a nonempty choices list binds only when it is in the list, and otherwise fails with `BadValue{name, value}`. An argument with no choices accepts every value. | Proved | proved | src/LAWS.bend choice_refused; src/LAWS.bend value_refused; src/LAWS.bend long_refused; src/LAWS.bend raw_refused; src/LAWS.bend letter_value_bad; src/LAWS.bend pos_next; src/LAWS.bend pos_binds; src/LAWS.bend raw_binds; src/LAWS.bend value_binds; src/LAWS.bend long_binds; src/LAWS.bend letter_value; src/LAWS.bend letter_value_eq |
 | SHAKE-PARSE-6 | After the last word, each argument of every command on the selected path that the words left unbound in that command and that has a default is bound to its default in that command's Matched. A bound argument's value is never replaced, and no argument without a default gains a binding. | Proved | proved | src/LAWS.bend default_filled; src/LAWS.bend bound_kept; src/LAWS.bend no_default; src/LAWS.bend no_argument |
 | SHAKE-PARSE-7 | A successful parse binds every required argument of every command on the selected path, in that command's Matched. Otherwise the parse fails with `Missing{name}`. | Proved | proved | src/LAWS.bend required_present; src/LAWS.bend required_missing |
-| SHAKE-PARSE-8 | Before `--` and before any positional of the current command is bound, a plain word `help` makes the parse fail with `NeedHelp{path}`, where `path` is the selected path followed by the remaining words, as long as each names a subcommand under the one before; the first remaining word that does not makes the parse fail with `Unexpected{word}`. | Proved | proved | src/LAWS.bend help_unknown; src/LAWS.bend help_step; src/LAWS.bend help_walk; src/LAWS.bend help_path |
+| SHAKE-PARSE-8 | Before `--` and before any positional of the current command is bound, a plain word `help`, or a word `--help` when no argument of the current command has the long spelling `help`, makes the parse fail with `NeedHelp{path}`, where `path` is the selected path followed by the remaining words, as long as each names a subcommand under the one before; the first remaining word that does not makes the parse fail with `Unexpected{word}`. A command that declares its own long `help` gets `--help` as that argument (SHAKE-TOK-1), and `help` still asks for help. | Proved | proved | src/LAWS.bend help_unknown; src/LAWS.bend help_step; src/LAWS.bend help_walk; src/LAWS.bend help_path; src/LAWS.bend dash_help_step; src/LAWS.bend dash_help_path |
 | SHAKE-PARSE-9 | Once a word makes the parse fail, the words after it do not change the error. | Proved | proved | src/LAWS.bend fail_stays |
 | SHAKE-PARSE-10 | A flag or an option built with `opt` that is given a second time while the same command is current, under any of its spellings, fails the parse with `Repeated{at, name}`; an argument of a parent command with the same name is a different argument (SHAKE-TOK-7). An option built with `many` binds every value given, in the order given, and `get_all` of its command's Matched reads them all. | Proved | proved | src/LAWS.bend repeated_long_flag; src/LAWS.bend repeated_long_opt; src/LAWS.bend letter_flag_again; src/LAWS.bend letter_opt_again; src/LAWS.bend long_binds; src/LAWS.bend letter_value; src/LAWS.bend letter_value_eq |
 
@@ -84,7 +84,7 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n
 
 | ID | Requirement | Level | Status | Law |
 | :---- | :---- | :---- | :---- | :---- |
-| SHAKE-ARGS-1 | The copy `argv` makes of the words `IO.args` gives keeps all of them, in order and unchanged: for every list, reading the copy back gives the list. | Proved | proved | src/LAWS.bend copy_keeps |
+| SHAKE-ARGS-1 | The copy `argv` makes of the words `IO.args` gives drops the first, the program as invoked, and keeps all the others, in order and unchanged: for every list, reading the copy back gives the list after its first word, and nothing for an empty list. | Proved | proved | src/LAWS.bend copy_keeps; src/LAWS.bend words_keeps |
 
 ## Left to prove
 
@@ -96,7 +96,7 @@ These assumptions sit outside the proofs. They are the complete list of Trusted
 
 | ID | Assumption | Why it is trusted |
 | :---- | :---- | :---- |
-| SHAKE-TRUST-1 | The Bend checker is sound: a proof it accepts proves its law. | It cannot be checked from inside Bend; this is EZ-TRUST-1. shake pins bend 2.0.27 through the flake. |
-| SHAKE-TRUST-2 | A program compiled by bend 2.0.27 hands `IO.args` the process's words after the program name, except that it stops examining words at the first `--`, drops that `--` and passes every later word through unchanged; before that `--` it removes `--threads` and `--gpu` with the word after each, and ends the process before `main` on `--help` and on `--gpu-build`. | It is the C `main` bend emits, read from bend 2.0.26's own source (in its binary) and confirmed against the demo; rechecked for 2.0.27, whose `main` is identical. It changes when bend does, so every bend bump rechecks it. |
-| SHAKE-TRUST-3 | The proof-gate runner fails the build unless the first line of `bend src/PROOF.bend` is `All terms check.` | It is ez's `mkProofs` running `ez prove`, run by `nix flake check` in CI; this is EZ-TRUST-4. |
-| SHAKE-TRUST-4 | `argv` hands on exactly the list `IO.args` answers, through the copy SHAKE-ARGS-1 is about. | It is IO, which no law can reach: `argv` in `src/args.bend` is one `IO.bind` of `IO.args` into `copy`, short enough to check by reading, and marked `# noqa: L001` for that reason. |
+| SHAKE-TRUST-1 | The Bend checker is sound: a proof it accepts proves its law. | It cannot be checked from inside Bend; this is EZ-TRUST-1. shake pins bend 2.0.34 through the flake. |
+| SHAKE-TRUST-2 | A program compiled by bend 2.0.34 hands `IO.args` the program as invoked (the process's `argv[0]`) followed by the process's words after it, except that at the first `--` it stops examining words, drops that `--` and passes every later word through unchanged; before that `--` it removes `--threads` and `--gpu` with the word after each (ending the process on a bad value), and ends the process before `main` on `--bend-help` and on `--gpu-build`. Every other word reaches `IO.args`, `--help` included. Run as `bend file.bend [args]`, `IO.args` is the file as given, then the arguments. | It is the C `main` bend emits (`main` in bend2/comp.ts and `IO.args` in bend2/effs/args.c), read from bend 2.0.34's source and confirmed against the demo; 2.0.29 stopped taking `--help` and 2.0.32 put the program first. It changes when bend does, so every bend bump rechecks it. |
+| SHAKE-TRUST-3 | The proof-gate runner fails the build unless the first line of `bend src/PROOF.bend` is `ALL PROOFS CHECK`. | It is the flake's `proofs` check, run by `nix flake check` in CI, which runs every PROOF.bend on the flake's bend and compares the first line; `ez prove` does the same once ez runs on bend 2.0.34. |
+| SHAKE-TRUST-4 | `argv` hands on exactly the list `IO.args` answers, through the copy SHAKE-ARGS-1 is about. | It is IO, which no law can reach: `argv` in `src/args.bend` is one `IO.bind` of `IO.args` into `words`, short enough to check by reading, and marked `# noqa: L001` for that reason. |

ez.lock.toml

@@ -4,8 +4,8 @@ hub = "https://hub.bend-lang.com"
 [tools]
 [tools.bolt]
 git = "https://github.com/Emerging-Patterns/bolt"
-rev = "02fb09377f5c0fbddb5f6b7c32c8ab4ae14240df"
-tag = "v1.8.0"
+rev = "d5a67600a96ba423f2212bd661a30c1fba38eb55"
+tag = "v1.9.0"
 root = "."
-narHash = "sha256-53zE+3lZ/jn9GvIeGoavvNMaFyUs5dEFWd7fwP49TlM="
+narHash = "sha256-HmJ8J1xDshBdSWXIiEp48GZ9qHsm+bmpHw06ZWwcDVE="
 entry = "main.bend"

ez.toml

@@ -4,8 +4,8 @@ entry = "main.bend"
 
 [tools.bolt]
 git = "https://github.com/Emerging-Patterns/bolt"
-rev = "02fb09377f5c0fbddb5f6b7c32c8ab4ae14240df"
-tag = "v1.8.0"
+rev = "d5a67600a96ba423f2212bd661a30c1fba38eb55"
+tag = "v1.9.0"
 root = "."
-narHash = "sha256-53zE+3lZ/jn9GvIeGoavvNMaFyUs5dEFWd7fwP49TlM="
+narHash = "sha256-HmJ8J1xDshBdSWXIiEp48GZ9qHsm+bmpHw06ZWwcDVE="
 entry = "main.bend"