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