Merge remote-tracking branch 'origin/main' into joss2024

.devcontainer/devcontainer.json

@@ -1,16 +1,20 @@
 {
   "image": "mcr.microsoft.com/vscode/devcontainers/javascript-node:20",
+  "features": {
+    "github-cli": "latest"
+  },
   "containerEnv": {
     "DATA_WORKSPACE": "/workspaces/web/data"
   },
   "remoteEnv": {
-    "PUBLIC_DATA_URL": "https://${localEnv:CODESPACE_NAME}-3141.${localEnv:GITHUB_CODESPACES_PORT_FORWARDING_DOMAIN}"
+    "VITE_PUBLIC_DATA_URL": "https://${localEnv:CODESPACE_NAME}-3141.${localEnv:GITHUB_CODESPACES_PORT_FORWARDING_DOMAIN}"
   },
   "onCreateCommand": "pnpm install && pnpm run --filter core build",
   "postAttachCommand": {
     "compile": "pnpm run --filter compile dev",
     "core": "pnpm run --filter core dev",
-    "viewer": "pnpm run --filter viewer dev --host"
+    "viewer": "pnpm run --filter viewer dev --host --open",
+    "port": "gh codespace ports visibility 3141:public -c $CODESPACE_NAME && exit"
   },
   "forwardPorts": [3141, 5173],
   "portsAttributes": {

.gitignore

@@ -2,3 +2,6 @@ coverage/
 dist/
 node_modules/
 data/
+out
+.vscode-test/
+*.vsix

.prettierignore

@@ -1,4 +1,6 @@
 coverage
 dist
+out
 pnpm-lock.yaml
 .svelte-kit
+.vscode-test

.tool-versions

@@ -1,3 +1,3 @@
 # Pinned here and in devcontainer to avoid OOM issues stemming from
 # https://github.com/TypeStrong/ts-node/issues/1995
-nodejs 20.11.0
+nodejs 20.14.0

LICENSE.md

@@ -1,4 +1,4 @@
-Copyright (c) 2014-2023 James Dabbs
+Copyright (c) 2014-2024 James Dabbs
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal

README.md

@@ -1,17 +1,69 @@
 [![test](https://github.com/pi-base/web/actions/workflows/test.yaml/badge.svg)](https://github.com/pi-base/web/actions/workflows/test.yaml)
 [![e2e](https://github.com/pi-base/web/actions/workflows/e2e.yaml/badge.svg)](https://github.com/pi-base/web/actions/workflows/e2e.yaml)
 
-Software monorepo for the [π-base](https://topology.pi-base.org) project.
+Software monorepo for the [π-base](https://github.com/pi-base) project.
 
-🔗s
+# What's this?
 
-- [π-base data](https://github.com/pi-base/data)
-- Error monitoring - [Sentry](https://james-dabbs.sentry.io/projects/pi-base/?project=5251960&statsPeriod=30d)
+**π-base** is software supporting the formalization of mathematical
+results that can be expressed in terms of *objects*, the *properties*
+they satisfy, and the *theorems* that guarantee the presence of which 
+properites imply the others.
+
+Its main implementation lives at
+<https://topology.pi-base.org>, modeling research in
+[general topology](https://en.wikipedia.org/wiki/General_topology).
+
+A fork is being developed at <https://github.com/pi-base-topos> in support
+of [topos theory](https://en.wikipedia.org/wiki/Topos).
+
+*(Researchers who are interested in contributing to these databases
+likely want to visit <https://github.com/pi-base/data> or
+<https://github.com/pi-base-topos/data> directly, or connect with us
+via the [`code4math` Zulip](https://code4math.zulipchat.com/).)*
+
+Four node packages are maintained as part of this monorepo:
+
+-   `packages/compile`:
+    Compiles, checks, and publishes a data bundle based upon a repository
+    of formalized results expressed in Markdown/YAML.
+-   `packages/viewer`:
+    Web application for browsing/querying formalized results, featuring
+    automated deduction. (i.e. <https://topology.pi-base.org>)
+-   `packages/vscode`:
+    Web extension for VS Code to aid contributors and reviewers to a
+    π-Base compatible repository of formalized results
+-   `packages/core`:
+    Shared data model for all π-Base utilities.
+
+# Getting Started
+
+The easiest way to try the software out is to use a Codespace; either press
+the comma (`,`) key on your keyboard while logged into GitHub on this page,
+or press the below button.
+
+[![Open in GitHub Codespaces](https://github.com/codespaces/badge.svg)](https://github.com/codespaces/new?hide_repo_select=true&ref=main&repo=391656710)
+
+A web version of VS Code with all the necessary dependencies and
+software installed will be made available to you, as well as a
+copy of the general topology repository at
+<https://github.com/pi-base/data>. A new tab will automatically
+open to your development preview of the web viewer application,
+and changes you make to your copy of the data repository will
+be immediately recompiled and available in the viewer upon refresh.
 
 # Documentation
 
 Various guides are available in the [`doc`](./doc/) directory.
 
+# 🔗s
+
+-   [π-base data](https://github.com/pi-base/data):
+    peer-reviewed repository of formalized results in general topology,
+    available online at <https://topology.pi-base.org>
+-   [Sentry](https://james-dabbs.sentry.io/projects/pi-base/?project=5251960&statsPeriod=30d):
+    error monitoring
+
 # Copyright and License
 
-Copyright 2014-2023 James Dabbs, [licensed for free public use](./LICENSE.md).
+Copyright 2014-2024 James Dabbs, [licensed for free public use](./LICENSE.md).

package.json

@@ -9,15 +9,15 @@
     "test:cov": "pnpm run --recursive test:cov"
   },
   "devDependencies": {
-    "@types/node": "^20.11.3",
-    "@vitest/coverage-v8": "^0.34.6",
+    "@types/node": "^20.14.0",
+    "@vitest/coverage-v8": "^1.3.0",
     "nodemon": "^2.0.22",
     "npm-check-updates": "^16.14.12",
     "prettier": "^2.8.8",
     "prettier-plugin-svelte": "^2.10.1",
     "ts-node": "^10.9.2",
-    "typescript": "^5.3.3",
-    "vite": "^4.5.1",
-    "vitest": "^0.34.6"
+    "typescript": "^5.4.5",
+    "vite": "^5.0.0",
+    "vitest": "^1.3.0"
   }
 }

packages/compile/package.json

@@ -37,7 +37,7 @@
     "glob": "^8.1.0",
     "js-yaml": "^4.1.0",
     "yaml-front-matter": "^4.1.1",
-    "zod": "^3.22.4"
+    "zod": "^3.23.8"
   },
   "devDependencies": {
     "@types/cors": "^2.8.17",

packages/compile/tsconfig.json

@@ -4,7 +4,7 @@
     "declaration": true,
     "declarationDir": "dist/types",
     "module": "es2022",
-    "moduleResolution": "node",
+    "moduleResolution": "bundler",
     "noImplicitAny": true,
     "outDir": "dist/esm",
     "preserveConstEnums": true,

packages/core/bin/build

@@ -0,0 +1,12 @@
+#!/bin/bash
+set -exo pipefail
+
+# VSCode extensions can only use CommonJS modules (for now), but we want to 
+# continue using our standard Vite/ESM build process elsewhere. This builds
+# both versions, corresponding to `package.json`'s `exports` field.
+
+tsc --module es2022 --outDir dist/esm/
+echo '{"type": "module"}' > dist/esm/package.json
+
+tsc --module commonjs --outDir dist/cjs/
+echo '{"type": "commonjs"}' > dist/cjs/package.json

packages/core/package.json

@@ -14,23 +14,27 @@
   },
   "license": "MIT",
   "author": "James Dabbs <james.dabbs@gmail.com> (https://jdabbs.com)",
-  "main": "./dist/esm/index.js",
   "types": "./dist/types/index.d.ts",
+  "exports": {
+    "types": "./dist/types/index.d.ts",
+    "require": "./dist/cjs/index.js",
+    "import": "./dist/esm/index.js"
+  },
   "repository": {
     "type": "git",
     "url": "git+https://github.com/pi-base/web.git"
   },
   "scripts": {
     "build:peg": "peggy --plugin ./node_modules/ts-pegjs/dist/tspegjs -o src/Formula/Grammar.ts --cache src/Formula/Grammar.pegjs",
-    "build": "pnpm build:peg && tsc",
+    "build": "pnpm build:peg && ./bin/build",
     "dev": "pnpm build:peg && tsc --watch",
     "test": "vitest run",
     "test:cov": "vitest run --coverage",
     "test:watch": "vitest"
   },
   "dependencies": {
     "debug": "^4.3.4",
-    "micromark-util-types": "1.0.2",
+    "js-yaml": "^4.1.0",
     "rehype-katex": "^6.0.3",
     "rehype-stringify": "^9.0.4",
     "remark": "^14.0.3",
@@ -40,15 +44,17 @@
     "unified": "^10.1.2",
     "unist-util-is": "^5.2.1",
     "unist-util-visit": "^4.1.2",
-    "zod": "^3.22.4"
+    "zod": "^3.23.8"
   },
   "devDependencies": {
     "@types/debug": "^4.1.12",
     "@types/hast": "^2.3.9",
+    "@types/js-yaml": "^4.0.9",
     "@types/mdast": "^3.0.15",
     "@types/unist": "^2.0.10",
     "hast-util-to-html": "^8.0.4",
     "mdast-util-from-markdown": "1.3.0",
+    "micromark-util-types": "1.0.2",
     "peggy": "^3.0.2",
     "ts-pegjs": "^4.2.1"
   }

packages/core/src/Document.ts

@@ -0,0 +1,19 @@
+import * as z from 'zod'
+import * as yaml from 'js-yaml'
+
+// TODO: unify with logic in packages/compiler
+export function parseDocument<T>(schema: z.ZodSchema<T>, contents: string) {
+  const match = contents.match(
+    /^(---)?\s*(?<frontmatter>[\s\S]*?)\s*---(?<body>[\s\S]*)/,
+  )
+  if (!match?.groups) {
+    return
+  }
+
+  const { frontmatter, body } = match.groups
+  const meta = yaml.load(frontmatter)
+  const data = { description: body.trim() }
+  const raw = typeof meta === 'object' ? { ...meta, ...data } : data
+
+  return schema.safeParse(raw)
+}

packages/core/src/Id.ts

@@ -54,3 +54,39 @@ export function toInt(id: string): number {
 
   return tagged.id
 }
+
+// TODO: these were extracted from other parallel-but-divergent implementations
+// and should be unified.
+
+type Pad = '' | '0' | '00' | '000' | '0000' | '00000' | '00000'
+type XId<Prefix extends string> = `${Prefix}${Pad}${number}`
+
+export type SId = XId<'S'>
+export type PId = XId<'P'>
+export type TId = XId<'T'>
+export type SPId = [SId, PId]
+export type EntityId = SId | PId | TId | SPId
+
+export function isSpaceId(token: string): token is SId {
+  return token.match(/^S\d{1,6}$/) !== null
+}
+
+export function isPropertyId(token: string): token is PId {
+  return token.match(/^P\d{1,6}$/) !== null
+}
+
+export function isTheoremId(token: string): token is SId {
+  return token.match(/^T\d{1,6}$/) !== null
+}
+
+export function isTraitId(pair: [string, string]): pair is SPId {
+  return isSpaceId(pair[0]) && isPropertyId(pair[1])
+}
+
+export const idExp = /[PST]\d{1,6}/g
+
+export function normalizeId(id: SId): SId
+export function normalizeId(id: PId): PId
+export function normalizeId(id: string) {
+  return `${id[0]}${id.slice(1).padStart(6, '0')}`
+}

packages/core/src/Parser.ts

@@ -13,7 +13,7 @@ import { truncate as truncator } from './Parser/truncate.js'
 import { unnest } from './Parser/unnest.js'
 
 export type Options = {
-  link: Linkers
+  link: Partial<Linkers>
   truncate?: boolean
 }
 

packages/core/src/Parser/links.ts

@@ -263,7 +263,7 @@ function isExternalLink(node: any): node is ExternalLinkNode {
 }
 
 function isExternalKind(kind: any): kind is ExternalLinkNode['kind'] {
-  return kind && ['doi', 'wikipedia', 'mr', 'mathse', 'mo'].includes(kind)
+  return kind && ['doi', 'wikipedia', 'mr', 'mathse', 'mo', 'zb'].includes(kind)
 }
 
 function isInternalLink(node: any): node is InternalLinkNode {

packages/core/src/Parser/references.ts

@@ -10,12 +10,30 @@ import { ExternalLinkNode, InternalLinkNode, Linkers } from './types'
  *
  * See https://github.com/syntax-tree/mdast-util-to-hast#fields-on-nodes
  */
-export function references({ internal, external }: Linkers) {
+export function references({ internal, external }: Partial<Linkers>) {
   return (): Transformer<Root, Root> => {
     return function transformer(tree: Root) {
       visit(tree, 'internalLink', (node: InternalLinkNode) => {
         const { kind, id } = node
 
+        if (!internal) {
+          Object.assign(node, {
+            data: {
+              hName: 'span',
+              hProperties: {
+                className: 'internal-link',
+              },
+              hChildren: [
+                {
+                  type: 'text',
+                  value: `${kind}${id}`,
+                },
+              ],
+            },
+          })
+          return
+        }
+
         const { href, title } = internal([kind, id])
 
         Object.assign(node, {
@@ -36,26 +54,27 @@ export function references({ internal, external }: Linkers) {
         })
       })
 
-      visit(tree, 'externalLink', (node: ExternalLinkNode) => {
-        const { href, title } = external([node.kind, node.id])
+      external &&
+        visit(tree, 'externalLink', (node: ExternalLinkNode) => {
+          const { href, title } = external([node.kind, node.id])
 
-        Object.assign(node, {
-          data: {
-            hName: 'a',
-            hProperties: {
-              href,
-              title,
-              className: 'external-link',
-            },
-            hChildren: [
-              {
-                type: 'text',
-                value: title,
+          Object.assign(node, {
+            data: {
+              hName: 'a',
+              hProperties: {
+                href,
+                title,
+                className: 'external-link',
               },
-            ],
-          },
+              hChildren: [
+                {
+                  type: 'text',
+                  value: title,
+                },
+              ],
+            },
+          })
         })
-      })
     }
   }
 }