From 61f66523e00aa0115795fc3d2789f11a90f437a4 Mon Sep 17 00:00:00 2001
From: Bokuan Li <bokuan.li@mail.mcgill.ca>
Date: Thu, 12 Mar 2026 21:26:34 -0400
Subject: [PATCH] Prepare for migration into spec.

---
 .chktexrc                        |   1 +
 .editorconfig                    |   2 +-
 .gitea/workflows/compile.yaml    |  18 +++++
 .zed/keymap.json                 |  18 -----
 .zed/settings.json               |  28 -------
 .zed/tasks.json                  |  14 ----
 README.md                        |  10 ---
 build-serve.sh                   |   2 -
 build.groovy                     | 131 -------------------------------
 build.sh                         |  22 ------
 gerby.code-workspace             |  15 ++++
 retag.sh                         |   5 --
 serve.sh                         |   3 -
 spec.toml                        |   2 +
 src/dg/derivative/derivative.tex |  98 +++++++++++------------
 tagger.py                        |  73 -----------------
 upload-software.sh               |   4 -
 upload.sh                        |  11 ---
 18 files changed, 86 insertions(+), 371 deletions(-)
 create mode 100644 .chktexrc
 create mode 100644 .gitea/workflows/compile.yaml
 delete mode 100644 .zed/keymap.json
 delete mode 100644 .zed/settings.json
 delete mode 100644 .zed/tasks.json
 delete mode 100644 README.md
 delete mode 100644 build-serve.sh
 delete mode 100644 build.groovy
 delete mode 100644 build.sh
 create mode 100644 gerby.code-workspace
 delete mode 100644 retag.sh
 delete mode 100644 serve.sh
 delete mode 100644 tagger.py
 delete mode 100644 upload-software.sh
 delete mode 100644 upload.sh

diff --git a/.chktexrc b/.chktexrc
new file mode 100644
index 0000000..e0cc452
--- /dev/null
+++ b/.chktexrc
@@ -0,0 +1 @@
+CmdLine { -n24 -n9 -n17 }
\ No newline at end of file
diff --git a/.editorconfig b/.editorconfig
index 57779a4..408c985 100644
--- a/.editorconfig
+++ b/.editorconfig
@@ -1,4 +1,4 @@
 root = true
 
 [*]
-end_of_line = lf
+end_of_line = lf
\ No newline at end of file
diff --git a/.gitea/workflows/compile.yaml b/.gitea/workflows/compile.yaml
new file mode 100644
index 0000000..2175030
--- /dev/null
+++ b/.gitea/workflows/compile.yaml
@@ -0,0 +1,18 @@
+name: Compile Project
+run-name: Compile the project using spec.
+on: [push]
+jobs:
+  Compile:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Check out repository code
+        uses: actions/checkout@v4
+      - name: Add to PATH
+        run: echo "/root/.nvm/versions/node/v24.14.0/bin" >> $GITHUB_PATH
+      - name: Copy source
+        run: |
+          mkdir -p /srv/builds/${{ github.event.repository.name }}
+          cp -r . /srv/builds/${{ github.event.repository.name }}/
+      - name: Compile Website
+        run: spec compile --all
+        working-directory: /srv/builds/${{ github.event.repository.name }}
\ No newline at end of file
diff --git a/.zed/keymap.json b/.zed/keymap.json
deleted file mode 100644
index 8162c5d..0000000
--- a/.zed/keymap.json
+++ /dev/null
@@ -1,18 +0,0 @@
-[
-  {
-    "context": "Editor",
-    "bindings": {
-      "ctrl-s": [
-        "workspace::Save",
-        ["task::Spawn", { "task_name": "Build and Serve" }],
-      ],
-      "ctrl-b": "editor::MoveLeft",
-      "ctrl-i": [
-        "editor::InsertSnippet",
-        {
-          "snippet": "\\textit{$1}$0",
-        },
-      ],
-    },
-  },
-]
diff --git a/.zed/settings.json b/.zed/settings.json
deleted file mode 100644
index 210610a..0000000
--- a/.zed/settings.json
+++ /dev/null
@@ -1,28 +0,0 @@
-// Folder-specific settings
-//
-// For a full list of overridable settings, and general information on folder-specific settings,
-// see the documentation: https://zed.dev/docs/configuring-zed#settings-files
-{
-  "lsp": {
-    "texlab": {
-      "settings": {
-        "texlab": {
-          "rootDirectory": ".",
-          "build": {
-            "auxDirectory": ".",
-          },
-        },
-      },
-    },
-  },
-  "languages": {
-    "HTML": {
-      "format_on_save": "off",
-    },
-    "Python": {
-      "format_on_save": "off",
-    },
-  },
-  "soft_wrap": "preferred_line_length",
-  "preferred_line_length": 80,
-}
diff --git a/.zed/tasks.json b/.zed/tasks.json
deleted file mode 100644
index 9a9e3b4..0000000
--- a/.zed/tasks.json
+++ /dev/null
@@ -1,14 +0,0 @@
-[
-  {
-    "label": "Build and Serve",
-    "command": "wsl",
-    "args": ["bash", "build-serve.sh"],
-    "cwd": "${ZED_WORKTREE_ROOT}",
-  },
-  {
-    "label": "Upload to Server",
-    "command": "wsl",
-    "args": ["bash", "upload.sh"],
-    "cwd": "${ZED_WORKTREE_ROOT}",
-  },
-]
diff --git a/README.md b/README.md
deleted file mode 100644
index 9ff04bb..0000000
--- a/README.md
+++ /dev/null
@@ -1,10 +0,0 @@
-[![pdf](https://github.com/gerby-project/hello-world/actions/workflows/example.yml/badge.svg)](https://github.com/gerby-project/hello-world/actions/workflows/example.yml)
-
-This repository documents a minimal working example for using Gerby.
-
-There are two things one can look at
-
-* the plasTeX-only check, see `.github/workflows/example.yml` (which is checked by the badge)
-* a full example using the now discontinued Travis, see `.travis.yml`.
-
-For more information, see [Gerby project](https://gerby-project.github.io).
diff --git a/build-serve.sh b/build-serve.sh
deleted file mode 100644
index af5e084..0000000
--- a/build-serve.sh
+++ /dev/null
@@ -1,2 +0,0 @@
-pgrep -f build.sh > /dev/null || ./build.sh
-pgrep -f serve.sh > /dev/null || ./serve.sh &
diff --git a/build.groovy b/build.groovy
deleted file mode 100644
index 699b3f3..0000000
--- a/build.groovy
+++ /dev/null
@@ -1,131 +0,0 @@
-def projectRoot = '/home/gerby/gerby'
-
-def vGPython = "${projectRoot}/gerby-venv/bin/python"
-def vGPip = "${projectRoot}/gerby-venv/bin/pip"
-
-def vPPython = "${projectRoot}/plastex-venv/bin/python"
-def vPPip = "${projectRoot}/plastex-venv/bin/pip"
-
-def vPlastex = "${projectRoot}/plastex-venv/bin/plastex"
-
-def discordHook = "https://discord.com/api/webhooks/1456391390513856676/yniOv0Gbxp2UwW1pbZcekpXsC8y1dYppGQ90O7He-df24IODggrgXdMFwvz-RMWM15j8"
-
-pipeline {
-    agent any
-
-    stages {
-        stage('Create Links') {
-            steps {
-                dir("${projectRoot}/gerby-website/gerby/tools/") {
-                    sh 'rm ./document || true'
-                    sh 'rm ./document.paux || true'
-                    sh 'rm ./tags || true'
-                    sh 'ln -s ../../../document      document'
-                    sh 'ln -s ../../../document.paux document.paux'
-                    sh 'ln -s ../../../tags          tags'
-                }
-                dir("${projectRoot}/gerby-website/") {
-                    sh 'rm ./hello-world.sqlite || true'
-                    sh 'rm ./comments.sqlite || true'
-                    sh 'ln -s gerby/tools/hello-world.sqlite hello-world.sqlite'
-                    sh 'ln -s gerby/tools/comments.sqlite    comments.sqlite'
-                }
-            }
-        }
-        stage('Bibliography') {
-            steps {
-                dir("${projectRoot}/") {
-                    sh 'pdflatex -interaction=nonstopmode document.tex || true'
-                    sh 'bibtex document || true'
-                    sh 'pdflatex -interaction=nonstopmode document.tex || true'
-                }
-            }
-        }
-        stage('Delete Tags') {
-            when {
-                expression { params['Redo Tags'] == true }
-            }
-            steps {
-                dir("${projectRoot}/") {
-                    sh 'rm ./tags || true'
-                    sh 'rm ./gerby-website/gerby/tools/hello-world.sqlite || true'
-                }
-            }
-        }
-        // The document folder is needed for the website to run, hence it is not cleared at the end of the compile process.
-        stage('Delete Previous Build') {
-            steps {
-                dir("${projectRoot}/") {
-                    sh "rm -r ./document"
-                }
-            }
-        }
-        stage('Tag') {
-            steps {
-                dir("${projectRoot}/") {
-                    sh "${vGPython} tagger.py >> tags"
-                }
-            }
-        }
-        stage('Plastex') {
-            steps {
-                dir("${projectRoot}/") {
-                    sh "${vPlastex} --renderer=Gerby ./document.tex"
-                }
-            }
-        }
-        stage('Update Database') {
-            steps {
-                dir("${projectRoot}/gerby-website/gerby/tools") {
-                    sh "${vGPython} update.py"
-                }
-            }
-        }
-    }
-
-    post {
-        always {
-            dir("${projectRoot}/") {
-                sh 'rm document.aux || true'
-                sh 'rm document.bbl || true'
-                sh 'rm document.blg || true'
-                sh 'rm document.log || true'
-                sh 'rm document.out || true'
-                sh 'rm document.pdf || true'
-            }
-            script {
-                def formatTime = { milliseconds ->
-                    long seconds = (long)(milliseconds / 1000)
-                    long mins = (long)(seconds / 60)
-                    long secs = seconds % 60
-                    return mins > 0 ? "${mins}m${secs}s" : "${secs}s"
-                }
-
-                def buildTitle = "Build Website #${env.BUILD_NUMBER}"
-                if (params['Redo Tags']) {
-                    buildTitle += " (Retag)"
-                }
-
-                def queueTimeMs = currentBuild.startTimeInMillis - currentBuild.timeInMillis
-                def queueTime = formatTime(queueTimeMs)
-                def buildTime = formatTime(currentBuild.duration)
-
-                def description = """
-                **Build:** [#${env.BUILD_NUMBER}](${env.BUILD_URL})
-                **Console:** [Console Output](${env.BUILD_URL}console)
-
-                **Queue Time:** ${queueTime}
-                **Build Duration:** ${buildTime}
-                **Status:** ${currentBuild.currentResult}
-                """.trim()
-
-                discordSend(
-                    webhookURL: discordHook,
-                    title: buildTitle,
-                    description: description,
-                    result: currentBuild.currentResult
-                )
-            }
-        }
-    }
-}
diff --git a/build.sh b/build.sh
deleted file mode 100644
index 2465f85..0000000
--- a/build.sh
+++ /dev/null
@@ -1,22 +0,0 @@
-rm -r ./document
-
-# Make the bibliography. Errors here don't matter.
-pdflatex -interaction=nonstopmode document.tex > /dev/null 2>&1
-bibtex document > /dev/null 2>&1
-pdflatex -interaction=nonstopmode document.tex > /dev/null 2>&1
-
-
-# Website compilation procedure
-python3 tagger.py >> tags
-./plastex-venv/bin/plastex --renderer=Gerby ./document.tex
-cd ./gerby-website/gerby/tools
-python3 update.py
-cd ../../..
-
-# Clean up the tex compilations.
-rm document.aux > /dev/null 2>&1
-rm document.bbl > /dev/null 2>&1
-rm document.blg > /dev/null 2>&1
-rm document.log > /dev/null 2>&1
-rm document.out > /dev/null 2>&1
-rm document.pdf > /dev/null 2>&1
diff --git a/gerby.code-workspace b/gerby.code-workspace
new file mode 100644
index 0000000..60d6fb8
--- /dev/null
+++ b/gerby.code-workspace
@@ -0,0 +1,15 @@
+{
+	"folders": [
+		{
+			"path": "."
+		}
+	],
+	"settings": {
+		"VsCodeTaskButtons.tasks": [
+			{
+				"label": "Watch",
+				"task": "Watch"
+			}
+		]
+	}
+}
\ No newline at end of file
diff --git a/retag.sh b/retag.sh
deleted file mode 100644
index 6f043c0..0000000
--- a/retag.sh
+++ /dev/null
@@ -1,5 +0,0 @@
-# Rebuilds the tag system. Requires administrative access.
-
-rm ./tags
-rm ./gerby-website/gerby/tools/hello-world.sqlite
-./build.sh
diff --git a/serve.sh b/serve.sh
deleted file mode 100644
index 472f556..0000000
--- a/serve.sh
+++ /dev/null
@@ -1,3 +0,0 @@
-cd gerby-website
-export FLASK_APP=gerby
-python3 -m flask run
diff --git a/spec.toml b/spec.toml
index 81aa901..76b6b5f 100644
--- a/spec.toml
+++ b/spec.toml
@@ -12,3 +12,5 @@ font = "roboto"
 primaryColour = "blue"
 neutralColour = "grey"
 searchLimit = 16
+maxSearchPages = 48
+advertiseSpec = true
diff --git a/src/dg/derivative/derivative.tex b/src/dg/derivative/derivative.tex
index 1c4c6b7..33be5f2 100644
--- a/src/dg/derivative/derivative.tex
+++ b/src/dg/derivative/derivative.tex
@@ -1,49 +1,49 @@
-\section{Derivatives and Remainders}
-\label{section:derivative}
-
-\begin{definition}[Derivatives and Remainders]
-\label{definition:derivative-system}
-    Let $E, F$ be TVSs over $K \in \RC$ and $\ch(E; F), \calr(E; F) \subset F^E$ be vector subspaces, then $\mathcal{HR} = (\ch(E; F), \calr(E; F))$ is a pair of \textbf{derivatives} and \textbf{remainders} if
-    \begin{enumerate}
-        \item[(T)] For any $T \in \ch$, if there exists $V \in \cn_E(0)$ and $r \in \calr$ such that $T|_V = r|_V$, then $T = 0$.
-    \end{enumerate}
-\end{definition}
-
-\begin{definition}[$\mathcal{HR}$-Differentiability]
-\label{definition:space-differentiability}
-    Let $E, F$ be TVSs over $K \in \RC$, $\mathcal{HR}$ be a pair of derivatives and remainders, $U \subset E$ be open, $f: U \to F$ be a function, and $x_0 \in U$, then $f$ is \textbf{$\mathcal{HR}$-differentiable} at $x_0$ if there exists $V \in \cn_E(0)$, $T \in \ch$, and $r \in \calr$ such that
-    \[
-    f(x_0 + h) = f(x_0) + Th + r(h)
-    \]
-
-    for all $h \in V$. In which case, $T = D_{\mathcal{HR}}f(x_0)$ is the unique element of $\ch$ satisfying the above, known as the \textbf{$\mathcal{HR}$-derivative} of $f$ at $x_0$.
-\end{definition}
-\begin{proof}
-	Let $S, T \in \ch$, $r, s \in \calr$, and $V \in \cn_E(0)$ such that
-	\[
-	f(x_0 + h) - f(x_0) = Sh + r(h) = Th + s(h)
-	\]
-
-	for all $h \in V$, then $(S - T)(h) = (s - r)(h)$. By (T), $S - T = 0$. Hence $S = T$.
-\end{proof}
-
-\begin{proposition}
-\label{proposition:derivative-linearity}
-    Let $E, F$ be TVSs over $K \in \RC$, $\mathcal{HR}$ be a pair of derivatives and remainders, $U \subset E$ be open, $f, g: U \to F$ be functions, and $x_0 \in U$. If $f, g$ are $\mathcal{HR}$-differentiable at $x_0$, then for any $\lambda \in K$, $\lambda f + g$ is $\mathcal{HR}$-differentiable at $x_0$, and
-    \[
-    D_{\mathcal{HR}}(\lambda f + g)(x_0) = \lambda D_{\mathcal{HR}}f(x_0) + D_{\mathcal{HR}}g(x_0)
-    \]
-
-\end{proposition}
-\begin{proof}
-    Let $V \in \cn_E(0)$ and $r, s \in \calr$ such that
-    \begin{align*}
-    f(x_0 + h) - f(x_0) &= D_{\mathcal{HR}}f(x_0)h + r(h) \\
-    g(x_0 + h) - f(x_0) &= D_{\mathcal{HR}}g(x_0)h + s(h)
-    \end{align*}
-    then
-    \[
-    (\lambda f + g)(x_0+h) - (\lambda f + g)(x_0) = \underbrace{[\lambda D_{\mathcal{HR}}f(x_0) + D_{\mathcal{HR}}g(x_0)]}_{\in \ch}h + \underbrace{(\lambda r + s)}_{\in \calr}(h)
-    \]
-
-\end{proof}
+\section{Derivatives and Remainders}
+\label{section:derivative}
+
+\begin{definition}[Derivatives and Remainders]
+\label{definition:derivative-system}
+    Let $E, F$ be TVSs over $K \in \RC$ and $\ch(E; F), \calr(E; F) \subset F^E$ be vector subspaces, then $\mathcal{HR} = (\ch(E; F), \calr(E; F))$ is a pair of \textbf{derivatives} and \textbf{remainders} if
+    \begin{enumerate}
+        \item[(T)] For any $T \in \ch$, if there exists $V \in \cn_E(0)$ and $r \in \calr$ such that $T|_V = r|_V$, then $T = 0$.
+    \end{enumerate}
+\end{definition}
+
+\begin{definition}[$\mathcal{HR}$-Differentiability]
+\label{definition:space-differentiability}
+    Let $E, F$ be TVSs over $K \in \RC$, $\mathcal{HR}$ be a pair of derivatives and remainders, $U \subset E$ be open, $f: U \to F$ be a function, and $x_0 \in U$, then $f$ is \textbf{$\mathcal{HR}$-differentiable} at $x_0$ if there exists $V \in \cn_E(0)$, $T \in \ch$, and $r \in \calr$ such that
+    \[
+    f(x_0 + h) = f(x_0) + Th + r(h)
+    \]
+
+    for all $h \in V$. In which case, $T = D_{\mathcal{HR}}f(x_0)$ is the unique element of $\ch$ satisfying the above, known as the \textbf{$\mathcal{HR}$-derivative} of $f$ at $x_0$.
+\end{definition}
+\begin{proof}
+	Let $S, T \in \ch$, $r, s \in \calr$, and $V \in \cn_E(0)$ such that
+	\[
+	f(x_0 + h) - f(x_0) = Sh + r(h) = Th + s(h)
+	\]
+
+	for all $h \in V$, then $(S - T)(h) = (s - r)(h)$. By (T), $S - T = 0$. Hence $S = T$.
+\end{proof}
+
+\begin{proposition}
+\label{proposition:derivative-linearity}
+    Let $E, F$ be TVSs over $K \in \RC$, $\mathcal{HR}$ be a pair of derivatives and remainders, $U \subset E$ be open, $f, g: U \to F$ be functions, and $x_0 \in U$. If $f, g$ are $\mathcal{HR}$-differentiable at $x_0$, then for any $\lambda \in K$, $\lambda f + g$ is $\mathcal{HR}$-differentiable at $x_0$, and
+    \[
+    D_{\mathcal{HR}}(\lambda f + g)(x_0) = \lambda D_{\mathcal{HR}}f(x_0) + D_{\mathcal{HR}}g(x_0)
+    \]
+
+\end{proposition}
+\begin{proof}
+    Let $V \in \cn_E(0)$ and $r, s \in \calr$ such that
+    \begin{align*}
+    f(x_0 + h) - f(x_0) &= D_{\mathcal{HR}}f(x_0)h + r(h) \\
+    g(x_0 + h) - f(x_0) &= D_{\mathcal{HR}}g(x_0)h + s(h)
+    \end{align*}
+    then
+    \[
+    (\lambda f + g)(x_0+h) - (\lambda f + g)(x_0) = \underbrace{[\lambda D_{\mathcal{HR}}f(x_0) + D_{\mathcal{HR}}g(x_0)]}_{\in \ch}h + \underbrace{(\lambda r + s)}_{\in \calr}(h)
+    \]
+
+\end{proof}
diff --git a/tagger.py b/tagger.py
deleted file mode 100644
index 0d48a2c..0000000
--- a/tagger.py
+++ /dev/null
@@ -1,73 +0,0 @@
-import glob
-import re
-
-# no I, no O
-CHARACTERS = "0123456789ABCDEFGHJKLMNPQRSTUVWXYZ"
-
-
-# convert integer to tag
-def tobase(i):
-    global CHARACTERS
-
-    assert i >= 0
-
-    if i < len(CHARACTERS):
-        return CHARACTERS[i]
-    else:
-        return tobase(i // len(CHARACTERS)) + CHARACTERS[i % len(CHARACTERS)]
-
-
-def totag(i):
-    return tobase(i).rjust(4, "0")
-
-
-# convert tag to integer
-def toint(tag):
-    global CHARACTERS
-    return sum(
-        [CHARACTERS.index(tag[i]) * len(CHARACTERS) ** (4 - i - 1) for i in range(4)]
-    )
-
-
-tags = dict()
-labels = dict()
-inactive = []
-
-try:
-    with open("tags") as f:
-        for line in f:
-            # actual tag
-            if not line.startswith("#"):
-                tags[line.split(",")[0]] = line.strip().split(",")[1]
-                labels[line.strip().split(",")[1]] = line.strip().split(",")[0]
-
-            # check for inactive tags too
-            elif len(line.split(",")) == 2 and len(line.split(",")[0]) == 4:
-                inactive.append(line.split(",")[0])
-
-except FileNotFoundError:
-    pass
-
-# determine last assigned tag
-try:
-    last = toint(sorted(list(tags.keys()) + inactive)[-1])
-except IndexError:
-    last = -1
-
-
-filenames = glob.glob("./src/**/*.tex", recursive=True) + ["document.tex"]
-# filenames = ["document.tex"]
-
-# where we should start
-i = last + 1
-
-for filename in filenames:
-    with open(filename) as f:
-        # do this line per line to deal with comments
-        for line in f:
-            matches = re.findall("\\\\label{([^}]+)}", line.split("%")[0])
-            for label in matches:
-                if not label in labels:
-                    tag = tobase(i).rjust(4, "0")
-                    print("%s,%s" % (tag, label))
-                    i = i + 1
diff --git a/upload-software.sh b/upload-software.sh
deleted file mode 100644
index 247d7b6..0000000
--- a/upload-software.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-ssh gerby@178.156.199.217 "rm -r /home/gerby/gerby/gerby-website"
-ssh gerby@178.156.199.217 "rm -r /home/gerby/gerby/plastex"
-
-rsync -avz gerby-website plastex gerby@178.156.199.217:/home/gerby/gerby
diff --git a/upload.sh b/upload.sh
deleted file mode 100644
index 35a44ee..0000000
--- a/upload.sh
+++ /dev/null
@@ -1,11 +0,0 @@
-ssh gerby@178.156.199.217 "rm /home/gerby/gerby/document.tex"
-ssh gerby@178.156.199.217 "rm /home/gerby/gerby/preamble.sty"
-ssh gerby@178.156.199.217 "rm -r /home/gerby/gerby/src"
-rsync -avz preamble.sty document.tex src gerby@178.156.199.217:/home/gerby/gerby
-
-USER="jerrylicious"
-API_TOKEN="1199813d21c0022313bd9e7c8fa98d47b0"
-BUILD_TOKEN="AAAAC3NzaC1lZDI1NTE5AAAAIBlYjedLVBgIxxutWbnFm0bgs87jswTfhgOfGaPzzqTZ"
-
-CRUMB=$(curl -s "https://$USER:$API_TOKEN@jenkins.jerrylicious.me/crumbIssuer/api/xml?xpath=concat(//crumbRequestField,\":\" ,//crumb)")
-curl -X POST -H "$CRUMB" "https://$USER:$API_TOKEN@jenkins.jerrylicious.me/job/Gerby/job/Build%20Project/buildWithParameters?token=$BUILD_TOKEN&Redo%20Tags=false"