Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions CONTRIBUTING.md
Original file line number Diff line number Diff line change
Expand Up @@ -128,6 +128,8 @@ When contributing new data (categories, functors, properties, implications), ple

- **Simplify Implications**: When adding a new implication, check if it simplifies existing implications and if it deduces some previously non-deduced properties for categories.

- **Long-form content**: If a proof for a property becomes very long, move it into a markdown-generated content page and link to that page. These files are located in the `/content` folder. For example, `/content/cocongruences_of_groups.md` is rendered at [`/content/cocongruences_of_groups`](https://catdat.app/content/cocongruences_of_groups). Content pages are also used for reusable lemmas that apply to multiple property assignments.

- **New Combinations**: Add new categories that satisfy combinations of satisfied properties and unsatisfied properties and not yet in the database. For example, you may add a category that is abelian but neither cocomplete nor essentially small (if it is not already present). The [page with missing data](https://catdat.app/missing) lists consistent combinations of the form $p \land \neg q$ that are not yet witnessed by a category in the database. The same remarks apply to functors.

### Redundancy Script
Expand Down
33 changes: 32 additions & 1 deletion src/routes/content/[id]/+page.server.ts
Original file line number Diff line number Diff line change
@@ -1,6 +1,9 @@
import { content_ids, get_rendered_content } from '$lib/server/markdown'
import { error } from '@sveltejs/kit'
import type { EntryGenerator } from './$types'
import { batch } from '$lib/server/db.catdat'
import sql from 'sql-template-tag'
import type { CategoryShort, PropertyShort } from '$lib/commons/types'

export const entries: EntryGenerator = () => {
return content_ids.map((id) => ({ id }))
Expand All @@ -10,5 +13,33 @@ export const load = async (event) => {
const id = event.params.id
const content = get_rendered_content(id)
if (!content) error(404, 'Not Found')
return content

const { results, err: err_categories } = batch<
[CategoryShort, PropertyShort, { id: string }]
>([
sql`
SELECT c.id, c.name FROM categories c
WHERE EXISTS (
SELECT 1
FROM category_property_assignments cp
WHERE
cp.category_id = c.id
AND cp.reason LIKE '%/content/' || ${id} || '%'
)
`,
sql`
SELECT id, relation FROM category_properties
WHERE description LIKE '%/content/' || ${id} || '%'
`,
sql`
SELECT id FROM category_implications
WHERE reason LIKE '%/content/' || ${id} || '%'
`,
])

if (err_categories) error(500, 'Could not load context')

const [categories, category_properties, category_implications] = results

return { ...content, categories, category_properties, category_implications }
}
33 changes: 33 additions & 0 deletions src/routes/content/[id]/+page.svelte
Original file line number Diff line number Diff line change
@@ -1,5 +1,8 @@
<script lang="ts">
import CategoryList from '$components/CategoryList.svelte'
import MetaData from '$components/MetaData.svelte'
import PropertyList from '$components/PropertyList.svelte'
import SuggestionForm from '$components/SuggestionForm.svelte'

let { data } = $props()
</script>
Expand All @@ -14,6 +17,36 @@
<p class="hint">Author: {data.meta_data.author}</p>
{/if}

{#if data.categories.length > 0 || data.category_properties.length > 0 || data.category_implications.length > 0}
<h3>Context</h3>

{#if data.categories.length > 0}
<p class="hint">This page is referenced by the following categories.</p>

<CategoryList categories={data.categories} />
{/if}

{#if data.category_properties.length > 0}
<p class="hint">This page is referenced by the following properties.</p>

<PropertyList properties={data.category_properties} />
{/if}

{#if data.category_implications.length > 0}
<p class="hint">This page is referenced by the following implications.</p>

<ul>
{#each data.category_implications as { id }}
<li>
<a href="/category-implication/{id}">{id}</a>
</li>
{/each}
</ul>
{/if}
{/if}

<SuggestionForm />

<style>
.content {
line-height: 1.6;
Expand Down