From ebf6c3857658790145d13010ea1722d0fc2d572a Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 15 Apr 2026 11:40:49 +0200 Subject: [PATCH 1/6] dirty fix for dual categories --- scripts/deduce-category-properties.ts | 69 +++++++++++++++++++-------- 1 file changed, 48 insertions(+), 21 deletions(-) diff --git a/scripts/deduce-category-properties.ts b/scripts/deduce-category-properties.ts index 00a54e6c..c3e86929 100644 --- a/scripts/deduce-category-properties.ts +++ b/scripts/deduce-category-properties.ts @@ -30,7 +30,25 @@ export async function deduce_category_properties(db: Client) { } for (const category of categories) { + const allowed = + category.dual_category_id !== null && + category.name.toLowerCase().startsWith('dual') // prevent circular deduction + + if (!allowed) continue + await deduce_dual_category_properties(tx, category) + await deduce_satisfied_category_properties( + tx, + category.id, + implications, + true, + ) + await deduce_unsatisfied_category_properties( + tx, + category.id, + implications, + true, + ) } await tx.commit() @@ -123,6 +141,7 @@ async function deduce_satisfied_category_properties( tx: Transaction, category_id: string, implications: NormalizedCategoryImplication[], + ignore_conflicts = false, ) { const satisfied_res = await tx.execute({ sql: ` @@ -175,13 +194,14 @@ async function deduce_satisfied_category_properties( values.push(category_id, id, reasons[id], i + 1) } - const insert_sql = ` - INSERT INTO category_property_assignments ( - category_id, property_id, is_satisfied, reason, position, is_deduced - ) - VALUES - ${value_fragments.join(',\n')} - ` + const insert_sql = !ignore_conflicts + ? `INSERT INTO category_property_assignments + (category_id, property_id, is_satisfied, reason, position, is_deduced) + VALUES ${value_fragments.join(',\n')}` + : `INSERT INTO category_property_assignments + (category_id, property_id, is_satisfied, reason, position, is_deduced) + VALUES ${value_fragments.join(',\n')} + ON CONFLICT (category_id, property_id) DO NOTHING` await tx.execute({ sql: insert_sql, args: values }) } @@ -195,6 +215,7 @@ async function deduce_unsatisfied_category_properties( tx: Transaction, category_id: string, implications: NormalizedCategoryImplication[], + ignore_conflicts = false, ) { const satisfied_res = await tx.execute({ sql: ` @@ -210,13 +231,21 @@ async function deduce_unsatisfied_category_properties( ) const unsatisfied_res = await tx.execute({ - sql: ` + sql: !ignore_conflicts + ? ` SELECT property_id FROM category_property_assignments WHERE category_id = ? AND is_satisfied = FALSE AND is_deduced = FALSE + ` + : ` + SELECT property_id + FROM category_property_assignments + WHERE + category_id = ? + AND is_satisfied = FALSE `, args: [category_id], }) @@ -278,12 +307,14 @@ async function deduce_unsatisfied_category_properties( values.push(category_id, id, reasons[id], i + 1) } - const insert_query = ` - INSERT INTO category_property_assignments ( - category_id, property_id, is_satisfied, reason, position, is_deduced - ) - VALUES - ${value_fragments.join(',\n')}` + const insert_query = !ignore_conflicts + ? `INSERT INTO category_property_assignments + (category_id, property_id, is_satisfied, reason, position, is_deduced) + VALUES ${value_fragments.join(',\n')}` + : `INSERT INTO category_property_assignments + (category_id, property_id, is_satisfied, reason, position, is_deduced) + VALUES ${value_fragments.join(',\n')} + ON CONFLICT (category_id, property_id) DO NOTHING` await tx.execute({ sql: insert_query, args: values }) } @@ -294,12 +325,6 @@ async function deduce_unsatisfied_category_properties( } async function deduce_dual_category_properties(tx: Transaction, category: CategoryMeta) { - const allowed = - category.dual_category_id !== null && - category.name.toLowerCase().startsWith('dual') // prevent circular deduction - - if (!allowed) return - const res = await tx.execute({ sql: ` INSERT OR REPLACE INTO category_property_assignments @@ -318,7 +343,9 @@ async function deduce_dual_category_properties(tx: Transaction, category: Catego FROM category_property_assignments a INNER JOIN properties p ON p.id = a.property_id INNER JOIN relations r ON r.relation= p.relation - WHERE a.category_id = ? AND p.dual_property_id IS NOT NULL + WHERE + a.category_id = ? + AND p.dual_property_id IS NOT NULL ORDER BY lower(p.dual_property_id) `, args: [category.id, category.dual_category_id], From f796f5816bc2de6fb73a08020303a8263e60d6a2 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 15 Apr 2026 12:00:46 +0200 Subject: [PATCH 2/6] small refactor --- scripts/deduce-category-properties.ts | 37 ++++++++------------------- 1 file changed, 11 insertions(+), 26 deletions(-) diff --git a/scripts/deduce-category-properties.ts b/scripts/deduce-category-properties.ts index c3e86929..284f322d 100644 --- a/scripts/deduce-category-properties.ts +++ b/scripts/deduce-category-properties.ts @@ -37,18 +37,12 @@ export async function deduce_category_properties(db: Client) { if (!allowed) continue await deduce_dual_category_properties(tx, category) - await deduce_satisfied_category_properties( - tx, - category.id, - implications, - true, - ) - await deduce_unsatisfied_category_properties( - tx, - category.id, - implications, - true, - ) + await deduce_satisfied_category_properties(tx, category.id, implications, { + check_conflicts: false, + }) + await deduce_unsatisfied_category_properties(tx, category.id, implications, { + check_conflicts: false, + }) } await tx.commit() @@ -141,7 +135,7 @@ async function deduce_satisfied_category_properties( tx: Transaction, category_id: string, implications: NormalizedCategoryImplication[], - ignore_conflicts = false, + options: { check_conflicts: boolean } = { check_conflicts: true }, ) { const satisfied_res = await tx.execute({ sql: ` @@ -194,7 +188,7 @@ async function deduce_satisfied_category_properties( values.push(category_id, id, reasons[id], i + 1) } - const insert_sql = !ignore_conflicts + const insert_sql = options.check_conflicts ? `INSERT INTO category_property_assignments (category_id, property_id, is_satisfied, reason, position, is_deduced) VALUES ${value_fragments.join(',\n')}` @@ -215,7 +209,7 @@ async function deduce_unsatisfied_category_properties( tx: Transaction, category_id: string, implications: NormalizedCategoryImplication[], - ignore_conflicts = false, + options: { check_conflicts: boolean } = { check_conflicts: true }, ) { const satisfied_res = await tx.execute({ sql: ` @@ -231,16 +225,7 @@ async function deduce_unsatisfied_category_properties( ) const unsatisfied_res = await tx.execute({ - sql: !ignore_conflicts - ? ` - SELECT property_id - FROM category_property_assignments - WHERE - category_id = ? - AND is_satisfied = FALSE - AND is_deduced = FALSE - ` - : ` + sql: ` SELECT property_id FROM category_property_assignments WHERE @@ -307,7 +292,7 @@ async function deduce_unsatisfied_category_properties( values.push(category_id, id, reasons[id], i + 1) } - const insert_query = !ignore_conflicts + const insert_query = options.check_conflicts ? `INSERT INTO category_property_assignments (category_id, property_id, is_satisfied, reason, position, is_deduced) VALUES ${value_fragments.join(',\n')}` From 7aea345540f639902a51e05476d641343aa51c81 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 15 Apr 2026 12:08:52 +0200 Subject: [PATCH 3/6] remove code duplication --- scripts/deduce-category-properties.ts | 56 ++++++++------------------ scripts/deduce-functor-properties.ts | 57 ++++++++------------------- 2 files changed, 34 insertions(+), 79 deletions(-) diff --git a/scripts/deduce-category-properties.ts b/scripts/deduce-category-properties.ts index 284f322d..a1283fa4 100644 --- a/scripts/deduce-category-properties.ts +++ b/scripts/deduce-category-properties.ts @@ -131,27 +131,30 @@ async function delete_deduced_category_properties(tx: Transaction, category_id: }) } -async function deduce_satisfied_category_properties( +async function get_decided_properties( tx: Transaction, category_id: string, - implications: NormalizedCategoryImplication[], - options: { check_conflicts: boolean } = { check_conflicts: true }, + value: boolean, ) { - const satisfied_res = await tx.execute({ + const res = await tx.execute({ sql: ` SELECT property_id FROM category_property_assignments - WHERE - category_id = ? - AND is_satisfied = TRUE - AND is_deduced = FALSE + WHERE category_id = ? AND is_satisfied = ? `, - args: [category_id], + args: [category_id, value], }) - const satisfied_props = new Set( - satisfied_res.rows.map((row) => row.property_id) as string[], - ) as Set + return new Set(res.rows.map((row) => row.property_id) as string[]) +} + +async function deduce_satisfied_category_properties( + tx: Transaction, + category_id: string, + implications: NormalizedCategoryImplication[], + options: { check_conflicts: boolean } = { check_conflicts: true }, +) { + const satisfied_props = await get_decided_properties(tx, category_id, true) const deduced_satisfied_props: string[] = [] const reasons: Record = {} @@ -211,33 +214,8 @@ async function deduce_unsatisfied_category_properties( implications: NormalizedCategoryImplication[], options: { check_conflicts: boolean } = { check_conflicts: true }, ) { - const satisfied_res = await tx.execute({ - sql: ` - SELECT property_id - FROM category_property_assignments - WHERE category_id = ? AND is_satisfied = TRUE - `, - args: [category_id], - }) - - const satisfied_props = new Set( - satisfied_res.rows.map((row) => row.property_id) as string[], - ) - - const unsatisfied_res = await tx.execute({ - sql: ` - SELECT property_id - FROM category_property_assignments - WHERE - category_id = ? - AND is_satisfied = FALSE - `, - args: [category_id], - }) - - const unsatisfied_props = new Set( - unsatisfied_res.rows.map((row) => row.property_id) as string[], - ) + const satisfied_props = await get_decided_properties(tx, category_id, true) + const unsatisfied_props = await get_decided_properties(tx, category_id, false) const deduced_unsatisfied_props: string[] = [] const reasons: Record = {} diff --git a/scripts/deduce-functor-properties.ts b/scripts/deduce-functor-properties.ts index 081e2697..f868318f 100644 --- a/scripts/deduce-functor-properties.ts +++ b/scripts/deduce-functor-properties.ts @@ -158,26 +158,29 @@ async function delete_deduced_functor_properties(tx: Transaction, functor: Funct }) } -async function deduce_satisfied_functor_properties( +async function get_decided_functor_properties( tx: Transaction, - functor: FunctorMeta, - implications: NormalizedFunctorImplication[], + functor_id: string, + value: boolean, ) { - const satisfied_res = await tx.execute({ + const res = await tx.execute({ sql: ` SELECT property_id FROM functor_property_assignments - WHERE - functor_id = ? - AND is_satisfied = TRUE - AND is_deduced = FALSE + WHERE functor_id = ? AND is_satisfied = ? `, - args: [functor.id], + args: [functor_id, value], }) - const satisfied_props = new Set( - satisfied_res.rows.map((row) => row.property_id) as string[], - ) as Set + return new Set(res.rows.map((row) => row.property_id) as string[]) +} + +async function deduce_satisfied_functor_properties( + tx: Transaction, + functor: FunctorMeta, + implications: NormalizedFunctorImplication[], +) { + const satisfied_props = await get_decided_functor_properties(tx, functor.id, true) const deduced_satisfied_props: string[] = [] const reasons: Record = {} @@ -237,34 +240,8 @@ async function deduce_unsatisfied_functor_properties( functor: FunctorMeta, implications: NormalizedFunctorImplication[], ) { - const satisfied_res = await tx.execute({ - sql: ` - SELECT property_id - FROM functor_property_assignments - WHERE functor_id = ? AND is_satisfied = TRUE - `, - args: [functor.id], - }) - - const satisfied_props = new Set( - satisfied_res.rows.map((row) => row.property_id) as string[], - ) - - const unsatisfied_res = await tx.execute({ - sql: ` - SELECT property_id - FROM functor_property_assignments - WHERE - functor_id = ? - AND is_satisfied = FALSE - AND is_deduced = FALSE - `, - args: [functor.id], - }) - - const unsatisfied_props = new Set( - unsatisfied_res.rows.map((row) => row.property_id) as string[], - ) + const satisfied_props = await get_decided_functor_properties(tx, functor.id, true) + const unsatisfied_props = await get_decided_functor_properties(tx, functor.id, false) const deduced_unsatisfied_props: string[] = [] const reasons: Record = {} From e2950e829ed2fb200b2348a391bf60963ef8fc0c Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 15 Apr 2026 12:33:34 +0200 Subject: [PATCH 4/6] add JSdocs --- scripts/deduce-category-implications.ts | 15 +++++++++ scripts/deduce-category-properties.ts | 41 +++++++++++++++++++++++++ scripts/deduce-functor-implications.ts | 12 ++++++++ scripts/deduce-functor-properties.ts | 38 +++++++++++++++++++++++ scripts/deduce-special-morphisms.ts | 4 +++ scripts/deduce-special-objects.ts | 4 +++ 6 files changed, 114 insertions(+) diff --git a/scripts/deduce-category-implications.ts b/scripts/deduce-category-implications.ts index 60b98d3d..839477d3 100644 --- a/scripts/deduce-category-implications.ts +++ b/scripts/deduce-category-implications.ts @@ -4,16 +4,27 @@ import dotenv from 'dotenv' dotenv.config({ quiet: true }) +/** + * Deduces implications from given ones. + */ export async function deduce_category_implications(db: Client) { await clear_deduced_category_implications(db) await create_dualized_category_implications(db) await create_self_dual_category_implications(db) } +/** + * Clears all deduced implications. This is done as a first step. + */ async function clear_deduced_category_implications(db: Client) { await db.execute(`DELETE FROM implications WHERE is_deduced = TRUE`) } +/** + * Dualizes all implications by dualizing the involved properties + * (in case they have a dual). For example, if P ===> Q holds, + * then P^op ===> Q^op holds as well. + */ async function create_dualized_category_implications(db: Client) { const res = await db.execute(` SELECT @@ -91,6 +102,10 @@ async function create_dualized_category_implications(db: Client) { console.info(`Dualized ${dualizable_implications.length} category implications`) } +/** + * Creates all trivial implications of the form + * self-dual + P ===> P^op + */ async function create_self_dual_category_implications(db: Client) { const { rows } = await db.execute(` INSERT INTO implication_input ( diff --git a/scripts/deduce-category-properties.ts b/scripts/deduce-category-properties.ts index a1283fa4..7d7f44d7 100644 --- a/scripts/deduce-category-properties.ts +++ b/scripts/deduce-category-properties.ts @@ -15,6 +15,10 @@ type CategoryMeta = { dual_category_id: string | null } +/** + * Deduce properties of categories from given ones + * by using the list of implications. + */ export async function deduce_category_properties(db: Client) { const tx = await db.transaction() @@ -53,6 +57,20 @@ export async function deduce_category_properties(db: Client) { } } +/** + * Implications have the form: + * + * P_1 + ... + P_n ----> Q_1 + ... + Q_m + * + * or + * + * P_1 + ... + P_n <---> Q_1 + ... + Q_m + * + * This function decomposes them into normalized implications, + * which have the form: + * + * P_1 + ... + P_n ----> Q + */ async function get_normalized_category_implications( tx: Transaction, ): Promise { @@ -113,6 +131,9 @@ async function get_normalized_category_implications( return implications } +/** + * Returns the list of categories saved in the database. + */ async function get_categories(tx: Transaction) { const res = await tx.execute(` SELECT id, name, dual_category_id @@ -121,6 +142,10 @@ async function get_categories(tx: Transaction) { return res.rows as unknown as CategoryMeta[] } +/** + * Clears all the deduced properties. + * This runs before the deduction starts. + */ async function delete_deduced_category_properties(tx: Transaction, category_id: string) { await tx.execute({ sql: ` @@ -131,6 +156,10 @@ async function delete_deduced_category_properties(tx: Transaction, category_id: }) } +/** + * Returns the list of properties that are satisfied or unsatisfied + * for a given category. + */ async function get_decided_properties( tx: Transaction, category_id: string, @@ -148,6 +177,10 @@ async function get_decided_properties( return new Set(res.rows.map((row) => row.property_id) as string[]) } +/** + * Deduce satisfied properties for a given category from given ones + * by using the list of normalized implications. + */ async function deduce_satisfied_category_properties( tx: Transaction, category_id: string, @@ -208,6 +241,10 @@ async function deduce_satisfied_category_properties( ) } +/** + * Deduce unsatisfied properties for a given category from given ones + * by using the satisfied properties and the list of normalized implications. + */ async function deduce_unsatisfied_category_properties( tx: Transaction, category_id: string, @@ -287,6 +324,10 @@ async function deduce_unsatisfied_category_properties( ) } +/** + * Assign dual properties to dual categories: + * If C has property P, then C^op has property P^op (if defined). + */ async function deduce_dual_category_properties(tx: Transaction, category: CategoryMeta) { const res = await tx.execute({ sql: ` diff --git a/scripts/deduce-functor-implications.ts b/scripts/deduce-functor-implications.ts index c5a523ba..9177c679 100644 --- a/scripts/deduce-functor-implications.ts +++ b/scripts/deduce-functor-implications.ts @@ -6,15 +6,27 @@ dotenv.config({ quiet: true }) // TODO: remove code duplication with category implication deduction script +/** + * Deduces functor implications from given ones. + */ export async function deduce_functor_implications(db: Client) { await clear_deduced_functor_implications(db) await create_dualized_functor_implications(db) } +/** + * Clears all deduced functor implications. This is done as a first step. + */ async function clear_deduced_functor_implications(db: Client) { await db.execute(`DELETE FROM functor_implications WHERE is_deduced = TRUE`) } +/** + * Dualizes all functor implications by dualizing the involved properties + * (in case they have a dual). For example, if P ===> Q holds, + * then P^op ===> Q^op holds as well. The assumptions of source and target + * categories (if any) need to be dualized as well. + */ async function create_dualized_functor_implications(db: Client) { const res = await db.execute(` SELECT diff --git a/scripts/deduce-functor-properties.ts b/scripts/deduce-functor-properties.ts index f868318f..b539d818 100644 --- a/scripts/deduce-functor-properties.ts +++ b/scripts/deduce-functor-properties.ts @@ -21,6 +21,10 @@ type FunctorMeta = { // TODO: remove code duplication with category deduction script // (not quite the same because we need source and target assumptions) +/** + * Deduce properties of functor from given ones + * by using the list of functor implications. + */ export async function deduce_functor_properties(db: Client) { const tx = await db.transaction() @@ -43,6 +47,20 @@ export async function deduce_functor_properties(db: Client) { } } +/** + * Implications have the form: + * + * P_1 + ... + P_n ----> Q_1 + ... + Q_m + * + * or + * + * P_1 + ... + P_n <---> Q_1 + ... + Q_m + * + * This function decomposes them into normalized implications, + * which have the form: + * + * P_1 + ... + P_n ----> Q + */ async function get_normalized_functor_implications( tx: Transaction, ): Promise { @@ -113,6 +131,10 @@ async function get_normalized_functor_implications( return implications } +/** + * Returns the list of functors saved in the database along with + * the satisfied properties of their source and target category. + */ async function get_functors(tx: Transaction) { const res = await tx.execute(` SELECT @@ -148,6 +170,10 @@ async function get_functors(tx: Transaction) { })) as FunctorMeta[] } +/** + * Clears all the deduced functor properties. + * This runs before the deduction starts. + */ async function delete_deduced_functor_properties(tx: Transaction, functor: FunctorMeta) { await tx.execute({ sql: ` @@ -158,6 +184,10 @@ async function delete_deduced_functor_properties(tx: Transaction, functor: Funct }) } +/** + * Returns the list of properties that are satisfied or unsatisfied + * for a given functor. + */ async function get_decided_functor_properties( tx: Transaction, functor_id: string, @@ -175,6 +205,10 @@ async function get_decided_functor_properties( return new Set(res.rows.map((row) => row.property_id) as string[]) } +/** + * Deduce satisfied properties for a given functor from given ones + * by using the list of normalized implications. + */ async function deduce_satisfied_functor_properties( tx: Transaction, functor: FunctorMeta, @@ -235,6 +269,10 @@ async function deduce_satisfied_functor_properties( ) } +/** + * Deduce unsatisfied properties for a given functor from given ones + * by using the satisfied properties and the list of normalized implications. + */ async function deduce_unsatisfied_functor_properties( tx: Transaction, functor: FunctorMeta, diff --git a/scripts/deduce-special-morphisms.ts b/scripts/deduce-special-morphisms.ts index 41197f1f..13c5e498 100644 --- a/scripts/deduce-special-morphisms.ts +++ b/scripts/deduce-special-morphisms.ts @@ -7,6 +7,10 @@ export async function deduce_special_morphisms(db: Client) { // e.g. regular monomorphisms = same as monomorphisms in mono-regular categories, } +/** + * Deduce special morphisms in dual categories. + * For example, monomorphisms in C describe epimorphisms in C^op. + */ async function deduce_special_morphisms_of_dual_categories(db: Client) { const res = await db.execute(` INSERT INTO special_morphisms (category_id, type, description, reason) diff --git a/scripts/deduce-special-objects.ts b/scripts/deduce-special-objects.ts index b5341238..dda411af 100644 --- a/scripts/deduce-special-objects.ts +++ b/scripts/deduce-special-objects.ts @@ -4,6 +4,10 @@ export async function deduce_special_objects(db: Client) { await deduce_special_objects_of_dual_categories(db) } +/** + * Deduce special objects in dual categories. + * For example, initial objects in C describe the terminal objects in C^op. + */ async function deduce_special_objects_of_dual_categories(db: Client) { const res = await db.execute(` INSERT INTO special_objects (category_id, type, description) From 5966808ec07ec4ed73a4a06b264308c1a4d7d0a6 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 15 Apr 2026 12:54:09 +0200 Subject: [PATCH 5/6] refactor scripts by encapsulation --- scripts/deduce-category-implications.ts | 5 +- scripts/deduce-category-properties.ts | 3 - scripts/deduce-functor-implications.ts | 5 +- scripts/deduce-functor-properties.ts | 3 - scripts/deduce-special-morphisms.ts | 9 +- scripts/deduce-special-objects.ts | 2 +- scripts/deduce.ts | 34 +++--- scripts/migrate.ts | 139 ++++++++++++++---------- scripts/seed.ts | 91 ++++++++-------- scripts/shared.ts | 14 +++ scripts/test.ts | 18 +-- 11 files changed, 163 insertions(+), 160 deletions(-) diff --git a/scripts/deduce-category-implications.ts b/scripts/deduce-category-implications.ts index 839477d3..3bc2d64d 100644 --- a/scripts/deduce-category-implications.ts +++ b/scripts/deduce-category-implications.ts @@ -1,8 +1,5 @@ -import { type Client } from '@libsql/client' +import type { Client } from '@libsql/client' import { are_equal_sets } from './shared' -import dotenv from 'dotenv' - -dotenv.config({ quiet: true }) /** * Deduces implications from given ones. diff --git a/scripts/deduce-category-properties.ts b/scripts/deduce-category-properties.ts index 7d7f44d7..ccfa2ae3 100644 --- a/scripts/deduce-category-properties.ts +++ b/scripts/deduce-category-properties.ts @@ -1,5 +1,4 @@ import type { Transaction, Client } from '@libsql/client' -import dotenv from 'dotenv' import { get_assumption_string, get_conclusion_string, @@ -7,8 +6,6 @@ import { NormalizedCategoryImplication, } from './shared' -dotenv.config({ quiet: true }) - type CategoryMeta = { id: string name: string diff --git a/scripts/deduce-functor-implications.ts b/scripts/deduce-functor-implications.ts index 9177c679..d36efc0e 100644 --- a/scripts/deduce-functor-implications.ts +++ b/scripts/deduce-functor-implications.ts @@ -1,8 +1,5 @@ -import { type Client } from '@libsql/client' +import type { Client } from '@libsql/client' import { are_equal_sets } from './shared' -import dotenv from 'dotenv' - -dotenv.config({ quiet: true }) // TODO: remove code duplication with category implication deduction script diff --git a/scripts/deduce-functor-properties.ts b/scripts/deduce-functor-properties.ts index b539d818..dfd12bcb 100644 --- a/scripts/deduce-functor-properties.ts +++ b/scripts/deduce-functor-properties.ts @@ -1,5 +1,4 @@ import type { Transaction, Client } from '@libsql/client' -import dotenv from 'dotenv' import { get_assumption_string, get_conclusion_string, @@ -7,8 +6,6 @@ import { NormalizedFunctorImplication, } from './shared' -dotenv.config({ quiet: true }) - type FunctorMeta = { id: string name: string diff --git a/scripts/deduce-special-morphisms.ts b/scripts/deduce-special-morphisms.ts index 13c5e498..170d998e 100644 --- a/scripts/deduce-special-morphisms.ts +++ b/scripts/deduce-special-morphisms.ts @@ -1,10 +1,11 @@ -import { Client } from '@libsql/client' +import type { Client } from '@libsql/client' + +// TODO: deduce further morphisms, +// e.g. isomorphisms = bijective morphisms in algebraic categories, +// e.g. regular monomorphisms = same as monomorphisms in mono-regular categories export async function deduce_special_morphisms(db: Client) { await deduce_special_morphisms_of_dual_categories(db) - // TODO: deduce further morphisms, - // e.g. isomorphisms = bijective morphisms in algebraic categories, - // e.g. regular monomorphisms = same as monomorphisms in mono-regular categories, } /** diff --git a/scripts/deduce-special-objects.ts b/scripts/deduce-special-objects.ts index dda411af..7d4f4d87 100644 --- a/scripts/deduce-special-objects.ts +++ b/scripts/deduce-special-objects.ts @@ -1,4 +1,4 @@ -import { Client } from '@libsql/client' +import type { Client } from '@libsql/client' export async function deduce_special_objects(db: Client) { await deduce_special_objects_of_dual_categories(db) diff --git a/scripts/deduce.ts b/scripts/deduce.ts index ce7c7838..ce3d846e 100644 --- a/scripts/deduce.ts +++ b/scripts/deduce.ts @@ -1,31 +1,27 @@ -import { createClient } from '@libsql/client' -import dotenv from 'dotenv' import { deduce_category_implications } from './deduce-category-implications' import { deduce_category_properties } from './deduce-category-properties' import { deduce_functor_implications } from './deduce-functor-implications' import { deduce_functor_properties } from './deduce-functor-properties' import { deduce_special_objects } from './deduce-special-objects' import { deduce_special_morphisms } from './deduce-special-morphisms' +import { get_client } from './shared' -dotenv.config({ quiet: true }) +/** + * Makes deductions for categories and functors. + */ +async function deduce() { + const db = get_client() -const DB_URL = process.env.DB_URL -const DB_AUTH_TOKEN = process.env.DB_AUTH_TOKEN + await db.execute('PRAGMA foreign_keys = ON') -if (!DB_URL) throw new Error('No DB_URL found') + await deduce_category_implications(db) + await deduce_category_properties(db) -const db = createClient({ - url: DB_URL, - authToken: DB_AUTH_TOKEN, -}) + await deduce_special_objects(db) + await deduce_special_morphisms(db) -await db.execute('PRAGMA foreign_keys = ON') + await deduce_functor_implications(db) + await deduce_functor_properties(db) +} -await deduce_category_implications(db) -await deduce_category_properties(db) - -await deduce_special_objects(db) -await deduce_special_morphisms(db) - -await deduce_functor_implications(db) -await deduce_functor_properties(db) +await deduce() diff --git a/scripts/migrate.ts b/scripts/migrate.ts index c992a589..e8a49b7d 100644 --- a/scripts/migrate.ts +++ b/scripts/migrate.ts @@ -1,21 +1,40 @@ -import { createClient } from '@libsql/client' +import { type Client, createClient } from '@libsql/client' import fs from 'node:fs/promises' import path from 'node:path' import dotenv from 'dotenv' +import { get_client } from './shared' dotenv.config({ quiet: true }) -const DB_VISITS_URL = process.env.DB_VISITS_URL -const DB_VISITS_AUTH_TOKEN = process.env.DB_VISITS_AUTH_TOKEN +await migrate() -if (!DB_VISITS_URL) throw new Error('No DB_VISITS_URL found') +/** + * Creates the tables, indexes, triggers, and views. + */ +async function migrate() { + await create_visits_table() -const db_visits = createClient({ - url: DB_VISITS_URL, - authToken: DB_VISITS_AUTH_TOKEN, -}) + const db = get_client() + await db.execute('PRAGMA foreign_keys = ON') + await create_migrations_table(db) + await apply_migrations(db) +} + +/** + * Creates the visits table. It is stored in a separate database. + */ +async function create_visits_table() { + const DB_VISITS_URL = process.env.DB_VISITS_URL + const DB_VISITS_AUTH_TOKEN = process.env.DB_VISITS_AUTH_TOKEN + + if (!DB_VISITS_URL) throw new Error('No DB_VISITS_URL found') + + const db_visits = createClient({ + url: DB_VISITS_URL, + authToken: DB_VISITS_AUTH_TOKEN, + }) -await db_visits.execute(` + await db_visits.execute(` CREATE TABLE IF NOT EXISTS visits ( id INTEGER PRIMARY KEY, created_at TEXT NOT NULL DEFAULT CURRENT_TIMESTAMP, @@ -25,63 +44,63 @@ await db_visits.execute(` ) `) -console.info('Created visits table') - -const DB_URL = process.env.DB_URL -const DB_AUTH_TOKEN = process.env.DB_AUTH_TOKEN - -if (!DB_URL) throw new Error('No DB_URL found') - -const db = createClient({ - url: DB_URL, - authToken: DB_AUTH_TOKEN, -}) - -await db.execute('PRAGMA foreign_keys = ON') + console.info('Created visits table') +} -await db.execute(` - CREATE TABLE IF NOT EXISTS migrations ( - file TEXT PRIMARY KEY, - applied_at TEXT NOT NULL DEFAULT CURRENT_TIMESTAMP - ) -`) +/** + * Creates the migration table that records + * which migrations have already been applied. + */ +async function create_migrations_table(db: Client) { + await db.execute(` + CREATE TABLE IF NOT EXISTS migrations ( + file TEXT PRIMARY KEY, + applied_at TEXT NOT NULL DEFAULT CURRENT_TIMESTAMP + ) + `) +} -const { rows } = await db.execute('SELECT file FROM migrations') -const applied_migrations = new Set(rows.map((row) => row.file) as string[]) +/** + * Applies all migrations that have not been applied yet. + */ +async function apply_migrations(db: Client) { + const { rows } = await db.execute('SELECT file FROM migrations') + const applied_migrations = new Set(rows.map((row) => row.file) as string[]) -const migrations_folder = path.join(process.cwd(), 'database', 'migrations') -const unsorted_files = await fs.readdir(migrations_folder, 'utf8') -const files = unsorted_files.filter((f) => f.endsWith('.sql')).sort() + const migrations_folder = path.join(process.cwd(), 'database', 'migrations') + const unsorted_files = await fs.readdir(migrations_folder, 'utf8') + const files = unsorted_files.filter((f) => f.endsWith('.sql')).sort() -const invalid_file = files.find((file) => !file.match(/^\d{3}_/)) -if (invalid_file) throw new Error(`Invalid file name: ${invalid_file}`) + const invalid_file = files.find((file) => !file.match(/^\d{3}_/)) + if (invalid_file) throw new Error(`Invalid file name: ${invalid_file}`) -const all_done = files.every((file) => applied_migrations.has(file)) + const all_done = files.every((file) => applied_migrations.has(file)) -if (all_done) { - console.info('No migrations need to be applied') - process.exit(0) -} + if (all_done) { + console.info('No migrations need to be applied') + process.exit(0) + } -for (const file of files) { - if (applied_migrations.has(file)) continue - - const sql = await fs.readFile(path.join(migrations_folder, file), 'utf8') - - const tx = await db.transaction() - try { - await tx.executeMultiple(sql) - await tx.execute({ - sql: 'INSERT INTO migrations (file) VALUES (?)', - args: [file], - }) - await tx.commit() - console.info(`Applied migration: ${file}`) - } catch (err) { - console.error(`Failed migration: ${file}`, err) - await tx.rollback() - process.exit(1) + for (const file of files) { + if (applied_migrations.has(file)) continue + + const sql = await fs.readFile(path.join(migrations_folder, file), 'utf8') + + const tx = await db.transaction() + try { + await tx.executeMultiple(sql) + await tx.execute({ + sql: 'INSERT INTO migrations (file) VALUES (?)', + args: [file], + }) + await tx.commit() + console.info(`Applied migration: ${file}`) + } catch (err) { + console.error(`Failed migration: ${file}`, err) + await tx.rollback() + process.exit(1) + } } -} -console.info('Applied all migrations') + console.info('Applied all migrations') +} diff --git a/scripts/seed.ts b/scripts/seed.ts index 29a7315e..4cfb36da 100644 --- a/scripts/seed.ts +++ b/scripts/seed.ts @@ -1,56 +1,51 @@ -import { createClient } from '@libsql/client' import fs from 'node:fs/promises' import path from 'node:path' -import dotenv from 'dotenv' - -dotenv.config({ quiet: true }) - -const DB_URL = process.env.DB_URL -const DB_AUTH_TOKEN = process.env.DB_AUTH_TOKEN - -if (!DB_URL) throw new Error('No DB_URL found') - -const db = createClient({ - url: DB_URL, - authToken: DB_AUTH_TOKEN, -}) - -const data_folder = path.join(process.cwd(), 'database', 'data') - -const subfolders = (await fs.readdir(data_folder, { withFileTypes: true })) - .filter((f) => f.isDirectory()) - .map((f) => f.name) - .sort() - -const invalid_folder = subfolders.find((f) => !f.match(/^\d{3}_/)) -if (invalid_folder) throw new Error(`Invalid folder name: ${invalid_folder}`) - -for (const folder of subfolders) { - const folder_path = path.join(data_folder, folder) - const files = (await fs.readdir(folder_path, { withFileTypes: true })) - .filter((f) => f.isFile() && f.name.endsWith('.sql')) - .map((f) => path.join(folder_path, f.name)) +import { get_client } from './shared' + +/** + * Seeds the data recorded in SQL files into the database. + */ +async function seed() { + const db = get_client() + const data_folder = path.join(process.cwd(), 'database', 'data') + + const subfolders = (await fs.readdir(data_folder, { withFileTypes: true })) + .filter((f) => f.isDirectory()) + .map((f) => f.name) .sort() - for (const file of files) { - const base = path.basename(file) - const is_valid = base?.match(/^[A-Za-z0-9_.,\-()]+$/) - if (!is_valid) { - throw new Error(`Invalid file name: ${base}`) - } - const sql = await fs.readFile(file, 'utf8') - const tx = await db.transaction() - try { - await tx.executeMultiple(sql) - await tx.commit() - const operation = file.includes('clear') ? 'Clear data' : 'Insert data' - console.info(`${operation}: ${base}`) - } catch (err) { - console.error(`Failed to process ${file}`, err) - await tx.rollback() - process.exit(1) + const invalid_folder = subfolders.find((f) => !f.match(/^\d{3}_/)) + if (invalid_folder) throw new Error(`Invalid folder name: ${invalid_folder}`) + + for (const folder of subfolders) { + const folder_path = path.join(data_folder, folder) + const files = (await fs.readdir(folder_path, { withFileTypes: true })) + .filter((f) => f.isFile() && f.name.endsWith('.sql')) + .map((f) => path.join(folder_path, f.name)) + .sort() + + for (const file of files) { + const base = path.basename(file) + const is_valid = base?.match(/^[A-Za-z0-9_.,\-()]+$/) + if (!is_valid) { + throw new Error(`Invalid file name: ${base}`) + } + const sql = await fs.readFile(file, 'utf8') + const tx = await db.transaction() + try { + await tx.executeMultiple(sql) + await tx.commit() + const operation = file.includes('clear') ? 'Clear data' : 'Insert data' + console.info(`${operation}: ${base}`) + } catch (err) { + console.error(`Failed to process ${file}`, err) + await tx.rollback() + process.exit(1) + } } } + + console.info('Inserted all data') } -console.info('Inserted all data') +await seed() diff --git a/scripts/shared.ts b/scripts/shared.ts index 883a13c1..eb574485 100644 --- a/scripts/shared.ts +++ b/scripts/shared.ts @@ -1,3 +1,8 @@ +import { createClient } from '@libsql/client' +import dotenv from 'dotenv' + +dotenv.config({ quiet: true }) + export function are_equal_sets(a: Set, b: Set) { return a.size === b.size && [...a].every((el) => b.has(el)) } @@ -9,6 +14,15 @@ export function is_subset(a: Set, b: Set, exception?: T) { return true } +export function get_client() { + const DB_URL = process.env.DB_URL + const DB_AUTH_TOKEN = process.env.DB_AUTH_TOKEN + + if (!DB_URL) throw new Error('No DB_URL found') + + return createClient({ url: DB_URL, authToken: DB_AUTH_TOKEN }) +} + type NormalizedImplication = { id: string assumptions: Set diff --git a/scripts/test.ts b/scripts/test.ts index eb63f950..1ca438f9 100644 --- a/scripts/test.ts +++ b/scripts/test.ts @@ -3,26 +3,16 @@ * It checks that the data behaves as expected. * If not, an error is thrown, which must be fixed. */ + import Set_expected from './expected-data/Set.json' import Ab_expected from './expected-data/Ab.json' import Top_expected from './expected-data/Top.json' import decided_categories from './expected-data/decided-categories.json' -import { createClient } from '@libsql/client' -import dotenv from 'dotenv' - -dotenv.config({ quiet: true }) - -const DB_URL = process.env.DB_URL -const DB_AUTH_TOKEN = process.env.DB_AUTH_TOKEN - -if (!DB_URL) throw new Error('No DB_URL found') +import { get_client } from './shared' -const db = createClient({ - url: DB_URL, - authToken: DB_AUTH_TOKEN, -}) +const db = get_client() -execute_tests() +await execute_tests() /** * The main test function verifying that the data behaves as expected. From ce2466e9b4522f1582d0aa438b60512b0505063d Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 15 Apr 2026 13:14:58 +0200 Subject: [PATCH 6/6] seed: one transaction per folder --- scripts/seed.ts | 32 ++++++++++++++++++-------------- 1 file changed, 18 insertions(+), 14 deletions(-) diff --git a/scripts/seed.ts b/scripts/seed.ts index 4cfb36da..3f50b304 100644 --- a/scripts/seed.ts +++ b/scripts/seed.ts @@ -24,24 +24,28 @@ async function seed() { .map((f) => path.join(folder_path, f.name)) .sort() - for (const file of files) { - const base = path.basename(file) - const is_valid = base?.match(/^[A-Za-z0-9_.,\-()]+$/) - if (!is_valid) { - throw new Error(`Invalid file name: ${base}`) - } - const sql = await fs.readFile(file, 'utf8') - const tx = await db.transaction() - try { + const tx = await db.transaction() + + try { + for (const file of files) { + const base = path.basename(file) + const is_valid = base?.match(/^[A-Za-z0-9_.,\-()]+$/) + if (!is_valid) { + throw new Error(`Invalid file name: ${base}`) + } + const sql = await fs.readFile(file, 'utf8') + await tx.executeMultiple(sql) - await tx.commit() + const operation = file.includes('clear') ? 'Clear data' : 'Insert data' console.info(`${operation}: ${base}`) - } catch (err) { - console.error(`Failed to process ${file}`, err) - await tx.rollback() - process.exit(1) } + + await tx.commit() + } catch (err) { + console.error(`Failed to seed ${folder}`, err) + await tx.rollback() + process.exit(1) } }