From 34d2239b68c948d8cc19a6cbd41c06b8b995930f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Wed, 23 Feb 2022 22:54:10 +0100
Subject: [PATCH] feat: actual CLI

---
 DocGen4/Load.lean |  8 ++++----
 Main.lean         | 28 +++++++++++++++++++---------
 lakefile.lean     |  4 ++++
 3 files changed, 27 insertions(+), 13 deletions(-)

diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean
index 20da38a..d220389 100644
--- a/DocGen4/Load.lean
+++ b/DocGen4/Load.lean
@@ -20,15 +20,15 @@ def getLakePath : IO FilePath := do
     pure $ lakePath.withExtension System.FilePath.exeExtension
 
 -- Modified from the LSP Server
-def lakeSetupSearchPath (lakePath : System.FilePath) (imports : Array String) : IO Lean.SearchPath := do
-  let args := #["print-paths"] ++ imports
-  let cmdStr := " ".intercalate (toString lakePath :: args.toList)
+def lakeSetupSearchPath (lakePath : System.FilePath) (imports : List String) : IO Lean.SearchPath := do
+  let args := "print-paths" :: imports
+  let cmdStr := " ".intercalate (toString lakePath :: args)
   let lakeProc ← Process.spawn {
     stdin  := Process.Stdio.null
     stdout := Process.Stdio.piped
     stderr := Process.Stdio.piped
     cmd    := lakePath.toString
-    args
+    args := args.toArray
   }
   let stdout := String.trim (← lakeProc.stdout.readToEnd)
   let stderr := String.trim (← lakeProc.stderr.readToEnd)
diff --git a/Main.lean b/Main.lean
index 13e530b..4a7c71d 100644
--- a/Main.lean
+++ b/Main.lean
@@ -1,17 +1,27 @@
 import DocGen4
 import Lean
+import Cli
 
-open DocGen4 Lean IO
+open DocGen4 Lean Cli
 
-def main (args : List String) : IO Unit := do
-  if args.isEmpty then
-    IO.println "Usage: doc-gen4 root/url/ Module1 Module2 ..."
-    IO.Process.exit 1
-    return
-  let root := args.head!
-  let modules := args.tail!
-  let path ← lakeSetupSearchPath (←getLakePath) modules.toArray
+def runDocGenCmd (p : Parsed) : IO UInt32 := do
+  let root := p.positionalArg! "root" |>.as! String
+  let modules : List String := p.variableArgsAs! String |>.toList
+  let path ← lakeSetupSearchPath (←getLakePath) modules
   IO.println s!"Loading modules from: {path}"
   let doc ← load $ modules.map Name.mkSimple
   IO.println "Outputting HTML"
   htmlOutput doc root
+  pure 0
+
+def docGenCmd : Cmd := `[Cli|
+  "doc-gen4" VIA runDocGenCmd; ["0.0.1"]
+  "A documentation generator for Lean 4."
+
+  ARGS:
+    root : String; "The root URL to generate the HTML for (will be relative in the future)"
+    ...modules : String; "The modules to generate the HTML for"
+]
+
+def main (args : List String) : IO UInt32 :=
+  docGenCmd.validate args
diff --git a/lakefile.lean b/lakefile.lean
index cc8dd0e..9d9c138 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -12,6 +12,10 @@ package «doc-gen4» {
     {
       name := `Unicode
       src := Source.git "https://github.com/xubaiw/Unicode.lean" "3b7b85472d42854a474099928a3423bb97d4fa64"
+    },
+    {
+      name := `Cli
+      src := Source.git "https://github.com/mhuisi/lean4-cli" "1f8663e3dafdcc11ff476d74ef9b99ae5bdaedd3"
     }
   ]
 }