Database Schema and Initialization

Defines the SQLite DDL (table definitions) and handles database creation, including schema versioning. The schema is versioned by two hashes:

• The DDL hash detects changes to table definitions (column additions, new tables, etc.).
• The type hash detects changes to Lean types that are serialized as blobs in the database (e.g., RenderedCode, RenderedCode.Tag). It is computed at compile time via inductiveRepr!.

If either hash doesn't match, the database is rejected with an error message asking the user to rebuild. This prevents some silent corruption resulting from reading blobs with a stale deserializer. Note that changes to the serialization procedures that don't change the datatypes will not invalidate the hashes, so this measure is not perfect; however, these instances are typically derived, so they should follow the structure of the type.

def DocGen4.DB.Internals.«termInductiveRepr![_,,]» : Lean.ParserDescr

Gets a string representation of inductive type definitions, computed at compile time.

Equations

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

def DocGen4.DB.serializedCodeTypeDefs : String

The datatypes that are serialized to the database. If they change, then the database should be rebuilt.

Equations

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

def DocGen4.DB.getDb (dbFile : System.FilePath) : IO SQLite

Equations

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

def DocGen4.DB.getDb.ddl : String

Equations

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