Extract separate proof length script

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

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.`,
+		)
+	}
+}

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.`,
-		)
-	}
-}

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
-}

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",