feat: render std

.github/workflows/build.yml

@@ -1,4 +1,4 @@
-name: std4 test build
+name: batteries test build
 
 on:
   push:
@@ -8,7 +8,7 @@ on:
 
 jobs:
   build:
-    name: std4 test build
+    name: batteries test build
     runs-on: ubuntu-latest
     steps:
       - name: Checkout repo

DocGen4/Load.lean

@@ -41,6 +41,6 @@ def load (task : Process.AnalyzeTask) : IO (Process.AnalyzerResult × Hierarchy)
   Prod.fst <$> Meta.MetaM.toIO (Process.process task) config { env := env } {} {}
 
 def loadCore : IO (Process.AnalyzerResult × Hierarchy) := do
-  load <| .loadAll #[`Init, `Lean, `Lake]
+  load <| .loadAll #[`Init, `Lean, `Lake, `Std]
 
 end DocGen4

DocGen4/Output/SourceLinker.lean

@@ -29,7 +29,7 @@ declarations into (optionally positional) Github URLs.
 def sourceLinker (gitUrl? : Option String) (module : Name) : Option DeclarationRange → String :=
   let root := module.getRoot
   let leanHash := Lean.githash
-  if root == `Lean ∨ root == `Init then
+  if root == `Lean ∨ root == `Init ∨ root == `Std then
     let parts := module.components.map Name.toString
     let path := "/".intercalate parts
     mkGithubSourceLinker s!"https://github.com/leanprover/lean4/blob/{leanHash}/src/{path}.lean"

Main.lean

@@ -71,7 +71,7 @@ def indexCmd := `[Cli|
 
 def genCoreCmd := `[Cli|
   genCore VIA runGenCoreCmd;
-  "Generate documentation for the core Lean modules: Init and Lean since they are not Lake projects"
+  "Generate documentation for the core Lean modules: Init, Lean, Lake and Std since they are not Lake projects"
 ]
 
 def bibPrepassCmd := `[Cli|

README.md

@@ -24,8 +24,8 @@ If you have multiple libraries you want to generate full documentation for:
 lake -R -Kenv=dev build Test:docs Foo:docs
 ```
 
-Note that `doc-gen4` currently always generates documentation for `Lean`, `Init`
-and `Lake` in addition to the provided targets.
+Note that `doc-gen4` currently always generates documentation for `Lean`, `Init`, `Lake` and `Std`
+in addition to the provided targets.
 
 The root of the built docs will be `.lake/build/doc/index.html`. However, due to the "Same Origin Policy", the
 generated website will be partially broken if you just open the generated html files in your browser.  You