feat: set up a subproject with a database in it for building docs

Author: david-christiansen

lake-manifest.json

@@ -1,7 +1,17 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/plausible",
+ [{"url": "https://github.com/leanprover/doc-gen4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "f178e492e7f345d7be5a57d2178e95f7a3cc070b",
+   "name": "«doc-gen4»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "",
@@ -30,6 +40,46 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": false,
-   "configFile": "lakefile.lean"}],
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/david-christiansen/leansqlite",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "739abe6c8ae0602d6ce56461d33f3e49837c9b70",
+   "name": "leansqlite",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "474983579ecce1ca7d8a63e65c7ae0b1a22db6a3",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "9484dd63d30bce157c7f98007a9f26ca4dfb7fb6",
+   "name": "UnicodeBasic",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/dupuisf/BibtexQuery",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "29e7df238aa51dba17463e360e68657a8d433f43",
+   "name": "BibtexQuery",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
  "name": "verso",
  "lakeDir": ".lake"}

lakefile.lean

@@ -4,6 +4,7 @@ open Lake DSL
 require subverso from git "https://github.com/leanprover/subverso"@"main"
 require MD4Lean from git "https://github.com/acmepjz/md4lean"@"main"
 require plausible from git "https://github.com/leanprover-community/plausible"@"main"
+require «doc-gen4» from git "https://github.com/leanprover/doc-gen4"@"main"
 
 package verso where
   precompileModules := false -- temporarily disabled to work around an issue with nightly-2025-03-30
@@ -197,3 +198,40 @@ package_facet literate pkg : Array System.FilePath := do
   let libs := Job.collectArray (← pkg.leanLibs.mapM (·.facet `literate |>.fetch))
   let exes := Job.collectArray (← pkg.leanExes.mapM (·.toLeanLib.facet `literate |>.fetch))
   return libs.zipWith (·.flatten ++ ·.flatten) exes
+
+lean_exe «verso-docgen-setup» where
+  root := `VersoManual.DB.Setup
+  srcDir := "src/verso-manual"
+  supportInterpreter := true
+
+package_facet docSource pkg : System.FilePath := do
+  let ws ← getWorkspace
+  let exeJob ← «verso-docgen-setup».fetch
+
+  let pkgDir := ws.root.dir
+  let buildDir := ws.root.buildDir
+  let tomlPath := pkgDir / "doc-sources.toml"
+  let wsDir := buildDir / "verso-doc-db"
+  let dbPath := wsDir / ".lake" / "build" / "api-docs.db"
+
+  let docgen4Dir := match ws.findPackageByName? `«doc-gen4» with
+    | some pkg => pkg.dir
+    | none => buildDir / ".." / "packages" / "doc-gen4"
+
+  exeJob.mapM fun exeFile => do
+    -- Add trace for the TOML config file so changes trigger rebuild
+    if ← tomlPath.pathExists then
+      addTrace (← fetchFileTrace tomlPath (text := true))
+
+    buildFileUnlessUpToDate' dbPath do
+      let args :=
+        if ← tomlPath.pathExists then
+          #[wsDir.toString, docgen4Dir.toString, pkgDir.toString, tomlPath.toString]
+        else
+          #[wsDir.toString, docgen4Dir.toString, pkgDir.toString]
+      proc {
+        cmd := exeFile.toString
+        args
+      }
+
+    pure dbPath

src/tests/TestMain.lean

@@ -153,6 +153,11 @@ def testBlog (_ : Config) : IO Unit := do
   if fails > 0 then
     throw <| .userError s!"{fails} blog tests failed"
 
+def testDocSourceConfig (_ : Config) : IO Unit := do
+  let fails ← runDocSourceConfigTests
+  if fails > 0 then
+    throw <| .userError s!"{fails} doc source config tests failed"
+
 -- Interactive tests via the LSP server
 def testInteractive (_ : Config) : IO Unit := do
   IO.println "Running interactive (LSP) tests..."
@@ -167,6 +172,7 @@ open Verso.Integration in
 def tests := [
   testSerialization,
   testBlog,
+  testDocSourceConfig,
   testStemmer,
   testTexOutput "sample-doc" SampleDoc.doc,
   testTexOutput "inheritance-doc" InheritanceDoc.doc,

src/tests/Tests.lean

@@ -31,3 +31,4 @@ import Tests.VersoBlog
 import Tests.VersoManual
 import Tests.Z85
 import Tests.Zip
+import Tests.DocSourceConfig