fix: test vector help text (aws#657)

lucasmcdonald3 · Oct 1, 2024 · 32d5d57 · 32d5d57
1 parent a86a193
commit 32d5d57
Show file tree

Hide file tree

Showing 3 changed files with 25 additions and 11 deletions.
diff --git a/Makefile b/Makefile
@@ -5,7 +5,7 @@ PROJECT_ROOT := $(abspath $(dir $(abspath $(lastword $(MAKEFILE_LIST)))))
 
 # This finds all Dafny projects in this repository
 # This makes building root level targets for each project easy
-PROJECTS = $(shell  find . -mindepth 2 -maxdepth 2 -type f -name "Makefile" | xargs dirname | xargs basename)
+PROJECTS = $(shell  find . -mindepth 2 -maxdepth 2 -type f -name "Makefile" | fgrep -v smithy-dafny | xargs dirname | xargs basename)
 
 verify:
 	$(foreach PROJECT, $(PROJECTS), \

diff --git a/StandardLibrary/src/GetOpt.dfy b/StandardLibrary/src/GetOpt.dfy
@@ -241,9 +241,15 @@ module {:options "-functionSyntax:4"} GetOpt {
     }
   }
 
+  predicate IsHelp(args : Parsed)
+  {
+    && |args.params| != 0
+    && args.params[0].name == HELP_STR
+  }
+
   function {:tailrecursion} NeedsHelp(opts : Options, args : Parsed, prefix : string := "") : Option<string>
   {
-    if |args.params| != 0 && args.params[0].name == HELP_STR then
+    if IsHelp(args) then
       Some(GetHelp(opts, prefix))
     else if args.subcommand.Some? then
       var pos :- GetSubOptions(opts.params, args.subcommand.value.command);
@@ -613,16 +619,19 @@ module {:options "-functionSyntax:4"} GetOpt {
 
   function /*{:tailrecursion}*/ PostProcess(opts : Options, args : Parsed) : Result<Parsed, string>
   {
-    var newParams :- PostProcess2(opts.params, args.params);
-    if args.subcommand.Some? then
-      var optPos := GetSubOptions(opts.params, args.subcommand.value.command);
-      if optPos.Some? then
-        var sub :- PostProcess(opts.params[optPos.value].options, args.subcommand.value);
-        Success(args.(params := args.params + newParams, subcommand := Some(sub)))
-      else
-        Failure("Internal error in GetOpt::PostProcess")
+    if IsHelp(args) then
+      Success(args)
     else
-      Success(args.(params := args.params + newParams))
+      var newParams :- PostProcess2(opts.params, args.params);
+      if args.subcommand.Some? then
+        var optPos := GetSubOptions(opts.params, args.subcommand.value.command);
+        if optPos.Some? then
+          var sub :- PostProcess(opts.params[optPos.value].options, args.subcommand.value);
+          Success(args.(params := args.params + newParams, subcommand := Some(sub)))
+        else
+          Failure("Internal error in GetOpt::PostProcess")
+      else
+        Success(args.(params := args.params + newParams))
   }
 
   predicate AllDigits(s : string)

diff --git a/...graphicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/Index.dfy b/...graphicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/Index.dfy
@@ -39,6 +39,11 @@ module {:options "-functionSyntax:4"} WrappedMaterialProvidersMain {
     var parsedOptions? := GetOptions(vectorOptions, args);
 
     if parsedOptions?.Success? {
+      var h := NeedsHelp(vectorOptions, parsedOptions?.value);
+      if h.Some? {
+        print h.value;
+        return;
+      }
       var op? := ParseCommandLineOptions(parsedOptions?.value);
 
       if op?.Success? {