Reading from the Database

This module contains the code used to read from the database. ReadDB is a structure of functions (like WriteDB) that load module data from a SQLite database. Each function wraps a prepared statement from ReadStmts.

ReadDB is constructed via mkReadDB (called from openForReading in DocGen4.DB). A single ReadDB can be shared across tasks without corruption due to the implicit state associated with SQLite prepared statements because the statements are behind a mutex, but for parallel workloads each task should call openForReading to get its own connection. See htmlOutputResultsParallel in DocGen4.Output.

Column access in the read methods uses positional indices (e.g., stmt.columnInt64 3) that must match the column order in the corresponding SQL query. When modifying a query, make sure to update the column indices in the reader method to match.

def DocGen4.DB.withDbContext {m : Type → Type u_1} {α : Type} [MonadLiftT BaseIO m] [MonadControlT IO m] [Monad m] (context : String) (act : m α) : m α

Equations

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

structure DocGen4.DB.ReadDB : Type

• getModuleNames : IO (Array Lean.Name)
• getModuleSourceUrls : IO (Std.HashMap Lean.Name String)
• getModuleImports : Lean.Name → IO (Array Lean.Name)
• buildName2ModIdx : Array Lean.Name → IO (Std.HashMap Lean.Name Lean.ModuleIdx)
• loadModule : Lean.Name → IO Process.Module
• loadAllTactics : IO (Array (Process.TacticInfo Process.MarkdownDocstring))
• getContainedNames : Lean.Name → IO (Std.HashMap Lean.Name (Std.HashSet Lean.Name))

  For a module, returns a map from each rendered declaration to the set of names whose declaration ranges are contained within it. This is used to find things like projection functions for inherited fields that are sometimes but not always produced by structure elaboration.

• getTransitiveImports : Array Lean.Name → IO (Array Lean.Name)

  Gets the transitive closure of imports for a set of modules. Called at most once per fromDb invocation, and only when explicit module roots are provided, to identify which HTML files to produce.

def SQLite.Stmt.bind {α : Type u_1} [NullableQueryParam α] (stmt : Stmt) (index : Int32) (param : α) : IO Unit

Equations

• stmt.bind index param = SQLite.NullableQueryParam.bind stmt index param

def DocGen4.DB.readRenderedCode (blob : ByteArray) : IO RenderedCode

Reads RenderedCode from a blob.

Equations

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

def DocGen4.DB.mkReadDB (sqlite : SQLite) (values : DocstringValues) : IO ReadDB

Equations

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