diff --git a/.claude/skills/check-proofs/SKILL.md b/.claude/skills/check-proofs/SKILL.md index 3ffdb4148..ba0249ede 100644 --- a/.claude/skills/check-proofs/SKILL.md +++ b/.claude/skills/check-proofs/SKILL.md @@ -37,4 +37,4 @@ All other argument text is additional context; consider it without narrowing the Start with an overall assessment (for a folder, also state how many files were reviewed). Then list actionable findings, grouped by file for a folder, each identified by the YAML record/property and `proof` field or by the Markdown claim and `::: Proof` block, with a `path:line` reference. For each finding, state severity (`major`, `minor`, or `uncertain`), the specific step or omission, and why it affects the argument. Distinguish a demonstrated logical gap from missing context or uncertainty. Do not report style preferences as mathematical errors. -If no actionable issue is found, say so, but make clear that this is an AI review and not a proof of correctness. Do not claim formal verification or certainty. The author remains responsible for checking the argument and writing the final proof in their own words, consistent with CatDat's contribution guidance. +If no actionable issue is found, say so, but make clear that this is an AI review and not a proof of correctness. Do not claim formal verification or certainty. The author remains responsible for checking the argument thoroughly and making sure the final proof is readable and understandable, consistent with CatDat's contribution guidance. diff --git a/.claude/skills/structure-proofs/SKILL.md b/.claude/skills/structure-proofs/SKILL.md new file mode 100644 index 000000000..229bbeb6b --- /dev/null +++ b/.claude/skills/structure-proofs/SKILL.md @@ -0,0 +1,106 @@ +--- +name: structure-proofs +description: Decide the unknown properties (and, for categories, the special objects and special morphisms) of an existing CatDat structure YAML file by proving or disproving them one at a time, then clean up redundant assignments and summarize. Use when asked to fill in, decide, or prove the properties of a structure. +argument-hint: '[structure file or ID] [optional time limit, e.g. 30m or 2h (default 60m)] (defaults to the current file)' +disable-model-invocation: true +allowed-tools: Read, Edit, Write, Grep, Glob, Bash(pnpm db:update), Bash(pnpm db:structure *), Bash(pnpm db:redundancies), Bash(pnpm db:redundancies *), Bash(pnpm cspell), Bash(date *), Bash(grep *), Bash(sqlite3 database/catdat.db *) +--- + +# Structure Proofs + +Starting from an existing structure YAML file (category, functor, morphism, or symmetric monoidal category) that already defines the structure (ID, name, description, and for categories the objects and morphisms) but has few or no decided properties, decide as many of its unknown properties as possible, one at a time, with proofs. Follow the proof guidelines in [CLAUDE.md](../../../CLAUDE.md) ("Writing proofs") and [CONTRIBUTING.md](../../../CONTRIBUTING.md) throughout. + +Arguments: `$ARGUMENTS` + +## Target and time limit + +- If the arguments contain a path to a YAML file under `database/data//`, use it. If they contain a bare structure ID, locate the file with Glob (`database/data/*/.yaml`). +- Otherwise, use the current file, i.e. the file most recently opened or selected in the IDE. If there is none, or it is not a structure file, ask the user. +- The structure type follows from the folder (`categories/`, `functors/`, `morphisms/`, `symmetric_monoidal_categories/`), and the property and implication folders follow from the type (e.g. `category-properties/`, `category-implications/`; for symmetric monoidal categories `symmetric_monoidal_category_properties/` and `symmetric_monoidal_category_implications/`). +- A time limit such as `30m`, `90m`, or `2h` may be given; the default is **60 minutes**. Record the start time with `date +%s` before the first decision and check it with `date +%s` before every new pick. Once the limit is exceeded, finish the property currently being written (or drop it if the proof is not yet complete), and go to the redundancy phase. + +State the target file, structure type, and time limit at the start. + +## Preparation + +1. Read the structure file in full. Understand the definition precisely: what the objects and morphisms are, how composition works, and any parameters (for parametrized structures such as `BG` or `R-Mod`, properties may depend on the parameter). +2. Read the files of the structures listed under `related`, `dual`, `parent`, and `associated`. Their proofs are templates for style and often for content (a proof for a similar category can frequently be adapted, or a property can be transferred along a functor via a lemma in `content/`). +3. Skim [database/data/macros.yaml](../../../database/data/macros.yaml) for available KaTeX macros and the file names in `content/` for reusable lemmas (e.g. `missing_cogenerator`, `subcategories`, `relationships-epis-monos`, `thin_extremal_generator`). +4. Run `pnpm db:update`, so that the database reflects the current YAML (a new structure only exists in the database after this). If it fails, stop and report the error to the user; do not start editing on a broken database. +5. Run `pnpm db:structure ` to see all groups and counts. For categories, also check which special objects and special morphisms are known, including deduced ones (from rules, parents, and dual categories): + + ``` + sqlite3 database/catdat.db "SELECT kind, is_deduced, description FROM special_morphism_assignments WHERE category_id = ''" + sqlite3 database/catdat.db "SELECT kind, is_deduced, description FROM special_object_assignments WHERE category_id = ''" + ``` + +## Special objects and morphisms (categories only) + +Special morphisms and properties depend on each other in both directions. Classifying the monomorphisms may need limits or a suitable functor (e.g. a representable forgetful functor), and conversely properties such as `balanced`, `well-powered`, `mono-regular`, `CSP`, `normal`, or the generators often need the classification of monomorphisms or epimorphisms. Therefore, treat each open special morphism kind as one more candidate in the decision loop, alongside the unknown properties, and attempt it whenever its prerequisites are available. Do not force it early. + +- **Special morphisms**: the kinds are `isomorphisms`, `monomorphisms`, `epimorphisms`, `regular monomorphisms`, and `regular epimorphisms`. A kind is open if it is neither in the YAML nor deduced. Classify the morphisms of that kind, with a proof, in the `special_morphisms` record (fields `description` and `proof`). Follow the style of existing entries (e.g. [Top.yaml](../../../database/data/categories/Top.yaml), [Pos.yaml](../../../database/data/categories/Pos.yaml), [Grp.yaml](../../../database/data/categories/Grp.yaml)): for the trivial direction write "For the non-trivial direction, ...", and use "same as monomorphisms" / "same as isomorphisms" style descriptions where appropriate. A classification proof may use properties assigned earlier in the file, and a property proof may use the classification ("(see below)"). Skip a kind you cannot classify with a complete proof; it stays open. +- **Special objects**: whenever the category is known to have a terminal object, initial object, products, or coproducts (already at the start or proven along the way), add a short `description` to the `special_objects` record (keys `terminal object`, `initial object`, `products`, `coproducts`). These entries take no proof. + +## Decision loop + +Repeat until no unknown properties (and, for categories, no open special morphism kinds) are left, every remaining candidate has been attempted without success, or the time limit is exceeded: + +1. **List the unknowns**: run `pnpm db:structure unknown`. For categories, also re-run the `special_morphism_assignments` query from the preparation to see which special morphism kinds are still open (deduction may have filled some in). +2. **Pick one candidate**, i.e. an unknown property or an open special morphism kind, that you have not yet attempted, or that you skipped earlier but whose missing prerequisites have since been established. Keep a running list of skipped candidates with a one-line reason each, including what they are waiting for. Priority guidelines: + - Pick whatever is provable now with the knowledge at hand. If a candidate needs another fact first (a limit construction for a monomorphism classification, the epimorphisms for `balanced` or `CSP`, ...), work on that fact first, and come back afterwards. + - Prefer well-known, basic properties over exotic ones, and easy ones over hard ones. If a property is defined in terms of others, or the implications show that it requires others (e.g. `generalized variety` requires `sifted colimits`; `locally presentable` requires `cocomplete`), decide the simpler prerequisites first. + - Exception: if a strong, standard classification clearly applies and has a standard proof or citation (e.g. the category is obviously `one-sorted finitary algebraic`, a `Grothendieck topos`, `locally finitely presentable`, `abelian`, or `small` and `finite`), decide it early, because deduction then settles many other properties at once. Likewise, an easy failure of a weak property (e.g. no `binary products`, not `locally small`) refutes many stronger ones. + - For **categories**, a typical order, based on what existing files assign directly, is: + 1. size and shape: `locally small`, `small`, `essentially small`, `finite`, `countable`, `essentially countable`, `locally finite`, `skeletal`, `thin`, `groupoid`, `connected`, `semi-strongly connected`, `strongly connected`, `pointed`, `self-dual`; + 2. (co)limits: `terminal object`, `initial object`, `binary products`, `binary coproducts`, `equalizers`, `coequalizers`, `pullbacks`, `pushouts`, `complete`, `cocomplete`, `filtered colimits`, `sifted colimits`, `cofiltered limits`, `sequential colimits`; + 3. generators and special morphisms: `generator`, `cogenerator`, `extremal generator`, `extremal cogenerator`, `well-powered`, `well-copowered`, `balanced`, `mono-regular`, `epi-regular`, `normal`, `conormal`, `CIP`, `CSP`, `unital`, `counital`; + 4. exactness and structure: `regular`, `coregular`, `Malcev`, `co-Malcev`, `effective congruences`, `effective cocongruences`, `infinitary extensive`, `distributive`, `cartesian closed`, `locally cartesian closed`, `subobject classifier`, `regular subobject classifier`, `regular quotient object classifier`, `natural numbers object`, `preadditive`, `additive`, `abelian`, `split abelian`; + 5. advanced: `accessible`, `ℵ₁-accessible`, `finitely accessible`, `locally presentable`, `coaccessible`, `generalized variety`, `multi-algebraic`, `finitary algebraic`, `elementary topos`, `Grothendieck topos`, `total`, `cototal`, `exact filtered colimits`, `cartesian filtered colimits`, `cofiltered-limit-stable epimorphisms`, `filtered-colimit-stable monomorphisms`, `cocartesian cofiltered limits`, `ℵ₁-cofiltered limits`. + - For **functors**, start with `faithful`, `full`, `essentially injective`, `essentially surjective`, `conservative`, `left adjoint` / `right adjoint`, `representable`, and the preservation of monomorphisms, epimorphisms, initial and terminal objects, (co)products, and (co)equalizers, before `finitary` and more specialized preservation properties. For **morphisms**, start with `monomorphism`, `epimorphism`, `isomorphism`, `split monomorphism`, `split epimorphism`, `constant`, `coconstant`, `zero morphism`, then the regular, strong, extremal, strict, normal, and effective variants. For **symmetric monoidal categories**, start with `strict`, `cartesian`, `cocartesian`, `closed`, `well-pointed`, then the remaining ones. In doubt, sample a few files of the same type for typical orderings. +3. **Understand the property**: read its definition in `database/data/-properties/.yaml` (do not rely on memory; CatDat definitions can differ in details from the literature, e.g. regarding size conditions). Grep the property ID in the implication folder to see what implies it and what it implies. +4. **Look for templates**: grep the property ID in the structure folder of the same type (e.g. `database/data/categories/`) and read how similar structures prove or refute it. Reuse lemmas from `content/` instead of repeating their arguments. +5. **Prove or disprove it** mathematically, rigorously and completely, following "Writing proofs" in CLAUDE.md: state the key idea first, name morphisms with source and target, give concrete counterexamples for unsatisfied properties, link to other structures and content pages, and use labels and `references` when a proof builds on another proof. You may use properties of this structure that are already satisfied or deduced ("We already know that ...") and its special morphisms ("(see below)"). + - **Aim for the right generality, not an ad hoc argument.** Do not just aim to reach the goal. First find out which feature of the situation makes the claim true, and write the proof at that level, so that it also conveys why the claim holds: + - If a refutation works for every object or morphism with some property (e.g. every non-regular epimorphism, every non-finitely generated subobject), argue with an arbitrary one, and give a concrete instance only as an illustration. + - If a step is an instance of a general categorical fact (e.g. a regular epimorphism is the coequalizer of its kernel pair, fully faithful functors reflect (co)limits, a limit-preserving inclusion computes limits as in the ambient category), cite that fact. Do not recompute it with elements in the specific category. + - Do as little manual work as possible: reduce to properties, classifications, and proofs already established (in this file, related structures, implications, or `content/` lemmas) before computing anything by hand. Repeating an element computation that another proof in the file already does is a sign that you missed a reduction. + - If the same general argument applies to several structures, mention in the summary that it could become a `content/` lemma. + - Before writing anything, check your argument adversarially: test degenerate cases (empty objects, identities, zero morphisms, coinciding elements), check every map is a morphism of this category, and check both directions of every "if and only if". + - Only write a proof you are confident is correct. If you are not confident, or the proof would require a substantial new result you cannot establish, do **not** guess: add the property to the skipped list with a note on what you tried and go to the next property. A wrong claim is far worse than an open one. +6. **Record the result** in the YAML file: + - satisfied → `satisfied_properties`; unsatisfied → `unsatisfied_properties`; + - `undecidable_properties` (rare): only with a proof that the answer depends on the parameters of the structure (e.g. "This holds if and only if $G$ is countable.") or that the question is independent of ZFC. + - Insert the entry at a sensible position: easy and trivial properties first, closely related properties grouped together (see "Order of assignments" in CLAUDE.md), not necessarily at the end. Create the list key if it does not exist yet (e.g. `unsatisfied_properties: []` must become a proper list). + - Do not add `check_redundancy: false` when recording an entry, even if the template you adapted has it. The flag is only set in the redundancy phase, for an assignment that the redundancy script actually reports. + - Use `>-` with blank lines between paragraphs for long proofs, single quotes for values containing `:`, existing macros, and the notation conventions from CLAUDE.md (`\varnothing`, `f : X \to Y`, `\coloneqq`, `non-empty`). Very long or reusable arguments may go into a new `content/` page, but prefer proofs inside the YAML file. +7. **Run `pnpm db:update` after every single proof**, so that new properties are deduced before the next pick. Then continue with step 1; deduction often decides many further properties at once. + - If seeding fails, fix the YAML syntax or schema error. + - If deduction reports a **contradiction**, the new claim conflicts with the existing data. Remove the new entry, re-examine the argument, and re-run `pnpm db:update`. If you remain convinced the new claim is right, leave it out and report the suspected inconsistency (with the conflicting implications or assignments) to the user instead of changing other files. + - If `db:test` fails because of this structure, report it; do not edit `expected-data/`. +8. Whenever a new (co)limit property is proven, also add the corresponding special object description (see above). Steps 3 to 7 apply in the same way to special morphism classifications. + +Edit only the target structure file, plus new `content/` pages if really needed and `.cspell.json` for legitimate new words. Never edit other structures, properties, implications, or `expected-data/`, and never edit the database directly. Do not commit. + +## Redundancy phase + +After the loop ends (also when the time limit was reached, since this phase is quick and leaves the file clean): + +1. Run `pnpm db:redundancies` and look for lines mentioning this structure (`for :`). The script reports at most one redundant satisfied and one redundant unsatisfied assignment per structure. +2. For a redundant **satisfied** assignment: keep it with `check_redundancy: false` if the proof is illuminating, constructs (co)limits used later, establishes an intermediate result used by later proofs, or avoids an overly complex deduction (see "No redundant assignments" in CLAUDE.md). Otherwise remove it. +3. For a redundant **unsatisfied** assignment: almost always remove it. +4. Before removing an entry, grep the file for its `label` and for phrases like "we already know"; if another proof relies on it, either keep the entry (with `check_redundancy: false`) or adjust the dependent proof and its `references`. +5. Run `pnpm db:update`, then `pnpm db:redundancies` again. Repeat until no redundancy for this structure is reported. +6. Test every `check_redundancy: false` flag in the file, one at a time: remove the flag, run `pnpm db:update` and `pnpm db:redundancies`. If the script does not report that assignment as redundant, the flag was unnecessary: keep it removed. Only restore the flag if the assignment is reported and should be kept (see step 2). + +Finally, run `pnpm cspell` and fix spelling issues in the target file (add legitimate mathematical terms to `.cspell.json`). + +## Summary + +End with a summary for the user: + +- **Counts** before and after (from `pnpm db:structure `): satisfied, unsatisfied, undecidable, unknown. +- **Decided in this run**: the properties added directly to the YAML file, grouped into satisfied, unsatisfied, and undecidable, and the number of properties that were deduced from them. For categories, the special objects and special morphisms that were added. +- **Redundancies**: which assignments were removed and which were kept with `check_redundancy: false` (and why). +- **Still unknown**: each remaining unknown property (and unclassified special morphism kind), with a short note on what was tried, why it was hard, or whether the time limit stopped the run. These are left open for further investigation. +- **Difficulty estimate**: a rough overall rating of how easy the proofs were, and a short list of the proofs that were involved (multi-step constructions, delicate counterexamples), relied on external citations, or used non-trivial theorems from other branches of mathematics (e.g. set theory, general topology, commutative algebra, group theory). Name the theorem in each case. +- A reminder that all proofs were written by AI and must be checked thoroughly by the contributor before submission, who must understand every argument and verify every claim, link, and citation (CONTRIBUTING.md). Point out claims that most need checking (e.g. citations that could not be verified), and suggest running `/check-proofs` on the file. diff --git a/.github/skills/check-proofs-file/SKILL.md b/.github/skills/check-proofs-file/SKILL.md deleted file mode 100644 index f28fd48ab..000000000 --- a/.github/skills/check-proofs-file/SKILL.md +++ /dev/null @@ -1,30 +0,0 @@ ---- -name: check-proofs-file -description: Review every mathematical proof in the active CatDat YAML data file or Markdown content page. Use when asked to check or review proofs in CatDat files. -argument-hint: '[optional focus or mathematical context]' -user-invocable: true -disable-model-invocation: true ---- - -# Check Proofs - -Review every proof in the active CatDat data file or content page. Supported files are YAML under `database/data/` and Markdown under `content/`. Review the entire file, not only the selection. If the user provides additional context after the command, consider it without narrowing the review unless requested. - -## Procedure - -1. Identify the active file from the editor context. Accept YAML files under `database/data/` and Markdown files under `content/`. If it is outside these locations or its identity is ambiguous, ask the user to open or provide the intended file rather than guessing. -2. Read the whole file and locate every proof using its format: - - In YAML, find every `proof` field, including fields nested in property assignments, implications, special morphisms, and other records, as well as block scalars and quoted multiline values. Associate each proof with its enclosing record and claim. - - In Markdown content pages, find every `::: Proof` directive block, from its opening line through the closing `:::`. Associate it with the preceding claim or statement block, which may be introduced by directives such as `::: Lemma`, `::: Proposition`, `::: Corollary`, or `::: Claim`. Preserve the distinction between the claim and its proof; do not mistake ordinary prose or displayed equations outside a proof block for a proof. -3. Assess each argument against the definitions, hypotheses, and prior steps stated in the file. Check that inferences are valid, important cases and edge conditions are handled, cited results support the claims, and the conclusion proves the associated claim. Do not silently supply missing assumptions or lemmas. Before accepting a proof, make a separate adversarial pass: check that every map and equation has the stated source and target; test degenerate cases such as equal variables, empty or singleton objects, zero or identity morphisms, and boundary values; and verify that constructions used to distinguish cases are well-defined morphisms satisfying all required conditions. In particular, when a proof handles arbitrary elements or pairs, check whether they may coincide, and when it claims a classification or universal property, test both directions and small counterexamples. -4. Use relevant repository context when a proof depends on a local definition or referenced CatDat entry. Keep the assessment grounded in available sources; flag context that cannot be checked. - - Prefer opening a known source file directly, especially when a CatDat link or entry ID identifies it. For content links, check the matching Markdown file under `content/`; for data entries, locate the YAML source under the appropriate `database/data/` directory. Do not rely on generated files under `build/`. - - When the path is unknown, search only the relevant source directory (`content/` or `database/data/`) with one short, distinctive plain-text term or the entry's filename/ID. Avoid long LaTeX expressions, complex regular expressions, and queries combining many alternatives. - - If search reports no matches or says the pattern may be excluded, treat that as an inconclusive search, not evidence that the reference is absent. Check the intended source path/file list, then retry with a simpler term or exact filename. Only report that context is unavailable after these checks fail; do not attribute a miss to ignore settings unless those settings actually exclude the source directory. -5. Do not edit files, suggest or apply fixes unless separately asked, run commands, or invoke database update workflows. - -## Report - -Start with an overall assessment. Then list actionable findings, each identified by the YAML record/property and `proof` field or by the Markdown claim and `::: Proof` block (include line numbers when available). For each finding, state severity (`major`, `minor`, or `uncertain`), the specific step or omission, and why it affects the argument. Distinguish a demonstrated logical gap from missing context or uncertainty. Avoid reporting style preferences as mathematical errors. - -If no actionable issue is found, say so, but make clear that this is an AI review and not a proof of correctness. Do not claim formal verification or certainty. The author remains responsible for checking the argument and writing the final proof in their own words, consistent with CatDat's contribution guidance. diff --git a/.github/skills/check-proofs-folder/SKILL.md b/.github/skills/check-proofs-folder/SKILL.md deleted file mode 100644 index 3393e20f5..000000000 --- a/.github/skills/check-proofs-folder/SKILL.md +++ /dev/null @@ -1,29 +0,0 @@ ---- -name: check-proofs-folder -description: Review every mathematical proof in YAML and Markdown files directly inside a specified folder. Use when asked to check proofs across a folder. -argument-hint: -user-invocable: true -disable-model-invocation: true ---- - -# Check Proofs in a Folder - -Review every proof in all eligible files directly inside the folder specified by the user. Include `.yaml`, `.yml`, and `.md` files. Do not process files in subfolders. If the folder path is missing or ambiguous, ask the user to specify it before proceeding. - -## Procedure - -1. Resolve the specified folder and list its immediate entries only. Do not traverse or inspect subfolders. -2. Select only files with `.yaml`, `.yml`, or `.md` extensions. Ignore all other file types. -3. Read each selected file in full and locate every proof using its format: - - In YAML, find every `proof` field, including fields nested in property assignments, implications, special morphisms, and other records, as well as block scalars and quoted multiline values. Associate each proof with its enclosing record and claim. - - In Markdown content pages, find every `::: Proof` directive block, from its opening line through the closing `:::`. Associate it with the preceding claim or statement block, which may be introduced by directives such as `::: Lemma`, `::: Proposition`, `::: Corollary`, or `::: Claim`. Preserve the distinction between the claim and its proof; do not mistake ordinary prose or displayed equations outside a proof block for a proof. -4. Assess every argument against definitions, hypotheses, and prior steps in its file. Check whether inferences follow, important cases are justified, references support the claims, and conclusions establish their associated claims. Do not silently supply missing assumptions or lemmas. -5. Make a separate adversarial pass over each proof before accepting it: check that every map and equation has the stated source and target; test degenerate cases such as equal variables, empty or singleton objects, zero or identity morphisms, and boundary values; and verify that constructions used to distinguish cases are well-defined morphisms satisfying all required conditions. In particular, when a proof handles arbitrary elements or pairs, check whether they may coincide, and when it claims a classification or universal property, test both directions and small counterexamples. -6. Use relevant repository context when a proof depends on a local definition or referenced CatDat entry. Prefer opening a known source file directly. For an unknown path, search only the relevant source directory with one short, distinctive plain-text term or exact filename/ID; avoid long LaTeX expressions, complex regular expressions, and queries with many alternatives. Treat a no-match or exclusion warning as inconclusive: verify the intended path and retry with a simpler term before reporting context unavailable. Do not rely on generated files under `build/`. -7. Do not edit files, suggest or apply fixes unless separately asked, run commands, or invoke database update workflows. Keep the review scope to eligible files directly inside the specified folder; read a supporting file outside it only when needed to verify a cited definition or result. - -## Report - -Start with an overall assessment and state how many eligible files were reviewed. List actionable findings grouped by file. Identify each finding by YAML record/property and `proof` field, or by Markdown claim and `::: Proof` block; include line numbers when available. For each finding, give severity (`major`, `minor`, or `uncertain`), the specific issue, and why it affects the argument. Distinguish a demonstrated logical gap from missing context or uncertainty. Do not report style preferences as mathematical errors. - -If no actionable issues are found, say so, but make clear that this is an AI review and not a proof of correctness. Do not claim formal verification or certainty. Authors remain responsible for checking arguments and writing final proofs in their own words, consistent with CatDat's contribution guidance. diff --git a/.github/skills/proofread-file/SKILL.md b/.github/skills/proofread-file/SKILL.md deleted file mode 100644 index 1eac799d5..000000000 --- a/.github/skills/proofread-file/SKILL.md +++ /dev/null @@ -1,28 +0,0 @@ ---- -name: proofread-file -description: Proofread and directly fix spelling, grammar, and clear notation typos in the currently open file. Use when asked to proofread, correct, or lightly polish the active file. -user-invocable: true -disable-model-invocation: true ---- - -# Proofread File - -Proofread the entire currently active editor file, not only the selection, and apply clear corrections directly. Work on the active editor buffer, including unsaved changes. Keep the active file as the focus of proofreading; you may read another file when directly relevant context is needed. - -## Scope - -- Correct genuine spelling, grammar, punctuation, and typographical mistakes in prose, comments, and human-readable string values. -- Support common source formats such as YAML, Markdown, Svelte, and TypeScript. In structured or code files, edit only human-language text and obvious text typos; preserve keys, identifiers, APIs, program behavior, markup, interpolation, and syntax. -- In mathematical notation, correct only an obvious local typo, such as a variable name that inconsistently changes from `$a$` to `$x$` where the surrounding text makes the intended symbol unambiguous. Preserve formulas and claims otherwise. -- Do not assess or correct the mathematical validity of proofs. That is the role of `/check-proofs-file`. Language mistakes inside proof text may still be corrected without changing the mathematical argument. -- Make stylistic changes sparingly. Only adjust wording when it is clearly awkward or ambiguous and a small change improves readability while preserving the author's meaning and voice. Prefer leaving acceptable personal style alone. - -## Boundaries - -- Keep all edits confined to the active file. Do not broaden the proofreading scope or modify supporting files. -- Do not reformat unrelated content, change meaning, rewrite whole passages, or make speculative edits. When a correction is not unambiguous, leave it as written. -- Apply the clear corrections directly to the active file. Do not modify any other file or create a separate report file. - -## Response - -Briefly summarize the types of corrections made. If nothing needed correction, say so. Mention any potentially problematic wording or notation you left unchanged because intent was unclear, without proposing mathematical proof changes. diff --git a/.github/skills/proofread-folder/SKILL.md b/.github/skills/proofread-folder/SKILL.md deleted file mode 100644 index 87ab74e31..000000000 --- a/.github/skills/proofread-folder/SKILL.md +++ /dev/null @@ -1,36 +0,0 @@ ---- -name: proofread-folder -description: Proofread and directly fix spelling, grammar, and clear notation typos in YAML and Markdown files directly inside a specified folder. Use when asked to proofread multiple files in one folder. -argument-hint: -user-invocable: true -disable-model-invocation: true ---- - -# Proofread Folder - -Proofread all YAML and Markdown files directly inside the folder specified by the user, and apply clear corrections directly. Include `.yaml`, `.yml`, and `.md` files. Do not process files in subfolders. If the folder path is missing or ambiguous, ask the user to specify it before proceeding. - -## Scope - -- Correct genuine spelling, grammar, punctuation, and typographical mistakes in prose, comments, and human-readable string values. -- In YAML and Markdown, edit only human-language text and obvious text typos. Preserve YAML keys, Markdown structure, identifiers, markup, links, interpolation, and syntax. -- In mathematical notation, correct only an obvious local typo, such as a variable name that inconsistently changes from `$a$` to `$x$` where the surrounding text makes the intended symbol unambiguous. Preserve formulas and claims otherwise. -- Do not assess or correct the mathematical validity of proofs. That is the role of `/check-proofs-folder`. Language mistakes inside proof text may still be corrected without changing the mathematical argument. -- Make stylistic changes sparingly. Only adjust wording when it is clearly awkward or ambiguous and a small change improves readability while preserving the author's meaning and voice. Prefer leaving acceptable personal style alone. - -## Procedure - -1. Resolve the user-specified folder and list its immediate files only. Do not traverse or inspect subfolders. -2. Select only files with `.yaml`, `.yml`, or `.md` extensions. Ignore all other file types. -3. Read and proofread each selected file in full. If a file has unsaved editor changes, preserve and work from those changes rather than replacing them with an older on-disk version. -4. Apply only unambiguous corrections to the selected files. If context from outside the specified folder is necessary to decide whether wording or notation is correct, leave it unchanged rather than expanding the read scope. - -## Boundaries - -- Read and edit only eligible files directly inside the specified folder. Do not touch files outside it, files in nested folders, or unsupported file types. -- Do not reformat unrelated content, change meaning, rewrite whole passages, or make speculative edits. When a correction is not unambiguous, leave it as written. -- Do not create report files or modify any other files. - -## Response - -Briefly list the files changed and summarize the types of corrections made. Also list eligible files that needed no changes. Mention any unclear wording or notation left untouched, without proposing mathematical proof changes. diff --git a/CLAUDE.md b/CLAUDE.md new file mode 100644 index 000000000..b050199fd --- /dev/null +++ b/CLAUDE.md @@ -0,0 +1,133 @@ +# CatDat + +_CatDat_ ([catdat.app](https://catdat.app)) is a searchable database of categorical structures and their properties, built by and for people who love category theory. It is an open-source community project. + +Four types of categorical structures are supported: **categories**, **functors**, **morphisms**, and **symmetric monoidal categories** (`STRUCTURE_TYPES` in [shared/config.ts](shared/config.ts)). The data has three kinds of entries: + +- **Structures**: e.g. `Set`, `Grp`, the abelianization functor. Each has a definition, satisfied and unsatisfied properties with proofs, and related structures. +- **Properties**: e.g. "cocomplete", "cartesian closed", "left adjoint". Each property belongs to one structure type. +- **Implications**: e.g. "abelian ⟹ regular", each with a proof. + +From the implications, a **deduction system** infers further properties of each structure and **dualizes** implications and property assignments automatically. The app has detail pages for structures, properties, and implications, a search for structures by satisfied and unsatisfied properties (which also detects inconsistent combinations), a comparison of structures, and a page that lists missing data (`/missing`). Long-form proofs and lemmas are Markdown pages in [content/](content/), rendered at `/content/`. + +The admin functionality is in a separate repository, [CatDatAdmin](https://github.com/ScriptRaccoon/CatDatAdmin). + +## Tech stack + +TypeScript, SvelteKit (Svelte 5), SQLite via `better-sqlite3`, KaTeX for math rendering, Playwright for end-to-end tests, Netlify for deployment, pnpm as package manager. Most pages are prerendered at build time; only the search and comparison pages are dynamic. See [DEPLOYMENT.md](DEPLOYMENT.md). + +## Repository layout + +- [database/data/](database/data/): **the source of truth.** YAML files for all structures, properties, and implications, one folder per kind and type (e.g. `categories/`, `category-properties/`, `category-implications/`, `functors/`, ...), plus `config.yaml` (tags, relations, special object and morphism kinds), `macros.yaml` (KaTeX macros), and `special-morphism-rules.yaml`. +- [database/schema/](database/schema/): SQL schema files, applied in order of their `NNN_` prefix. +- [database/scripts/](database/scripts/): the `db:*` scripts (seeding, deduction, tests). `expected-data/` holds the expected property data used by `db:test`. +- [shared/](shared/): code used by both the database scripts and the app (`$shared/*` alias), e.g. the DB client and the structure type config. `structure.history.json` records when each structure was added; `db:seed` updates it, and the homepage reads it for "Recently added structures". +- [src/](src/): the SvelteKit app. Routes are generic over the structure type (`src/routes/[type]`, `[type]-property`, `[type]-implication`, `[type]-search`, ...). Page components are in `src/pages/`, shared components in `src/components/`, server-side DB access in `src/lib/server/`. +- [content/](content/): Markdown content pages for long proofs and reusable lemmas. +- [tests/](tests/): Playwright end-to-end tests. + +## Commands + +General: + +- `pnpm dev`: start the dev server. +- `pnpm build` / `pnpm preview`: build and preview the production app. +- `pnpm check`: run the Svelte and TypeScript checks (also runs as a pre-push hook). +- `pnpm format` / `pnpm lint`: format with Prettier / check formatting. +- `pnpm cspell`: spell-check `content/` and `database/`. +- `pnpm e2e`: run the Playwright end-to-end tests (`e2e:debug` and `e2e:ui` are variants). + +Database (all scripts run with `tsx` using [database/tsconfig.json](database/tsconfig.json)): + +- `pnpm db:setup`: delete `database/catdat.db` and recreate it from the SQL schema files. It also stores a hash of the schema in `database/schema/schema.json`. Required after any schema change; `db:seed` aborts if the schema hash is outdated. +- `pnpm db:seed`: clear all data and insert the entries parsed from the YAML files (validated with `valibot` schemas in `database/scripts/utils/seed.schemas.ts`). +- `pnpm db:deduce`: for each structure type, dualize implications and deduce satisfied and unsatisfied properties (for categories also special objects and morphisms). Deduced rows are marked with `is_deduced`. +- `pnpm db:test`: check data quality: properties and their duals are mutual, structures and their duals are mutual, all properties are decided for the structures listed in `expected-data/decided-*.json`, and the properties of selected structures (`Set`, `Ab`, `Top`, ...) exactly match `expected-data/`. +- `pnpm db:snapshot`: copy the database to `static/databases/catdat-snapshot.db` for the download page. +- `pnpm db:update`: run `db:seed`, `db:deduce`, `db:test`, and `db:snapshot` in sequence. **This is the standard command after editing any YAML data.** Use `--watch` to rerun it whenever a file in `database/data/` changes. +- `pnpm db:text`: fast path for text-only changes to existing structures (names, notations, descriptions, nLab links, proofs). It updates changed fields without rebuilding relations or running deductions. Properties and implications are not covered. Supports `--watch`. +- `pnpm db:redundancies`: report property assignments that could already be deduced from others. It reports at most one per structure and kind, so rerun it after each removal. Not part of `db:update`. +- `pnpm db:combinations [ ...]`: list the combinations p ∧ ¬q that the given structures (or their duals) witness and that no other structure in the database witnesses. Needs only the IDs, not the type (all IDs must have the same type). Useful to judge whether a structure adds new information. +- `pnpm db:structure [group]`: print the property IDs of a structure, grouped into `satisfied`, `unsatisfied`, `unknown`, and `undecidable` with counts (a terminal version of the structure detail page). An optional group argument restricts the output to that group, e.g. `pnpm db:structure Ab unsatisfied`. Needs only the ID, not the type. +- `pnpm db:shell`: open a `sqlite3` shell on the local database. + +First-time setup: `pnpm install`, `pnpm db:setup`, `pnpm db:update`, `pnpm dev`. Neither `database/catdat.db` nor the snapshot is committed; both are generated. + +## Database + +The SQLite database `database/catdat.db` is generated entirely from the YAML files and is **read-only at runtime**. Never edit the database directly; change the YAML files (or the schema) and regenerate. User submissions and page visits are stored in a separate database (`app.db`, hosted on Turso), which is unrelated to the data scripts. See [DATABASE.md](DATABASE.md) for details. + +Main tables (full schema in [database/schema/](database/schema/)): + +- `structure_types`: the four types. Most tables carry a `type` column, and composite foreign keys `(id, type)` ensure that, for example, a category property is only assigned to categories. +- `structures`: data common to all structures (`id`, `type`, `name`, `notation`, `description`, `nlab_link`, `dual_structure_id`, `parent_structure_id`). The `categories` table adds `objects` and `morphisms` for categories. +- `structure_associations` / `associated_structures`: typed links between structures, e.g. a functor's `domain`, `codomain`, `left_adjoint`, `right_adjoint`, a morphism's `category`, or a symmetric monoidal category's `underlying_category`. +- `properties`: primary key `(id, type)`, with a `relation` ("is", "has", "preserves", ...), `description`, `dual_property_id`, and `invariant_under_equivalences`. +- `property_assignments`: links structures to properties with `is_satisfied` (TRUE, FALSE, or NULL for undecidable), `proof`, `is_deduced`, `check_redundancy`, and an optional `label`. Proofs can cite labeled assignments, recorded in `proof_references`. +- `implications`, `assumptions`, `conclusions`: implications between properties of one type, with `is_equivalence`, `is_deduced`, and `dual_implication_id`. The `implications_view` view combines them into JSON arrays. +- `associated_assumptions`: implication assumptions about associated structures, e.g. a functor implication that requires the domain category to be complete. +- `special_objects` / `special_object_assignments` and `special_morphisms` / `special_morphism_assignments` / `special_morphism_rules`: special objects (terminal, initial, products, coproducts) and special morphisms (isos, monos, epis, regular monos and epis) of categories. +- Additional tables: tags (`structure_tags`, `property_tags`, and their assignment tables), `related_structures`, `related_properties`, `structure_comments`, `relations`. + +The YAML files never contain derived data. Everything marked `is_deduced` is produced by `db:deduce`. + +## YAML data format + +Use existing files as templates: [database/data/categories/N.yaml](database/data/categories/N.yaml) for categories, [database/data/functors/abelianization.yaml](database/data/functors/abelianization.yaml) for functors, `category-properties/*.yaml` for properties (one property per file), and `category-implications/*.yaml` for implications (a list of related implications per file). Property and structure references in YAML use the human-readable property ID, e.g. `finitely cocomplete`. + +- String values may contain HTML (``, ``, `
    `, ...) and KaTeX math (`$...$`, `$$...$$`). +- Use single quotes for values that contain `:`, and escape a literal single quote as `''`. +- Use `>-` for multiline text rendered as one paragraph, and `|-` when line breaks should be kept (rendered as `
    `). +- Set `check_redundancy: false` on a satisfied property assignment that is redundant but deliberately kept (see below). + +## Contribution guidelines + +Full guidelines: [CONTRIBUTING.md](CONTRIBUTING.md). Contributions come in through the suggestion form on the site, GitHub issues, or pull requests from forks. The essentials for data changes: + +- **Proofs for every claim**: satisfied and unsatisfied properties, implications, and special morphisms all need a proof or reference. If a proof refers to another proof, make the link explicit with labels and references. Move very long proofs or reusable lemmas into a `content/` page and link to it. +- **Reduce unknowns**: when adding a structure, decide as many of its properties as possible. When adding a property, try to decide it for all existing structures, and include implications connecting it to existing properties. For the structures in `expected-data/decided-*.json`, deciding every property is mandatory (enforced by `db:test`). +- **No redundant assignments**: only assign properties that cannot be deduced. Redundant satisfied assignments may be kept when the proof is trivial anyway, insightful, constructs (co)limits used later, avoids an overly complex automatic deduction, or establishes an intermediate result used later. Mark them with `check_redundancy: false`. Removing redundant assignments is not required but recommended, especially for unsatisfied properties. +- **Atomic implications**: do not add implications that follow from others, and do not add dual implications, since dualization is automatic. Prefer the "limit" variant over the "colimit" variant. When adding an implication, check whether it simplifies existing ones. +- **Positive properties only**: never add negated properties (e.g. "large" for "not small"); record them as unsatisfied instead. Every category property must hold for the trivial category, and every functor property must hold for identity functors. +- **Counterexamples**: every new property needs at least one structure that does not satisfy it. If none exists yet, add one. +- **No duplicates**: do not add the dual of an existing category (assign the dual properties to the original instead), and do not add categories equivalent or isomorphic to existing ones, except when this matters for non-invariant properties such as being skeletal. +- **Special objects and morphisms**: for each new category, try to specify its special objects and special morphisms. +- **Order of assignments**: assignments are shown in file order, so list trivial and easy properties first and group closely related ones. +- **New combinations**: structures that witness new consistent combinations p ∧ ¬q are especially valuable (see `/missing` and `db:combinations`). +- **Small pull requests**: one focused change per PR, roughly no more than four new properties or structures. + +Writing and notation conventions: + +- Write `non-empty`, `non-unital`, `non-expansive` (with a hyphen). +- Use `\varnothing` (not `\emptyset`), `f : X \to Y` (not `\colon`), and `\coloneqq` (not `:=`). +- Define recurring LaTeX notation as a macro in [database/data/macros.yaml](database/data/macros.yaml) (e.g. `\IN`, `\Grp`, `\Ab`). +- Run `pnpm cspell` after editing text, and add legitimate new words to `.cspell.json`. + +Responsible use of AI (from CONTRIBUTING.md): AI-generated code and data (including proofs) are accepted if they are readable, understandable, and checked thoroughly by the human author, who must understand every line and argument and takes responsibility for every claim, link, and citation; PR descriptions and commit messages must be written manually. + +## Writing proofs + +Proofs are written for professional mathematicians. Readers are expected to know groups, rings, modules, topological spaces, and basic category theory (limits, adjunctions, the Yoneda lemma, ...), so standard facts from these areas need no proof. More specialized notions should be defined or linked. + +Content: + +- **Self-contained**: a reader should be able to follow the proof using only the structure's description, the property's definition, and the pages the proof links to. Prefer a direct argument to a bare citation. When citing a source, consider adding a direct argument as well ("Alternatively, here is a direct proof: ..."). Citing alone is fine for deep or standard theorems, such as the Special Adjoint Functor Theorem. +- **Easy to understand**: state the claim or key idea first, then the details ("We claim that ... To see this, ..."). Name objects and morphisms explicitly with source and target (`f : X \to Y`). For unsatisfied properties, give a concrete counterexample (e.g. "the embedding $C_2 \hookrightarrow S_3$") rather than an existence argument, whenever possible. +- **Complete**: do not skip steps. Phrases like "It is easy to see" or "clearly" are only for exceptional cases, namely steps that are routine for the intended reader. One-line proofs such as "This is trivial." or "This holds by definition." are only for claims that follow immediately from the definitions. +- **Classifications and equivalences**: when one direction is immediate, prove only the other one and say so ("For the non-trivial direction, ..."), as in most special-morphism proofs. In content pages, mark the two directions with `($\Rightarrow$)` and `($\Leftarrow$)`. +- **Building on known facts**: a proof may use properties of the same structure that are assigned earlier in the file or deduced from them ("We already know that ..."), as well as its classification of special morphisms ("(see below)"). Results about other structures may be used with a link to them. If a proof depends on the proof of another assignment, give that assignment a `label` of the form `_` (e.g. `grp_no_cogenerator`) and list the label under `references`. +- **Reuse instead of repetition**: put general lemmas in `content/` pages instead of repeating an argument in several YAML files, and apply them explicitly, e.g. "apply the contrapositive of the dual of Lemma 2     here to the forgetful functor $\Ab \to \Grp$". + +Format: + +- Write in full sentences, using "we". Introduce notation with `\coloneqq`, and use `$$...$$` for displayed formulas. In long YAML proofs, use a `>-` block and separate paragraphs with a blank line. +- Internal links in YAML: structures as `$\Set$` (with the notation as link text), properties as `...`, and content pages as `here` or `this lemma`. +- External links in YAML get `target="_blank"` and point to a specific result: `See Prop. 4.2 at the nLab.`, `MSE/601463` (`MO/...` for MathOverflow), and books with the author as link text followed by the location, e.g. `Mac Lane, Ch. V, Theorem 5.1`. +- Content pages are Markdown with `title` and `description` in the front matter and use Markdown links. Statements go in blocks such as `::: Lemma 1` (also `Proposition`, `Corollary`, `Claim`), closed by `:::`, followed by a `::: Proof` block. Do not state the dual version of a result unless it is used often (as for Lemma 2 in [content/subcategories.md](content/subcategories.md)). + +## Workflow after changing data + +1. Edit the YAML files in `database/data/` (or the `content/` pages). +2. Run `pnpm db:update`, or `pnpm db:text` for text-only structure changes. If the schema changed, run `pnpm db:setup` first. +3. If `db:update` fails, the cause is usually malformed YAML or a schema validation error, a contradiction found during deduction, or a failing data-quality test. +4. Optionally run `pnpm db:redundancies`, and run `pnpm cspell`. diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index e129c67e1..42f5c1c6c 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -180,13 +180,11 @@ As a practical guideline, avoid introducing more than four properties (or four c ### Responsible Use of AI -AI tools may be used to assist with development in this repository, but not to replace the act of programming. +AI tools may be used for both code and data in this repository, as long as a human author takes full responsibility for the result. -- Use AI to support your workflow (e.g. by asking questions, getting suggestions, or creating snippets), not to generate complete features or large portions of code without your active involvement. -- AI agents that autonomously generate or modify code are not allowed. Pull requests that are mainly written by AI agents will be closed. -- AI can also be used to find proofs for properties of categorical structures, but they must be checked thoroughly and written in your own words. +- AI-generated code and data (proofs, structures, properties, implications) are accepted as long as they are readable, understandable, and have been checked thoroughly by you. +- You are the author: you must understand every line of code and every argument and be able to explain them, check every claim, link, and citation, and fix anything that is unclear, incomplete, or wrong before submitting it. - AI may also be used to improve English writing (e.g. grammar, clarity, phrasing), particularly if you are not a native speaker. -- Every line of code in a pull request must be understood by the person submitting it. - Pull request descriptions and commit messages must be written manually. AI-generated summaries are often superficial, meaningless, and do not tell the whole story. In summary, treat AI as a productivity tool, not as a substitute for understanding or authorship. diff --git a/DATABASE.md b/DATABASE.md index 269585207..c7c2bff54 100644 --- a/DATABASE.md +++ b/DATABASE.md @@ -107,6 +107,16 @@ pnpm db:redundancies to check for redundant assignments of properties to categorical structures. +## Properties of a structure + +Use the command + +``` +pnpm db:structure [group] +``` + +to list the satisfied, unsatisfied, unknown, and undecidable properties of a structure in the terminal, grouped as on its detail page. Pass one of these groups as a second argument to list only that group. + ## Diagram This is the database schema as of 18.09.2026; changes may occur. diff --git a/database/scripts/combinations.ts b/database/scripts/combinations.ts index c289ec628..5f67616c3 100644 --- a/database/scripts/combinations.ts +++ b/database/scripts/combinations.ts @@ -1,5 +1,5 @@ import { get_client } from '$shared/db' -import { is_structure_type, type StructureType } from '$shared/config' +import type { StructureType } from '$shared/config' import { remove_underscores } from '$shared/utils' /** @@ -10,19 +10,20 @@ import { remove_underscores } from '$shared/utils' const db = get_client({ readonly: true }) -const args = process.argv.slice(2) +const structure_ids = process.argv.slice(2) -const [type, ...structure_ids] = args - -if (!type || structure_ids.length === 0) { - console.error( - 'Expected arguments: ...' - ) +if (structure_ids.length === 0) { + console.error('Expected arguments: ...') process.exit(1) } -if (!is_structure_type(type)) { - console.error(`Unknown structure type: ${type}`) +const type = db + .prepare<[string], StructureType>(`SELECT type FROM structures WHERE id = ?`) + .pluck() + .get(structure_ids[0]) + +if (!type) { + console.error(`No structure with ID "${structure_ids[0]}" exists in the database.`) process.exit(1) } diff --git a/database/scripts/structure.ts b/database/scripts/structure.ts new file mode 100644 index 000000000..bb42bf773 --- /dev/null +++ b/database/scripts/structure.ts @@ -0,0 +1,89 @@ +import { get_client } from '$shared/db' +import type { StructureType } from '$shared/config' + +/** + * This script prints the satisfied, unsatisfied, unknown, and undecidable + * properties of the supplied structure, similar to its detail page. + */ + +const db = get_client({ readonly: true }) + +const GROUPS = ['satisfied', 'unsatisfied', 'unknown', 'undecidable'] as const + +type Group = (typeof GROUPS)[number] + +const [id, group] = process.argv.slice(2) + +if (!id) { + console.error(`Expected arguments: [${GROUPS.join(' | ')}]`) + process.exit(1) +} + +if (group && !is_group(group)) { + console.error(`Unknown group: ${group}. Expected one of: ${GROUPS.join(', ')}`) + process.exit(1) +} + +const type = db + .prepare<[string], StructureType>(`SELECT type FROM structures WHERE id = ?`) + .pluck() + .get(id) + +if (!type) { + console.error(`No structure with ID "${id}" exists in the database.`) + process.exit(1) +} + +const assignments = db + .prepare<[string], { id: string; is_satisfied: 0 | 1 | null }>( + `SELECT pa.property_id AS id, pa.is_satisfied + FROM property_assignments pa + WHERE pa.structure_id = ? + ORDER BY pa.id` + ) + .all(id) + +const unknown_properties = db + .prepare<[StructureType, string], string>( + `SELECT p.id + FROM properties p + WHERE p.type = ? + AND NOT EXISTS ( + SELECT 1 FROM property_assignments + WHERE structure_id = ? AND property_id = p.id + ) + ORDER BY lower(p.id)` + ) + .pluck() + .all(type, id) + +const groups: Record = { + satisfied: assignments.filter((a) => a.is_satisfied === 1).map((a) => a.id), + unsatisfied: assignments.filter((a) => a.is_satisfied === 0).map((a) => a.id), + unknown: unknown_properties, + undecidable: assignments.filter((a) => a.is_satisfied === null).map((a) => a.id) +} + +const selected_groups: readonly Group[] = group ? [group as Group] : GROUPS + +const output = selected_groups + .map((label) => + [ + `${label} (${groups[label].length}):`, + ...groups[label].map((property_id) => ` ${property_id}`) + ].join('\n') + ) + .join('\n') + +// ignore a closed pipe, e.g. when the output is piped into head +process.stdout.on('error', (err: NodeJS.ErrnoException) => { + if (err.code !== 'EPIPE') throw err +}) + +console.info(output) + +// Helper functions + +function is_group(value: string): value is Group { + return (GROUPS as readonly string[]).includes(value) +} diff --git a/package.json b/package.json index 995dbdf7d..93b1b9c31 100644 --- a/package.json +++ b/package.json @@ -25,6 +25,7 @@ "db:update": "tsx --tsconfig database/tsconfig.json database/scripts/update.ts", "db:redundancies": "tsx --tsconfig database/tsconfig.json database/scripts/redundancies.ts", "db:combinations": "tsx --tsconfig database/tsconfig.json database/scripts/combinations.ts", + "db:structure": "tsx --tsconfig database/tsconfig.json database/scripts/structure.ts", "e2e": "PUBLIC_PLAYWRIGHT=true pnpm exec playwright test", "e2e:debug": "PUBLIC_PLAYWRIGHT=true pnpm exec playwright test --debug", "e2e:ui": "PUBLIC_PLAYWRIGHT=true pnpm exec playwright test --ui"