Migrations

A migration is a numbered step with an up and a down, each a schema-transaction body. Schema transactions can also read and write data, so a step can change the schema and backfill data atomically.

Driver.migrate applies, in version order, every step newer than the database's latest applied one. Each step runs in its own schema transaction together with the insertion of its history record, so a failed step leaves no trace and the steps before it stay applied. The history lives in the database itself, as typedb-lean-migration entities.

Every step has a checksum of its name and fingerprint. Migrating fails before running anything if an applied step's checksum no longer matches the list, which catches edits to steps that have already run. Lean functions cannot be hashed, so steps written as code must say what identifies them in fingerprint; steps built from TypeQL text (Migration.tql, Migration.define) use the text itself.

Driver.rollback runs down steps in reverse version order, each with the removal of its history record. A step whose down is .irreversible stops the rollback.

inductive TypeDB.Down : Type

How a migration is undone.

• step (body : Tx TxMode.schema Unit) : Down
• irreversible : Down

  The step cannot be undone, e.g. because it drops data.

structure TypeDB.Migration : Type

One versioned migration step.

• version : Nat
• name : String
• up : Tx TxMode.schema Unit
• down : Down
• fingerprint : String

  What identifies the step's content for the checksum: its TypeQL, or a description that changes whenever the step's code does.

def TypeDB.Migration.tql (version : Nat) (name up : String) (down : Option String := none) : Migration

A step from TypeQL text, with an optional TypeQL down.

Equations

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

def TypeDB.Migration.define (version : Nat) (name : String) (specs : List TypeSpec) (down : Down := Down.irreversible) : Migration

A step that defines the mapped types; down undefines nothing and is irreversible unless given.

Equations

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

def TypeDB.Migration.ofFile (version : Nat) (name : String) (path : System.FilePath) (down : Down := Down.irreversible) : IO Migration

A step from a TypeQL file, read now so that its checksum covers the file's content.

Equations

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

def TypeDB.Migration.checksum (m : Migration) : String

Equations

• m.checksum = TypeDB.Str.padLeft (String.ofList (Nat.toDigits 16 (hash (m.name ++ "\n" ++ m.fingerprint)).toNat)) 16 '0'

structure TypeDB.AppliedMigration : Type

A row of the migration history.

• version : Nat
• name : String
• checksum : String
• appliedAt : Std.Time.PlainDateTime

@[instance_reducible]

instance TypeDB.instFromRowAppliedMigration : FromRow AppliedMigration

Equations

• TypeDB.instFromRowAppliedMigration = { decoder := TypeDB.AppliedMigration.mk <$> TypeDB.col "v" <*> TypeDB.col "n" <*> TypeDB.col "c" <*> TypeDB.col "t" }

structure TypeDB.MigrationReport : Type

What migrate or rollback did: the steps run, in order.

• steps : Array (Nat × String)

def TypeDB.instReprMigrationReport.repr : MigrationReport → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TypeDB.instReprMigrationReport : Repr MigrationReport

Equations

• TypeDB.instReprMigrationReport = { reprPrec := TypeDB.instReprMigrationReport.repr }

@[instance_reducible]

instance TypeDB.instInhabitedMigrationReport : Inhabited MigrationReport

Equations

• TypeDB.instInhabitedMigrationReport = { default := TypeDB.instInhabitedMigrationReport.default }

def TypeDB.Migrations.historyType : String

Equations

• TypeDB.Migrations.historyType = "typedb-lean-migration"

def TypeDB.Migrations.historySchema : Query TxMode.schema

Equations

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

def TypeDB.Migrations.historyQuery : Query TxMode.read

Equations

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

def TypeDB.Migrations.validate (ms : List Migration) : Except TypeDBError Unit

Checks that versions are unique and strictly increasing.

Equations

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

def TypeDB.Migrations.history (d : Driver) (db : String) : EIO TypeDBError (Array AppliedMigration)

The applied history, oldest first.

Equations

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

def TypeDB.Driver.migrateSync (d : Driver) (db : String) (ms : List Migration) : EIO TypeDBError MigrationReport

Applies every step newer than the latest applied one, each in its own schema transaction.

Equations

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

def TypeDB.Driver.rollbackSync (d : Driver) (db : String) (ms : List Migration) (to : Nat) : EIO TypeDBError MigrationReport

Runs the down steps of every applied step newer than to, newest first.

Equations

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

def TypeDB.Driver.migrate (d : Driver) (db : String) (ms : List Migration) : Std.Async.EAsync TypeDBError MigrationReport

Equations

• d.migrate db ms = TypeDB.blocking (d.migrateSync db ms)

def TypeDB.Driver.rollback (d : Driver) (db : String) (ms : List Migration) (to : Nat) : Std.Async.EAsync TypeDBError MigrationReport

Equations

• d.rollback db ms to = TypeDB.blocking (d.rollbackSync db ms to)