Add comprehensive help text for pyAnalyze and pyAnalyzeLaurel commands

StrataMain.lean

@@ -244,10 +244,16 @@ def tryReadPythonSource (ionPath : String) : IO (Option (String × Lean.FileMap)
 
 def pyAnalyzeCommand : Command where
   name := "pyAnalyze"
-  args := [ "file", "verbose" ]
-  help := "Analyze a Strata Python Ion file. Write results to stdout."
+  args := [ "ion_file", "verbose" ]
+  help := "Verify `assert` and `cover` commands in a Strata Python Ion file after inlining procedure calls. " ++
+          "<ion_file>: path to a .python.st.ion file generated from Python source. " ++
+          "<verbose>: set to '1' for verbose output (displays parsed program, Core translation, and inlined program), or '0' for concise verification results only."
   callback := fun _ v => do
-    let verbose := v[1] == "1"
+    let verbose ←
+      match v[1] with
+      | "0" => pure false
+      | "1" => pure true
+      | other => exitFailure ("Invalid value for <verbose>: " ++ other ++ ". Expected '0' or '1'.")
     let filePath := v[0]
     let pgm ← readPythonStrata filePath
     -- Try to read the Python source for line number conversion
@@ -322,10 +328,16 @@ def pyAnalyzeCommand : Command where
 
 def pyAnalyzeLaurelCommand : Command where
   name := "pyAnalyzeLaurel"
-  args := [ "file", "verbose" ]
-  help := "Analyze a Strata Python Ion file through Laurel. Write results to stdout."
+  args := [ "ion_file", "verbose" ]
+  help := "Verify `assert` and `cover` commands in a Strata Python Ion file via the Laurel intermediate representation. " ++
+          "<ion_file>: path to a .python.st.ion file generated from Python source. " ++
+          "<verbose>: set to '1' for verbose output (displays parsed program, Laurel translation, Core translation, and verification details), or '0' for concise verification results only."
   callback := fun _ v => do
-    let verbose := v[1] == "1"
+    let verbose ←
+      match v[1] with
+      | "0" => pure false
+      | "1" => pure true
+      | other => exitFailure ("Invalid value for <verbose>: " ++ other ++ ". Expected '0' or '1'.")
     let filePath := v[0]
     let pgm ← readPythonStrata filePath
     let pySourceOpt ← tryReadPythonSource filePath
@@ -475,7 +487,8 @@ def main (args : List String) : IO Unit := do
     IO.println "Usage: strata <command> [flags]...\n"
     for cmd in commandList do
       let args := cmd.args.foldl (init := s!"  {cmd.name}") fun s a => s!"{s} <{a}>"
-      IO.println s!"  {args}: {cmd.help}"
+      IO.println s!"{args}"
+      IO.println s!"      {cmd.help}"
     IO.println "\nFlags:"
     IO.println "  --include path: Adds a path to Strata for searching for dialects."
   | cmd :: args =>