Merge pull request #74 from tydeu/docs-facet

feat:  experimental module facet for producing docs

DocGen4/Process/Hierarchy.lean

@@ -99,21 +99,24 @@ def baseDirBlackList : HashSet String :=
     "style.css"
   ]
 
-
 partial def fromDirectoryAux (dir : System.FilePath) (previous : Name) : IO (Array Name) := do
   let mut children := #[]
   for entry in ←System.FilePath.readDir dir do
     if (←entry.path.isDir) then
       children := children ++ (←fromDirectoryAux entry.path (.str previous entry.fileName))
-    else
+    else if entry.path.extension = some "html" then
       children := children.push <| .str previous (entry.fileName.dropRight ".html".length)
   pure children
 
 def fromDirectory (dir : System.FilePath) : IO Hierarchy := do
     let mut children := #[]
     for entry in ←System.FilePath.readDir dir do
-      if !baseDirBlackList.contains entry.fileName && (←entry.path.isDir) then
+      if baseDirBlackList.contains entry.fileName then
+        continue
+      else if ←entry.path.isDir then
         children := children ++ (←fromDirectoryAux entry.path (.mkSimple entry.fileName))
+      else if entry.path.extension = some "html" then
+        children := children.push <| .mkSimple (entry.fileName.dropRight ".html".length)
     pure <| Hierarchy.fromArray children
 
 end Hierarchy

lakefile.lean

@@ -1,5 +1,6 @@
 import Lake
-open Lake DSL
+import Lake.CLI.Main
+open System Lake DSL
 
 package «doc-gen4»
 
@@ -25,3 +26,22 @@ require lake from git
 
 require leanInk from git
   "https://github.com/hargonix/LeanInk" @ "doc-gen"
+
+module_facet docs : FilePath := fun mod => do
+  let some docGen4 ← findLeanExe? `«doc-gen4»
+    | error "no doc-gen4 executable configuration found in workspace"
+  let exeTarget ← docGen4.exe.recBuild
+  let modTarget ← mod.leanBin.recBuild
+  let buildDir := (← getWorkspace).root.buildDir
+  let docFile := mod.filePath (buildDir / "doc") "html"
+  let task ← show SchedulerM _ from do
+    exeTarget.bindAsync fun exeFile exeTrace => do
+    modTarget.bindSync fun _ modTrace => do
+      let depTrace := exeTrace.mix modTrace
+      buildFileUnlessUpToDate docFile depTrace do
+        proc {
+          cmd := exeFile.toString
+          args := #["single", mod.name.toString]
+          env := #[("LEAN_PATH", (← getAugmentedLeanPath).toString)]
+        }
+  return ActiveTarget.mk docFile task