Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Options: print the option's help when arguments are wrong #3649

Merged
merged 2 commits into from
Jan 5, 2025
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 7 additions & 7 deletions ocaml/fstar-lib/FStarC_Getopt.ml
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ type opt = unit opt'
type parse_cmdline_res =
| Empty
| Help
| Error of string
| Error of (string * string)
| Success

let bind l f =
Expand Down Expand Up @@ -46,17 +46,17 @@ let rec parse (opts:opt list) def ar ix max i : parse_cmdline_res =
let go_on () = bind (def arg) (fun _ -> parse opts def ar (ix + 1) max (i + 1)) in
match find_matching_opt opts arg with
| None -> go_on ()
| Some (None, _) -> Error ("unrecognized option '" ^ arg ^ "'\n")
| Some (Some (_, _, p), argtrim) ->
| Some (None, _) -> Error ("unrecognized option '" ^ arg ^ "'\n", arg)
| Some (Some (_, opt, p), argtrim) ->
begin match p with
| ZeroArgs f -> f (); parse opts def ar (ix + 1) max (i + 1)
| OneArg (f, _) ->
| OneArg (f, name) ->
if ix + 1 > max
then Error ("last option '" ^ argtrim ^ "' takes an argument but has none\n")
then Error ("last option '" ^ argtrim ^ "' takes an argument but has none\n", opt)
else
let r =
try (f (ar.(ix + 1)); Success)
with _ -> Error ("wrong argument given to option `" ^ argtrim ^ "`\n")
with _ -> Error ("wrong argument given to option `" ^ argtrim ^ "`\n", opt)
in bind r (fun () -> parse opts def ar (ix + 2) max (i + 1))
end

Expand Down Expand Up @@ -97,7 +97,7 @@ let parse_string specs others (str:string) =

in
match split_quoted_fragments str with
| None -> Error("Failed to parse options; unmatched quote \"'\"")
| None -> Error("Failed to parse options; unmatched quote \"'\"", "")
| Some args ->
parse_array specs others (Array.of_list args) 0

Expand Down
4 changes: 2 additions & 2 deletions ocaml/fstar-lib/generated/FStarC_Errors.ml

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion ocaml/fstar-lib/generated/FStarC_Interactive_Ide.ml

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

13 changes: 11 additions & 2 deletions ocaml/fstar-lib/generated/FStarC_Main.ml

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

166 changes: 90 additions & 76 deletions ocaml/fstar-lib/generated/FStarC_Options.ml

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

11 changes: 8 additions & 3 deletions ocaml/fstar-lib/generated/FStarC_Syntax_Util.ml

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion ocaml/fstar-lib/generated/FStarC_Tactics_V1_Basic.ml

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion ocaml/fstar-lib/generated/FStarC_Tactics_V2_Basic.ml

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion ocaml/fstar-tests/generated/FStarC_Tests_Test.ml

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion src/basic/FStarC.Errors.fst
Original file line number Diff line number Diff line change
Expand Up @@ -436,7 +436,7 @@ let t_set_parse_warn_error,
Getopt.Success
with Invalid_warn_error_setting msg ->
(BU.smap_add error_flags we None;
Getopt.Error ("Invalid --warn_error setting: " ^ msg ^ "\n"))
Getopt.Error ("Invalid --warn_error setting: " ^ msg ^ "\n", "warn_error"))
in
(* get_error_flags is called when logging an issue to figure out
which error level to report a particular issue at (Warning, Error etc.)
Expand Down
2 changes: 1 addition & 1 deletion src/basic/FStarC.Getopt.fsti
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ type opt = opt' unit
type parse_cmdline_res =
| Empty
| Help
| Error of string
| Error of (string & string) // second arg is the long name of the failed option
| Success

val parse_cmdline: list opt -> (string -> parse_cmdline_res) -> parse_cmdline_res
Expand Down
Loading
Loading