Merge pull request #53 from Seasawher/Seasawher/issue32

use Cli tool for Lean

Mdgen.lean

@@ -1 +1,5 @@
-import Mdgen.Main
+import Mdgen.Cli
+
+
+def main (args : List String) : IO UInt32 :=
+  mkMdgenCmd.validate args

Mdgen/Cli.lean

@@ -0,0 +1,32 @@
+import Mdgen.File
+import Mdgen.ConvertToMd
+import Cli
+
+open Cli System
+
+def runMdgenCmd (p : Parsed) : IO UInt32 := do
+  let inputDir : FilePath := p.positionalArg! "input_dir" |>.as! String
+  let outputDir : FilePath := p.positionalArg! "output_dir" |>.as! String
+
+  let paths ← getLeanFilePaths inputDir
+
+  for path in paths do
+    let mut content ← IO.FS.lines path
+    content := content.map (fun line => line.replace "\r" "")
+
+    let outputFilePath := outputFilePath
+      inputDir.components
+      outputDir.components
+      path.components
+
+    createFile (genPath outputFilePath) (convertToMd content.toList)
+  return 0
+
+def mkMdgenCmd : Cmd := `[Cli|
+  mkMdgenCmd VIA runMdgenCmd; ["1.4.0"]
+  "mdgen is a tool to generate .md files from .lean files."
+
+  ARGS:
+    input_dir : String; "The directory containing the input Lean files."
+    output_dir : String; "The directory to write the markdown files."
+]

Mdgen/File.lean

@@ -23,3 +23,17 @@ def genPath (l : List String) : FilePath :=
     |> List.foldl (· ++ ·) ""
     |> (String.dropRight · 1)
     |> FilePath.mk
+
+partial def getLeanFilePaths (fp : FilePath) (acc : Array FilePath := #[]) :
+    IO $ Array FilePath := do
+  if ← fp.isDir then
+    (← fp.readDir).foldlM (fun acc dir => getLeanFilePaths dir.path acc) acc
+  else return if fp.extension == some "lean" then acc.push fp else acc
+
+/-- create a file with given path and content. -/
+def createFile (path : FilePath) (content : String) : IO Unit := do
+  match path.parent with
+  | none => IO.FS.writeFile path content
+  | some parent =>
+    IO.FS.createDirAll parent
+    IO.FS.writeFile path content

lake-manifest.json

@@ -1,5 +1,15 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
- "packages": [],
+ "packages":
+ [{"url": "https://github.com/leanprover/lean4-cli.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.toml"}],
  "name": "mdgen",
  "lakeDir": ".lake"}

lakefile.lean

@@ -13,6 +13,9 @@ lean_lib «Mdgen» where
   -- add library configuration options here
   globs := #[.submodules `Mdgen]
 
+require Cli from git
+  "https://github.com/leanprover/lean4-cli.git" @ "main"
+
 lean_exe «mdgen» where
   root := `Mdgen