From ba756ccba2760e6766a53ea866c44301a72099db Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Sun, 1 Sep 2024 10:16:36 -0400
Subject: [PATCH] fix: test vector help text

---
 Makefile                                      |  2 +-
 StandardLibrary/src/GetOpt.dfy                | 29 ++++++++++++-------
 .../src/Index.dfy                             |  5 ++++
 3 files changed, 25 insertions(+), 11 deletions(-)

diff --git a/Makefile b/Makefile
index 64c691472..8e3cacb2c 100644
--- 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
index 74c21ddf2..54f344f60 100644
--- 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/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/Index.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/Index.dfy
index 542c4f689..90c8e961e 100644
--- a/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/Index.dfy
+++ b/TestVectorsAwsCryptographicMaterialProviders/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? {