From 5e78890ec03678ee494b3eb705220a97cc45013e Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Sat, 23 Jul 2022 20:07:30 -0400
Subject: [PATCH] feat:  experimental module facet for producing docs

---
 lakefile.lean | 22 +++++++++++++++++++++-
 1 file changed, 21 insertions(+), 1 deletion(-)

diff --git a/lakefile.lean b/lakefile.lean
index c72a90d..6a1cd23 100644
--- a/lakefile.lean
+++ b/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