Add more database checks

.github/workflows/test.yaml

@@ -0,0 +1,38 @@
+name: Test Workflow
+
+on:
+    # push:
+    #     branches: [main]
+    # pull_request:
+    #     branches: [main]
+    workflow_dispatch:
+
+jobs:
+    test:
+        runs-on: ubuntu-latest
+        steps:
+            - name: Checkout code
+              uses: actions/checkout@v5
+
+            - name: Install pnpm
+              uses: pnpm/action-setup@v5
+              with:
+                  version: 10
+
+            - name: Use Node.js
+              uses: actions/setup-node@v5
+              with:
+                  node-version: 24.14.0
+                  cache: 'pnpm'
+
+            - name: Install Dependencies
+              run: pnpm i
+
+            - name: Generate SvelteKit config
+              run: pnpm svelte-kit sync
+
+            - name: Update and Test database
+              env:
+                  DB_URL: file:database/local.db
+                  DB_VISITS_URL: file:database/visits.db
+              run: pnpm db:update

CONTRIBUTING.md

@@ -65,9 +65,19 @@ to continuously run this update when a file in the subfolder [/database/data](/d
 
 ### Troubleshooting
 
-If the command `pnpm db:update` throws an error, check the error message to identify the cause. It could be malformed SQL, or it could be a failing test in the script `pnpm db:test`. These tests verify that the data behaves as expected and that every property is assigned at least to the "core categories" (see below).
+- If the local database is corrupted, delete the `local.db` file and recreate it using `pnpm db:update`.
+- If the `pnpm db:update` command fails, examine the error message to determine the cause. It could be due to malformed SQL or a failing test in the `pnpm db:test` script (which also runs as part of the update command), as explained below.
 
-If the local database is broken, just delete the `local.db` file and recreate it using `pnpm db:update`.
+### Tests for Data Quality
+
+The `pnpm db:test` command runs several tests to ensure the data behaves as expected and maintains good quality:
+
+1. Properties and their duals are mutual.
+2. Categories and their duals are mutual.
+3. For a specified list of categories (see [decided-categories.json](/scripts/expected-data/decided-categories.json)), all properties have been decided.
+4. Every property of the "core categories" (currently: `Set`, `Ab`, `Top`) matches precisely the expected properties defined in the [/scripts/expected-data](/scripts/expected-data/) folder.
+
+If any of these tests fail, adjust the data accordingly.
 
 ### Example Commits
 
@@ -98,9 +108,7 @@ When contributing new data (categories, functors, properties, implications), ple
 
 - **Special Objects and Morphisms**: For each new category, try to specify its special objects (terminal object, initial object, etc.) in the corresponding table. Also try to specify its special morphisms (isomorphisms, monomorphisms, epimorphisms).
 
-- **Proofs for New Properties**: For every new property, for each existing category or functor, try to find a proof for whether it has this property or not, in case this has not already been deduced automatically. Use the property detail page to check unknown categories.
-
-- **Assign Properties to Core Categories**: For all new properties of categories, you must assign them to the "core categories" (currently: $\mathbf{Set}$, $\mathbf{Top}$, $\mathbf{Ab}$), specifying whether they are satisfied or not. This decision should also be recorded in the JSON files located in [/scripts/expected-data](/scripts/expected-data/).
+- **Proofs for New Properties**: For every new property, for each existing category or functor, try to find a proof for whether it has this property or not, in case this has not already been deduced automatically via some implication. Use the property detail page to check unknown categories. As mentioned in the section on tests, for a list of selected categories it is actually mandatory to decide their properties.
 
 - **Counterexamples**: Ensure that at least one category does not satisfy any new property of categories that is added. If no existing category fits, add a new category that does not have the new property. The same remarks apply to properties of functors.
 

scripts/expected-data/_INFO.md

@@ -0,0 +1,2 @@
+- The JSON file `decided-categories.json` lists various categories whose properties need to be decided. If a new property is added to the database, make sure to decide it _at least_ for these categories.
+- The other JSON files specify precisely which properties are satisfied by a small collection of "core categories" (currently: `Set`, `Top`, `Ab`). If a new property is added to the database, make sure to add the value here.

scripts/expected-data/decided-categories.json

@@ -0,0 +1,17 @@
+[
+	"0",
+	"1",
+	"2",
+	"Ab",
+	"Grp",
+	"N",
+	"R-Mod",
+	"CRing",
+	"Ring",
+	"Set",
+	"Set*",
+	"Top",
+	"Top*",
+	"Vect",
+	"walking_morphism"
+]

scripts/test.ts

@@ -1,6 +1,12 @@
+/**
+ * This file is executed via `pnpm db:test`.
+ * 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'
 
@@ -16,63 +22,21 @@ const db = createClient({
 	authToken: DB_AUTH_TOKEN,
 })
 
-await test_mutual_category_duals()
+execute_tests()
 
-await test_mutual_property_duals()
-
-const expected = {
-	Set: Set_expected,
-	Ab: Ab_expected,
-	Top: Top_expected,
-} as Record<string, Record<string, boolean>>
-
-for (const cat in expected) {
-	await test_properties(cat, expected[cat])
-}
-
-async function test_properties(category_id: string, expected: Record<string, boolean>) {
-	const [props_res, unknown_props_res] = await db.batch([
-		{
-			sql: `
-				SELECT property_id AS id, is_satisfied
-				FROM category_property_assignments
-				WHERE category_id = ?`,
-			args: [category_id],
-		},
-		{
-			sql: `
-				SELECT p.id FROM properties p
-				WHERE NOT EXISTS
-					(
-						SELECT 1 FROM category_property_assignments
-						WHERE category_id = ? AND property_id = p.id
-					)
-			`,
-			args: [category_id],
-		},
-	])
-
-	const properties = props_res.rows as unknown as { id: string; is_satisfied: number }[]
-
-	const unknown_properties = unknown_props_res.rows.map((row) => row.id) as string[]
-
-	for (const { id, is_satisfied } of properties) {
-		const ok = Boolean(is_satisfied) === expected[id]
-		if (!ok) {
-			throw new Error(`❌ Incorrect property of ${category_id}: ${id}`)
-		}
-	}
-
-	if (unknown_properties.length > 0) {
-		throw new Error(
-			`❌ Found unknown properties of ${category_id}: ` +
-				unknown_properties.join(','),
-		)
-	}
-
-	console.info(`✅ Properties of ${category_id} are correct`)
+/**
+ * The main test function verifying that the data behaves as expected.
+ */
+async function execute_tests() {
+	await test_mutual_category_duals()
+	await test_mutual_property_duals()
+	await test_decided_categories()
+	await test_properties_of_core_categories()
 }
 
+/**
+ * Tests for all category properties p,q that if p is dual to q, then q is dual to p.
+ */
 async function test_mutual_property_duals() {
 	const res = await db.execute('SELECT id, dual_property_id FROM properties')
 	const dict: Record<string, string | null> = {}
@@ -96,6 +60,9 @@ async function test_mutual_property_duals() {
 	console.info(`✅ Properties are mutually dual`)
 }
 
+/**
+ * Tests for all categories C,D that if C is dual to D, then D is dual to C.
+ */
 async function test_mutual_category_duals() {
 	const res = await db.execute('SELECT id, dual_category_id FROM categories')
 	const dict: Record<string, string | null> = {}
@@ -118,3 +85,85 @@ async function test_mutual_category_duals() {
 
 	console.info(`✅ Categories are mutually dual`)
 }
+
+/**
+ * Tests if for a specified list of categories all properties have been decided.
+ * If this test fails, property assignments or implications are missing.
+ */
+async function test_decided_categories() {
+	for (const category_id of decided_categories) {
+		await test_decided_category(category_id)
+	}
+}
+
+/**
+ * Tests for a given category if all properties have been decided,
+ * i.e. are either satisfied or unsatisfied.
+ */
+async function test_decided_category(category_id: string) {
+	const res = await db.execute(
+		`
+		SELECT p.id FROM properties p
+		WHERE NOT EXISTS
+			(
+				SELECT 1 FROM category_property_assignments
+				WHERE category_id = ? AND property_id = p.id
+			)
+		`,
+		[category_id],
+	)
+
+	const unknown_properties = res.rows.map((row) => row.id)
+
+	if (unknown_properties.length > 0) {
+		throw new Error(
+			`❌ Found unknown properties of ${category_id}:\n${unknown_properties.join(', ')}.\nEvery property needs to be decided for this category.`,
+		)
+	}
+
+	console.info(`✅ All properties have been decided for ${category_id}`)
+}
+
+/**
+ * Tests if the "core categories" (currently: Set, Ab, Top) behave as expected:
+ * All of their properties in the database have to match those in the
+ * respective JSON files in the subfolder "expected-data".
+ */
+async function test_properties_of_core_categories() {
+	const expected = {
+		Set: Set_expected,
+		Ab: Ab_expected,
+		Top: Top_expected,
+	} as Record<string, Record<string, boolean>>
+
+	for (const cat in expected) {
+		await test_core_category(cat, expected[cat])
+	}
+}
+
+/**
+ * Tests if a "core category" has the expected properties.
+ */
+async function test_core_category(
+	category_id: string,
+	expected: Record<string, boolean>,
+) {
+	const res = await db.execute(
+		`
+		SELECT property_id AS id, is_satisfied
+		FROM category_property_assignments
+		WHERE category_id = ?`,
+		[category_id],
+	)
+
+	const properties = res.rows as unknown as { id: string; is_satisfied: number }[]
+
+	for (const { id, is_satisfied } of properties) {
+		const ok = Boolean(is_satisfied) === expected[id]
+		if (!ok) {
+			throw new Error(`❌ Incorrect property of ${category_id}: ${id}`)
+		}
+	}
+
+	console.info(`✅ Properties of ${category_id} are correct`)
+}