From 9b6ee093d87af9c65213c5fc1de582a628072c96 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 27 Feb 2026 12:03:22 +0100 Subject: [PATCH 1/2] feat: set up a subproject with a database in it for building docs --- lake-manifest.json | 54 ++- lakefile.lean | 38 +++ src/tests/TestMain.lean | 6 + src/tests/Tests.lean | 1 + src/tests/Tests/DocSourceConfig.lean | 361 ++++++++++++++++++++ src/verso-manual/VersoManual.lean | 1 + src/verso-manual/VersoManual/DB.lean | 6 + src/verso-manual/VersoManual/DB/Config.lean | 188 ++++++++++ src/verso-manual/VersoManual/DB/Setup.lean | 143 ++++++++ 9 files changed, 796 insertions(+), 2 deletions(-) create mode 100644 src/tests/Tests/DocSourceConfig.lean create mode 100644 src/verso-manual/VersoManual/DB.lean create mode 100644 src/verso-manual/VersoManual/DB/Config.lean create mode 100644 src/verso-manual/VersoManual/DB/Setup.lean diff --git a/lake-manifest.json b/lake-manifest.json index 03cf5b53..165aff77 100644 --- a/lake-manifest.json +++ b/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"} diff --git a/lakefile.lean b/lakefile.lean index dbedffd7..cde7862f 100644 --- a/lakefile.lean +++ b/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 diff --git a/src/tests/TestMain.lean b/src/tests/TestMain.lean index 22534291..a5434416 100644 --- a/src/tests/TestMain.lean +++ b/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, diff --git a/src/tests/Tests.lean b/src/tests/Tests.lean index 704aeeea..77d2d92f 100644 --- a/src/tests/Tests.lean +++ b/src/tests/Tests.lean @@ -31,3 +31,4 @@ import Tests.VersoBlog import Tests.VersoManual import Tests.Z85 import Tests.Zip +import Tests.DocSourceConfig diff --git a/src/tests/Tests/DocSourceConfig.lean b/src/tests/Tests/DocSourceConfig.lean new file mode 100644 index 00000000..2dd6aa5a --- /dev/null +++ b/src/tests/Tests/DocSourceConfig.lean @@ -0,0 +1,361 @@ +/- +Copyright (c) 2025-2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +import Lake.Toml +import VersoManual.DB.Config + +/-! # Tests for Doc Source Configuration Parsing + +Tests for `Verso.Genre.Manual.DocSource.Config` — TOML parsing and lakefile generation. +-/ + +open Verso.Genre.Manual.DocSource +open Lake.Toml + +/-- Parse a TOML string into a `Table`. Throws on parse error. -/ +private def parseToml (input : String) : IO Table := do + let ictx := Lean.Parser.mkInputContext input "" + match (← Lake.Toml.loadToml ictx |>.toBaseIO) with + | .ok table => pure table + | .error msgs => + let msgStrs ← msgs.toList.mapM fun msg => msg.data.toString + throw <| .userError s!"TOML parse error:\n{"\n".intercalate msgStrs}" + +/-- Assert that two values are equal, throwing a descriptive error if not. -/ +private def assertEqual [BEq α] [Repr α] (label : String) (expected actual : α) : IO Unit := do + unless expected == actual do + throw <| IO.userError s!"{label}: expected\n {repr expected}\nbut got\n {repr actual}" + +/-- Assert that a result is an error. -/ +private def assertError [Repr α] (label : String) (result : Except String α) : IO Unit := do + match result with + | .error _ => pure () + | .ok v => throw <| IO.userError s!"{label}: expected an error but got\n {repr v}" + +/-- Assert that a string contains a substring. -/ +private def assertContains (label : String) (haystack needle : String) : IO Unit := do + unless (haystack.splitOn needle).length > 1 do + throw <| IO.userError s!"{label}: expected string to contain '{needle}' but got:\n {haystack}" + +-- ============================================================================ +-- Config.ofToml tests +-- ============================================================================ + +private def testEmptyConfig : IO Unit := do + let table ← parseToml "" + let config ← IO.ofExcept <| Config.ofToml table + assertEqual "empty config require" #[] config.require + assertEqual "empty config libraries" #[] config.libraries + assertEqual "empty config setup" #[] config.setup + +private def testPathDependency : IO Unit := do + let table ← parseToml " +[[require]] +name = \"Batteries\" +path = \"../batteries\" +" + let config ← IO.ofExcept <| Config.ofToml table + assertEqual "path dep count" 1 config.require.size + let req := config.require[0]! + assertEqual "path dep name" "Batteries" req.name + assertEqual "path dep path" (some ⟨"../batteries"⟩) req.path + assertEqual "path dep git" none req.git + assertEqual "path dep rev" none req.rev + +private def testGitDependency : IO Unit := do + let table ← parseToml " +[[require]] +name = \"Mathlib\" +git = \"https://github.com/leanprover-community/mathlib4\" +rev = \"main\" +" + let config ← IO.ofExcept <| Config.ofToml table + assertEqual "git dep count" 1 config.require.size + let req := config.require[0]! + assertEqual "git dep name" "Mathlib" req.name + assertEqual "git dep git" (some "https://github.com/leanprover-community/mathlib4") req.git + assertEqual "git dep rev" (some "main") req.rev + assertEqual "git dep path" none req.path + +private def testGitDepWithSubDir : IO Unit := do + let table ← parseToml " +[[require]] +name = \"MyLib\" +git = \"https://github.com/example/monorepo\" +rev = \"v1.0\" +subDir = \"packages/mylib\" +" + let config ← IO.ofExcept <| Config.ofToml table + let req := config.require[0]! + assertEqual "subDir dep name" "MyLib" req.name + assertEqual "subDir dep subDir" (some "packages/mylib") req.subDir + +private def testMultipleRequires : IO Unit := do + let table ← parseToml " +[[require]] +name = \"Batteries\" +git = \"https://github.com/leanprover/batteries\" +rev = \"main\" + +[[require]] +name = \"Mathlib\" +git = \"https://github.com/leanprover-community/mathlib4\" +rev = \"main\" +" + let config ← IO.ofExcept <| Config.ofToml table + assertEqual "multi req count" 2 config.require.size + assertEqual "multi req first name" "Batteries" config.require[0]!.name + assertEqual "multi req second name" "Mathlib" config.require[1]!.name + +private def testLibrariesField : IO Unit := do + let table ← parseToml " +libraries = [\"Mathlib\", \"Batteries\"] + +[[require]] +name = \"Mathlib\" +git = \"https://github.com/leanprover-community/mathlib4\" +rev = \"main\" +" + let config ← IO.ofExcept <| Config.ofToml table + assertEqual "libraries" #["Mathlib", "Batteries"] config.libraries + +private def testSetupField : IO Unit := do + let table ← parseToml " +setup = [\"lake exe cache get\", \"lake build Foo\"] +" + let config ← IO.ofExcept <| Config.ofToml table + assertEqual "setup" #["lake exe cache get", "lake build Foo"] config.setup + +private def testFullConfig : IO Unit := do + let table ← parseToml " +setup = [\"lake exe cache get\"] +libraries = [\"Mathlib\"] + +[[require]] +name = \"Mathlib\" +git = \"https://github.com/leanprover-community/mathlib4\" +rev = \"main\" +" + let config ← IO.ofExcept <| Config.ofToml table + assertEqual "full config setup" #["lake exe cache get"] config.setup + assertEqual "full config libraries" #["Mathlib"] config.libraries + assertEqual "full config require count" 1 config.require.size + assertEqual "full config require name" "Mathlib" config.require[0]!.name + +private def testMissingName : IO Unit := do + let table ← parseToml " +[[require]] +git = \"https://github.com/example/lib\" +" + let result := Config.ofToml table + assertError "missing name" result + +private def testNoRequireEntries : IO Unit := do + let table ← parseToml " +libraries = [\"Init\"] +" + let config ← IO.ofExcept <| Config.ofToml table + assertEqual "no requires" #[] config.require + assertEqual "libraries only" #["Init"] config.libraries + +-- ============================================================================ +-- Lakefile generation tests +-- ============================================================================ + +private def testLakefileGenCoreOnly : IO Unit := do + let lakefile := generateLakefile none "/abs/path/to/doc-gen4" "/project" + assertContains "core-only header" lakefile "import Lake" + assertContains "core-only package" lakefile "package «docgen-workspace»" + assertContains "core-only docgen4" lakefile "require «doc-gen4» from \"/abs/path/to/doc-gen4\"" + -- Should not contain any user requires + let lines := lakefile.splitOn "\n" + let requireCount := lines.filter (·.startsWith "require") |>.length + -- Only the doc-gen4 require + assertEqual "core-only require count" 1 requireCount + +private def testLakefileGenGitDep : IO Unit := do + let config : Config := { + require := #[{ + name := "Mathlib" + git := some "https://github.com/leanprover-community/mathlib4" + rev := some "main" + }] + } + let lakefile := generateLakefile (some config) "/path/to/doc-gen4" "/project" + assertContains "git dep lakefile docgen4" lakefile "require «doc-gen4» from \"/path/to/doc-gen4\"" + assertContains "git dep lakefile Mathlib" lakefile "require «Mathlib» from git" + assertContains "git dep lakefile url" lakefile "\"https://github.com/leanprover-community/mathlib4\"" + assertContains "git dep lakefile rev" lakefile "@ \"main\"" + +private def testLakefileGenPathDep : IO Unit := do + let config : Config := { + require := #[{ + name := "Batteries" + path := some "../batteries" + }] + } + let lakefile := generateLakefile (some config) "/path/to/doc-gen4" "/project" + -- Path should be resolved to absolute + assertContains "path dep lakefile abs" lakefile "require «Batteries» from \"/project/../batteries\"" + +private def testLakefileGenAbsPathDep : IO Unit := do + let config : Config := { + require := #[{ + name := "Batteries" + path := some "/absolute/path/to/batteries" + }] + } + let lakefile := generateLakefile (some config) "/path/to/doc-gen4" "/project" + assertContains "abs path dep lakefile" lakefile "require «Batteries» from \"/absolute/path/to/batteries\"" + +private def testLakefileGenMultipleDeps : IO Unit := do + let config : Config := { + require := #[ + { name := "Batteries", git := some "https://github.com/leanprover/batteries", rev := some "main" }, + { name := "Mathlib", git := some "https://github.com/leanprover-community/mathlib4", rev := some "main" } + ] + } + let lakefile := generateLakefile (some config) "/path/to/doc-gen4" "/project" + assertContains "multi dep Batteries" lakefile "require «Batteries»" + assertContains "multi dep Mathlib" lakefile "require «Mathlib»" + +-- ============================================================================ +-- splitCommand tests +-- ============================================================================ + +private def testSplitSimple : IO Unit := do + assertEqual "simple" (some ("lake", #["exe", "cache", "get"])) (splitCommand "lake exe cache get") + +private def testSplitSingleArg : IO Unit := do + assertEqual "single arg" (some ("lake", #[])) (splitCommand "lake") + +private def testSplitEmpty : IO Unit := do + assertEqual "empty" none (splitCommand "") + +private def testSplitOnlySpaces : IO Unit := do + assertEqual "only spaces" none (splitCommand " ") + +private def testSplitLeadingTrailingSpaces : IO Unit := do + assertEqual "leading/trailing" (some ("lake", #["build"])) (splitCommand " lake build ") + +private def testSplitTabs : IO Unit := do + assertEqual "tabs" (some ("lake", #["build", "Foo"])) (splitCommand "lake\tbuild\tFoo") + +private def testSplitMixedWhitespace : IO Unit := do + assertEqual "mixed ws" (some ("lake", #["build"])) (splitCommand " \t lake \t build \t ") + +private def testSplitDoubleQuoted : IO Unit := do + assertEqual "double quoted" (some ("echo", #["hello world"])) (splitCommand "echo \"hello world\"") + +private def testSplitSingleQuoted : IO Unit := do + assertEqual "single quoted" (some ("echo", #["hello world"])) (splitCommand "echo 'hello world'") + +private def testSplitDoubleQuotedBackslash : IO Unit := do + assertEqual "dq backslash" (some ("echo", #["hello\"world"])) (splitCommand "echo \"hello\\\"world\"") + +private def testSplitDoubleQuotedBackslashN : IO Unit := do + assertEqual "dq backslash-n" (some ("echo", #["hellonworld"])) (splitCommand "echo \"hello\\nworld\"") + +private def testSplitSingleQuotedNoEscape : IO Unit := do + assertEqual "sq no escape" (some ("echo", #["hello\\nworld"])) (splitCommand "echo 'hello\\nworld'") + +private def testSplitEmptyDoubleQuotes : IO Unit := do + assertEqual "empty dq" (some ("echo", #[""])) (splitCommand "echo \"\"") + +private def testSplitEmptySingleQuotes : IO Unit := do + assertEqual "empty sq" (some ("echo", #[""])) (splitCommand "echo ''") + +private def testSplitQuotedConcat : IO Unit := do + -- "hello"' '"world" → hello world (quotes are just delimiters, adjacent runs concatenate) + assertEqual "quoted concat" (some ("echo", #["hello world"])) (splitCommand "echo \"hello\"' 'world") + +private def testSplitMixedQuotesInArg : IO Unit := do + assertEqual "mixed quotes" (some ("cmd", #["it's", "a \"test\""])) (splitCommand "cmd \"it's\" 'a \"test\"'") + +private def testSplitUnclosedDoubleQuote : IO Unit := do + -- Unmatched quote is treated as if closed at end of string + assertEqual "unclosed dq" (some ("echo", #["hello world"])) (splitCommand "echo \"hello world") + +private def testSplitUnclosedSingleQuote : IO Unit := do + assertEqual "unclosed sq" (some ("echo", #["hello world"])) (splitCommand "echo 'hello world") + +private def testSplitQuotedEmpty : IO Unit := do + -- Just a pair of quotes produces a single empty-string argument (the executable name) + assertEqual "just quotes" (some ("", #[])) (splitCommand "\"\"") + +private def testSplitBackslashInDoubleQuotes : IO Unit := do + -- Backslash at end of double-quoted string + assertEqual "trailing backslash in dq" (some ("echo", #["hello\\"])) (splitCommand "echo \"hello\\\\\"") + +private def testSplitMultipleQuotedArgs : IO Unit := do + assertEqual "multi quoted" (some ("cmd", #["arg one", "arg two", "three"])) (splitCommand "cmd 'arg one' \"arg two\" three") + +private def testSplitPathWithSpaces : IO Unit := do + assertEqual "path with spaces" (some ("cd", #["/path/to/my project"])) (splitCommand "cd '/path/to/my project'") + +private def testSplitConsecutiveSpaces : IO Unit := do + assertEqual "consecutive spaces" (some ("a", #["b", "c"])) (splitCommand "a b c") + +private def testSplitTabsAndSpaces : IO Unit := do + assertEqual "tabs and spaces" (some ("a", #["b"])) (splitCommand "\t a \t b \t") + +-- ============================================================================ +-- Test runner +-- ============================================================================ + +private def docSourceConfigTests : List (String × IO Unit) := [ + ("Config.ofToml: empty config", testEmptyConfig), + ("Config.ofToml: path dependency", testPathDependency), + ("Config.ofToml: git dependency", testGitDependency), + ("Config.ofToml: git dep with subDir", testGitDepWithSubDir), + ("Config.ofToml: multiple requires", testMultipleRequires), + ("Config.ofToml: libraries field", testLibrariesField), + ("Config.ofToml: setup field", testSetupField), + ("Config.ofToml: full config", testFullConfig), + ("Config.ofToml: missing name error", testMissingName), + ("Config.ofToml: no require entries", testNoRequireEntries), + ("generateLakefile: core-only", testLakefileGenCoreOnly), + ("generateLakefile: git dependency", testLakefileGenGitDep), + ("generateLakefile: path dependency (relative)", testLakefileGenPathDep), + ("generateLakefile: path dependency (absolute)", testLakefileGenAbsPathDep), + ("generateLakefile: multiple dependencies", testLakefileGenMultipleDeps), + ("splitCommand: simple", testSplitSimple), + ("splitCommand: single arg", testSplitSingleArg), + ("splitCommand: empty", testSplitEmpty), + ("splitCommand: only spaces", testSplitOnlySpaces), + ("splitCommand: leading/trailing spaces", testSplitLeadingTrailingSpaces), + ("splitCommand: tabs", testSplitTabs), + ("splitCommand: mixed whitespace", testSplitMixedWhitespace), + ("splitCommand: double quoted", testSplitDoubleQuoted), + ("splitCommand: single quoted", testSplitSingleQuoted), + ("splitCommand: dq backslash escape", testSplitDoubleQuotedBackslash), + ("splitCommand: dq backslash-n", testSplitDoubleQuotedBackslashN), + ("splitCommand: sq no escape", testSplitSingleQuotedNoEscape), + ("splitCommand: empty double quotes", testSplitEmptyDoubleQuotes), + ("splitCommand: empty single quotes", testSplitEmptySingleQuotes), + ("splitCommand: quoted concatenation", testSplitQuotedConcat), + ("splitCommand: mixed quotes in arg", testSplitMixedQuotesInArg), + ("splitCommand: unclosed double quote", testSplitUnclosedDoubleQuote), + ("splitCommand: unclosed single quote", testSplitUnclosedSingleQuote), + ("splitCommand: just quotes", testSplitQuotedEmpty), + ("splitCommand: backslash in double quotes", testSplitBackslashInDoubleQuotes), + ("splitCommand: multiple quoted args", testSplitMultipleQuotedArgs), + ("splitCommand: path with spaces", testSplitPathWithSpaces), + ("splitCommand: consecutive spaces", testSplitConsecutiveSpaces), + ("splitCommand: tabs and spaces", testSplitTabsAndSpaces), +] + +public def runDocSourceConfigTests : IO Nat := do + IO.println "Running doc source config tests..." + let mut failures := 0 + for (name, test) in docSourceConfigTests do + IO.print s!" {name}: " + try + test + IO.println "ok" + catch e => + IO.println s!"FAIL\n {e}" + failures := failures + 1 + return failures diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean index ab43b0b7..e52c9c1e 100644 --- a/src/verso-manual/VersoManual.lean +++ b/src/verso-manual/VersoManual.lean @@ -42,6 +42,7 @@ import VersoManual.Literate import VersoManual.Marginalia import VersoManual.Bibliography import VersoManual.Table +import VersoManual.DB open Lean (Name NameMap Json ToJson FromJson quote) diff --git a/src/verso-manual/VersoManual/DB.lean b/src/verso-manual/VersoManual/DB.lean new file mode 100644 index 00000000..ef408fde --- /dev/null +++ b/src/verso-manual/VersoManual/DB.lean @@ -0,0 +1,6 @@ +/- +Copyright (c) 2025-2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +import VersoManual.DB.Config diff --git a/src/verso-manual/VersoManual/DB/Config.lean b/src/verso-manual/VersoManual/DB/Config.lean new file mode 100644 index 00000000..c5edeaa0 --- /dev/null +++ b/src/verso-manual/VersoManual/DB/Config.lean @@ -0,0 +1,188 @@ +/- +Copyright (c) 2025-2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +import Lake.Toml + +/-! # Doc Source Configuration + +Parsing and code generation for `doc-sources.toml`, which declares which packages' documentation +should be built by the `docSource` Lake package facet. + +The `[[require]]` entries use the same field names as `lakefile.toml`. +-/ + +namespace Verso.Genre.Manual.DocSource + +open Lake.Toml + +/-- A dependency entry from `doc-sources.toml`, mirroring `[[require]]` in `lakefile.toml`. -/ +structure Require where + /-- The package name (must match the name declared in its lakefile). -/ + name : String + /-- Git repository URL. -/ + git : Option String := none + /-- Git revision (branch, tag, or commit hash). -/ + rev : Option String := none + /-- Local filesystem path (relative to the project root). -/ + path : Option System.FilePath := none + /-- Subdirectory within the repository. -/ + subDir : Option String := none +deriving Repr, BEq, Inhabited + +/-- Parsed contents of a `doc-sources.toml` file. -/ +structure Config where + /-- Package dependencies whose documentation should be built. -/ + require : Array Require := #[] + /-- + Which library targets to document. Defaults to default library targets of all required + packages. + -/ + libraries : Array String := #[] + /-- Shell commands to run in the managed workspace before building (e.g., `lake exe cache get`). -/ + setup : Array String := #[] +deriving Repr, BEq, Inhabited + +/-- Extract a `String` from a TOML `Value`, or `none` if it's not a string. -/ +private def tomlString? : Value → Option String + | .string _ s => some s + | _ => none + +/-- +Extract an `Array String` from a TOML array of strings. Non-string elements are silently +skipped. +-/ +private def tomlStringArray? : Value → Option (Array String) + | .array _ vs => some <| vs.filterMap tomlString? + | _ => none + +/-- Parse a single `[[require]]` entry from a TOML table value. -/ +def Require.ofToml (v : Value) : Except String Require := do + match v with + | .table' _ t => + let name ← match t.find? `name with + | some v => match tomlString? v with + | some s => pure s + | none => throw "[[require]] entry 'name' field must be a string" + | none => throw "[[require]] entry is missing the required 'name' field" + let git := t.find? `git >>= tomlString? + let rev := t.find? `rev >>= tomlString? + let path := t.find? `path >>= tomlString? |>.map System.FilePath.mk + let subDir := t.find? `subDir >>= tomlString? + pure { name, git, rev, path, subDir } + | _ => throw "[[require]] entry must be a table" + +/-- Parse a `Config` from a TOML `Table`. -/ +def Config.ofToml (table : Table) : Except String Config := do + let require ← match table.find? `require with + | some (.array _ vs) => vs.mapM Require.ofToml + | some _ => throw "'require' must be an array of tables ([[require]])" + | none => pure #[] + let libraries := match table.find? `libraries with + | some v => tomlStringArray? v |>.getD #[] + | none => #[] + let setup := match table.find? `setup with + | some v => tomlStringArray? v |>.getD #[] + | none => #[] + pure { require, libraries, setup } + +/-- Load and parse a `doc-sources.toml` file. -/ +def Config.load (filePath : System.FilePath) : IO Config := do + let input ← IO.FS.readFile filePath + let ictx := Lean.Parser.mkInputContext input filePath.toString + match (← Lake.Toml.loadToml ictx |>.toBaseIO) with + | .ok table => + match Config.ofToml table with + | .ok config => pure config + | .error e => throw <| .userError s!"Error parsing {filePath}: {e}" + | .error msgs => + let msgStrs ← msgs.toList.mapM fun msg => msg.data.toString + throw <| .userError s!"Error parsing {filePath}:\n{"\n".intercalate msgStrs}" + +/-- +Split a command string into an executable name and arguments, respecting single and double +quotes. Backslash escapes the next character inside double quotes. Unmatched quotes are +treated as if closed at the end of the string. +-/ +def splitCommand (cmd : String) : Option (String × Array String) := do + let mut args : Array String := #[] + let mut cur : String := "" + -- Track whether the current word contains any content (including empty quotes) + let mut inWord := false + let mut i := 0 + let chars := cmd.toList + while i < chars.length do + let c := chars[i]! + if c == '\'' then + -- Single-quoted: everything up to closing ' is literal + inWord := true + i := i + 1 + while i < chars.length && chars[i]! != '\'' do + cur := cur.push chars[i]! + i := i + 1 + -- skip closing quote (or end of string) + i := i + 1 + else if c == '"' then + -- Double-quoted: backslash escapes the next character + inWord := true + i := i + 1 + while i < chars.length && chars[i]! != '"' do + if chars[i]! == '\\' && i + 1 < chars.length then + i := i + 1 + cur := cur.push chars[i]! + else + cur := cur.push chars[i]! + i := i + 1 + -- skip closing quote (or end of string) + i := i + 1 + else if c == ' ' || c == '\t' then + if inWord then + args := args.push cur + cur := "" + inWord := false + i := i + 1 + else + cur := cur.push c + inWord := true + i := i + 1 + if inWord then + args := args.push cur + match args.toList with + | [] => none + | exe :: rest => some (exe, rest.toArray) + +/-- Generate a `require` declaration in lakefile.lean syntax for a single dependency. -/ +def Require.toLakefileEntry (r : Require) (projectDir : System.FilePath) : String := + let name := s!"require «{r.name}»" + match r.git, r.path with + | some url, _ => + let revPart := r.rev.map (s!" @ \"{·}\"") |>.getD "" + let subDirPart := r.subDir.map (s!" / \"{·}\"") |>.getD "" + s!"{name} from git\n \"{url}\"{revPart}{subDirPart}\n" + | _, some path => + -- Resolve relative paths against the project root to produce absolute paths, + -- since the generated lakefile lives in the managed workspace, not the project root. + let absPath := if path.isAbsolute then path else projectDir / path + s!"{name} from \"{absPath}\"\n" + | none, none => + -- No source specified — Lake will look it up in the registry + s!"{name}\n" + +/-- +Generate a complete `lakefile.lean` for the managed doc-gen workspace. + +`config` is the parsed `doc-sources.toml` (or `none` for a core-only build). +`docgen4Dir` is the absolute path to the doc-gen4 package checkout. +`projectDir` is the absolute path to the user's project root. +-/ +def generateLakefile (config : Option Config) + (docgen4Dir : System.FilePath) (projectDir : System.FilePath) : String := + let header := "import Lake\nopen Lake DSL\n\npackage «docgen-workspace»\n\n" + let docgenReq := s!"require «doc-gen4» from \"{docgen4Dir}\"\n\n" + let userReqs := match config with + | some cfg => cfg.require.map (·.toLakefileEntry projectDir) |>.toList |> String.join + | none => "" + header ++ docgenReq ++ userReqs + +end Verso.Genre.Manual.DocSource diff --git a/src/verso-manual/VersoManual/DB/Setup.lean b/src/verso-manual/VersoManual/DB/Setup.lean new file mode 100644 index 00000000..e77bf65e --- /dev/null +++ b/src/verso-manual/VersoManual/DB/Setup.lean @@ -0,0 +1,143 @@ +/- +Copyright (c) 2025-2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +import VersoManual.DB.Config + +/-! # Doc Source Workspace Setup + +Executable that manages the doc-gen4 build workspace. Called by the `docSource` Lake package facet. + +Usage: `verso-docgen-setup [toml-path]` + +This executable: +1. Parses `doc-sources.toml` (if provided and exists) +2. Generates a `lakefile.lean` and `lean-toolchain` in the managed workspace +3. Runs any configured setup commands +4. Runs `lake build` to produce `api-docs.db` +5. Verifies the database was produced +-/ + +open Verso.Genre.Manual.DocSource + +/-- +Lake environment variables to clear when spawning a child `lake` process, to avoid inheriting +the parent Lake's workspace configuration. Same set used by `VersoBlog.LiterateLeanPage`. +-/ +private def lakeVars : Array String := + #["LAKE", "LAKE_HOME", "LAKE_PKG_URL_MAP", + "LEAN_SYSROOT", "LEAN_AR", "LEAN_PATH", "LEAN_SRC_PATH", + "LEAN_GITHASH", + "ELAN_TOOLCHAIN", "DYLD_LIBRARY_PATH", "LD_LIBRARY_PATH"] + +/-- Environment variable settings that unset all Lake variables. -/ +private def cleanEnv : Array (String × Option String) := + lakeVars.map (·, none) + +/-- Read the `lean-toolchain` file from a directory. -/ +private def readToolchain (dir : System.FilePath) : IO String := do + let tcPath := dir / "lean-toolchain" + unless ← tcPath.pathExists do + throw <| .userError s!"lean-toolchain not found at {tcPath}" + let contents ← IO.FS.readFile tcPath + return contents.trimAscii.toString + +/-- Run a shell command in the given directory, printing output and throwing on failure. -/ +private def runCmd (cmd : String) (args : Array String) (cwd : System.FilePath) : IO Unit := do + IO.println s!" Running: {cmd} {" ".intercalate args.toList}" + let result ← IO.Process.output { + cmd, args, cwd := some cwd + env := cleanEnv + } + unless result.stdout.isEmpty do IO.print result.stdout + unless result.stderr.isEmpty do IO.eprint result.stderr + unless result.exitCode == 0 do + throw <| .userError s!"Command '{cmd}' exited with code {result.exitCode}" + +/-- Check for a toolchain mismatch between the project and any path dependencies. -/ +private def checkToolchainMismatch + (projectDir : System.FilePath) (config : Config) : IO (Option String) := do + let ourTc ← readToolchain projectDir + for req in config.require do + if let some path := req.path then + let depDir := if path.isAbsolute then path else projectDir / path + let depTcPath := depDir / "lean-toolchain" + if ← depTcPath.pathExists then + let depTc ← IO.FS.readFile depTcPath + let depTc := depTc.trimAscii.toString + if depTc != ourTc then + return some s!"Toolchain mismatch: this project uses '{ourTc}' but '{req.name}' uses '{depTc}'. The documented library must build with the same toolchain as your Verso project." + return none + +def main (args : List String) : IO UInt32 := do + -- Parse arguments + let (wsDir, docgen4Dir, projectDir, tomlPath?) ← match args with + | [ws, dg, proj, toml] => + let r : System.FilePath × System.FilePath × System.FilePath × Option System.FilePath := + (⟨ws⟩, ⟨dg⟩, ⟨proj⟩, some ⟨toml⟩) + pure r + | [ws, dg, proj] => + let r : System.FilePath × System.FilePath × System.FilePath × Option System.FilePath := + (⟨ws⟩, ⟨dg⟩, ⟨proj⟩, none) + pure r + | _ => + IO.eprintln "Usage: verso-docgen-setup [toml-path]" + return 1 + + -- Parse doc-sources.toml if provided and exists + let config? ← do + if let some (tomlPath : System.FilePath) := tomlPath? then + if ← tomlPath.pathExists then + some <$> Config.load tomlPath + else + pure none + else + pure none + + -- Create workspace directory + IO.FS.createDirAll wsDir + + -- Write lakefile.lean + let lakefileContent := generateLakefile config? docgen4Dir projectDir + IO.FS.writeFile (wsDir / "lakefile.lean") lakefileContent + IO.println s!"Wrote {wsDir / "lakefile.lean"}" + + -- Write lean-toolchain + let toolchain ← readToolchain projectDir + IO.FS.writeFile (wsDir / "lean-toolchain") (toolchain ++ "\n") + IO.println s!"Wrote {wsDir / "lean-toolchain"} ({toolchain})" + + -- Run setup commands + if let some config := config? then + for cmd in config.setup do + if let some (exe, cmdArgs) := splitCommand cmd then + runCmd exe cmdArgs wsDir + + -- Run lake build + let libraries := config?.map (·.libraries) |>.getD #[] + let targets := if libraries.isEmpty + then #[":docInfo"] + else libraries.map (· ++ ":docInfo") + + IO.println s!"Building documentation sources..." + for target in targets do + try + runCmd "lake" #["build", target] wsDir + catch e => + -- On build failure, check for toolchain mismatch + if let some config := config? then + if let some mismatchMsg ← checkToolchainMismatch projectDir config then + IO.eprintln s!"Note: {mismatchMsg}" + throw e + + -- Verify the database was produced inside the sub-workspace's build directory. + let dbPath := wsDir / ".lake" / "build" / "api-docs.db" + unless ← dbPath.pathExists do + IO.eprintln s!"Documentation database not found at {dbPath} after build." + IO.eprintln "This may indicate an incompatible doc-gen4 version or misconfigured library targets." + IO.eprintln s!"Try running 'cd {wsDir} && lake build' manually to diagnose." + return 1 + + IO.println s!"Documentation database ready at {dbPath}" + return 0 From a2ea28e34172fbe8b3f2eaaa4d5637e7e266a3c8 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Sun, 1 Mar 2026 16:22:13 +0100 Subject: [PATCH 2/2] wip: read docstrings from doc-gen This PR implements an alternative path to docstring rendering that reads the necessary data from a doc-gen4 SQLite database, to work around the fact that docstring info is no longer available in the environment with the module system and to allow a global view of the project for things like instance lists. --- doc/UsersGuide/Manuals.lean | 47 ++- lakefile.lean | 27 +- src/tests/Tests/DocSourceConfig.lean | 8 +- src/verso-manual/VersoManual/DB.lean | 3 + src/verso-manual/VersoManual/DB/Config.lean | 26 +- src/verso-manual/VersoManual/DB/Convert.lean | 65 ++++ .../VersoManual/DB/Docstring.lean | 164 ++++++++ src/verso-manual/VersoManual/DB/Query.lean | 349 ++++++++++++++++++ src/verso-manual/VersoManual/DB/Setup.lean | 29 +- 9 files changed, 673 insertions(+), 45 deletions(-) create mode 100644 src/verso-manual/VersoManual/DB/Convert.lean create mode 100644 src/verso-manual/VersoManual/DB/Docstring.lean create mode 100644 src/verso-manual/VersoManual/DB/Query.lean diff --git a/doc/UsersGuide/Manuals.lean b/doc/UsersGuide/Manuals.lean index 21576de2..18811910 100644 --- a/doc/UsersGuide/Manuals.lean +++ b/doc/UsersGuide/Manuals.lean @@ -6,8 +6,9 @@ Author: David Thrane Christiansen import Lean.DocString.Syntax import VersoManual import VersoBlog +import VersoManual.DB -open Verso Genre Manual +open Verso Genre Manual DB open InlineLean open Verso.Doc @@ -21,25 +22,47 @@ htmlSplit := .never Verso's {name}`Manual` genre can be used to write reference manuals, textbooks, or other book-like documents. It supports generating both HTML and PDFs via LaTeX, but the PDF support is relatively immature and untested compared to the HTML support. +{dbDocstring Manual} {docstring Manual} + + + +{dbDocstring Manual.PartMetadata} {docstring Manual.PartMetadata} + + +{dbDocstring Manual.HtmlSplitMode} {docstring Manual.HtmlSplitMode} + + The {name}`Manual` genre's block and inline element types are extensible. In the document, they consist of instances of {name}`Manual.Block` and {name}`Manual.Inline`, respectively: +{dbDocstring Manual.Block} {docstring Manual.Block} + + +{dbDocstring Manual.Inline} {docstring Manual.Inline} + + The fields {name}`Block.name` and {name Manual.Inline.name}`Inline.name` are used to look up concrete implementations of traversal and output generation in run-time tables that contain descriptions: +{dbDocstring Manual.BlockDescr} {docstring Manual.BlockDescr} + + +{dbDocstring Manual.InlineDescr} {docstring Manual.InlineDescr} + + Typically, the `inline_extension` and `block_extension` commands are used to simultaneously define an element and its descriptor, registering them for use by {name}`manualMain`. :::paragraph @@ -47,12 +70,18 @@ The type {name}`HtmlAssets` contains CSS and JavaScript code. {name}`Manual.TraverseState`, {name}`Manual.BlockDescr`, and {name}`Manual.InlineDescr` all inherit from this structure. During traversal, HTML assets are collected; they are all included in the final rendered document. +{dbDocstring Manual.HtmlAssets} {docstring Manual.HtmlAssets} + + Use {name}`HtmlAssets.combine` to combine multiple assets. +{dbDocstring Manual.HtmlAssets.combine} {docstring Manual.HtmlAssets.combine} + + ::: # Tags and References @@ -92,13 +121,19 @@ tag := "docstrings" Docstrings can be included using the `docstring` directive. For instance, ``` +{dbDocstring List.forM} {docstring List.forM} + + ``` results in +{dbDocstring List.forM} {docstring List.forM} + + The {name}`docstring` command takes a positional parameter which is the documented name. It also accepts the following optional named parameters: @@ -154,11 +189,17 @@ Elsewhere in the document, `tech` can be used to annotate a use site of a techni A {deftech}_technical term_ is a term with a specific meaning that's used precisely, like this one. References to technical terms are valid both before and after their definition sites. +{dbDocstring deftech} {docstring deftech} + + +{dbDocstring tech} {docstring tech} + + # Open-Source Licenses %%% tag := "oss-licenses" @@ -168,8 +209,12 @@ To facilitate providing appropriate credit to the authors of open-source JavaScr This is done using the {name HtmlAssets.licenseInfo}`licenseInfo` field that {name}`BlockDescr` and {name}`InlineDescr` inherit from {name}`HtmlAssets`. These contain a {name}`LicenseInfo`: +{dbDocstring LicenseInfo} {docstring LicenseInfo} + + The {name}`licenseInfo` command displays the licenses for all components that were included in the generated document: +{dbDocstring licenseInfo} {docstring licenseInfo} diff --git a/lakefile.lean b/lakefile.lean index cde7862f..dd7c9a2b 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -106,6 +106,7 @@ lean_exe «verso-demo» where lean_lib UsersGuide where srcDir := "doc" leanOptions := #[⟨`weak.linter.verso.manual.headerTags, true⟩] + needs := #[`@:docSource] @[default_target] lean_exe usersguide where @@ -219,19 +220,17 @@ package_facet docSource pkg : System.FilePath := do | 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 - } + -- Always run the setup exe and let the inner `lake build` handle incrementality. + -- This avoids stale DB issues from incomplete traces — the inner workspace's own + -- build system correctly tracks all dependencies (doc-gen4, documented libraries, etc.). + 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 diff --git a/src/tests/Tests/DocSourceConfig.lean b/src/tests/Tests/DocSourceConfig.lean index 2dd6aa5a..151470ed 100644 --- a/src/tests/Tests/DocSourceConfig.lean +++ b/src/tests/Tests/DocSourceConfig.lean @@ -14,7 +14,7 @@ Tests for `Verso.Genre.Manual.DocSource.Config` — TOML parsing and lakefile ge open Verso.Genre.Manual.DocSource open Lake.Toml -/-- Parse a TOML string into a `Table`. Throws on parse error. -/ +/-- Parses a TOML string into a `Table`. Throws on parse error. -/ private def parseToml (input : String) : IO Table := do let ictx := Lean.Parser.mkInputContext input "" match (← Lake.Toml.loadToml ictx |>.toBaseIO) with @@ -23,18 +23,18 @@ private def parseToml (input : String) : IO Table := do let msgStrs ← msgs.toList.mapM fun msg => msg.data.toString throw <| .userError s!"TOML parse error:\n{"\n".intercalate msgStrs}" -/-- Assert that two values are equal, throwing a descriptive error if not. -/ +/-- Asserts that two values are equal, throwing a descriptive error if not. -/ private def assertEqual [BEq α] [Repr α] (label : String) (expected actual : α) : IO Unit := do unless expected == actual do throw <| IO.userError s!"{label}: expected\n {repr expected}\nbut got\n {repr actual}" -/-- Assert that a result is an error. -/ +/-- Asserts that a result is an error. -/ private def assertError [Repr α] (label : String) (result : Except String α) : IO Unit := do match result with | .error _ => pure () | .ok v => throw <| IO.userError s!"{label}: expected an error but got\n {repr v}" -/-- Assert that a string contains a substring. -/ +/-- Asserts that a string contains a substring. -/ private def assertContains (label : String) (haystack needle : String) : IO Unit := do unless (haystack.splitOn needle).length > 1 do throw <| IO.userError s!"{label}: expected string to contain '{needle}' but got:\n {haystack}" diff --git a/src/verso-manual/VersoManual/DB.lean b/src/verso-manual/VersoManual/DB.lean index ef408fde..d4599092 100644 --- a/src/verso-manual/VersoManual/DB.lean +++ b/src/verso-manual/VersoManual/DB.lean @@ -4,3 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ import VersoManual.DB.Config +import VersoManual.DB.Convert +import VersoManual.DB.Query +import VersoManual.DB.Docstring diff --git a/src/verso-manual/VersoManual/DB/Config.lean b/src/verso-manual/VersoManual/DB/Config.lean index c5edeaa0..f617036a 100644 --- a/src/verso-manual/VersoManual/DB/Config.lean +++ b/src/verso-manual/VersoManual/DB/Config.lean @@ -17,7 +17,7 @@ namespace Verso.Genre.Manual.DocSource open Lake.Toml -/-- A dependency entry from `doc-sources.toml`, mirroring `[[require]]` in `lakefile.toml`. -/ +/-- Dependency entry from `doc-sources.toml`, mirroring `[[require]]` in `lakefile.toml`. -/ structure Require where /-- The package name (must match the name declared in its lakefile). -/ name : String @@ -44,20 +44,20 @@ structure Config where setup : Array String := #[] deriving Repr, BEq, Inhabited -/-- Extract a `String` from a TOML `Value`, or `none` if it's not a string. -/ +/-- Extracts a `String` from a TOML `Value`, or `none` if it's not a string. -/ private def tomlString? : Value → Option String | .string _ s => some s | _ => none /-- -Extract an `Array String` from a TOML array of strings. Non-string elements are silently +Extracts an `Array String` from a TOML array of strings. Non-string elements are silently skipped. -/ private def tomlStringArray? : Value → Option (Array String) | .array _ vs => some <| vs.filterMap tomlString? | _ => none -/-- Parse a single `[[require]]` entry from a TOML table value. -/ +/-- Parses a single `[[require]]` entry from a TOML table value. -/ def Require.ofToml (v : Value) : Except String Require := do match v with | .table' _ t => @@ -73,7 +73,7 @@ def Require.ofToml (v : Value) : Except String Require := do pure { name, git, rev, path, subDir } | _ => throw "[[require]] entry must be a table" -/-- Parse a `Config` from a TOML `Table`. -/ +/-- Parses a `Config` from a TOML `Table`. -/ def Config.ofToml (table : Table) : Except String Config := do let require ← match table.find? `require with | some (.array _ vs) => vs.mapM Require.ofToml @@ -87,7 +87,7 @@ def Config.ofToml (table : Table) : Except String Config := do | none => #[] pure { require, libraries, setup } -/-- Load and parse a `doc-sources.toml` file. -/ +/-- Loads and parses a `doc-sources.toml` file. -/ def Config.load (filePath : System.FilePath) : IO Config := do let input ← IO.FS.readFile filePath let ictx := Lean.Parser.mkInputContext input filePath.toString @@ -101,7 +101,7 @@ def Config.load (filePath : System.FilePath) : IO Config := do throw <| .userError s!"Error parsing {filePath}:\n{"\n".intercalate msgStrs}" /-- -Split a command string into an executable name and arguments, respecting single and double +Splits a command string into an executable name and arguments, respecting single and double quotes. Backslash escapes the next character inside double quotes. Unmatched quotes are treated as if closed at the end of the string. -/ @@ -152,14 +152,18 @@ def splitCommand (cmd : String) : Option (String × Array String) := do | [] => none | exe :: rest => some (exe, rest.toArray) -/-- Generate a `require` declaration in lakefile.lean syntax for a single dependency. -/ +/-- Generates a `require` declaration in lakefile.lean syntax for a single dependency. -/ def Require.toLakefileEntry (r : Require) (projectDir : System.FilePath) : String := let name := s!"require «{r.name}»" match r.git, r.path with | some url, _ => + -- Resolve relative git URLs against the project root, since the generated + -- lakefile lives in the managed workspace, not the project root. + let absUrl := if System.FilePath.isAbsolute ⟨url⟩ || (url.splitOn "://").length > 1 then url + else (projectDir / url).toString let revPart := r.rev.map (s!" @ \"{·}\"") |>.getD "" let subDirPart := r.subDir.map (s!" / \"{·}\"") |>.getD "" - s!"{name} from git\n \"{url}\"{revPart}{subDirPart}\n" + s!"{name} from git\n \"{absUrl}\"{revPart}{subDirPart}\n" | _, some path => -- Resolve relative paths against the project root to produce absolute paths, -- since the generated lakefile lives in the managed workspace, not the project root. @@ -170,7 +174,7 @@ def Require.toLakefileEntry (r : Require) (projectDir : System.FilePath) : Strin s!"{name}\n" /-- -Generate a complete `lakefile.lean` for the managed doc-gen workspace. +Generates a complete `lakefile.lean` for the managed doc-gen workspace. `config` is the parsed `doc-sources.toml` (or `none` for a core-only build). `docgen4Dir` is the absolute path to the doc-gen4 package checkout. @@ -179,7 +183,7 @@ Generate a complete `lakefile.lean` for the managed doc-gen workspace. def generateLakefile (config : Option Config) (docgen4Dir : System.FilePath) (projectDir : System.FilePath) : String := let header := "import Lake\nopen Lake DSL\n\npackage «docgen-workspace»\n\n" - let docgenReq := s!"require «doc-gen4» from \"{docgen4Dir}\"\n\n" + let docgenReq := s!"require «doc-gen4» from git\n \"{docgen4Dir}\"\n\n" let userReqs := match config with | some cfg => cfg.require.map (·.toLakefileEntry projectDir) |>.toList |> String.join | none => "" diff --git a/src/verso-manual/VersoManual/DB/Convert.lean b/src/verso-manual/VersoManual/DB/Convert.lean new file mode 100644 index 00000000..9988f8c0 --- /dev/null +++ b/src/verso-manual/VersoManual/DB/Convert.lean @@ -0,0 +1,65 @@ +/- +Copyright (c) 2025-2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +import DocGen4.RenderedCode +import SubVerso.Highlighting.Highlighted + +/-! # RenderedCode → Highlighted Conversion + +Doc-gen4 stores types as `RenderedCode` (`TaggedText RenderedCode.Tag`) binary blobs. Verso renders +all code using SubVerso's `Highlighted` type. This module converts between them. + +The conversion is lossy: `RenderedCode` does not carry hover info, variable types, or go-to-definition +targets. The visual rendering is the same — tokens that were keywords, string literals, or constant +references are tagged appropriately for syntax highlighting and linking. +-/ + +namespace Verso.Genre.Manual.DB + +open DocGen4 (RenderedCode SortFormer) +open SubVerso.Highlighting (Highlighted Token) + +/-- Extract plain text content from a `RenderedCode` tree, discarding all tags. -/ +partial def renderedCodeText : RenderedCode → String + | .text s => s + | .tag _ inner => renderedCodeText inner + | .append xs => String.join (xs.toList.map renderedCodeText) + +/-- +Convert a `RenderedCode` value (from doc-gen4's database) to a `Highlighted` value (for Verso's +rendering pipeline). Tags are mapped as follows: + +- `.keyword` → `Token.Kind.keyword` (no name or docs) +- `.string` → `Token.Kind.str` +- `.const name` → `Token.Kind.const` (with signature and docstring from `constInfo` if available) +- `.sort` → `Token.Kind.sort` (no docs) +- `.otherExpr` → plain `Highlighted.text` (no semantic info) + +The `constInfo` parameter provides hover data for known constants: a map from `Name` to +`(signature, docstring?)`. +-/ +partial def renderedCodeToHighlighted (constInfo : Lean.NameMap (String × Option String) := {}) + : RenderedCode → Highlighted + | .text s => .text s + | .tag t inner => + let content := renderedCodeText inner + match t with + | .keyword => .token ⟨.keyword none none none, content⟩ + | .string => .token ⟨.str content, content⟩ + | .const name => + let (sig, doc?) := constInfo.find? name |>.getD ("", none) + .token ⟨.const name sig doc? false none, content⟩ + | .sort _former => .token ⟨.sort none, content⟩ + | .otherExpr => renderedCodeToHighlighted constInfo inner + | .append xs => .seq (xs.map (renderedCodeToHighlighted constInfo)) + +/-- Collect all constant names referenced in a `RenderedCode` tree. -/ +partial def renderedCodeConstNames (acc : Lean.NameSet := {}) : RenderedCode → Lean.NameSet + | .text _ => acc + | .tag (.const name) inner => renderedCodeConstNames (acc.insert name) inner + | .tag _ inner => renderedCodeConstNames acc inner + | .append xs => xs.foldl (init := acc) fun a x => renderedCodeConstNames a x + +end Verso.Genre.Manual.DB diff --git a/src/verso-manual/VersoManual/DB/Docstring.lean b/src/verso-manual/VersoManual/DB/Docstring.lean new file mode 100644 index 00000000..3348435a --- /dev/null +++ b/src/verso-manual/VersoManual/DB/Docstring.lean @@ -0,0 +1,164 @@ +/- +Copyright (c) 2025-2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +import VersoManual.DB.Query +import VersoManual.Docstring +import VersoManual.Markdown + +import Verso.Doc.Elab.Block +import Verso.Doc.Elab.Monad +import Verso.Doc.ArgParse +import Verso.Doc.PointOfInterest + +import MD4Lean + +/-! # DB-Backed Docstring Command + +A `{dbDocstring}` block command that reads documentation data from a doc-gen4 SQLite database rather +than from the Lean `Environment`. Produces the same `Block.docstring` output as the existing +environment-based `{docstring}` command, so the HTML/TeX rendering pipeline works unchanged. +-/ + +open Lean +open Verso.Doc.Elab.PartElabM +open Verso.Code +open Verso.ArgParse +open SubVerso.Highlighting + +namespace Verso.Genre.Manual.DB + +/-- Locate the doc-gen4 database path relative to the current working directory. -/ +private def getDbPath : IO System.FilePath := do + let cwd ← IO.currentDir + return cwd / ".lake" / "build" / "verso-doc-db" / ".lake" / "build" / "api-docs.db" + + +private structure DBDocstringConfig where + name : Ident × Name + allowMissing : Bool + hideFields : Bool := false + hideStructureConstructor : Bool := false + label : Option String := none + +section +variable {m} [Monad m] [MonadOptions m] [MonadEnv m] [MonadLiftT CoreM m] [MonadError m] + [MonadLog m] [AddMessageContext m] [Lean.Elab.MonadInfoTree m] [MonadLiftT MetaM m] + +private def DBDocstringConfig.parse : ArgParse m DBDocstringConfig := + DBDocstringConfig.mk <$> + .positional `name .documentableName <*> + .flagM `allowMissing (verso.docstring.allowMissing.get <$> getOptions) + "Warn instead of error on missing docstrings (defaults to value of option `verso.docstring.allowMissing)" <*> + .flag `hideFields false <*> + .flag `hideStructureConstructor false <*> + .named `label .string true + +instance : FromArgs DBDocstringConfig m := ⟨DBDocstringConfig.parse⟩ + +end + +private def getExtras (name : Name) (declType : Block.Docstring.DeclType) : + Verso.Doc.Elab.DocElabM (Array Term) := + match declType with + | .structure isClass constructor? _ fieldInfo parents _ => do + let ctorRow : Option Term ← constructor?.mapM fun constructor => do + let header := if isClass then "Instance Constructor" else "Constructor" + let sigDesc : Array Term ← + if let some docs := constructor.docstring? then + let some mdAst := MD4Lean.parse docs + | throwError "Failed to parse docstring as Markdown" + mdAst.blocks.mapM (Markdown.blockFromMarkdown · (handleHeaders := Markdown.strongEmphHeaders)) + else pure (#[] : Array Term) + let sig ← `(Verso.Doc.Block.other (Verso.Genre.Manual.Block.internalSignature $(quote constructor.hlName) none) #[$sigDesc,*]) + ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstringSection $(quote header)) #[$sig]) + + let parentsRow : Option Term ← do + if parents.isEmpty then pure none + else + let header := "Extends" + let inh ← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.inheritance $(quote name) $(quote parents)) #[]) + some <$> ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstringSection $(quote header)) #[$inh]) + + let fieldsRow : Option Term ← do + let header := if isClass then "Methods" else "Fields" + let fieldInfo := fieldInfo.filter (·.subobject?.isNone) + let fieldSigs : Array Term ← fieldInfo.mapM fun i => do + let inheritedFrom : Option Nat := + i.fieldFrom.head?.bind (fun n => parents.findIdx? (·.name == n.name)) + let sigDesc : Array Term ← + if let some docs := i.docString? then + let some mdAst := MD4Lean.parse docs + | throwError "Failed to parse docstring as Markdown" + mdAst.blocks.mapM (Markdown.blockFromMarkdown · (handleHeaders := Markdown.strongEmphHeaders)) + else + pure (#[] : Array Term) + ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.fieldSignature $(quote i.visibility) $(quote i.fieldName) $(quote i.type) $(quote inheritedFrom) $(quote <| parents.map (·.parent))) #[$sigDesc,*]) + if fieldSigs.isEmpty then pure none + else some <$> ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstringSection $(quote header)) #[$fieldSigs,*]) + + pure <| ctorRow.toArray ++ parentsRow.toArray ++ fieldsRow.toArray + | .inductive ctors .. => do + let ctorSigs : Array Term ← + ctors.mapM fun c => do + let sigDesc ← + if let some docs := c.docstring? then + let some mdAst := MD4Lean.parse docs + | throwError "Failed to parse docstring as Markdown" + mdAst.blocks.mapM (Markdown.blockFromMarkdown · (handleHeaders := Markdown.strongEmphHeaders)) + else pure (#[] : Array Term) + ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.constructorSignature $(quote c.signature)) #[$sigDesc,*]) + pure #[← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstringSection "Constructors") #[$ctorSigs,*])] + | _ => pure #[] + +open Verso.Genre.Manual.Markdown in +open Verso.Doc.Elab in +@[block_command] +def dbDocstring : BlockCommandOf DBDocstringConfig + | ⟨(x, name), allowMissing, hideFields, hideCtor, customLabel⟩ => do + let opts : Options → Options := + (verso.docstring.allowMissing.set · allowMissing) + withOptions opts do + Doc.PointOfInterest.save (← getRef) name.toString (detail? := some "Documentation") + + -- Locate and open the database + let dbPath ← getDbPath + unless ← dbPath.pathExists do + throwErrorAt x m!"Documentation database not found at '{dbPath}'. Run `lake build` to generate it." + + -- Look up the declaration + let some docInfo ← lookupDocInfo dbPath name + | throwErrorAt x m!"'{name}' not found in the documentation database." + + let info := docInfo.toInfo + let ci ← constInfoMap dbPath docInfo + + -- Extract and parse docstring + let blockStx ← do + match docStringOfDoc? info.doc with + | none => pure #[] + | some docs => + let some ast := MD4Lean.parse docs + | throwErrorAt x "Failed to parse docstring as Markdown" + ast.blocks.mapM (blockFromMarkdown · (handleHeaders := strongEmphHeaders)) + + -- Check deprecation + let isDeprecated := info.attrs.any (·.startsWith "deprecated") + if !(← Docstring.getAllowDeprecated) && isDeprecated then + Lean.logError m!"'{name}' is deprecated.\n\nSet option 'verso.docstring.allowDeprecated' to 'true' to allow documentation for deprecated names." + + -- Build DeclType from DocInfo + let declType := buildDeclType docInfo (hideFields := hideFields) (hideStructureConstructor := hideCtor) ci + + -- Build Signature (includes declaration name) + let signature := signatureOfInfo info ci + + -- Build extras for structures and inductives + let extras ← getExtras name declType + + ``(Verso.Doc.Block.other + (Verso.Genre.Manual.Block.docstring $(quote name) $(quote declType) $(quote signature) $(quote customLabel) $(quote (#[] : Array Name))) + #[$(blockStx ++ extras),*]) + +end Verso.Genre.Manual.DB diff --git a/src/verso-manual/VersoManual/DB/Query.lean b/src/verso-manual/VersoManual/DB/Query.lean new file mode 100644 index 00000000..c8a3f82c --- /dev/null +++ b/src/verso-manual/VersoManual/DB/Query.lean @@ -0,0 +1,349 @@ +/- +Copyright (c) 2025-2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +import DocGen4.DB +import DocGen4.DB.VersoDocString +import DocGen4.Process.Base +import SQLite + +import VersoManual.DB.Convert +import VersoManual.Docstring + +/-! # DB Querying and Type Reconstruction + +High-level API for querying the doc-gen4 database and converting the results into Verso's +documentation types (`DeclType`, `Signature`, `DocName`, `FieldInfo`, `ParentInfo`). +-/ + +namespace Verso.Genre.Manual.DB + +open Lean +open DocGen4 (RenderedCode) +open DocGen4.Process (DocInfo NameInfo) +open DocGen4.DB (ReadDB openForReading builtinDocstringValues) +open SubVerso.Highlighting (Highlighted Token) +open Verso.Genre.Manual (Signature) +open Verso.Genre.Manual.Block.Docstring (DeclType DocName FieldInfo ParentInfo Visibility) + +/-- Extract a markdown docstring from a doc-gen4 `NameInfo.doc` field. -/ +def docStringOfDoc? (doc : Option (String ⊕ VersoDocString)) : Option String := + doc.bind fun + | .inl md => some md + | .inr v => some (DocGen4.Process.versoDocToMarkdown v) + +/-- Build a `DocName` from a doc-gen4 `NameInfo`. +When `showNamespace` is `true` (the default), the full qualified name is displayed. +When `false`, only the last component is shown (used for inductive constructors). +The `sigOverride` parameter allows providing a custom hover signature string (e.g., with named +parameters for structure constructors). -/ +def docNameOfNameInfo (ni : NameInfo) + (constInfo : Lean.NameMap (String × Option String) := {}) + (showNamespace : Bool := true) + (sigOverride : Option String := none) : DocName := + let docstring? := docStringOfDoc? ni.doc + let sigStr := sigOverride.getD s!"{ni.name} : {renderedCodeText ni.type}" + let displayName := if showNamespace then ni.name.toString else ni.name.getString! + let nameHl := Highlighted.token ⟨.const ni.name sigStr docstring? false none, displayName⟩ + { name := ni.name + hlName := nameHl + signature := .seq #[nameHl, .text " : ", renderedCodeToHighlighted constInfo ni.type] + docstring? } + +/-- Build a `Signature` from a doc-gen4 `Info`, including the declaration name. -/ +def signatureOfInfo (info : DocGen4.Process.Info) + (constInfo : Lean.NameMap (String × Option String) := {}) : Signature := + let docstring? := docStringOfDoc? info.doc + let sigStr := s!"{info.name} : {renderedCodeText info.type}" + let nameHl := Highlighted.token ⟨.const info.name sigStr docstring? false none, info.name.toString⟩ + let argsHl := info.args.map fun arg => + Highlighted.seq #[.text " ", renderedCodeToHighlighted constInfo arg.binder] + let sepHl := Highlighted.text " : " + let typeHl := renderedCodeToHighlighted constInfo info.type + let sig := Highlighted.seq (#[nameHl] ++ argsHl ++ #[sepHl, typeHl]) + { wide := sig, narrow := sig } + +/-- +Extract the parent structure name from a `RenderedCode` type by finding the first `.const` tag. +Falls back to `.anonymous` if no constant reference is found. +-/ +private partial def parentNameOfRenderedCode : RenderedCode → Name + | .text _ => .anonymous + | .tag (.const name) _ => name + | .tag _ inner => parentNameOfRenderedCode inner + | .append xs => xs.foldl (init := .anonymous) fun acc x => + if acc != .anonymous then acc else parentNameOfRenderedCode x + +/-- Convert doc-gen4's `StructureParentInfo` array to Verso's `ParentInfo` array. -/ +def convertParents (parents : Array DocGen4.Process.StructureParentInfo) + (constInfo : Lean.NameMap (String × Option String) := {}) : Array ParentInfo := + parents.mapIdx fun i p => { + projFn := p.projFn + name := parentNameOfRenderedCode p.type + parent := renderedCodeToHighlighted constInfo p.type + index := i + } + +/-- +Convert a doc-gen4 `Process.FieldInfo` to Verso's `Block.Docstring.FieldInfo`. + +Some fields are simplified because the database doesn't carry the full information: +- `subobject?` is always `none` +- `binderInfo` is always `BinderInfo.default` +- `autoParam` is always `false` +- `visibility` is always `.public` + +For inherited fields (`isDirect = false`), the `fieldFrom` list is populated by matching the +field's projection function name prefix against parent structure names. This enables the +"Inherited from" display and checkbox-based parent field filtering in the HTML output. +-/ +def convertFieldInfo (field : DocGen4.Process.FieldInfo) + (parents : Array ParentInfo) + (constInfo : Lean.NameMap (String × Option String) := {}) : FieldInfo := + let fieldNameStr := field.name.getString! + let docString? := docStringOfDoc? field.doc + let sigStr := s!"{field.name} : {renderedCodeText field.type}" + let fieldName := + Highlighted.token ⟨.const field.name sigStr docString? true none, fieldNameStr⟩ + let fieldFrom : List DocName := + if field.isDirect then [] + else + -- For inherited fields, determine which parent owns this field by matching + -- the field's projection function name prefix against parent names. + -- E.g., field `Verso.Genre.Manual.HtmlAssets.extraCss` → parent `HtmlAssets` + let fieldPrefix := field.name.getPrefix + match parents.find? (·.name == fieldPrefix) with + | some parent => + let parentDocName : DocName := { + name := parent.name + hlName := .token ⟨.const parent.name "" none false none, parent.name.toString⟩ + signature := parent.parent + docstring? := none + } + [parentDocName] + | none => [] + { + fieldName + fieldFrom + type := renderedCodeToHighlighted constInfo field.type + projFn := field.name + subobject? := none + binderInfo := .default + autoParam := false + docString? + visibility := .public + } + +/-- Build a pretty constructor hover signature from a structure's fields. +Groups consecutive fields with the same type, e.g. `(shortTitle shortContextTitle : Option String)`. +Returns a string like `Struct.mk (field1 : Type1) (field2 field3 : Type2) : Struct`. + +NOTE: This is a workaround because doc-gen4 currently stores the structure constructor as `NameInfo` +(without args). Once doc-gen4 is changed to store the constructor as `Info` (with pretty-printed +binder args), this function should be replaced by directly using the constructor's `args` field. -/ +private def prettyCtorSig (ctorName : Name) (structName : Name) + (fields : Array DocGen4.Process.FieldInfo) : String := + let resultType := structName.toString + if fields.isEmpty then + s!"{ctorName} : {resultType}" + else Id.run do + -- Group consecutive fields with the same rendered type + let mut groups : Array (Array String × String) := #[] + for field in fields do + let typeStr := renderedCodeText field.type + let fieldName := field.name.getString! + match groups.back? with + | some (names, t) => + if t == typeStr then + groups := groups.pop.push (names.push fieldName, t) + else + groups := groups.push (#[fieldName], typeStr) + | none => + groups := groups.push (#[fieldName], typeStr) + let params := groups.map fun (names, typeStr) => + let nameStr := " ".intercalate names.toList + s!"({nameStr} : {typeStr})" + let paramStr := "\n ".intercalate params.toList + s!"{ctorName} {paramStr} : {resultType}" + +private def buildStructureDeclType (isClass : Bool) (info : DocGen4.Process.StructureInfo) + (hideFields : Bool) (hideStructureConstructor : Bool) + (constInfo : Lean.NameMap (String × Option String) := {}) : DeclType := + let ctorSig := prettyCtorSig info.ctor.name info.toInfo.name info.fieldInfo + let ctor? := + if hideStructureConstructor then none + else some (docNameOfNameInfo info.ctor constInfo (sigOverride := some ctorSig)) + let fieldNames := + if hideFields then #[] + else info.fieldInfo.map (·.name) + let parents := convertParents info.parents constInfo + let fieldInfo := + if hideFields then #[] + else info.fieldInfo.map (convertFieldInfo · parents constInfo) + .structure isClass ctor? fieldNames fieldInfo parents #[] + +/-- +Reconstruct a `DeclType` from a doc-gen4 `DocInfo`. + +For structures and classes, converts constructor, field, and parent information. +For inductives, converts constructor `DocName` values. +For definitions, opaques, axioms: extracts safety information. +-/ +def buildDeclType (docInfo : DocInfo) (hideFields : Bool) (hideStructureConstructor : Bool) + (constInfo : Lean.NameMap (String × Option String) := {}) : DeclType := + match docInfo with + | .axiomInfo info => + .axiom (if info.isUnsafe then .unsafe else .safe) + | .theoremInfo _ => + .theorem + | .opaqueInfo info => + .opaque info.definitionSafety + | .definitionInfo info => + .def (if info.isUnsafe then .unsafe else .safe) + | .instanceInfo info => + .def (if info.isUnsafe then .unsafe else .safe) + | .inductiveInfo info => + let ctors := info.ctors.toArray.map fun ctor => + docNameOfNameInfo ctor.toNameInfo constInfo (showNamespace := false) + .inductive ctors 0 false + | .structureInfo info => + buildStructureDeclType false info hideFields hideStructureConstructor constInfo + | .classInfo info => + buildStructureDeclType true info hideFields hideStructureConstructor constInfo + | .classInductiveInfo info => + let ctors := info.ctors.toArray.map fun ctor => + docNameOfNameInfo ctor.toNameInfo constInfo (showNamespace := false) + .inductive ctors 0 false + | .ctorInfo _info => + .other + +/-- Build a `NameMap` of hover data for constants directly contained in a `DocInfo` +(the declaration itself, its fields, constructors, etc.). -/ +private def localConstInfoMap (docInfo : DocInfo) : Lean.NameMap (String × Option String) := + let info := docInfo.toInfo + let sig := s!"{info.name} : {renderedCodeText info.type}" + let m : Lean.NameMap (String × Option String) := + ({} : Lean.NameMap _).insert info.name (sig, docStringOfDoc? info.doc) + match docInfo with + | .inductiveInfo ind => + ind.ctors.foldl (init := m) fun m c => + m.insert c.name (s!"{c.name} : {renderedCodeText c.type}", docStringOfDoc? c.doc) + | .structureInfo s => + let ctorSig := prettyCtorSig s.ctor.name info.name s.fieldInfo + let m := m.insert s.ctor.name (ctorSig, docStringOfDoc? s.ctor.doc) + s.fieldInfo.foldl (init := m) fun m f => + m.insert f.name (s!"{f.name} : {renderedCodeText f.type}", docStringOfDoc? f.doc) + | .classInfo s => + let ctorSig := prettyCtorSig s.ctor.name info.name s.fieldInfo + let m := m.insert s.ctor.name (ctorSig, docStringOfDoc? s.ctor.doc) + s.fieldInfo.foldl (init := m) fun m f => + m.insert f.name (s!"{f.name} : {renderedCodeText f.type}", docStringOfDoc? f.doc) + | _ => m + +/-- Collect all `RenderedCode` values from a `DocInfo` (type, args, fields, constructors, parents). -/ +private def allRenderedCodes (docInfo : DocInfo) : Array RenderedCode := + let info := docInfo.toInfo + let codes := #[info.type] ++ info.args.map (·.binder) + match docInfo with + | .inductiveInfo ind => + codes ++ ind.ctors.toArray.map (·.type) + | .structureInfo s => + codes ++ #[s.ctor.type] ++ s.fieldInfo.map (·.type) ++ s.parents.map (·.type) + | .classInfo s => + codes ++ #[s.ctor.type] ++ s.fieldInfo.map (·.type) ++ s.parents.map (·.type) + | _ => codes + +/-- Collect all constant names referenced in any `RenderedCode` of a `DocInfo`. -/ +private def referencedConstNames (docInfo : DocInfo) : Lean.NameSet := + (allRenderedCodes docInfo).foldl (init := {}) fun acc rc => + renderedCodeConstNames acc rc + +/-- +Query the database for type and docstring hover data for a set of constant names. +Returns a `NameMap` of `(typeString, docstring?)` suitable for use as `constInfo`. +-/ +private def queryConstHoverData (dbPath : System.FilePath) (names : Lean.NameSet) : + IO (Lean.NameMap (String × Option String)) := do + let sqlite ← SQLite.openWith dbPath .readonly + let typeStmt ← sqlite.prepare + "SELECT type, module_name, position FROM name_info WHERE name = ?" + let mdDocStmt ← sqlite.prepare + "SELECT text FROM declaration_markdown_docstrings WHERE module_name = ? AND position = ?" + let versoDocStmt ← sqlite.prepare + "SELECT content FROM declaration_verso_docstrings WHERE module_name = ? AND position = ?" + let mut result : Lean.NameMap (String × Option String) := {} + have : SQLite.Blob.FromBinary VersoDocString := DocGen4.DB.versoDocStringFromBinary builtinDocstringValues + for name in names do + typeStmt.bind 1 name.toString + if ← typeStmt.step then + let typeBlob ← typeStmt.columnBlob 0 + let moduleName ← typeStmt.columnText 1 + let position ← typeStmt.columnInt64 2 + -- Look up docstring: try markdown first, then verso + let mut doc? : Option String := none + mdDocStmt.bind 1 moduleName + mdDocStmt.bind 2 position + if ← mdDocStmt.step then + doc? := some (← mdDocStmt.columnText 0) + mdDocStmt.reset + mdDocStmt.clearBindings + if doc?.isNone then + versoDocStmt.bind 1 moduleName + versoDocStmt.bind 2 position + if ← versoDocStmt.step then + let blob ← versoDocStmt.columnBlob 0 + match SQLite.Blob.fromBinary (α := VersoDocString) blob with + | Except.ok vds => + doc? := some (DocGen4.Process.versoDocToMarkdown vds) + | Except.error _ => pure () + versoDocStmt.reset + versoDocStmt.clearBindings + match SQLite.Blob.fromBinary (α := RenderedCode) typeBlob with + | Except.ok rc => + let sig := s!"{name} : {renderedCodeText rc}" + result := result.insert name (sig, doc?) + | Except.error _ => + pure () + typeStmt.reset + typeStmt.clearBindings + return result + +/-- +Build a complete `NameMap` of hover data for a `DocInfo`, including both locally-defined names +(the declaration, its fields/constructors) and externally-referenced constants (looked up in the DB). +-/ +def constInfoMap (dbPath : System.FilePath) (docInfo : DocInfo) : + IO (Lean.NameMap (String × Option String)) := do + let local_ := localConstInfoMap docInfo + let referenced := referencedConstNames docInfo + -- Only query the DB for names not already in the local map + let mut missing : Lean.NameSet := {} + for name in referenced do + unless local_.contains name do + missing := missing.insert name + if missing.isEmpty then return local_ + let external ← queryConstHoverData dbPath missing + -- Merge: local takes precedence + return external.foldl (init := local_) fun m name val => + if m.contains name then m else m.insert name val + +/-- +Open the doc-gen4 database at the given path and look up a declaration by name. + +Returns `none` if the name is not found. Throws on IO errors (missing file, corrupt DB). +-/ +def lookupDocInfo (dbPath : System.FilePath) (name : Name) : + IO (Option DocInfo) := do + let db ← openForReading dbPath builtinDocstringValues + let moduleNames ← db.getModuleNames + let name2ModIdx ← db.buildName2ModIdx moduleNames + let some modIdx := name2ModIdx[name]? + | return none + let modName := moduleNames[modIdx.toNat]! + let mod ← db.loadModule modName + return mod.members.findSome? fun + | .docInfo di => if di.toInfo.name == name then some di else none + | _ => none + +end Verso.Genre.Manual.DB diff --git a/src/verso-manual/VersoManual/DB/Setup.lean b/src/verso-manual/VersoManual/DB/Setup.lean index e77bf65e..36131069 100644 --- a/src/verso-manual/VersoManual/DB/Setup.lean +++ b/src/verso-manual/VersoManual/DB/Setup.lean @@ -23,7 +23,7 @@ open Verso.Genre.Manual.DocSource /-- Lake environment variables to clear when spawning a child `lake` process, to avoid inheriting -the parent Lake's workspace configuration. Same set used by `VersoBlog.LiterateLeanPage`. +the parent Lake's workspace configuration. -/ private def lakeVars : Array String := #["LAKE", "LAKE_HOME", "LAKE_PKG_URL_MAP", @@ -31,11 +31,11 @@ private def lakeVars : Array String := "LEAN_GITHASH", "ELAN_TOOLCHAIN", "DYLD_LIBRARY_PATH", "LD_LIBRARY_PATH"] -/-- Environment variable settings that unset all Lake variables. -/ +/-- Environment variable settings that unset all Lake variables and disable doc-gen4 source links. -/ private def cleanEnv : Array (String × Option String) := - lakeVars.map (·, none) + lakeVars.map (·, none) ++ #[("DOCGEN_SRC", some "file")] -/-- Read the `lean-toolchain` file from a directory. -/ +/-- Reads the `lean-toolchain` file from a directory. -/ private def readToolchain (dir : System.FilePath) : IO String := do let tcPath := dir / "lean-toolchain" unless ← tcPath.pathExists do @@ -43,7 +43,7 @@ private def readToolchain (dir : System.FilePath) : IO String := do let contents ← IO.FS.readFile tcPath return contents.trimAscii.toString -/-- Run a shell command in the given directory, printing output and throwing on failure. -/ +/-- Runs a shell command in the given directory, printing output and throwing on failure. -/ private def runCmd (cmd : String) (args : Array String) (cwd : System.FilePath) : IO Unit := do IO.println s!" Running: {cmd} {" ".intercalate args.toList}" let result ← IO.Process.output { @@ -55,7 +55,7 @@ private def runCmd (cmd : String) (args : Array String) (cwd : System.FilePath) unless result.exitCode == 0 do throw <| .userError s!"Command '{cmd}' exited with code {result.exitCode}" -/-- Check for a toolchain mismatch between the project and any path dependencies. -/ +/-- Checks for a toolchain mismatch between the project and any path dependencies. -/ private def checkToolchainMismatch (projectDir : System.FilePath) (config : Config) : IO (Option String) := do let ourTc ← readToolchain projectDir @@ -121,15 +121,14 @@ def main (args : List String) : IO UInt32 := do else libraries.map (· ++ ":docInfo") IO.println s!"Building documentation sources..." - for target in targets do - try - runCmd "lake" #["build", target] wsDir - catch e => - -- On build failure, check for toolchain mismatch - if let some config := config? then - if let some mismatchMsg ← checkToolchainMismatch projectDir config then - IO.eprintln s!"Note: {mismatchMsg}" - throw e + try + runCmd "lake" (#["build"] ++ targets) wsDir + catch e => + -- On build failure, check for toolchain mismatch + if let some config := config? then + if let some mismatchMsg ← checkToolchainMismatch projectDir config then + IO.eprintln s!"Note: {mismatchMsg}" + throw e -- Verify the database was produced inside the sub-workspace's build directory. let dbPath := wsDir / ".lake" / "build" / "api-docs.db"