Skip to content

Commit 3980144

Browse files
committed
mention YAML files in documentation
1 parent 982b89e commit 3980144

2 files changed

Lines changed: 12 additions & 6 deletions

File tree

CONTRIBUTING.md

Lines changed: 10 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,9 @@ You need to have [Git](https://git-scm.com/), [NodeJS](https://nodejs.org/) and
5656

5757
### Updating the Database
5858

59-
All updates to the database are made by modifying the SQL files in the folder [/databases/catdat](databases/catdat), primarily those in the subfolder [/databases/catdat/data](databases/catdat/data). See [DATABASE.md](/DATABASE.md) for an overview of the database structure.
59+
All updates to the database are made by modifying the YAML files in the folder [/databases/catdat/data](databases/catdat/data). See [DATABASE.md](/DATABASE.md) for an overview of the database structure.
60+
61+
If you are not familiar with YAML, a short beginner-friendly introduction can be found at https://www.youtube.com/watch?v=1uFVr15xDGg. You can also look at the existing files in the data folder to get a feel for how the data is structured.
6062

6163
Apply the updates using:
6264

@@ -75,7 +77,7 @@ to continuously run this update when a file in the subfolder [/databases/catdat/
7577
### Troubleshooting
7678

7779
- If the local database is corrupted, or its schema has changed, recreate it using `pnpm db:setup`.
78-
- If the `pnpm db:update` command fails, examine the error message to determine the cause. It could be due to malformed SQL, a contradictory property, or a failing test in the `pnpm db:test` script (which also runs as part of the update command), as explained below.
80+
- If the `pnpm db:update` command fails, examine the error message to determine the cause. It could be due to malformed YAML, a contradictory property, or a failing test in the `pnpm db:test` script (which also runs as part of the update command), as explained below.
7981

8082
### Tests for Data Quality
8183

@@ -90,12 +92,16 @@ If any of these tests fail, adjust the data accordingly.
9092

9193
### Example Commits
9294

95+
_These commits refer to an old version of CatDat and will be replaced by more current ones._
96+
9397
- [Add category of Hausdorff spaces](https://github.com/ScriptRaccoon/CatDat/commit/390ed9c7996334138f8bc61c0b3f8e822003248a)
9498
- [Add two tiny categories](https://github.com/ScriptRaccoon/CatDat/commit/e5781d87bdc084a65cf0ec67c7efc5b3e29c4303)
9599
- [Add regular and coregular categories](https://github.com/ScriptRaccoon/CatDat/commit/e06f85fa13e5f8eeb42049880b5662be7fc36a50)
96100

97101
### Example Pull Requests
98102

103+
_These pull requests refer to an old version of CatDat and will be replaced by more current ones._
104+
99105
- [CMon is not coregular](https://github.com/ScriptRaccoon/CatDat/pull/27/changes)
100106
- [Add "locally cartesian closed" property](https://github.com/ScriptRaccoon/CatDat/pull/3/changes)
101107
- [Add "locally strongly finitely presentable" as a property](https://github.com/ScriptRaccoon/CatDat/pull/21/changes)
@@ -156,7 +162,7 @@ In particular, it often makes sense to **keep** a redundant assignment of a sati
156162

157163
For example, you may first prove that a category has zero morphisms, and then prove that it is normal. Although the database contains the implication "normal => zero morphisms", in practice the latter is used as a prerequisite. Similarly, when proving that a category is extensive, it is often clearer to first show that finite coproducts exist, rather than relying on the implication "extensive => finite coproducts". Also, an explicit description of finite coproducts is useful for deciding other properties involving coproducts.
158164

159-
Every redundant assignment of a satisfied property that is intentionally kept must be explicitly marked to skip the redundancy check. See `N.sql` for an example.
165+
Every redundant assignment of a satisfied property that is intentionally kept must be explicitly marked to skip the redundancy check. See `N.yaml` for an example.
160166

161167
### Keep Pull Requests Focused
162168

@@ -168,7 +174,7 @@ Examples of appropriate pull requests include:
168174

169175
- adding a single category property and determining it for several categories in the database,
170176
- adding a single category together with its properties,
171-
- adding a single missing proof ([Example](https://github.com/ScriptRaccoon/CatDat/pull/27))
177+
- adding a single missing proof
172178
- clarifying definitions, explanations, or documentation.
173179

174180
As a practical guideline, avoid introducing more than four properties (or four categories) in a single pull request.

DATABASE.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -47,11 +47,11 @@ For functors there are similar tables, such as:
4747

4848
The schema defines the structure of the database: tables, views, indexes, and triggers. It is specified in several SQL files located in the subfolder [/databases/catdat/schema](/databases/catdat/schema/). The command `pnpm db:setup` deletes the old database file (if it exists) and creates a new one using this schema. This is required when the schema changes, so it is recommended to run it periodically.
4949

50-
Database entries (categories, properties, implications, etc.) are defined in SQL files located in the subfolder [/databases/catdat/data](/databases/catdat/data/). The command `pnpm db:seed` replaces the current contents of the database by clearing all existing data and inserting the entries defined in these SQL files.
50+
Database entries (categories, properties, implications, etc.) are defined in YAML files located in the subfolder [/databases/catdat/data](/databases/catdat/data/). The command `pnpm db:seed` rebuilds the database by clearing all existing data and then parsing and inserting the entries defined in these YAML files.
5151

5252
## Derived Data
5353

54-
From the defined satisfied properties of a given category, new properties can be automatically deduced using the implications. (For example, when a category has equalizers and products, we can infer that it is complete.) The same applies to unsatisfied properties. Additionally, suitable implications may be dualized, and a category inherits all dualized properties of its dual category, if available. Note that the SQL files mentioned above do _not_ contain any derived data.
54+
From the defined satisfied properties of a given category, new properties can be automatically deduced using the implications. (For example, when a category has equalizers and products, we can infer that it is complete.) The same applies to unsatisfied properties. Additionally, suitable implications may be dualized, and a category inherits all dualized properties of its dual category, if available. Note that the YAML files mentioned above do _not_ contain any derived data.
5555

5656
The command `pnpm db:deduce` deduces implications, satisfied properties, and unsatisfied properties.
5757

0 commit comments

Comments
 (0)