From 244ace87c3ffb19f3180eac9292e47ef74f69a2d Mon Sep 17 00:00:00 2001
From: qwjyh <urataw421@gmail.com>
Date: Wed, 23 Oct 2024 14:31:20 +0900
Subject: [PATCH] argument for starting directory (completed)

---
 Doug/Basic.lean | 17 ++++++++++++++---
 lakefile.lean   |  1 -
 2 files changed, 14 insertions(+), 4 deletions(-)

diff --git a/Doug/Basic.lean b/Doug/Basic.lean
index 55de2b5..4ba3324 100644
--- a/Doug/Basic.lean
+++ b/Doug/Basic.lean
@@ -3,7 +3,9 @@ def hello := "world"
 structure Config where
   useASCII : Bool := false
   printAll : Bool := false
+  rootPath : System.FilePath := "."
   currentPrefix : String := ""
+deriving Repr
 
 abbrev ConfigIO (α : Type) : Type := ReaderT Config IO α
 
@@ -29,7 +31,11 @@ def configFromArgs (args : List String) : Option Config :=
     match arg with
     | "--ascii" => some {cfg with useASCII := true}
     | "-a" => some {cfg with printAll := true}
-    | _ => none
+    | path =>
+      if path.startsWith "-" then
+        none
+      else
+        some {cfg with rootPath := path}
   args.foldlM parse_arg {}
 
 inductive Entry where
@@ -84,8 +90,13 @@ partial def dirTree (path : System.FilePath) : ConfigIO Unit := do
 def main (args : List String) : IO UInt32 := do
   match configFromArgs args with
   | some config =>
-    (dirTree (← IO.currentDir)).run config
-    pure 0
+    if ← config.rootPath.pathExists then
+      (dirTree (← IO.FS.realPath config.rootPath)).run config
+      IO.println s!"config {repr config}"
+      pure 0
+    else
+      IO.eprintln s!"Path doesn't exist {config.rootPath}"
+      pure 1
   | none =>
     IO.eprintln s!"Didn't understand argument(s) {" ".intercalate args}\n"
     IO.eprintln usage
diff --git a/lakefile.lean b/lakefile.lean
index 8289cfc..3cf731e 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -24,7 +24,6 @@ script test (args) do
   let proc ← IO.Process.spawn
     ⟨{stdin := .inherit, stdout := .piped, stderr := .piped},
       exe.toString, args.toArray, none, #[], false ⟩
-  IO.println s!"{← proc.tryWait}"
   IO.print (← proc.stdout.readToEnd)
   IO.eprintln (← IO.FS.Handle.readToEnd proc.stderr)
   let ret ← proc.wait