feat!: bend 2.0.34, argv drops the program name, --help asks for help - #49
Merged
Merged
Conversation
Bend 2.0.32 puts the program as invoked first in IO.args, so argv now drops that word (args.words) and every Shake.argv() caller still gets just the arguments; SHAKE-ARGS-1 gains words_keeps. Compiled binaries pass --help through since 2.0.29, and shake now reads a bare --help, before -- and before any positional of the current command is bound, as a request for help exactly like `help` (SHAKE-PARSE-8, laws dash_help_step and dash_help_path). A command that declares its own long `help` keeps it: the help request only takes an unknown --help, so check reports nothing new. The proofs port to the new String.eq (Cmp.is_eq of String.order), SPEC's trust rows restate bend 2.0.34's C main and the ALL PROOFS CHECK gate, and the flake pins bend 2.0.34 with a proofs check that runs PROOF.bend on it, ez pinned to its own bend 2.0.31. bolt moves to v1.9.0, since v1.8.0 does not build on that bend. BREAKING CHANGE: shake needs bend 2.0.32 or later: argv() drops the first word of IO.args, which on older bend is a real argument. A bare --help is now a request for help (help_path is Some) instead of an UnknownFlag error. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Ports shake to bend 2.0.34.
IO.args.argv()now drops it (src/args.bendwords), soShake.argv()callers still get just the arguments. SHAKE-ARGS-1 gainswords_keeps; SHAKE-TRUST-2 restates bend 2.0.34's Cmain(runtime takes--threads/--gpu+ value, exits on--bend-help/--gpu-build, takes the first--;--helpnow reaches the program); SHAKE-TRUST-4 nameswords.--help, before--and before any positional of the current command is bound, is a request for help likehelp(SHAKE-PARSE-8; new lawsdash_help_step,dash_help_path). A command that declares its own longhelpkeeps it, since only an unknown--helpasks for help, socheckreports nothing new.unknown_long*laws gain the premise that the word is not such a--help(SHAKE-TOK-7 says so).string_eq_selfre-proved againstString.eq = Cmp.is_eq(String.order(..))(String.eq.fin is gone). The walker invariants (gw/gv/gn/nd/nu) cover the newtake_long.found/take_long.helpsteps.proofsrunCommand that requiresALL PROOFS CHECKin place ofez.mkProofs. bolt[tools.bolt]moves v1.8.0 → v1.9.0, because v1.8.0 no longer builds on ez's bend (duplicate declaration: Set).Shake.argv(), with a note that code passingIO.args()straight toparsemust drop the first word on bend ≥ 2.0.32; the runtime section is updated for 2.0.34.bend src/PROOF.bend→ALL PROOFS CHECK;nix flake checkpasses (demo, proofs, lint clean).BREAKING CHANGE: needs bend 2.0.32+;
--helpis now a help request.🤖 Generated with Claude Code