Tracking issue for the next time bolt bumps shake past v0.1.1. This is WP8 of shake's docs/rfc/shake-walker-proofs.md; REVIEW-W2 there was approved. It needs a shake release pinned in ez.toml: the refactor is still landing on shake's main, and the maintainer plans to publish to bendhub when it is done.
1. Delete the walker lemmas shake now proves
bolt proved lemmas about shake's walker in bolt/PROOF.bend (the cli.* block, lines ~1299–1990 at 38da7d9). shake now carries them, generalized, in src/walk.bend (prefix wk.), inside its own proof gate.
In shake, same name: false_true, true_false, nor_l, nor_r, not_true, and_l, and_r, and_true, none_of, dash.if, dash, plain_dd, plain_help, plain_dash, word_step, walk_plain, walk_raw.
Covered by other shake laws:
walk_dead → shake's dead_walk and fail_stays (SHAKE-PARSE-9).
bolt-specific, so they stay or are restated against bolt's spec: append_nil, append_one, walk_help, rev_pushed, no_version, files_back, files_out, unfound_nil, loose_plain, miss3, loose_unfound, sub_plain, err_stop.
sub_plain and walk_help state walker states directly (Shake.St{...}). The walker's shape changed, so they have to be restated. The new shape is in section 3; they may be derivable from shake's wk.walk_plain and PARSE-8 once those rows land.
2. Narrow BOLT-TRUST-8
BOLT-TRUST-8 currently trusts "shake v0.1.1 parses argv as its spec says" as a whole. After the bump:
- rows shake proves at the pinned version are cited, not trusted;
- the row lists only the SHAKE rows still pending at that version.
At shake main today:
- proved: SHAKE-TOK-4, TOK-6, PARSE-9, GET-1, GET-2, ERR-1, ARGS-1;
- pending with partial laws: SHAKE-TOK-1, TOK-5, TOK-7, PARSE-2, PARSE-5, PARSE-8, PARSE-10.
See shake's SPEC.md "Left to prove" for exactly what each pending row still misses. bolt's CLI rows lean mostly on PARSE-2 and PARSE-3 (the files rest positional).
3. Breaking API changes to adapt to
- Constructors and errors.
- Import shake's
main.bend only; shake/main.bend moved to src/.
ParseErr constructors are no longer matchable from outside. asks_help becomes Shake.help_path(ee), which is Some{path} exactly for a request for help (SHAKE-ERR-1).
- Every error but
NeedHelp now carries at.
get answers Maybe<String> (REVIEW-11).
- Bindings are per command, as in clap (REVIEW-16).
Matched is read one command at a time.
get, get_all and on on the root's Matched read only the root's bindings.
- So
cli_runs' Shake.get_all(mm, "files") would miss lint's and check's files. Read the selected command's own Matched instead: Shake.at(mm, Shake.path_of(mm)), or Shake.sub_of(mm, "lint").
on(mm, "version") reads the root's flag only, which is where bolt declares it.
- A flag or
opt option given twice in one command is refused with Repeated. An option meant to repeat is built with many (REVIEW-4, reversed).
- Short options cluster (REVIEW-14), and
-n=v drops the = (REVIEW-5, reversed).
- Walker internals changed.
St's specs field is now up: List<Level>: the commands above the current one, nearest first, each with its own arguments and bindings. Matched is Leaf{binds} / Node{binds, name, sub}.
All of these are on shake's main since b93357a. Each decision is recorded in shake's docs/rfc/shake-spec.md, under "Decided behavior changes" and the REVIEW items.
Tracking issue for the next time bolt bumps shake past v0.1.1. This is WP8 of shake's
docs/rfc/shake-walker-proofs.md; REVIEW-W2 there was approved. It needs a shake release pinned inez.toml: the refactor is still landing on shake'smain, and the maintainer plans to publish to bendhub when it is done.1. Delete the walker lemmas shake now proves
bolt proved lemmas about shake's walker in
bolt/PROOF.bend(thecli.*block, lines ~1299–1990 at38da7d9). shake now carries them, generalized, insrc/walk.bend(prefixwk.), inside its own proof gate.In shake, same name:
false_true,true_false,nor_l,nor_r,not_true,and_l,and_r,and_true,none_of,dash.if,dash,plain_dd,plain_help,plain_dash,word_step,walk_plain,walk_raw.Covered by other shake laws:
walk_dead→ shake'sdead_walkandfail_stays(SHAKE-PARSE-9).bolt-specific, so they stay or are restated against bolt's spec:
append_nil,append_one,walk_help,rev_pushed,no_version,files_back,files_out,unfound_nil,loose_plain,miss3,loose_unfound,sub_plain,err_stop.sub_plainandwalk_helpstate walker states directly (Shake.St{...}). The walker's shape changed, so they have to be restated. The new shape is in section 3; they may be derivable from shake'swk.walk_plainand PARSE-8 once those rows land.2. Narrow BOLT-TRUST-8
BOLT-TRUST-8 currently trusts "shake v0.1.1 parses argv as its spec says" as a whole. After the bump:
At shake
maintoday:See shake's
SPEC.md"Left to prove" for exactly what each pending row still misses. bolt's CLI rows lean mostly on PARSE-2 and PARSE-3 (thefilesrest positional).3. Breaking API changes to adapt to
main.bendonly;shake/main.bendmoved tosrc/.ParseErrconstructors are no longer matchable from outside.asks_helpbecomesShake.help_path(ee), which isSome{path}exactly for a request for help (SHAKE-ERR-1).NeedHelpnow carriesat.getanswersMaybe<String>(REVIEW-11).Matchedis read one command at a time.get,get_allandonon the root'sMatchedread only the root's bindings.cli_runs'Shake.get_all(mm, "files")would misslint's andcheck's files. Read the selected command's ownMatchedinstead:Shake.at(mm, Shake.path_of(mm)), orShake.sub_of(mm, "lint").on(mm, "version")reads the root's flag only, which is where bolt declares it.optoption given twice in one command is refused withRepeated. An option meant to repeat is built withmany(REVIEW-4, reversed).-n=vdrops the=(REVIEW-5, reversed).St'sspecsfield is nowup: List<Level>: the commands above the current one, nearest first, each with its own arguments and bindings.MatchedisLeaf{binds}/Node{binds, name, sub}.All of these are on shake's
mainsinceb93357a. Each decision is recorded in shake'sdocs/rfc/shake-spec.md, under "Decided behavior changes" and the REVIEW items.