feat: env-var fallbacks and did-you-mean for unknown flags

README.md

@@ -64,11 +64,13 @@ On bend 2.0.32 and later, `IO.args()` starts with the program as invoked
 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
-`spec_err_text`, `parse`, the readers (`get`, `get_all`, `on`, `sub_name`,
-`sub_of`, `at`, `path_of`), `help`, `err_text`, `help_path`, `err_path` and
-`argv`. Everything under `src/` is
+`Shake.Arg`, `Shake.Matched`, `Shake.ParseErr`, `Shake.SpecErr`,
+`Shake.Var`), the builders (`app`, `sub`, `flag`, `opt`, `many`, `pos`,
+`rest`, `env`), `check` and `spec_err_text`, `parse` and `parse_env`, the
+readers (`get`, `get_all`, `on`, `sub_name`, `sub_of`, `at`, `path_of`),
+`help`, `err_text`, `help_path`, `err_path`, `suggestion`, `argv` and
+`env_vars`.
+Everything under `src/` is
 internal and may change in any release; import only `main.bend`.
 [SPEC.md](SPEC.md) lists what shake guarantees, and which of it is proved.
 
@@ -82,7 +84,11 @@ passes, so check yours once, at start or in your own laws.
 `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.
+which `err_text` describes. For a mistyped long option, `err_text` adds
+clap's tip (`tip: a similar argument exists: '--name'` for `--nmae`), and
+`suggestion` gives that long option word on its own. It picks the closest
+long spelling of the current command's flags and options, and nothing when
+none is close.
 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
@@ -93,6 +99,25 @@ positional keeps every leftover word under one name; `get_all` reads that
 list, and `get` still reads one value. `argv` is the process's
 arguments, each word reusable.
 
+`env(arg, "NAME")` gives an argument an env var to fall back to, as clap's
+`.env("NAME")`: `parse_env(spec, words, vars)` binds what the words give,
+then fills an argument they left unbound from its env var, then from its
+default. `env_vars(spec)` reads the env vars the spec names, as
+`(name, value)` pairs; a test passes its own, as in
+`parse_env(spec(), [], [("HI_NAME", "Ada")])`. An env var set to the empty
+string counts as unset. A flag's env var sets it unless its value, in any
+case, is `0`, `false`, `no`, `off`, `n` or `f`. An env value outside the
+argument's choices fails the parse with `BadValue`. Help shows
+`[env: NAME]` after the argument's help text. `parse` ignores env vars.
+
+```bend
+def main() -> IO(Unit):
+  do IO<Unit>:
+    av : List<&2, String> <- Shake.argv()
+    ev : List<&2, Shake.Var> <- Shake.env_vars(spec())
+    IO.print(greet(Shake.parse_env(spec(), av, ev)))
+```
+
 A compiled Bend program's runtime reads the command line before shake does
 (bend 2.0.34):
 

SPEC.md

@@ -1,14 +1,16 @@
 # shake specification
 
-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.
+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`, `parse_env`, `check`, the readers, `help`, `err_text`, `help_path`, `err_path`, `suggestion`, `argv` and `env_vars`. 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 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`, 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.
+An argument's **env var** is the name `env` gives it; an argument built without `env` has none. `parse_env` also receives **vars**, a list of name and value pairs, which in a compiled program come from `env_vars` (SHAKE-TRUST-5). An argument's **env value** is the value of the first pair in vars named by its env var, when that value is not empty; an env var no pair names, or whose first pair's value is empty, gives no env value.
+
+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. The env and suggestion rows (SHAKE-PARSE-11, PARSE-12, HELP-3, ERR-3, ERR-4, ARGS-2, TRUST-5) are designed in [docs/rfc/shake-env-and-suggestions.md](docs/rfc/shake-env-and-suggestions.md).
 
 ## Format
 
@@ -52,6 +54,8 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n
 | 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 |
+| SHAKE-PARSE-11 | `parse_env(spec, words, vars)` reads `words` exactly as `parse` reads them against `spec` with every argument's default, in every command, replaced by its **fallback**, and answers what that parse answers, except as SHAKE-PARSE-12 says. An argument's fallback is its env value when it has one and is not a flag; for a flag with an env value, `true` when that value, lowercased, is none of `0`, `false`, `no`, `off`, `n` and `f`, and no fallback otherwise; and for an argument with no env value, its default. So a value the words bind wins over the env value and the env value over the default (SHAKE-PARSE-6), an argument with a fallback is filled by it and needs nothing from the words to satisfy `required` (SHAKE-PARSE-7), a required positional with a fallback does not block a subcommand (SHAKE-PARSE-4), and `parse_env(spec, words, [])` is `parse(spec, words)`. | Proved | proved | src/LAWS.bend env_sets; src/LAWS.bend env_of_none; src/LAWS.bend env_of_nil; src/LAWS.bend env_of_hit; src/LAWS.bend env_of_empty; src/LAWS.bend env_of_skip; src/LAWS.bend fallback_env; src/LAWS.bend fallback_flag_on; src/LAWS.bend fallback_flag_off; src/LAWS.bend fallback_default; src/LAWS.bend resolve_spec; src/LAWS.bend resolve_args_con; src/LAWS.bend resolve_subs_con; src/LAWS.bend env_parse; src/LAWS.bend env_none |
+| SHAKE-PARSE-12 | When the parse SHAKE-PARSE-11 describes succeeds and an argument other than a flag, of a command on the selected path, has an env value outside its nonempty choices that the command's Matched binds to it, `parse_env` fails instead with `BadValue{at, name, value}` of the first such argument, the root command first and each command's arguments in spec order, where `at` is the selected path. A word's value outside the choices never binds (SHAKE-PARSE-5), so only an argument filled from its env value can be bound to it. When that parse fails, `parse_env` fails with the same error. | Proved | proved | src/LAWS.bend env_check_fail; src/LAWS.bend env_check_good; src/LAWS.bend env_check_bad; src/LAWS.bend bad_go_leaf; src/LAWS.bend bad_go_root; src/LAWS.bend bad_go_down; src/LAWS.bend bad_args_here; src/LAWS.bend bad_args_next; src/LAWS.bend bad_args_nil; src/LAWS.bend bad_arg_some; src/LAWS.bend bad_arg_unset; src/LAWS.bend bad_arg_flag; src/LAWS.bend bad_arg_allowed; src/LAWS.bend bad_arg_unbound |
 
 ### Checking a spec (SHAKE-SPEC)
 
@@ -72,19 +76,23 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n
 | :---- | :---- | :---- | :---- | :---- |
 | SHAKE-HELP-1 | `help(spec, path)` renders the page of the command reached by following each name of `path` from the root through the subcommands, skipping a name that is not a subcommand where it stands. | Proved | proved | src/LAWS.bend help_page; src/LAWS.bend reach_child; src/LAWS.bend reach_skip |
 | SHAKE-HELP-2 | A page lists each subcommand of its command exactly once, in spec order, followed by `help`, and each flag and option exactly once, in spec order. Its usage line names each positional exactly once, in spec order, as `<NAME>` when required and `[NAME]` otherwise, with `...` after a rest positional. | Proved | proved | src/LAWS.bend cmds_listed; src/LAWS.bend opts_listed; src/LAWS.bend usage_listed |
+| SHAKE-HELP-3 | The Options line of a flag or option that has an env var `NAME` shows `[env: NAME]` after its help text, before its `[default: ...]` and `[possible values: ...]`, as clap's does; the line of one with no env var is what it would be without this row. A positional has no Options line (SHAKE-HELP-2), so its env var is not shown. | Proved | proved | src/LAWS.bend help_env_shown; src/LAWS.bend help_env_none |
 
 ### Errors (SHAKE-ERR)
 
 | ID | Requirement | Level | Status | Law |
 | :---- | :---- | :---- | :---- | :---- |
 | SHAKE-ERR-1 | `err_text(spec, err)` is empty exactly when `help_path(err)` is `Some`, that is, when the parse failed with a request for help. | Proved | proved | src/LAWS.bend err_text_help; src/LAWS.bend err_text_iff |
 | SHAKE-ERR-2 | For every error but a request for help, `err_path(err)` is the path of subcommands the parse had selected at the word that failed it, and `err_text(spec, err)` shows the usage line of the command at that path, as `help(spec, err_path(err))` does. | Proved | proved | src/LAWS.bend err_path_at; src/LAWS.bend err_text_usage; src/LAWS.bend help_page; src/LAWS.bend unknown_long; src/LAWS.bend unknown_short; src/LAWS.bend no_pos_left; src/LAWS.bend choice_refused; src/LAWS.bend flag_long_valued; src/LAWS.bend value_flag_shaped; src/LAWS.bend value_absent; src/LAWS.bend help_unknown; src/LAWS.bend long_no_name; src/LAWS.bend repeated_long_flag; src/LAWS.bend repeated_long_opt; src/LAWS.bend value_refused; src/LAWS.bend long_refused; src/LAWS.bend raw_no_pos; src/LAWS.bend raw_refused; src/LAWS.bend enter_missing; src/LAWS.bend required_missing; src/LAWS.bend letter_flag_eq; src/LAWS.bend letter_unknown; src/LAWS.bend letter_flag_again; src/LAWS.bend letter_opt_again; src/LAWS.bend letter_value_bad |
+| SHAKE-ERR-3 | `suggestion(spec, err)` is `None` for every error but an `UnknownFlag{at, word}` whose word starts with `--` (SHAKE-TOK-1, TOK-7). For such a word, let `typed` be its chars after `--` up to its first `=`, and the **candidates** the long spellings of the flags and options of the command at `at`, reached as `help(spec, at)` reaches it (SHAKE-HELP-1), in spec order; a parent command's arguments, subcommands and `help` are not candidates. A candidate `c` is **close** when `0 < d` and `3 * d <= max(length(typed), length(c))`, where `d` is the optimal string alignment distance from `typed` to `c`: the fewest single-char insertions, deletions, substitutions and swaps of two adjacent chars that turn one into the other, editing no char twice. The suggestion is `Some{"--" ++ c}` for the close candidate with the least `d`, the first in spec order among equals, and `None` when no candidate is close. A short option word never gets one. | Proved | proved | src/LAWS.bend sug_other; src/LAWS.bend sug_short; src/LAWS.bend sug_long; src/LAWS.bend sug_found_some; src/LAWS.bend cands_some; src/LAWS.bend cands_none; src/LAWS.bend sug_close; src/LAWS.bend best_nil; src/LAWS.bend best_far; src/LAWS.bend best_only; src/LAWS.bend best_here; src/LAWS.bend best_there |
+| SHAKE-ERR-4 | When `suggestion(spec, err)` is `Some{s}`, `err_text(spec, err)` contains `s`. | Proved | proved | src/LAWS.bend err_text_tip |
 
 ### The argument list (SHAKE-ARGS)
 
 | ID | Requirement | Level | Status | Law |
 | :---- | :---- | :---- | :---- | :---- |
 | 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 |
+| SHAKE-ARGS-2 | The names `env_vars(spec)` asks `IO.get_env` for are the env vars of the arguments that have one, the root command's arguments first and then each subcommand's, depth first, each command's arguments in spec order. | Proved | proved | src/LAWS.bend env_names_root; src/LAWS.bend env_names_forest; src/LAWS.bend env_names_some; src/LAWS.bend env_names_none |
 
 ## Left to prove
 
@@ -100,3 +108,4 @@ These assumptions sit outside the proofs. They are the complete list of Trusted
 | 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. |
+| SHAKE-TRUST-5 | `env_vars(spec)` answers, for each name it asks for (SHAKE-ARGS-2) and in that order, the pair of the name and the value `IO.get_env` answers for it, unchanged and empty included, and no pair for a name `IO.get_env` fails for. A program compiled by bend 2.0.34 answers `getenv`'s value for a variable that is set and fails for one that is not. | It is IO, which no law can reach: `env_vars` in `src/args.bend` is one `IO.bind` of `IO.get_env` per name, short enough to check by reading and marked `# noqa: L001`. What `IO.get_env` answers is `io_get_env_run` in bend2/effs/get_env.c, read from bend 2.0.34's source; every bend bump rechecks it, as for SHAKE-TRUST-2. |