Writing the Database

This file defines WriteDB, the interface for populating the database. Lake runs one single command per module (and genCore for Init/Std/Lake/Lean), each of which writes to the shared SQLite database through WriteDB. Later, the fromDb command reads everything back via ReadDB (defined in DocGen4.DB.Read) and generates HTML.

WriteDB and ReadDB are separate types because writers and readers have different needs. The database schema lives in DocGen4.DB.Schema.

Module Item Positions

Within a module, each item (declaration, module doc, constructor) is assigned a sequential Int64 position starting from 0. This position serves as the item's identity within the module: the composite key (module_name, position) is the primary key for most tables. Positions are assigned in the order items appear in the module's members array, with constructors and structure fields interleaved between their parent declarations. For example, a module containing a module doc, a definition, and an inductive with two constructors might have positions:

0: module doc 1: definition 2: inductive 3: constructor 1 (of the inductive at position 2) 4: constructor 2 (of the inductive at position 2)

The position counter is a mutable Int64 in updateModuleDb. Structures consume extra positions for their constructor and fields. The read side reconstructs module members by querying name_info and module_docs_markdown ordered by position.

Changing the Schema

When adding a new column or table:

1. Add the DDL in DocGen4.DB.Schema (the ddl string in getDb).
2. Add a prepared statement to WriteStmts and its prepare method below.
3. Add a WriteStmts.saveXyz method with positional bind calls that match the SQL.
4. Expose it through WriteDB (the structure at the top of this file) and the mutex wrapper in ensureWriteDb.
5. Add a prepared statement and loader to ReadStmts in DocGen4.DB.Read.
6. If the change affects serialized blob types, check that there is an update serializedCodeTypeDefs in DocGen4.DB.Schema so the type hash invalidates stale databases. Otherwise, assess the risk of users getting old databases and consider adding another invalidation.

structure DocGen4.DB.WriteDB : Type

A write-only database handle. Used during the analysis phase to populate the database.

• sqlite : SQLite
• deleteModule (modName : String) : IO Unit
• saveModule (modName : String) (sourceUrl? : Option String) : IO Unit
• saveImport (modName : String) (imported : Lean.Name) : IO Unit
• saveMarkdownDocstring (modName : String) (position : Int64) (text : String) : IO Unit
• saveModuleDoc (modName : String) (position : Int64) (text : String) : IO Unit
• saveVersoDocstring (modName : String) (position : Int64) (text : Lean.VersoDocString) : IO Unit
• saveDeclarationRange (modName : String) (position : Int64) (declRange : Lean.DeclarationRange) : IO Unit
• saveInfo (modName : String) (position : Int64) (kind : String) (info : Process.Info) : IO Unit
• saveAxiom (modName : String) (position : Int64) (isUnsafe : Bool) : IO Unit
• saveOpaque (modName : String) (position : Int64) (safety : Lean.DefinitionSafety) : IO Unit
• saveDefinition (modName : String) (position : Int64) (isUnsafe : Bool) (hints : Lean.ReducibilityHints) (isNonComputable : Bool) : IO Unit
• saveDefinitionEquation (modName : String) (position : Int64) (code : RenderedCode) (sequence : Int64) : IO Unit
• saveInstance (modName : String) (position : Int64) (className : String) : IO Unit
• saveInstanceArg (modName : String) (position sequence : Int64) (typeName : String) : IO Unit
• saveInductive (modName : String) (position : Int64) (isUnsafe : Bool) : IO Unit
• saveConstructor (modName : String) (position typePosition : Int64) : IO Unit
• saveClassInductive (modName : String) (position : Int64) (isUnsafe : Bool) : IO Unit
• saveStructure (modName : String) (position : Int64) (isClass : Bool) : IO Unit
• saveStructureConstructor (modName : String) (position ctorPos : Int64) (info : Process.NameInfo) : IO Unit
• saveNameOnly (modName : String) (position : Int64) (kind : String) (name : Lean.Name) (type : RenderedCode) (declRange : Lean.DeclarationRange) : IO Unit

  Save minimal info to name_info for name lookups (not for rendering)

• saveStructureParent (modName : String) (position : Int64) (sequence : Int32) (projectionFn : String) (type : RenderedCode) : IO Unit
• saveStructureField (modName : String) (position sequence : Int64) (projName : String) (type : RenderedCode) (isDirect : Bool) : IO Unit
• saveStructureFieldArg (modName : String) (position fieldSeq argSeq : Int64) (binder : RenderedCode) (isImplicit : Bool) : IO Unit
• saveInternalName (name : Lean.Name) (targetModule : String) (targetPosition : Int64) : IO Unit

  Save an internal name (like a recursor) that should link to its target declaration

• saveTactic (modName : String) (tactic : Process.TacticInfo Process.MarkdownDocstring) : IO Unit

  Save a tactic defined in this module

def DocGen4.DB.WriteDB.saveDocstring (db : WriteDB) (modName : String) (position : Int64) (text : String ⊕ Lean.VersoDocString) : IO Unit

Equations

• db.saveDocstring modName position (Sum.inl md) = db.saveMarkdownDocstring modName position md
• db.saveDocstring modName position (Sum.inr v) = db.saveVersoDocstring modName position v

@[implicit_reducible]

instance DocGen4.DB.instCoeWriteDBSQLite : Coe WriteDB SQLite

Equations

• DocGen4.DB.instCoeWriteDBSQLite = { coe := DocGen4.DB.WriteDB.sqlite }

@[implicit_reducible]

instance DocGen4.DB.instQueryParamDefinitionSafety_docGen4 : SQLite.QueryParam Lean.DefinitionSafety

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance DocGen4.DB.instQueryParamReducibilityHints_docGen4 : SQLite.QueryParam Lean.ReducibilityHints

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance DocGen4.DB.instQueryParamRenderedCode : SQLite.QueryParam RenderedCode

Equations

• One or more equations did not get rendered due to their size.

def DocGen4.DB.ensureWriteDb (values : DocstringValues) (dbFile : System.FilePath) : IO WriteDB

Equations

• One or more equations did not get rendered due to their size.

structure DocGen4.DB.DBM.Context : Type

• values : DocstringValues
• db : WriteDB

@[reducible, inline]

abbrev DocGen4.DB.DBM (α : Type) : Type

Equations

• DocGen4.DB.DBM α = ReaderT DocGen4.DB.DBM.Context IO α

def DocGen4.DB.DBM.run {α : Type} (values : DocstringValues) (dbFile : System.FilePath) (act : DBM α) : IO α

Equations

• DocGen4.DB.DBM.run values dbFile act = do let db ← DocGen4.DB.ensureWriteDb values dbFile ReaderT.run act { values := values, db := db }

def DocGen4.DB.withDB {α : Type} (f : WriteDB → DBM α) : DBM α

Equations

• DocGen4.DB.withDB f = do let __do_lift ← read f __do_lift.db

def DocGen4.DB.withSQLite {α : Type} (f : SQLite → DBM α) : DBM α

Equations

• DocGen4.DB.withSQLite f = do let __do_lift ← read f __do_lift.db.sqlite

def DocGen4.DB.openForReading (dbFile : System.FilePath) (values : DocstringValues) : IO ReadDB

Open a database for reading only.

Read operations are protected by a Std.Mutex internally (see mkReadDB), so a single ReadDB can be shared across tasks without corrupting state. However, sharing serializes all reads through one SQLite connection. For parallel workloads, each task should call openForReading to get its own connection.

Equations

• DocGen4.DB.openForReading dbFile values = do let sqlite ← SQLite.openWith dbFile SQLite.OpenFlags.readonly none 1800000 DocGen4.DB.mkReadDB sqlite values

DB Reading

structure DocGen4.DB.LinkingContext : Type

Context needed for cross-module linking, without loading full module contents.

• moduleNames : Array Lean.Name
• sourceUrls : Std.HashMap Lean.Name String
• name2ModIdx : Std.HashMap Lean.Name Lean.ModuleIdx

def DocGen4.DB.ReadDB.loadLinkingContext (db : ReadDB) : IO LinkingContext

Load the linking context from the database.

Equations

• One or more equations did not get rendered due to their size.

def DocGen4.updateModuleDb (values : DB.DocstringValues) (doc : Process.AnalyzerResult) (buildDir : System.FilePath) (dbFile : String) (sourceUrl? : Option String) : IO Unit

Equations

• One or more equations did not get rendered due to their size.

def DocGen4.updateModuleDb.saveRecursors (name2ModIdx : Std.HashMap Lean.Name Lean.ModuleIdx) (db : DB.WriteDB) (modName : String) (pos : Int64) (indName : Lean.Name) : IO Unit

Equations

• One or more equations did not get rendered due to their size.

def DocGen4.updateModuleDb.saveStructureMetadata (isClass : Bool) (info : Process.StructureInfo) (db : DB.WriteDB) (modName : String) (pos : Int64) (name2ModIdx : Std.HashMap Lean.Name Lean.ModuleIdx) : StateT Int64 IO Unit

Equations

• One or more equations did not get rendered due to their size.

def DocGen4.updateModuleDb.saveStructureFields (info : Process.StructureInfo) (db : DB.WriteDB) (modName : String) (pos : Int64) : IO Unit

Equations

• One or more equations did not get rendered due to their size.

def DocGen4.updateModuleDb.infoKind : Process.DocInfo → String

Equations

• DocGen4.updateModuleDb.infoKind (DocGen4.Process.DocInfo.axiomInfo info) = "axiom"
• DocGen4.updateModuleDb.infoKind (DocGen4.Process.DocInfo.theoremInfo info) = "theorem"
• DocGen4.updateModuleDb.infoKind (DocGen4.Process.DocInfo.opaqueInfo info) = "opaque"
• DocGen4.updateModuleDb.infoKind (DocGen4.Process.DocInfo.definitionInfo info) = "definition"
• DocGen4.updateModuleDb.infoKind (DocGen4.Process.DocInfo.instanceInfo info) = "instance"
• DocGen4.updateModuleDb.infoKind (DocGen4.Process.DocInfo.inductiveInfo info) = "inductive"
• DocGen4.updateModuleDb.infoKind (DocGen4.Process.DocInfo.structureInfo info) = "structure"
• DocGen4.updateModuleDb.infoKind (DocGen4.Process.DocInfo.classInfo info) = "class"
• DocGen4.updateModuleDb.infoKind (DocGen4.Process.DocInfo.classInductiveInfo info) = "class inductive"
• DocGen4.updateModuleDb.infoKind (DocGen4.Process.DocInfo.ctorInfo info) = "constructor"