Allow dependencies between pages on the wiki

.gitignore

@@ -1,3 +1,4 @@
 CM
 .cm
-src/frontend/buildid.sml
+src/frontend/buildid.sml
+TEST/regression-wiki.txt

TEST/regression-wiki.mjs

@@ -1,3 +1,4 @@
+import { exec } from "child_process";
 import { readdirSync, writeFileSync } from "fs";
 
 /* Only files that are broken *on purpose* (because they're templates
@@ -28,18 +29,17 @@ const UNSAFE_WIKI_FILES = new Set([
  "user-hdeyoung-monweakfoc-elf",
 ]);
 
+exec("node elf-watcher.mjs", { cwd: "../wiki/" });
 const WIKI_TWELF_LOC = "../wiki/pages/";
 const cfgs = [];
 for (const file of readdirSync(WIKI_TWELF_LOC)) {
- if (file.endsWith(".elf")) {
+ if (file.endsWith(".cfg")) {
  const base = file.slice(0, file.length - 4);
  if (IGNORED_WIKI_FILES.has(base)) continue;
- const cfg = base + ".cfg";
- writeFileSync(WIKI_TWELF_LOC + cfg, file);
  cfgs.push(
  `test${
  UNSAFE_WIKI_FILES.has(base) ? "Unsafe" : ""
- } ${WIKI_TWELF_LOC}${cfg}`
+ } ${WIKI_TWELF_LOC}${file}`
  );
  }
 }

wiki/elf-to-mdx.mjs

@@ -67,9 +67,11 @@ async function hashToHex(content) {
  *
  * @param {string} elfFilename
  * The Elf file to process
+ * @param {string[]} prelude
+ * Any Elf prelude that should get appended to the Twelf context
  * @returns {Promise<string>}
  */
-export async function elfToMdx(elfFilename) {
+export async function elfToMdx(elfFilename, prelude = []) {
  const elfFile = readFileSync(elfFilename, "utf-8");
 
  /* Parse out header */
@@ -87,7 +89,7 @@ export async function elfToMdx(elfFilename) {
  /** @type {string[]} */
  let body = [];
  /** @type {string[]} */
- let twelfcontext = [];
+ let twelfcontext = prelude.slice();
 
  /** @typedef {{ type: "twelf", subtype: null | "hidden" | "checked", accum: string[] }} TwelfState */
  /** @typedef {{ type: "markdown-block", subtype: "math" | "twelf" | "checkedtwelf", accum: string[] }} MarkdownBlockState */
@@ -104,7 +106,11 @@ export async function elfToMdx(elfFilename) {
  (state.subtype === "twelf" || state.subtype === "checkedtwelf"))
  )
  ) {
- throw new TypeError(`state ${state.type} - ${state.type !== 'markdown' ? state.subtype : 'none'}`);
+ throw new TypeError(
+ `state ${state.type} - ${
+ state.type !== "markdown" ? state.subtype : "none"
+ }`
+ );
  }
  mutablyTrimEmptyLines(state.accum);
 

wiki/elf-watcher.mjs

@@ -1,6 +1,14 @@
-import { existsSync, mkdirSync, readdirSync, watch, writeFileSync } from "fs";
+import {
+ existsSync,
+ mkdirSync,
+ readFileSync,
+ readdirSync,
+ watch,
+ writeFileSync,
+} from "fs";
 import { argv } from "process";
 import { elfToMdx } from "./elf-to-mdx.mjs";
+import { getImportedPrelude } from "./elf-wiki-imports.mjs";
 
 const DIR_OF_ELF = "pages";
 const DIR_OF_MDX = "src/content/docs/wiki";
@@ -17,10 +25,49 @@ async function mdxOfFile(file) {
  if (!file.endsWith(".elf") || !existsSync(elfname)) return;
 
  const base = file.slice(0, file.length - 4);
+ const cfgname = `${DIR_OF_ELF}/${base}.cfg`;
  const mdxname = `${DIR_OF_MDX}/${base}.mdx`;
  console.log(`elf->mdx transforming ${file}`);
- const mdxFile = await elfToMdx(elfname);
- writeFileSync(mdxname, mdxFile);
+ try {
+ const prelude = getImportedPrelude(`${DIR_OF_ELF}/`, file);
+ const mdxFile = await elfToMdx(
+ elfname,
+ prelude.map(({ file, contents }) => `%%! file: ${file}\n${contents}\n`)
+ );
+ const cfg = `
+% DO NOT EDIT
+% Automatically generated by running "npm run dev" or "npm run build" in the
+% wiki directory.
+% Edit twelf/wiki/${file} instead
+
+${prelude.map(({ file }) => file).join("\n")}
+${file}
+`.trim();
+ if (
+ !existsSync(cfgname) ||
+ readFileSync(cfgname).toString("utf-8") !== cfg
+ ) {
+ if (existsSync(cfgname)) {
+ console.log(`elf->mdx: updating ${cfgname}`);
+ }
+ writeFileSync(cfgname, cfg);
+ }
+
+ writeFileSync(mdxname, mdxFile);
+ } catch (e) {
+ console.log(e);
+ writeFileSync(
+ mdxname,
+ `
+---
+---
+
+Error transforming ${file}
+
+${e}
+`
+ );
+ }
 }
 
 console.log(`elf->mdx checking existing files...`);

wiki/elf-wiki-imports.mjs

@@ -0,0 +1,72 @@
+import { readFileSync } from "fs";
+
+/**
+ * Read the file's header to get all of the imported elf files
+ * (in reverse order)
+ *
+ * @param {string} contents
+ */
+function getImportedFilenames(contents) {
+ /**@type {string[]} */
+ const importStatements = [];
+
+ for (const line of contents.split("\n")) {
+ if (!line.startsWith("%%! ")) break;
+ if (line.startsWith("%%! import: ")) {
+ importStatements.push(line.slice(12).trim());
+ }
+ }
+
+ return importStatements;
+}
+
+/**
+ * Uses a DFS traversal
+ *
+ * @param {string} base
+ * Relative path of elf files
+ * @param {Set<string>} known
+ * Avoids double-importing by tracking all the filenames ever added to `accum` in the process of this traversal
+ * @param {{file: string, contents: string}[]} accum
+ * Accumulates the files, making sure that files are added after their dependencies
+ * @param {string} elfname
+ * Name of an ELF file that is a dependency of the file we're trying to load
+ */
+function dfsAccumImportedPrelude(base, known, accum, elfname) {
+ if (!elfname.match(/^[a-zA-Z.\-_0-9]*[.]elf*$/)) {
+ throw new Error(
+ `Imported path ${elfname} invalid: must include only letters, numbers, dashes, and underscores and end in .elf`
+ );
+ }
+ const contents = readFileSync(`${base}${elfname}`).toString("utf-8");
+ for (const importElf in getImportedFilenames(contents)) {
+ if (!known.has(importElf)) {
+ known.add(importElf);
+ dfsAccumImportedPrelude(base, known, accum, importElf);
+ }
+ }
+ accum.push({ file: elfname, contents });
+}
+
+/**
+ *
+ * @param {string} base
+ * Relative path of elf files
+ * @param {string} elfname
+ */
+export function getImportedPrelude(base, elfname) {
+ /**@type {Set<string>} */
+ const known = new Set();
+
+ /**@type {{file: string, contents: string}[]} */
+ const dependencies = [];
+
+ for (const file of getImportedFilenames(
+ readFileSync(`${base}${elfname}`).toString("utf-8")
+ )) {
+ known.add(file);
+ dfsAccumImportedPrelude(base, known, dependencies, file);
+ }
+
+ return dependencies;
+}

wiki/pages/proving-metatheorems-proving-totality-assertions-about-the-natural-numbers.elf

@@ -142,7 +142,7 @@ plus-bad-output : plus (s N1) N2 (s (s N3))
 
 Here we have insisted that the output of the premise has the form ``s N3`` for some ``N3``. Twelf correctly reports an output coverage error because this condition can fail (for example, if the premise was ``plus-z : plus z z z``). 
 
-Pattern-matching the output of a premise is like an [[inversion]] step in a proof: you're insisting that the premise derivation must conclude a particular fact that is more specific than the judgement form itself. For Twelf to accept a relation as total, Twelf must notice that all of these inversions are permissible. Twelf permits such inversions when it is readily apparent that they are justified, and those inversions that Twelf does not accept can be proved explicitly.
+Pattern-matching the output of a premise is like an <Todo>inversion</Todo> step in a proof: you're insisting that the premise derivation must conclude a particular fact that is more specific than the judgement form itself. For Twelf to accept a relation as total, Twelf must notice that all of these inversions are permissible. Twelf permits such inversions when it is readily apparent that they are justified, and those inversions that Twelf does not accept can be proved explicitly.
 
 In this example, we got an output coverage error because we constrained the output of the premise by insisting it be formed by a particular constant. The other way to get output coverage errors is to insist that the output of a premise be a variable that occurs elsewhere in the type. For example:
 

.gitignore

@@ -1,3 +1,4 @@
 CM
 .cm
-src/frontend/buildid.sml
+src/frontend/buildid.sml
+TEST/regression-wiki.txt

TEST/regression-wiki.mjs

@@ -1,3 +1,4 @@
+import { exec } from "child_process";
 import { readdirSync, writeFileSync } from "fs";
 
 /* Only files that are broken *on purpose* (because they're templates
@@ -28,18 +29,17 @@ const UNSAFE_WIKI_FILES = new Set([
  "user-hdeyoung-monweakfoc-elf",
 ]);
 
+exec("node elf-watcher.mjs", { cwd: "../wiki/" });
 const WIKI_TWELF_LOC = "../wiki/pages/";
 const cfgs = [];
 for (const file of readdirSync(WIKI_TWELF_LOC)) {
- if (file.endsWith(".elf")) {
+ if (file.endsWith(".cfg")) {
  const base = file.slice(0, file.length - 4);
  if (IGNORED_WIKI_FILES.has(base)) continue;
- const cfg = base + ".cfg";
- writeFileSync(WIKI_TWELF_LOC + cfg, file);
  cfgs.push(
  `test${
  UNSAFE_WIKI_FILES.has(base) ? "Unsafe" : ""
- } ${WIKI_TWELF_LOC}${cfg}`
+ } ${WIKI_TWELF_LOC}${file}`
  );
  }
 }

wiki/elf-to-mdx.mjs

@@ -67,9 +67,11 @@ async function hashToHex(content) {
  *
  * @param {string} elfFilename
  * The Elf file to process
+ * @param {string[]} prelude
+ * Any Elf prelude that should get appended to the Twelf context
  * @returns {Promise<string>}
  */
-export async function elfToMdx(elfFilename) {
+export async function elfToMdx(elfFilename, prelude = []) {
  const elfFile = readFileSync(elfFilename, "utf-8");
 
  /* Parse out header */
@@ -87,7 +89,7 @@ export async function elfToMdx(elfFilename) {
  /** @type {string[]} */
  let body = [];
  /** @type {string[]} */
- let twelfcontext = [];
+ let twelfcontext = prelude.slice();
 
  /** @typedef {{ type: "twelf", subtype: null | "hidden" | "checked", accum: string[] }} TwelfState */
  /** @typedef {{ type: "markdown-block", subtype: "math" | "twelf" | "checkedtwelf", accum: string[] }} MarkdownBlockState */
@@ -104,7 +106,11 @@ export async function elfToMdx(elfFilename) {
  (state.subtype === "twelf" || state.subtype === "checkedtwelf"))
  )
  ) {
- throw new TypeError(`state ${state.type} - ${state.type !== 'markdown' ? state.subtype : 'none'}`);
+ throw new TypeError(
+ `state ${state.type} - ${
+ state.type !== "markdown" ? state.subtype : "none"
+ }`
+ );
  }
  mutablyTrimEmptyLines(state.accum);
 

wiki/elf-watcher.mjs

@@ -1,6 +1,14 @@
-import { existsSync, mkdirSync, readdirSync, watch, writeFileSync } from "fs";
+import {
+ existsSync,
+ mkdirSync,
+ readFileSync,
+ readdirSync,
+ watch,
+ writeFileSync,
+} from "fs";
 import { argv } from "process";
 import { elfToMdx } from "./elf-to-mdx.mjs";
+import { getImportedPrelude } from "./elf-wiki-imports.mjs";
 
 const DIR_OF_ELF = "pages";
 const DIR_OF_MDX = "src/content/docs/wiki";
@@ -17,10 +25,49 @@ async function mdxOfFile(file) {
  if (!file.endsWith(".elf") || !existsSync(elfname)) return;
 
  const base = file.slice(0, file.length - 4);
+ const cfgname = `${DIR_OF_ELF}/${base}.cfg`;
  const mdxname = `${DIR_OF_MDX}/${base}.mdx`;
  console.log(`elf->mdx transforming ${file}`);
- const mdxFile = await elfToMdx(elfname);
- writeFileSync(mdxname, mdxFile);
+ try {
+ const prelude = getImportedPrelude(`${DIR_OF_ELF}/`, file);
+ const mdxFile = await elfToMdx(
+ elfname,
+ prelude.map(({ file, contents }) => `%%! file: ${file}\n${contents}\n`)
+ );
+ const cfg = `
+% DO NOT EDIT
+% Automatically generated by running "npm run dev" or "npm run build" in the
+% wiki directory.
+% Edit twelf/wiki/${file} instead
+
+${prelude.map(({ file }) => file).join("\n")}
+${file}
+`.trim();
+ if (
+ !existsSync(cfgname) ||
+ readFileSync(cfgname).toString("utf-8") !== cfg
+ ) {
+ if (existsSync(cfgname)) {
+ console.log(`elf->mdx: updating ${cfgname}`);
+ }
+ writeFileSync(cfgname, cfg);
+ }
+
+ writeFileSync(mdxname, mdxFile);
+ } catch (e) {
+ console.log(e);
+ writeFileSync(
+ mdxname,
+ `
+---
+---
+
+Error transforming ${file}
+
+${e}
+`
+ );
+ }
 }
 
 console.log(`elf->mdx checking existing files...`);

wiki/elf-wiki-imports.mjs

@@ -0,0 +1,72 @@
+import { readFileSync } from "fs";
+
+/**
+ * Read the file's header to get all of the imported elf files
+ * (in reverse order)
+ *
+ * @param {string} contents
+ */
+function getImportedFilenames(contents) {
+ /**@type {string[]} */
+ const importStatements = [];
+
+ for (const line of contents.split("\n")) {
+ if (!line.startsWith("%%! ")) break;
+ if (line.startsWith("%%! import: ")) {
+ importStatements.push(line.slice(12).trim());
+ }
+ }
+
+ return importStatements;
+}
+
+/**
+ * Uses a DFS traversal
+ *
+ * @param {string} base
+ * Relative path of elf files
+ * @param {Set<string>} known
+ * Avoids double-importing by tracking all the filenames ever added to `accum` in the process of this traversal
+ * @param {{file: string, contents: string}[]} accum
+ * Accumulates the files, making sure that files are added after their dependencies
+ * @param {string} elfname
+ * Name of an ELF file that is a dependency of the file we're trying to load
+ */
+function dfsAccumImportedPrelude(base, known, accum, elfname) {
+ if (!elfname.match(/^[a-zA-Z.\-_0-9]*[.]elf*$/)) {
+ throw new Error(
+ `Imported path ${elfname} invalid: must include only letters, numbers, dashes, and underscores and end in .elf`
+ );
+ }
+ const contents = readFileSync(`${base}${elfname}`).toString("utf-8");
+ for (const importElf in getImportedFilenames(contents)) {
+ if (!known.has(importElf)) {
+ known.add(importElf);
+ dfsAccumImportedPrelude(base, known, accum, importElf);
+ }
+ }
+ accum.push({ file: elfname, contents });
+}
+
+/**
+ *
+ * @param {string} base
+ * Relative path of elf files
+ * @param {string} elfname
+ */
+export function getImportedPrelude(base, elfname) {
+ /**@type {Set<string>} */
+ const known = new Set();
+
+ /**@type {{file: string, contents: string}[]} */
+ const dependencies = [];
+
+ for (const file of getImportedFilenames(
+ readFileSync(`${base}${elfname}`).toString("utf-8")
+ )) {
+ known.add(file);
+ dfsAccumImportedPrelude(base, known, dependencies, file);
+ }
+
+ return dependencies;
+}

wiki/pages/proving-metatheorems-proving-totality-assertions-about-the-natural-numbers.elf

@@ -142,7 +142,7 @@ plus-bad-output : plus (s N1) N2 (s (s N3))
 
 Here we have insisted that the output of the premise has the form ``s N3`` for some ``N3``. Twelf correctly reports an output coverage error because this condition can fail (for example, if the premise was ``plus-z : plus z z z``). 
 
-Pattern-matching the output of a premise is like an [[inversion]] step in a proof: you're insisting that the premise derivation must conclude a particular fact that is more specific than the judgement form itself. For Twelf to accept a relation as total, Twelf must notice that all of these inversions are permissible. Twelf permits such inversions when it is readily apparent that they are justified, and those inversions that Twelf does not accept can be proved explicitly.
+Pattern-matching the output of a premise is like an <Todo>inversion</Todo> step in a proof: you're insisting that the premise derivation must conclude a particular fact that is more specific than the judgement form itself. For Twelf to accept a relation as total, Twelf must notice that all of these inversions are permissible. Twelf permits such inversions when it is readily apparent that they are justified, and those inversions that Twelf does not accept can be proved explicitly.
 
 In this example, we got an output coverage error because we constrained the output of the premise by insisting it be formed by a particular constant. The other way to get output coverage errors is to insist that the output of a premise be a variable that occurs elsewhere in the type. For example:
 

.gitignore

@@ -1,3 +1,4 @@
 CM
 .cm
-src/frontend/buildid.sml
+src/frontend/buildid.sml
+TEST/regression-wiki.txt

TEST/regression-wiki.mjs

@@ -1,3 +1,4 @@
+import { exec } from "child_process";
 import { readdirSync, writeFileSync } from "fs";
 
 /* Only files that are broken *on purpose* (because they're templates
@@ -28,18 +29,17 @@ const UNSAFE_WIKI_FILES = new Set([
  "user-hdeyoung-monweakfoc-elf",
 ]);
 
+exec("node elf-watcher.mjs", { cwd: "../wiki/" });
 const WIKI_TWELF_LOC = "../wiki/pages/";
 const cfgs = [];
 for (const file of readdirSync(WIKI_TWELF_LOC)) {
- if (file.endsWith(".elf")) {
+ if (file.endsWith(".cfg")) {
  const base = file.slice(0, file.length - 4);
  if (IGNORED_WIKI_FILES.has(base)) continue;
- const cfg = base + ".cfg";
- writeFileSync(WIKI_TWELF_LOC + cfg, file);
  cfgs.push(
  `test${
  UNSAFE_WIKI_FILES.has(base) ? "Unsafe" : ""
- } ${WIKI_TWELF_LOC}${cfg}`
+ } ${WIKI_TWELF_LOC}${file}`
  );
  }
 }

wiki/elf-to-mdx.mjs

@@ -67,9 +67,11 @@ async function hashToHex(content) {
  *
  * @param {string} elfFilename
  * The Elf file to process
+ * @param {string[]} prelude
+ * Any Elf prelude that should get appended to the Twelf context
  * @returns {Promise<string>}
  */
-export async function elfToMdx(elfFilename) {
+export async function elfToMdx(elfFilename, prelude = []) {
  const elfFile = readFileSync(elfFilename, "utf-8");
 
  /* Parse out header */
@@ -87,7 +89,7 @@ export async function elfToMdx(elfFilename) {
  /** @type {string[]} */
  let body = [];
  /** @type {string[]} */
- let twelfcontext = [];
+ let twelfcontext = prelude.slice();
 
  /** @typedef {{ type: "twelf", subtype: null | "hidden" | "checked", accum: string[] }} TwelfState */
  /** @typedef {{ type: "markdown-block", subtype: "math" | "twelf" | "checkedtwelf", accum: string[] }} MarkdownBlockState */
@@ -104,7 +106,11 @@ export async function elfToMdx(elfFilename) {
  (state.subtype === "twelf" || state.subtype === "checkedtwelf"))
  )
  ) {
- throw new TypeError(`state ${state.type} - ${state.type !== 'markdown' ? state.subtype : 'none'}`);
+ throw new TypeError(
+ `state ${state.type} - ${
+ state.type !== "markdown" ? state.subtype : "none"
+ }`
+ );
  }
  mutablyTrimEmptyLines(state.accum);
 

wiki/elf-watcher.mjs

@@ -1,6 +1,14 @@
-import { existsSync, mkdirSync, readdirSync, watch, writeFileSync } from "fs";
+import {
+ existsSync,
+ mkdirSync,
+ readFileSync,
+ readdirSync,
+ watch,
+ writeFileSync,
+} from "fs";
 import { argv } from "process";
 import { elfToMdx } from "./elf-to-mdx.mjs";
+import { getImportedPrelude } from "./elf-wiki-imports.mjs";
 
 const DIR_OF_ELF = "pages";
 const DIR_OF_MDX = "src/content/docs/wiki";
@@ -17,10 +25,49 @@ async function mdxOfFile(file) {
  if (!file.endsWith(".elf") || !existsSync(elfname)) return;
 
  const base = file.slice(0, file.length - 4);
+ const cfgname = `${DIR_OF_ELF}/${base}.cfg`;
  const mdxname = `${DIR_OF_MDX}/${base}.mdx`;
  console.log(`elf->mdx transforming ${file}`);
- const mdxFile = await elfToMdx(elfname);
- writeFileSync(mdxname, mdxFile);
+ try {
+ const prelude = getImportedPrelude(`${DIR_OF_ELF}/`, file);
+ const mdxFile = await elfToMdx(
+ elfname,
+ prelude.map(({ file, contents }) => `%%! file: ${file}\n${contents}\n`)
+ );
+ const cfg = `
+% DO NOT EDIT
+% Automatically generated by running "npm run dev" or "npm run build" in the
+% wiki directory.
+% Edit twelf/wiki/${file} instead
+
+${prelude.map(({ file }) => file).join("\n")}
+${file}
+`.trim();
+ if (
+ !existsSync(cfgname) ||
+ readFileSync(cfgname).toString("utf-8") !== cfg
+ ) {
+ if (existsSync(cfgname)) {
+ console.log(`elf->mdx: updating ${cfgname}`);
+ }
+ writeFileSync(cfgname, cfg);
+ }
+
+ writeFileSync(mdxname, mdxFile);
+ } catch (e) {
+ console.log(e);
+ writeFileSync(
+ mdxname,
+ `
+---
+---
+
+Error transforming ${file}
+
+${e}
+`
+ );
+ }
 }
 
 console.log(`elf->mdx checking existing files...`);

wiki/elf-wiki-imports.mjs

@@ -0,0 +1,72 @@
+import { readFileSync } from "fs";
+
+/**
+ * Read the file's header to get all of the imported elf files
+ * (in reverse order)
+ *
+ * @param {string} contents
+ */
+function getImportedFilenames(contents) {
+ /**@type {string[]} */
+ const importStatements = [];
+
+ for (const line of contents.split("\n")) {
+ if (!line.startsWith("%%! ")) break;
+ if (line.startsWith("%%! import: ")) {
+ importStatements.push(line.slice(12).trim());
+ }
+ }
+
+ return importStatements;
+}
+
+/**
+ * Uses a DFS traversal
+ *
+ * @param {string} base
+ * Relative path of elf files
+ * @param {Set<string>} known
+ * Avoids double-importing by tracking all the filenames ever added to `accum` in the process of this traversal
+ * @param {{file: string, contents: string}[]} accum
+ * Accumulates the files, making sure that files are added after their dependencies
+ * @param {string} elfname
+ * Name of an ELF file that is a dependency of the file we're trying to load
+ */
+function dfsAccumImportedPrelude(base, known, accum, elfname) {
+ if (!elfname.match(/^[a-zA-Z.\-_0-9]*[.]elf*$/)) {
+ throw new Error(
+ `Imported path ${elfname} invalid: must include only letters, numbers, dashes, and underscores and end in .elf`
+ );
+ }
+ const contents = readFileSync(`${base}${elfname}`).toString("utf-8");
+ for (const importElf in getImportedFilenames(contents)) {
+ if (!known.has(importElf)) {
+ known.add(importElf);
+ dfsAccumImportedPrelude(base, known, accum, importElf);
+ }
+ }
+ accum.push({ file: elfname, contents });
+}
+
+/**
+ *
+ * @param {string} base
+ * Relative path of elf files
+ * @param {string} elfname
+ */
+export function getImportedPrelude(base, elfname) {
+ /**@type {Set<string>} */
+ const known = new Set();
+
+ /**@type {{file: string, contents: string}[]} */
+ const dependencies = [];
+
+ for (const file of getImportedFilenames(
+ readFileSync(`${base}${elfname}`).toString("utf-8")
+ )) {
+ known.add(file);
+ dfsAccumImportedPrelude(base, known, dependencies, file);
+ }
+
+ return dependencies;
+}

wiki/pages/proving-metatheorems-proving-totality-assertions-about-the-natural-numbers.elf

@@ -142,7 +142,7 @@ plus-bad-output : plus (s N1) N2 (s (s N3))
 
 Here we have insisted that the output of the premise has the form ``s N3`` for some ``N3``. Twelf correctly reports an output coverage error because this condition can fail (for example, if the premise was ``plus-z : plus z z z``). 
 
-Pattern-matching the output of a premise is like an [[inversion]] step in a proof: you're insisting that the premise derivation must conclude a particular fact that is more specific than the judgement form itself. For Twelf to accept a relation as total, Twelf must notice that all of these inversions are permissible. Twelf permits such inversions when it is readily apparent that they are justified, and those inversions that Twelf does not accept can be proved explicitly.
+Pattern-matching the output of a premise is like an <Todo>inversion</Todo> step in a proof: you're insisting that the premise derivation must conclude a particular fact that is more specific than the judgement form itself. For Twelf to accept a relation as total, Twelf must notice that all of these inversions are permissible. Twelf permits such inversions when it is readily apparent that they are justified, and those inversions that Twelf does not accept can be proved explicitly.
 
 In this example, we got an output coverage error because we constrained the output of the premise by insisting it be formed by a particular constant. The other way to get output coverage errors is to insist that the output of a premise be a variable that occurs elsewhere in the type. For example:
 

.gitignore

@@ -1,3 +1,4 @@
 CM
 .cm
-src/frontend/buildid.sml
+src/frontend/buildid.sml
+TEST/regression-wiki.txt

TEST/regression-wiki.mjs

@@ -1,3 +1,4 @@
+import { exec } from "child_process";
 import { readdirSync, writeFileSync } from "fs";
 
 /* Only files that are broken *on purpose* (because they're templates
@@ -28,18 +29,17 @@ const UNSAFE_WIKI_FILES = new Set([
  "user-hdeyoung-monweakfoc-elf",
 ]);
 
+exec("node elf-watcher.mjs", { cwd: "../wiki/" });
 const WIKI_TWELF_LOC = "../wiki/pages/";
 const cfgs = [];
 for (const file of readdirSync(WIKI_TWELF_LOC)) {
- if (file.endsWith(".elf")) {
+ if (file.endsWith(".cfg")) {
  const base = file.slice(0, file.length - 4);
  if (IGNORED_WIKI_FILES.has(base)) continue;
- const cfg = base + ".cfg";
- writeFileSync(WIKI_TWELF_LOC + cfg, file);
  cfgs.push(
  `test${
  UNSAFE_WIKI_FILES.has(base) ? "Unsafe" : ""
- } ${WIKI_TWELF_LOC}${cfg}`
+ } ${WIKI_TWELF_LOC}${file}`
  );
  }
 }

wiki/elf-to-mdx.mjs

@@ -67,9 +67,11 @@ async function hashToHex(content) {
  *
  * @param {string} elfFilename
  * The Elf file to process
+ * @param {string[]} prelude
+ * Any Elf prelude that should get appended to the Twelf context
  * @returns {Promise<string>}
  */
-export async function elfToMdx(elfFilename) {
+export async function elfToMdx(elfFilename, prelude = []) {
  const elfFile = readFileSync(elfFilename, "utf-8");
 
  /* Parse out header */
@@ -87,7 +89,7 @@ export async function elfToMdx(elfFilename) {
  /** @type {string[]} */
  let body = [];
  /** @type {string[]} */
- let twelfcontext = [];
+ let twelfcontext = prelude.slice();
 
  /** @typedef {{ type: "twelf", subtype: null | "hidden" | "checked", accum: string[] }} TwelfState */
  /** @typedef {{ type: "markdown-block", subtype: "math" | "twelf" | "checkedtwelf", accum: string[] }} MarkdownBlockState */
@@ -104,7 +106,11 @@ export async function elfToMdx(elfFilename) {
  (state.subtype === "twelf" || state.subtype === "checkedtwelf"))
  )
  ) {
- throw new TypeError(`state ${state.type} - ${state.type !== 'markdown' ? state.subtype : 'none'}`);
+ throw new TypeError(
+ `state ${state.type} - ${
+ state.type !== "markdown" ? state.subtype : "none"
+ }`
+ );
  }
  mutablyTrimEmptyLines(state.accum);
 

wiki/elf-watcher.mjs

@@ -1,6 +1,14 @@
-import { existsSync, mkdirSync, readdirSync, watch, writeFileSync } from "fs";
+import {
+ existsSync,
+ mkdirSync,
+ readFileSync,
+ readdirSync,
+ watch,
+ writeFileSync,
+} from "fs";
 import { argv } from "process";
 import { elfToMdx } from "./elf-to-mdx.mjs";
+import { getImportedPrelude } from "./elf-wiki-imports.mjs";
 
 const DIR_OF_ELF = "pages";
 const DIR_OF_MDX = "src/content/docs/wiki";
@@ -17,10 +25,49 @@ async function mdxOfFile(file) {
  if (!file.endsWith(".elf") || !existsSync(elfname)) return;
 
  const base = file.slice(0, file.length - 4);
+ const cfgname = `${DIR_OF_ELF}/${base}.cfg`;
  const mdxname = `${DIR_OF_MDX}/${base}.mdx`;
  console.log(`elf->mdx transforming ${file}`);
- const mdxFile = await elfToMdx(elfname);
- writeFileSync(mdxname, mdxFile);
+ try {
+ const prelude = getImportedPrelude(`${DIR_OF_ELF}/`, file);
+ const mdxFile = await elfToMdx(
+ elfname,
+ prelude.map(({ file, contents }) => `%%! file: ${file}\n${contents}\n`)
+ );
+ const cfg = `
+% DO NOT EDIT
+% Automatically generated by running "npm run dev" or "npm run build" in the
+% wiki directory.
+% Edit twelf/wiki/${file} instead
+
+${prelude.map(({ file }) => file).join("\n")}
+${file}
+`.trim();
+ if (
+ !existsSync(cfgname) ||
+ readFileSync(cfgname).toString("utf-8") !== cfg
+ ) {
+ if (existsSync(cfgname)) {
+ console.log(`elf->mdx: updating ${cfgname}`);
+ }
+ writeFileSync(cfgname, cfg);
+ }
+
+ writeFileSync(mdxname, mdxFile);
+ } catch (e) {
+ console.log(e);
+ writeFileSync(
+ mdxname,
+ `
+---
+---
+
+Error transforming ${file}
+
+${e}
+`
+ );
+ }
 }
 
 console.log(`elf->mdx checking existing files...`);

wiki/elf-wiki-imports.mjs

@@ -0,0 +1,72 @@
+import { readFileSync } from "fs";
+
+/**
+ * Read the file's header to get all of the imported elf files
+ * (in reverse order)
+ *
+ * @param {string} contents
+ */
+function getImportedFilenames(contents) {
+ /**@type {string[]} */
+ const importStatements = [];
+
+ for (const line of contents.split("\n")) {
+ if (!line.startsWith("%%! ")) break;
+ if (line.startsWith("%%! import: ")) {
+ importStatements.push(line.slice(12).trim());
+ }
+ }
+
+ return importStatements;
+}
+
+/**
+ * Uses a DFS traversal
+ *
+ * @param {string} base
+ * Relative path of elf files
+ * @param {Set<string>} known
+ * Avoids double-importing by tracking all the filenames ever added to `accum` in the process of this traversal
+ * @param {{file: string, contents: string}[]} accum
+ * Accumulates the files, making sure that files are added after their dependencies
+ * @param {string} elfname
+ * Name of an ELF file that is a dependency of the file we're trying to load
+ */
+function dfsAccumImportedPrelude(base, known, accum, elfname) {
+ if (!elfname.match(/^[a-zA-Z.\-_0-9]*[.]elf*$/)) {
+ throw new Error(
+ `Imported path ${elfname} invalid: must include only letters, numbers, dashes, and underscores and end in .elf`
+ );
+ }
+ const contents = readFileSync(`${base}${elfname}`).toString("utf-8");
+ for (const importElf in getImportedFilenames(contents)) {
+ if (!known.has(importElf)) {
+ known.add(importElf);
+ dfsAccumImportedPrelude(base, known, accum, importElf);
+ }
+ }
+ accum.push({ file: elfname, contents });
+}
+
+/**
+ *
+ * @param {string} base
+ * Relative path of elf files
+ * @param {string} elfname
+ */
+export function getImportedPrelude(base, elfname) {
+ /**@type {Set<string>} */
+ const known = new Set();
+
+ /**@type {{file: string, contents: string}[]} */
+ const dependencies = [];
+
+ for (const file of getImportedFilenames(
+ readFileSync(`${base}${elfname}`).toString("utf-8")
+ )) {
+ known.add(file);
+ dfsAccumImportedPrelude(base, known, dependencies, file);
+ }
+
+ return dependencies;
+}

wiki/pages/proving-metatheorems-proving-totality-assertions-about-the-natural-numbers.elf

@@ -142,7 +142,7 @@ plus-bad-output : plus (s N1) N2 (s (s N3))
 
 Here we have insisted that the output of the premise has the form ``s N3`` for some ``N3``. Twelf correctly reports an output coverage error because this condition can fail (for example, if the premise was ``plus-z : plus z z z``). 
 
-Pattern-matching the output of a premise is like an [[inversion]] step in a proof: you're insisting that the premise derivation must conclude a particular fact that is more specific than the judgement form itself. For Twelf to accept a relation as total, Twelf must notice that all of these inversions are permissible. Twelf permits such inversions when it is readily apparent that they are justified, and those inversions that Twelf does not accept can be proved explicitly.
+Pattern-matching the output of a premise is like an <Todo>inversion</Todo> step in a proof: you're insisting that the premise derivation must conclude a particular fact that is more specific than the judgement form itself. For Twelf to accept a relation as total, Twelf must notice that all of these inversions are permissible. Twelf permits such inversions when it is readily apparent that they are justified, and those inversions that Twelf does not accept can be proved explicitly.
 
 In this example, we got an output coverage error because we constrained the output of the premise by insisting it be formed by a particular constant. The other way to get output coverage errors is to insist that the output of a premise be a variable that occurs elsewhere in the type. For example:
 

.gitignore

@@ -1,3 +1,4 @@
 CM
 .cm
-src/frontend/buildid.sml
+src/frontend/buildid.sml
+TEST/regression-wiki.txt

TEST/regression-wiki.mjs

@@ -1,3 +1,4 @@
+import { exec } from "child_process";
 import { readdirSync, writeFileSync } from "fs";
 
 /* Only files that are broken *on purpose* (because they're templates
@@ -28,18 +29,17 @@ const UNSAFE_WIKI_FILES = new Set([
  "user-hdeyoung-monweakfoc-elf",
 ]);
 
+exec("node elf-watcher.mjs", { cwd: "../wiki/" });
 const WIKI_TWELF_LOC = "../wiki/pages/";
 const cfgs = [];
 for (const file of readdirSync(WIKI_TWELF_LOC)) {
- if (file.endsWith(".elf")) {
+ if (file.endsWith(".cfg")) {
  const base = file.slice(0, file.length - 4);
  if (IGNORED_WIKI_FILES.has(base)) continue;
- const cfg = base + ".cfg";
- writeFileSync(WIKI_TWELF_LOC + cfg, file);
  cfgs.push(
  `test${
  UNSAFE_WIKI_FILES.has(base) ? "Unsafe" : ""
- } ${WIKI_TWELF_LOC}${cfg}`
+ } ${WIKI_TWELF_LOC}${file}`
  );
  }
 }

wiki/elf-to-mdx.mjs

@@ -67,9 +67,11 @@ async function hashToHex(content) {
  *
  * @param {string} elfFilename
  * The Elf file to process
+ * @param {string[]} prelude
+ * Any Elf prelude that should get appended to the Twelf context
  * @returns {Promise<string>}
  */
-export async function elfToMdx(elfFilename) {
+export async function elfToMdx(elfFilename, prelude = []) {
  const elfFile = readFileSync(elfFilename, "utf-8");
 
  /* Parse out header */
@@ -87,7 +89,7 @@ export async function elfToMdx(elfFilename) {
  /** @type {string[]} */
  let body = [];
  /** @type {string[]} */
- let twelfcontext = [];
+ let twelfcontext = prelude.slice();
 
  /** @typedef {{ type: "twelf", subtype: null | "hidden" | "checked", accum: string[] }} TwelfState */
  /** @typedef {{ type: "markdown-block", subtype: "math" | "twelf" | "checkedtwelf", accum: string[] }} MarkdownBlockState */
@@ -104,7 +106,11 @@ export async function elfToMdx(elfFilename) {
  (state.subtype === "twelf" || state.subtype === "checkedtwelf"))
  )
  ) {
- throw new TypeError(`state ${state.type} - ${state.type !== 'markdown' ? state.subtype : 'none'}`);
+ throw new TypeError(
+ `state ${state.type} - ${
+ state.type !== "markdown" ? state.subtype : "none"
+ }`
+ );
  }
  mutablyTrimEmptyLines(state.accum);
 

wiki/elf-watcher.mjs

@@ -1,6 +1,14 @@
-import { existsSync, mkdirSync, readdirSync, watch, writeFileSync } from "fs";
+import {
+ existsSync,
+ mkdirSync,
+ readFileSync,
+ readdirSync,
+ watch,
+ writeFileSync,
+} from "fs";
 import { argv } from "process";
 import { elfToMdx } from "./elf-to-mdx.mjs";
+import { getImportedPrelude } from "./elf-wiki-imports.mjs";
 
 const DIR_OF_ELF = "pages";
 const DIR_OF_MDX = "src/content/docs/wiki";
@@ -17,10 +25,49 @@ async function mdxOfFile(file) {
  if (!file.endsWith(".elf") || !existsSync(elfname)) return;
 
  const base = file.slice(0, file.length - 4);
+ const cfgname = `${DIR_OF_ELF}/${base}.cfg`;
  const mdxname = `${DIR_OF_MDX}/${base}.mdx`;
  console.log(`elf->mdx transforming ${file}`);
- const mdxFile = await elfToMdx(elfname);
- writeFileSync(mdxname, mdxFile);
+ try {
+ const prelude = getImportedPrelude(`${DIR_OF_ELF}/`, file);
+ const mdxFile = await elfToMdx(
+ elfname,
+ prelude.map(({ file, contents }) => `%%! file: ${file}\n${contents}\n`)
+ );
+ const cfg = `
+% DO NOT EDIT
+% Automatically generated by running "npm run dev" or "npm run build" in the
+% wiki directory.
+% Edit twelf/wiki/${file} instead
+
+${prelude.map(({ file }) => file).join("\n")}
+${file}
+`.trim();
+ if (
+ !existsSync(cfgname) ||
+ readFileSync(cfgname).toString("utf-8") !== cfg
+ ) {
+ if (existsSync(cfgname)) {
+ console.log(`elf->mdx: updating ${cfgname}`);
+ }
+ writeFileSync(cfgname, cfg);
+ }
+
+ writeFileSync(mdxname, mdxFile);
+ } catch (e) {
+ console.log(e);
+ writeFileSync(
+ mdxname,
+ `
+---
+---
+
+Error transforming ${file}
+
+${e}
+`
+ );
+ }
 }
 
 console.log(`elf->mdx checking existing files...`);

wiki/elf-wiki-imports.mjs

@@ -0,0 +1,72 @@
+import { readFileSync } from "fs";
+
+/**
+ * Read the file's header to get all of the imported elf files
+ * (in reverse order)
+ *
+ * @param {string} contents
+ */
+function getImportedFilenames(contents) {
+ /**@type {string[]} */
+ const importStatements = [];
+
+ for (const line of contents.split("\n")) {
+ if (!line.startsWith("%%! ")) break;
+ if (line.startsWith("%%! import: ")) {
+ importStatements.push(line.slice(12).trim());
+ }
+ }
+
+ return importStatements;
+}
+
+/**
+ * Uses a DFS traversal
+ *
+ * @param {string} base
+ * Relative path of elf files
+ * @param {Set<string>} known
+ * Avoids double-importing by tracking all the filenames ever added to `accum` in the process of this traversal
+ * @param {{file: string, contents: string}[]} accum
+ * Accumulates the files, making sure that files are added after their dependencies
+ * @param {string} elfname
+ * Name of an ELF file that is a dependency of the file we're trying to load
+ */
+function dfsAccumImportedPrelude(base, known, accum, elfname) {
+ if (!elfname.match(/^[a-zA-Z.\-_0-9]*[.]elf*$/)) {
+ throw new Error(
+ `Imported path ${elfname} invalid: must include only letters, numbers, dashes, and underscores and end in .elf`
+ );
+ }
+ const contents = readFileSync(`${base}${elfname}`).toString("utf-8");
+ for (const importElf in getImportedFilenames(contents)) {
+ if (!known.has(importElf)) {
+ known.add(importElf);
+ dfsAccumImportedPrelude(base, known, accum, importElf);
+ }
+ }
+ accum.push({ file: elfname, contents });
+}
+
+/**
+ *
+ * @param {string} base
+ * Relative path of elf files
+ * @param {string} elfname
+ */
+export function getImportedPrelude(base, elfname) {
+ /**@type {Set<string>} */
+ const known = new Set();
+
+ /**@type {{file: string, contents: string}[]} */
+ const dependencies = [];
+
+ for (const file of getImportedFilenames(
+ readFileSync(`${base}${elfname}`).toString("utf-8")
+ )) {
+ known.add(file);
+ dfsAccumImportedPrelude(base, known, dependencies, file);
+ }
+
+ return dependencies;
+}

wiki/pages/proving-metatheorems-proving-totality-assertions-about-the-natural-numbers.elf

@@ -142,7 +142,7 @@ plus-bad-output : plus (s N1) N2 (s (s N3))
 
 Here we have insisted that the output of the premise has the form ``s N3`` for some ``N3``. Twelf correctly reports an output coverage error because this condition can fail (for example, if the premise was ``plus-z : plus z z z``). 
 
-Pattern-matching the output of a premise is like an [[inversion]] step in a proof: you're insisting that the premise derivation must conclude a particular fact that is more specific than the judgement form itself. For Twelf to accept a relation as total, Twelf must notice that all of these inversions are permissible. Twelf permits such inversions when it is readily apparent that they are justified, and those inversions that Twelf does not accept can be proved explicitly.
+Pattern-matching the output of a premise is like an <Todo>inversion</Todo> step in a proof: you're insisting that the premise derivation must conclude a particular fact that is more specific than the judgement form itself. For Twelf to accept a relation as total, Twelf must notice that all of these inversions are permissible. Twelf permits such inversions when it is readily apparent that they are justified, and those inversions that Twelf does not accept can be proved explicitly.
 
 In this example, we got an output coverage error because we constrained the output of the premise by insisting it be formed by a particular constant. The other way to get output coverage errors is to insist that the output of a premise be a variable that occurs elsewhere in the type. For example:
 

.gitignore

@@ -1,3 +1,4 @@
 CM
 .cm
-src/frontend/buildid.sml
+src/frontend/buildid.sml
+TEST/regression-wiki.txt

TEST/regression-wiki.mjs

@@ -1,3 +1,4 @@
+import { exec } from "child_process";
 import { readdirSync, writeFileSync } from "fs";
 
 /* Only files that are broken *on purpose* (because they're templates
@@ -28,18 +29,17 @@ const UNSAFE_WIKI_FILES = new Set([
  "user-hdeyoung-monweakfoc-elf",
 ]);
 
+exec("node elf-watcher.mjs", { cwd: "../wiki/" });
 const WIKI_TWELF_LOC = "../wiki/pages/";
 const cfgs = [];
 for (const file of readdirSync(WIKI_TWELF_LOC)) {
- if (file.endsWith(".elf")) {
+ if (file.endsWith(".cfg")) {
  const base = file.slice(0, file.length - 4);
  if (IGNORED_WIKI_FILES.has(base)) continue;
- const cfg = base + ".cfg";
- writeFileSync(WIKI_TWELF_LOC + cfg, file);
  cfgs.push(
  `test${
  UNSAFE_WIKI_FILES.has(base) ? "Unsafe" : ""
- } ${WIKI_TWELF_LOC}${cfg}`
+ } ${WIKI_TWELF_LOC}${file}`
  );
  }
 }

wiki/elf-to-mdx.mjs

@@ -67,9 +67,11 @@ async function hashToHex(content) {
  *
  * @param {string} elfFilename
  * The Elf file to process
+ * @param {string[]} prelude
+ * Any Elf prelude that should get appended to the Twelf context
  * @returns {Promise<string>}
  */
-export async function elfToMdx(elfFilename) {
+export async function elfToMdx(elfFilename, prelude = []) {
  const elfFile = readFileSync(elfFilename, "utf-8");
 
  /* Parse out header */
@@ -87,7 +89,7 @@ export async function elfToMdx(elfFilename) {
  /** @type {string[]} */
  let body = [];
  /** @type {string[]} */
- let twelfcontext = [];
+ let twelfcontext = prelude.slice();
 
  /** @typedef {{ type: "twelf", subtype: null | "hidden" | "checked", accum: string[] }} TwelfState */
  /** @typedef {{ type: "markdown-block", subtype: "math" | "twelf" | "checkedtwelf", accum: string[] }} MarkdownBlockState */
@@ -104,7 +106,11 @@ export async function elfToMdx(elfFilename) {
  (state.subtype === "twelf" || state.subtype === "checkedtwelf"))
  )
  ) {
- throw new TypeError(`state ${state.type} - ${state.type !== 'markdown' ? state.subtype : 'none'}`);
+ throw new TypeError(
+ `state ${state.type} - ${
+ state.type !== "markdown" ? state.subtype : "none"
+ }`
+ );
  }
  mutablyTrimEmptyLines(state.accum);
 

wiki/elf-watcher.mjs

@@ -1,6 +1,14 @@
-import { existsSync, mkdirSync, readdirSync, watch, writeFileSync } from "fs";
+import {
+ existsSync,
+ mkdirSync,
+ readFileSync,
+ readdirSync,
+ watch,
+ writeFileSync,
+} from "fs";
 import { argv } from "process";
 import { elfToMdx } from "./elf-to-mdx.mjs";
+import { getImportedPrelude } from "./elf-wiki-imports.mjs";
 
 const DIR_OF_ELF = "pages";
 const DIR_OF_MDX = "src/content/docs/wiki";
@@ -17,10 +25,49 @@ async function mdxOfFile(file) {
  if (!file.endsWith(".elf") || !existsSync(elfname)) return;
 
  const base = file.slice(0, file.length - 4);
+ const cfgname = `${DIR_OF_ELF}/${base}.cfg`;
  const mdxname = `${DIR_OF_MDX}/${base}.mdx`;
  console.log(`elf->mdx transforming ${file}`);
- const mdxFile = await elfToMdx(elfname);
- writeFileSync(mdxname, mdxFile);
+ try {
+ const prelude = getImportedPrelude(`${DIR_OF_ELF}/`, file);
+ const mdxFile = await elfToMdx(
+ elfname,
+ prelude.map(({ file, contents }) => `%%! file: ${file}\n${contents}\n`)
+ );
+ const cfg = `
+% DO NOT EDIT
+% Automatically generated by running "npm run dev" or "npm run build" in the
+% wiki directory.
+% Edit twelf/wiki/${file} instead
+
+${prelude.map(({ file }) => file).join("\n")}
+${file}
+`.trim();
+ if (
+ !existsSync(cfgname) ||
+ readFileSync(cfgname).toString("utf-8") !== cfg
+ ) {
+ if (existsSync(cfgname)) {
+ console.log(`elf->mdx: updating ${cfgname}`);
+ }
+ writeFileSync(cfgname, cfg);
+ }
+
+ writeFileSync(mdxname, mdxFile);
+ } catch (e) {
+ console.log(e);
+ writeFileSync(
+ mdxname,
+ `
+---
+---
+
+Error transforming ${file}
+
+${e}
+`
+ );
+ }
 }
 
 console.log(`elf->mdx checking existing files...`);

wiki/elf-wiki-imports.mjs

@@ -0,0 +1,72 @@
+import { readFileSync } from "fs";
+
+/**
+ * Read the file's header to get all of the imported elf files
+ * (in reverse order)
+ *
+ * @param {string} contents
+ */
+function getImportedFilenames(contents) {
+ /**@type {string[]} */
+ const importStatements = [];
+
+ for (const line of contents.split("\n")) {
+ if (!line.startsWith("%%! ")) break;
+ if (line.startsWith("%%! import: ")) {
+ importStatements.push(line.slice(12).trim());
+ }
+ }
+
+ return importStatements;
+}
+
+/**
+ * Uses a DFS traversal
+ *
+ * @param {string} base
+ * Relative path of elf files
+ * @param {Set<string>} known
+ * Avoids double-importing by tracking all the filenames ever added to `accum` in the process of this traversal
+ * @param {{file: string, contents: string}[]} accum
+ * Accumulates the files, making sure that files are added after their dependencies
+ * @param {string} elfname
+ * Name of an ELF file that is a dependency of the file we're trying to load
+ */
+function dfsAccumImportedPrelude(base, known, accum, elfname) {
+ if (!elfname.match(/^[a-zA-Z.\-_0-9]*[.]elf*$/)) {
+ throw new Error(
+ `Imported path ${elfname} invalid: must include only letters, numbers, dashes, and underscores and end in .elf`
+ );
+ }
+ const contents = readFileSync(`${base}${elfname}`).toString("utf-8");
+ for (const importElf in getImportedFilenames(contents)) {
+ if (!known.has(importElf)) {
+ known.add(importElf);
+ dfsAccumImportedPrelude(base, known, accum, importElf);
+ }
+ }
+ accum.push({ file: elfname, contents });
+}
+
+/**
+ *
+ * @param {string} base
+ * Relative path of elf files
+ * @param {string} elfname
+ */
+export function getImportedPrelude(base, elfname) {
+ /**@type {Set<string>} */
+ const known = new Set();
+
+ /**@type {{file: string, contents: string}[]} */
+ const dependencies = [];
+
+ for (const file of getImportedFilenames(
+ readFileSync(`${base}${elfname}`).toString("utf-8")
+ )) {
+ known.add(file);
+ dfsAccumImportedPrelude(base, known, dependencies, file);
+ }
+
+ return dependencies;
+}

wiki/pages/proving-metatheorems-proving-totality-assertions-about-the-natural-numbers.elf

@@ -142,7 +142,7 @@ plus-bad-output : plus (s N1) N2 (s (s N3))
 
 Here we have insisted that the output of the premise has the form ``s N3`` for some ``N3``. Twelf correctly reports an output coverage error because this condition can fail (for example, if the premise was ``plus-z : plus z z z``). 
 
-Pattern-matching the output of a premise is like an [[inversion]] step in a proof: you're insisting that the premise derivation must conclude a particular fact that is more specific than the judgement form itself. For Twelf to accept a relation as total, Twelf must notice that all of these inversions are permissible. Twelf permits such inversions when it is readily apparent that they are justified, and those inversions that Twelf does not accept can be proved explicitly.
+Pattern-matching the output of a premise is like an <Todo>inversion</Todo> step in a proof: you're insisting that the premise derivation must conclude a particular fact that is more specific than the judgement form itself. For Twelf to accept a relation as total, Twelf must notice that all of these inversions are permissible. Twelf permits such inversions when it is readily apparent that they are justified, and those inversions that Twelf does not accept can be proved explicitly.
 
 In this example, we got an output coverage error because we constrained the output of the premise by insisting it be formed by a particular constant. The other way to get output coverage errors is to insist that the output of a premise be a variable that occurs elsewhere in the type. For example:
 

.gitignore

@@ -1,3 +1,4 @@
 CM
 .cm
-src/frontend/buildid.sml
+src/frontend/buildid.sml
+TEST/regression-wiki.txt

TEST/regression-wiki.mjs

@@ -1,3 +1,4 @@
+import { exec } from "child_process";
 import { readdirSync, writeFileSync } from "fs";
 
 /* Only files that are broken *on purpose* (because they're templates
@@ -28,18 +29,17 @@ const UNSAFE_WIKI_FILES = new Set([
  "user-hdeyoung-monweakfoc-elf",
 ]);
 
+exec("node elf-watcher.mjs", { cwd: "../wiki/" });
 const WIKI_TWELF_LOC = "../wiki/pages/";
 const cfgs = [];
 for (const file of readdirSync(WIKI_TWELF_LOC)) {
- if (file.endsWith(".elf")) {
+ if (file.endsWith(".cfg")) {
  const base = file.slice(0, file.length - 4);
  if (IGNORED_WIKI_FILES.has(base)) continue;
- const cfg = base + ".cfg";
- writeFileSync(WIKI_TWELF_LOC + cfg, file);
  cfgs.push(
  `test${
  UNSAFE_WIKI_FILES.has(base) ? "Unsafe" : ""
- } ${WIKI_TWELF_LOC}${cfg}`
+ } ${WIKI_TWELF_LOC}${file}`
  );
  }
 }

wiki/elf-to-mdx.mjs

@@ -67,9 +67,11 @@ async function hashToHex(content) {
  *
  * @param {string} elfFilename
  * The Elf file to process
+ * @param {string[]} prelude
+ * Any Elf prelude that should get appended to the Twelf context
  * @returns {Promise<string>}
  */
-export async function elfToMdx(elfFilename) {
+export async function elfToMdx(elfFilename, prelude = []) {
  const elfFile = readFileSync(elfFilename, "utf-8");
 
  /* Parse out header */
@@ -87,7 +89,7 @@ export async function elfToMdx(elfFilename) {
  /** @type {string[]} */
  let body = [];
  /** @type {string[]} */
- let twelfcontext = [];
+ let twelfcontext = prelude.slice();
 
  /** @typedef {{ type: "twelf", subtype: null | "hidden" | "checked", accum: string[] }} TwelfState */
  /** @typedef {{ type: "markdown-block", subtype: "math" | "twelf" | "checkedtwelf", accum: string[] }} MarkdownBlockState */
@@ -104,7 +106,11 @@ export async function elfToMdx(elfFilename) {
  (state.subtype === "twelf" || state.subtype === "checkedtwelf"))
  )
  ) {
- throw new TypeError(`state ${state.type} - ${state.type !== 'markdown' ? state.subtype : 'none'}`);
+ throw new TypeError(
+ `state ${state.type} - ${
+ state.type !== "markdown" ? state.subtype : "none"
+ }`
+ );
  }
  mutablyTrimEmptyLines(state.accum);
 

wiki/elf-watcher.mjs

@@ -1,6 +1,14 @@
-import { existsSync, mkdirSync, readdirSync, watch, writeFileSync } from "fs";
+import {
+ existsSync,
+ mkdirSync,
+ readFileSync,
+ readdirSync,
+ watch,
+ writeFileSync,
+} from "fs";
 import { argv } from "process";
 import { elfToMdx } from "./elf-to-mdx.mjs";
+import { getImportedPrelude } from "./elf-wiki-imports.mjs";
 
 const DIR_OF_ELF = "pages";
 const DIR_OF_MDX = "src/content/docs/wiki";
@@ -17,10 +25,49 @@ async function mdxOfFile(file) {
  if (!file.endsWith(".elf") || !existsSync(elfname)) return;
 
  const base = file.slice(0, file.length - 4);
+ const cfgname = `${DIR_OF_ELF}/${base}.cfg`;
  const mdxname = `${DIR_OF_MDX}/${base}.mdx`;
  console.log(`elf->mdx transforming ${file}`);
- const mdxFile = await elfToMdx(elfname);
- writeFileSync(mdxname, mdxFile);
+ try {
+ const prelude = getImportedPrelude(`${DIR_OF_ELF}/`, file);
+ const mdxFile = await elfToMdx(
+ elfname,
+ prelude.map(({ file, contents }) => `%%! file: ${file}\n${contents}\n`)
+ );
+ const cfg = `
+% DO NOT EDIT
+% Automatically generated by running "npm run dev" or "npm run build" in the
+% wiki directory.
+% Edit twelf/wiki/${file} instead
+
+${prelude.map(({ file }) => file).join("\n")}
+${file}
+`.trim();
+ if (
+ !existsSync(cfgname) ||
+ readFileSync(cfgname).toString("utf-8") !== cfg
+ ) {
+ if (existsSync(cfgname)) {
+ console.log(`elf->mdx: updating ${cfgname}`);
+ }
+ writeFileSync(cfgname, cfg);
+ }
+
+ writeFileSync(mdxname, mdxFile);
+ } catch (e) {
+ console.log(e);
+ writeFileSync(
+ mdxname,
+ `
+---
+---
+
+Error transforming ${file}
+
+${e}
+`
+ );
+ }
 }
 
 console.log(`elf->mdx checking existing files...`);

wiki/elf-wiki-imports.mjs

@@ -0,0 +1,72 @@
+import { readFileSync } from "fs";
+
+/**
+ * Read the file's header to get all of the imported elf files
+ * (in reverse order)
+ *
+ * @param {string} contents
+ */
+function getImportedFilenames(contents) {
+ /**@type {string[]} */
+ const importStatements = [];
+
+ for (const line of contents.split("\n")) {
+ if (!line.startsWith("%%! ")) break;
+ if (line.startsWith("%%! import: ")) {
+ importStatements.push(line.slice(12).trim());
+ }
+ }
+
+ return importStatements;
+}
+
+/**
+ * Uses a DFS traversal
+ *
+ * @param {string} base
+ * Relative path of elf files
+ * @param {Set<string>} known
+ * Avoids double-importing by tracking all the filenames ever added to `accum` in the process of this traversal
+ * @param {{file: string, contents: string}[]} accum
+ * Accumulates the files, making sure that files are added after their dependencies
+ * @param {string} elfname
+ * Name of an ELF file that is a dependency of the file we're trying to load
+ */
+function dfsAccumImportedPrelude(base, known, accum, elfname) {
+ if (!elfname.match(/^[a-zA-Z.\-_0-9]*[.]elf*$/)) {
+ throw new Error(
+ `Imported path ${elfname} invalid: must include only letters, numbers, dashes, and underscores and end in .elf`
+ );
+ }
+ const contents = readFileSync(`${base}${elfname}`).toString("utf-8");
+ for (const importElf in getImportedFilenames(contents)) {
+ if (!known.has(importElf)) {
+ known.add(importElf);
+ dfsAccumImportedPrelude(base, known, accum, importElf);
+ }
+ }
+ accum.push({ file: elfname, contents });
+}
+
+/**
+ *
+ * @param {string} base
+ * Relative path of elf files
+ * @param {string} elfname
+ */
+export function getImportedPrelude(base, elfname) {
+ /**@type {Set<string>} */
+ const known = new Set();
+
+ /**@type {{file: string, contents: string}[]} */
+ const dependencies = [];
+
+ for (const file of getImportedFilenames(
+ readFileSync(`${base}${elfname}`).toString("utf-8")
+ )) {
+ known.add(file);
+ dfsAccumImportedPrelude(base, known, dependencies, file);
+ }
+
+ return dependencies;
+}

wiki/pages/proving-metatheorems-proving-totality-assertions-about-the-natural-numbers.elf

@@ -142,7 +142,7 @@ plus-bad-output : plus (s N1) N2 (s (s N3))
 
 Here we have insisted that the output of the premise has the form ``s N3`` for some ``N3``. Twelf correctly reports an output coverage error because this condition can fail (for example, if the premise was ``plus-z : plus z z z``). 
 
-Pattern-matching the output of a premise is like an [[inversion]] step in a proof: you're insisting that the premise derivation must conclude a particular fact that is more specific than the judgement form itself. For Twelf to accept a relation as total, Twelf must notice that all of these inversions are permissible. Twelf permits such inversions when it is readily apparent that they are justified, and those inversions that Twelf does not accept can be proved explicitly.
+Pattern-matching the output of a premise is like an <Todo>inversion</Todo> step in a proof: you're insisting that the premise derivation must conclude a particular fact that is more specific than the judgement form itself. For Twelf to accept a relation as total, Twelf must notice that all of these inversions are permissible. Twelf permits such inversions when it is readily apparent that they are justified, and those inversions that Twelf does not accept can be proved explicitly.
 
 In this example, we got an output coverage error because we constrained the output of the premise by insisting it be formed by a particular constant. The other way to get output coverage errors is to insist that the output of a premise be a variable that occurs elsewhere in the type. For example:
 

.gitignore

@@ -1,3 +1,4 @@
 CM
 .cm
-src/frontend/buildid.sml
+src/frontend/buildid.sml
+TEST/regression-wiki.txt

TEST/regression-wiki.mjs

@@ -1,3 +1,4 @@
+import { exec } from "child_process";
 import { readdirSync, writeFileSync } from "fs";
 
 /* Only files that are broken *on purpose* (because they're templates
@@ -28,18 +29,17 @@ const UNSAFE_WIKI_FILES = new Set([
  "user-hdeyoung-monweakfoc-elf",
 ]);
 
+exec("node elf-watcher.mjs", { cwd: "../wiki/" });
 const WIKI_TWELF_LOC = "../wiki/pages/";
 const cfgs = [];
 for (const file of readdirSync(WIKI_TWELF_LOC)) {
- if (file.endsWith(".elf")) {
+ if (file.endsWith(".cfg")) {
  const base = file.slice(0, file.length - 4);
  if (IGNORED_WIKI_FILES.has(base)) continue;
- const cfg = base + ".cfg";
- writeFileSync(WIKI_TWELF_LOC + cfg, file);
  cfgs.push(
  `test${
  UNSAFE_WIKI_FILES.has(base) ? "Unsafe" : ""
- } ${WIKI_TWELF_LOC}${cfg}`
+ } ${WIKI_TWELF_LOC}${file}`
  );
  }
 }

wiki/elf-to-mdx.mjs

@@ -67,9 +67,11 @@ async function hashToHex(content) {
  *
  * @param {string} elfFilename
  * The Elf file to process
+ * @param {string[]} prelude
+ * Any Elf prelude that should get appended to the Twelf context
  * @returns {Promise<string>}
  */
-export async function elfToMdx(elfFilename) {
+export async function elfToMdx(elfFilename, prelude = []) {
  const elfFile = readFileSync(elfFilename, "utf-8");
 
  /* Parse out header */
@@ -87,7 +89,7 @@ export async function elfToMdx(elfFilename) {
  /** @type {string[]} */
  let body = [];
  /** @type {string[]} */
- let twelfcontext = [];
+ let twelfcontext = prelude.slice();
 
  /** @typedef {{ type: "twelf", subtype: null | "hidden" | "checked", accum: string[] }} TwelfState */
  /** @typedef {{ type: "markdown-block", subtype: "math" | "twelf" | "checkedtwelf", accum: string[] }} MarkdownBlockState */
@@ -104,7 +106,11 @@ export async function elfToMdx(elfFilename) {
  (state.subtype === "twelf" || state.subtype === "checkedtwelf"))
  )
  ) {
- throw new TypeError(`state ${state.type} - ${state.type !== 'markdown' ? state.subtype : 'none'}`);
+ throw new TypeError(
+ `state ${state.type} - ${
+ state.type !== "markdown" ? state.subtype : "none"
+ }`
+ );
  }
  mutablyTrimEmptyLines(state.accum);
 

wiki/elf-watcher.mjs

@@ -1,6 +1,14 @@
-import { existsSync, mkdirSync, readdirSync, watch, writeFileSync } from "fs";
+import {
+ existsSync,
+ mkdirSync,
+ readFileSync,
+ readdirSync,
+ watch,
+ writeFileSync,
+} from "fs";
 import { argv } from "process";
 import { elfToMdx } from "./elf-to-mdx.mjs";
+import { getImportedPrelude } from "./elf-wiki-imports.mjs";
 
 const DIR_OF_ELF = "pages";
 const DIR_OF_MDX = "src/content/docs/wiki";
@@ -17,10 +25,49 @@ async function mdxOfFile(file) {
  if (!file.endsWith(".elf") || !existsSync(elfname)) return;
 
  const base = file.slice(0, file.length - 4);
+ const cfgname = `${DIR_OF_ELF}/${base}.cfg`;
  const mdxname = `${DIR_OF_MDX}/${base}.mdx`;
  console.log(`elf->mdx transforming ${file}`);
- const mdxFile = await elfToMdx(elfname);
- writeFileSync(mdxname, mdxFile);
+ try {
+ const prelude = getImportedPrelude(`${DIR_OF_ELF}/`, file);
+ const mdxFile = await elfToMdx(
+ elfname,
+ prelude.map(({ file, contents }) => `%%! file: ${file}\n${contents}\n`)
+ );
+ const cfg = `
+% DO NOT EDIT
+% Automatically generated by running "npm run dev" or "npm run build" in the
+% wiki directory.
+% Edit twelf/wiki/${file} instead
+
+${prelude.map(({ file }) => file).join("\n")}
+${file}
+`.trim();
+ if (
+ !existsSync(cfgname) ||
+ readFileSync(cfgname).toString("utf-8") !== cfg
+ ) {
+ if (existsSync(cfgname)) {
+ console.log(`elf->mdx: updating ${cfgname}`);
+ }
+ writeFileSync(cfgname, cfg);
+ }
+
+ writeFileSync(mdxname, mdxFile);
+ } catch (e) {
+ console.log(e);
+ writeFileSync(
+ mdxname,
+ `
+---
+---
+
+Error transforming ${file}
+
+${e}
+`
+ );
+ }
 }
 
 console.log(`elf->mdx checking existing files...`);

wiki/elf-wiki-imports.mjs

@@ -0,0 +1,72 @@
+import { readFileSync } from "fs";
+
+/**
+ * Read the file's header to get all of the imported elf files
+ * (in reverse order)
+ *
+ * @param {string} contents
+ */
+function getImportedFilenames(contents) {
+ /**@type {string[]} */
+ const importStatements = [];
+
+ for (const line of contents.split("\n")) {
+ if (!line.startsWith("%%! ")) break;
+ if (line.startsWith("%%! import: ")) {
+ importStatements.push(line.slice(12).trim());
+ }
+ }
+
+ return importStatements;
+}
+
+/**
+ * Uses a DFS traversal
+ *
+ * @param {string} base
+ * Relative path of elf files
+ * @param {Set<string>} known
+ * Avoids double-importing by tracking all the filenames ever added to `accum` in the process of this traversal
+ * @param {{file: string, contents: string}[]} accum
+ * Accumulates the files, making sure that files are added after their dependencies
+ * @param {string} elfname
+ * Name of an ELF file that is a dependency of the file we're trying to load
+ */
+function dfsAccumImportedPrelude(base, known, accum, elfname) {
+ if (!elfname.match(/^[a-zA-Z.\-_0-9]*[.]elf*$/)) {
+ throw new Error(
+ `Imported path ${elfname} invalid: must include only letters, numbers, dashes, and underscores and end in .elf`
+ );
+ }
+ const contents = readFileSync(`${base}${elfname}`).toString("utf-8");
+ for (const importElf in getImportedFilenames(contents)) {
+ if (!known.has(importElf)) {
+ known.add(importElf);
+ dfsAccumImportedPrelude(base, known, accum, importElf);
+ }
+ }
+ accum.push({ file: elfname, contents });
+}
+
+/**
+ *
+ * @param {string} base
+ * Relative path of elf files
+ * @param {string} elfname
+ */
+export function getImportedPrelude(base, elfname) {
+ /**@type {Set<string>} */
+ const known = new Set();
+
+ /**@type {{file: string, contents: string}[]} */
+ const dependencies = [];
+
+ for (const file of getImportedFilenames(
+ readFileSync(`${base}${elfname}`).toString("utf-8")
+ )) {
+ known.add(file);
+ dfsAccumImportedPrelude(base, known, dependencies, file);
+ }
+
+ return dependencies;
+}

wiki/pages/proving-metatheorems-proving-totality-assertions-about-the-natural-numbers.elf

@@ -142,7 +142,7 @@ plus-bad-output : plus (s N1) N2 (s (s N3))
 
 Here we have insisted that the output of the premise has the form ``s N3`` for some ``N3``. Twelf correctly reports an output coverage error because this condition can fail (for example, if the premise was ``plus-z : plus z z z``). 
 
-Pattern-matching the output of a premise is like an [[inversion]] step in a proof: you're insisting that the premise derivation must conclude a particular fact that is more specific than the judgement form itself. For Twelf to accept a relation as total, Twelf must notice that all of these inversions are permissible. Twelf permits such inversions when it is readily apparent that they are justified, and those inversions that Twelf does not accept can be proved explicitly.
+Pattern-matching the output of a premise is like an <Todo>inversion</Todo> step in a proof: you're insisting that the premise derivation must conclude a particular fact that is more specific than the judgement form itself. For Twelf to accept a relation as total, Twelf must notice that all of these inversions are permissible. Twelf permits such inversions when it is readily apparent that they are justified, and those inversions that Twelf does not accept can be proved explicitly.
 
 In this example, we got an output coverage error because we constrained the output of the premise by insisting it be formed by a particular constant. The other way to get output coverage errors is to insist that the output of a premise be a variable that occurs elsewhere in the type. For example: