diff --git a/bun.lockb b/bun.lockb index 23e0969..da1d5c9 100755 Binary files a/bun.lockb and b/bun.lockb differ diff --git a/package.json b/package.json index 37fbb11..b5c3ee1 100644 --- a/package.json +++ b/package.json @@ -1,22 +1,32 @@ { "name": "remark-agda", + "version": "0.0.1", + + "main": "dist/index.js", "module": "src/index.ts", + "types": "dist/index.d.ts", "type": "module", "devDependencies": { "@biomejs/biome": "^1.9.0", "@types/bun": "latest", + "rehype-raw": "^7.0.0", "rehype-stringify": "^10.0.0", "remark-parse": "^11.0.0", "remark-rehype": "^11.1.0", - "vfile": "^6.0.3" + "to-vfile": "^8.0.0", + "vfile": "^6.0.3", + "vfile-reporter": "^8.1.1" }, "peerDependencies": { "typescript": "^5.0.0" }, "dependencies": { + "hast": "^1.0.0", "hast-util-from-html": "^2.0.2", "unified": "^11.0.5", + "unist": "^0.0.1", "unist-util-visit": "^5.0.0" }, - "trustedDependencies": ["@biomejs/biome"] + "trustedDependencies": ["@biomejs/biome"], + "files": ["dist/index.js", "dist/index.d.ts"] } diff --git a/scripts/prepare-release.sh b/scripts/prepare-release.sh new file mode 100755 index 0000000..05cc57b --- /dev/null +++ b/scripts/prepare-release.sh @@ -0,0 +1,5 @@ +#!/usr/bin/env bash + +mkdir -p dist/ +bun build --target node src/index.ts > dist/index.js +bunx tsc \ No newline at end of file diff --git a/src/index.ts b/src/index.ts index f792e9c..d5965da 100644 --- a/src/index.ts +++ b/src/index.ts @@ -1,6 +1,6 @@ import { join, parse } from "node:path"; import { tmpdir } from "node:os"; -import { spawnSync, spawn } from "node:child_process"; +import { spawnSync } from "node:child_process"; import { readdir, mkdtemp, @@ -10,12 +10,13 @@ import { writeFile, } from "node:fs/promises"; import { mkdirSync } from "node:fs"; - import type { Plugin } from "unified"; import { visit } from "unist-util-visit"; import { fromMarkdown } from "mdast-util-from-markdown"; import { fromHtml } from "hast-util-from-html"; import { toHtml } from "hast-util-to-html"; +import type { RootContent } from "hast"; +import type { Node as UnistNode } from "unist"; export interface RemarkAgdaOptions { /** Place to output the HTML files */ @@ -31,7 +32,7 @@ export interface RemarkAgdaOptions { extraAgdaFlags?: string[]; } -const remarkAgda: Plugin<[RemarkAgdaOptions]> = ({ +export const remarkAgda: Plugin<[RemarkAgdaOptions]> = ({ agdaBin, extraAgdaFlags, destDir, @@ -48,19 +49,14 @@ const remarkAgda: Plugin<[RemarkAgdaOptions]> = ({ } const path = history[history.length - 1]; - // console.log("path", path); // if (!(path.endsWith(".lagda.md") || path.endsWith(".agda"))) return; - // console.log("AGDA:processing path", path); - const agdaOutDir = await mkdtemp(join(tmpdir(), "agdaRender.")); // const agdaOutDir = join(tempDir, "output"); const agdaOutFilename = parse(path).base.replace(/\.lagda.md$/, ".md"); const agdaOutFile = join(agdaOutDir, agdaOutFilename); - console.log("looking for file", agdaOutFile); // mkdirSync(agdaOutDir, { recursive: true }); - - const childOutput = await spawnSync( + const childOutput = spawnSync( agdaBin ?? "agda", [ "--html", @@ -94,7 +90,6 @@ const remarkAgda: Plugin<[RemarkAgdaOptions]> = ({ // console.error(childOutput.stdout?.toString()); // console.error(childOutput.stderr?.toString()); // console.error("--AGDA OUTPUT--"); - const referencedFiles = new Set(); const writtenFiles = await readdir(agdaOutDir); @@ -118,48 +113,70 @@ const remarkAgda: Plugin<[RemarkAgdaOptions]> = ({ const htmlname = parse(path).base.replace(/\.lagda.md/, ".html"); - const doc = await readFile(agdaOutFile); + const doc = await readFile(agdaOutFile, { encoding: "utf-8" }); // This is the post-processed markdown with HTML code blocks replacing the Agda code blocks const tree2 = fromMarkdown(doc); - const collectedCodeBlocks: RootContent[] = []; + const collectedCodeBlocks: string[] = []; + visit(tree2, "html", (node) => { const html = fromHtml(node.value, { fragment: true }); - const firstChild: RootContent = html.children[0]!; - visit(html, "element", (node) => { if (node.tagName !== "a") return; - if (node.properties.href) { + if (typeof node.properties.href === "string") { // Trim off end const [href, hash, ...rest] = node.properties.href.split("#"); if (rest.length > 0) throw new Error("come look at this"); if (href === htmlname) node.properties.href = `#${hash}`; - if (referencedFiles.has(href)) { - node.properties.href = `${base}generated/agda/${href}${hash ? `#${hash}` : ""}`; - node.properties.target = "_blank"; - } + // TODO: Transform + // if (referencedFiles.has(href)) { + // node.properties.href = `${base}generated/agda/${href}${hash ? `#${hash}` : ""}`; + // node.properties.target = "_blank"; + // } } }); - if (!firstChild?.properties?.className?.includes("Agda")) return; + while (true) { + if (html.children.length > 0) { + const firstChild: RootContent = html.children[0]; - const stringContents = toHtml(firstChild); - collectedCodeBlocks.push({ - contents: stringContents, - }); + if (firstChild.type !== "element") break; + + const className = firstChild.properties.className; + + // @ts-ignore TODO: Fix this + if (!className?.includes("Agda")) break; + + const stringContents = toHtml(firstChild); + collectedCodeBlocks.push(stringContents); + } + break; + } }); + console.log(`Collected ${collectedCodeBlocks.length} blocks!`); + let idx = 0; - visit(tree, "code", (node) => { + + visit(tree, "code", (node: UnistNode) => { + // Make sure it's either null (which gets interpreted as agda), or agda + // @ts-ignore if (!(node.lang === null || node.lang === "agda")) return; + // node.type = "html"; + node.type = "html"; - node.value = collectedCodeBlocks[idx].contents; + + // @ts-ignore + node.value = collectedCodeBlocks[idx]; + + console.log(node); + idx += 1; }); }; diff --git a/test/Simple.lagda.md b/test/Simple.lagda.md index 68d0de7..88c4498 100644 --- a/test/Simple.lagda.md +++ b/test/Simple.lagda.md @@ -1,3 +1,10 @@ +# Commutativity of addition + +This document shows how to prove commutativity of addition on natural numbers. + +
+Imports + ``` module Simple where @@ -5,23 +12,39 @@ open import Agda.Primitive open import Relation.Binary.PropositionalEquality.Core variable - l : Level + l : Level +``` +
+ +Declare our data structures: + +``` data ℕ : Set where - zero : ℕ - suc : ℕ → ℕ + zero : ℕ + suc : ℕ → ℕ +``` +Define addition: + +``` _+_ : ℕ → ℕ → ℕ zero + b = b suc a + b = suc (a + b) +``` +Prove commutativity: + +``` +-comm : (m n : ℕ) → m + n ≡ n + m +-comm zero n = lemma n where - lemma : (n : ℕ) → n ≡ n + zero - lemma zero = refl - lemma (suc n) = cong suc (lemma n) + lemma : (n : ℕ) → n ≡ n + zero + lemma zero = refl + lemma (suc n) = cong suc (lemma n) +-comm (suc m) n = trans (cong suc (+-comm m n)) (sym (lemma n m)) where - lemma : (m n : ℕ) → m + suc n ≡ suc (m + n) - lemma zero n = refl - lemma (suc m) n = cong suc (lemma m n) -``` \ No newline at end of file + lemma : (m n : ℕ) → m + suc n ≡ suc (m + n) + lemma zero n = refl + lemma (suc m) n = cong suc (lemma m n) +``` + +That's it! \ No newline at end of file diff --git a/test/index.test.ts b/test/index.test.ts index 519556c..ceada6f 100644 --- a/test/index.test.ts +++ b/test/index.test.ts @@ -1,22 +1,22 @@ import { test } from "bun:test"; import { resolve, dirname, join } from "node:path"; import { unified } from "unified"; -import remarkAgda from "../src"; import remarkParse from "remark-parse"; import remarkRehype from "remark-rehype"; import rehypeStringify from "rehype-stringify"; -import { VFile } from "vfile"; +import rehypeRaw from "rehype-raw"; +import { read } from "to-vfile"; + +import remarkAgda, { type RemarkAgdaOptions } from "../src"; test("simple case", async () => { const file = join(dirname(import.meta.path), "Simple.lagda.md"); - const vfile = new VFile({ path: file }); + const vfile = await read(file); - const result = await unified() - .use(remarkParse) - .use(remarkAgda, { - destDir: join(dirname(import.meta.path), "results"), - transformHtml: (src) => { - return ` + const options: RemarkAgdaOptions = { + destDir: join(dirname(import.meta.path), "results"), + transformHtml: (src) => { + return ` @@ -29,10 +29,14 @@ test("simple case", async () => { `; - }, - }) - .use(remarkRehype) + }, + }; + + await unified() + .use(remarkParse) + .use(remarkAgda, options) + .use(remarkRehype, { allowDangerousHtml: true }) + .use(rehypeRaw) .use(rehypeStringify) .process(vfile); - console.log("result", result); }); diff --git a/tsconfig.json b/tsconfig.json index 238655f..8ea97b4 100644 --- a/tsconfig.json +++ b/tsconfig.json @@ -12,16 +12,20 @@ "moduleResolution": "bundler", "allowImportingTsExtensions": true, "verbatimModuleSyntax": true, - "noEmit": true, // Best practices "strict": true, "skipLibCheck": true, "noFallthroughCasesInSwitch": true, + "emitDeclarationOnly": true, // Some stricter flags (disabled by default) "noUnusedLocals": false, "noUnusedParameters": false, - "noPropertyAccessFromIndexSignature": false - } + "noPropertyAccessFromIndexSignature": false, + + "outDir": "dist", + "declaration": true + }, + "files": ["src/index.ts"] }