diff --git a/databases/catdat/scripts/config.ts b/databases/catdat/scripts/config.ts index 027cdd85..1c592c59 100644 --- a/databases/catdat/scripts/config.ts +++ b/databases/catdat/scripts/config.ts @@ -6,9 +6,3 @@ export const PLURALS = { category: 'categories', functor: 'functors', } - -/** - * Proofs longer than this value raise a warning - * that suggests to use content pages instead. - */ -export const PROOF_LENGTH_THRESHOLD = 1200 diff --git a/databases/catdat/scripts/proof-length.ts b/databases/catdat/scripts/proof-length.ts new file mode 100644 index 00000000..3af494b0 --- /dev/null +++ b/databases/catdat/scripts/proof-length.ts @@ -0,0 +1,66 @@ +import { PLURALS, type StructureType } from './config' +import { get_client } from './utils/helpers' + +const db = get_client() + +const PROOF_LENGTH_THRESHOLD = 1200 + +report_long_proofs() + +/** + * Prints proofs whose lengths exceed the given threshold and should + * perhaps be moved to a separate content page. + */ +function report_long_proofs() { + report_long_property_proofs('category') + report_long_property_proofs('functor') + report_long_implication_proofs('category') + report_long_implication_proofs('functor') +} + +function report_long_property_proofs(type: StructureType) { + const long_proofs = db + .prepare<[number], { id: string; property: string; length: number }>( + `SELECT + ${type}_id AS id, + property_id AS property, + length(proof) AS length + FROM ${type}_property_assignments + WHERE is_deduced = FALSE AND length(proof) >= ? + ORDER BY length(proof) DESC`, + ) + .all(PROOF_LENGTH_THRESHOLD) + + if (!long_proofs.length) return + + console.info(`\n--- Long property proofs for ${PLURALS[type]} ---`) + + for (const { id, property, length } of long_proofs) { + console.warn( + `🟡 The proof for (${id}, ${property}) has ${length} characters. Consider moving it to a content page.`, + ) + } +} + +function report_long_implication_proofs(type: StructureType) { + const long_proofs = db + .prepare<[number], { id: string; length: number }>( + `SELECT + id, + length(proof) AS length + FROM ${type}_implications + WHERE is_deduced = FALSE AND length(proof) >= ? + ORDER BY length(proof) DESC`, + ) + .all(PROOF_LENGTH_THRESHOLD) + + if (!long_proofs.length) return + + console.info(`\n--- Long implication proofs for ${PLURALS[type]} ---`) + + for (const { id, length } of long_proofs) { + console.warn( + `🟡 The proof for ${id} has ${length} characters. Consider moving it to a content page.`, + ) + } +} diff --git a/databases/catdat/scripts/seed.ts b/databases/catdat/scripts/seed.ts index c38f5b81..cda73c40 100644 --- a/databases/catdat/scripts/seed.ts +++ b/databases/catdat/scripts/seed.ts @@ -8,18 +8,15 @@ import type { FunctorImplicationYaml, FunctorPropertyYaml, FunctorYaml, - ProofWarning, PropertyEntry, } from './seed.types' import { create_schema_hash, get_saved_schema_hash } from './utils/schema' -import { PLURALS, PROOF_LENGTH_THRESHOLD, STRUCTURES } from './config' +import { PLURALS, STRUCTURES } from './config' const db = get_client() const data_folder = path.resolve('databases', 'catdat', 'data') -const proof_length_warnings: ProofWarning[] = [] - seed() /** @@ -47,8 +44,6 @@ function seed() { seed_functor_properties() seed_functor_implications() seed_functors() - - print_proof_length_warnings() } /** @@ -280,13 +275,6 @@ function seed_categories() { entry.proof, entry.check_redundancy === false ? 0 : 1, ) - if (entry.proof.length >= PROOF_LENGTH_THRESHOLD) { - proof_length_warnings.push({ - structure_id: category_id, - property: entry.property, - length: entry.proof.length, - }) - } } } @@ -490,13 +478,6 @@ function seed_functors() { entry.proof, entry.check_redundancy === false ? 0 : 1, ) - if (entry.proof.length >= PROOF_LENGTH_THRESHOLD) { - proof_length_warnings.push({ - structure_id: functor_id, - property: entry.property, - length: entry.proof.length, - }) - } } } @@ -538,17 +519,3 @@ function seed_functors() { seed_files(db, 'functors', path.join(data_folder, 'functors'), insert_functor) } - -function print_proof_length_warnings() { - if (!proof_length_warnings.length) return - - console.info('\n--- Proof Length Warnings ---') - - proof_length_warnings.sort((a, b) => b.length - a.length) - - for (const { structure_id, property, length } of proof_length_warnings) { - console.warn( - `🟡 The proof for (${structure_id}, ${property}) has ${length} characters. Consider moving it to a content page.`, - ) - } -} diff --git a/databases/catdat/scripts/seed.types.ts b/databases/catdat/scripts/seed.types.ts index a08e1c66..bfe7e29c 100644 --- a/databases/catdat/scripts/seed.types.ts +++ b/databases/catdat/scripts/seed.types.ts @@ -106,9 +106,3 @@ export type FunctorYaml = { undecidable_properties?: PropertyEntry[] comments?: string[] } - -export type ProofWarning = { - structure_id: string - property: string - length: number -} diff --git a/package.json b/package.json index a6fe16bf..bb31ed5c 100644 --- a/package.json +++ b/package.json @@ -24,7 +24,8 @@ "db:snapshot": "cp databases/catdat/catdat.db static/databases/catdat-snapshot.db", "db:update": "pnpm db:seed && pnpm db:deduce && pnpm db:test && pnpm db:snapshot", "db:watch": "tsx databases/catdat/scripts/watch.ts", - "db:redundancies": "tsx databases/catdat/scripts/redundancies.ts" + "db:redundancies": "tsx databases/catdat/scripts/redundancies.ts", + "db:proof-length": "tsx databases/catdat/scripts/proof-length.ts" }, "devDependencies": { "@sveltejs/adapter-netlify": "^6.0.4",