commit 7d147032428e6787298ddf5a269b96b2ed584c83 Author: Michael Zhang Date: Thu Sep 12 18:38:07 2024 -0500 initial diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..509c6d3 --- /dev/null +++ b/.gitignore @@ -0,0 +1,178 @@ +# Based on https://raw.githubusercontent.com/github/gitignore/main/Node.gitignore + +# Logs + +logs +_.log +npm-debug.log_ +yarn-debug.log* +yarn-error.log* +lerna-debug.log* +.pnpm-debug.log* + +# Caches + +.cache + +# Diagnostic reports (https://nodejs.org/api/report.html) + +report.[0-9]_.[0-9]_.[0-9]_.[0-9]_.json + +# Runtime data + +pids +_.pid +_.seed +*.pid.lock + +# Directory for instrumented libs generated by jscoverage/JSCover + +lib-cov + +# Coverage directory used by tools like istanbul + +coverage +*.lcov + +# nyc test coverage + +.nyc_output + +# Grunt intermediate storage (https://gruntjs.com/creating-plugins#storing-task-files) + +.grunt + +# Bower dependency directory (https://bower.io/) + +bower_components + +# node-waf configuration + +.lock-wscript + +# Compiled binary addons (https://nodejs.org/api/addons.html) + +build/Release + +# Dependency directories + +node_modules/ +jspm_packages/ + +# Snowpack dependency directory (https://snowpack.dev/) + +web_modules/ + +# TypeScript cache + +*.tsbuildinfo + +# Optional npm cache directory + +.npm + +# Optional eslint cache + +.eslintcache + +# Optional stylelint cache + +.stylelintcache + +# Microbundle cache + +.rpt2_cache/ +.rts2_cache_cjs/ +.rts2_cache_es/ +.rts2_cache_umd/ + +# Optional REPL history + +.node_repl_history + +# Output of 'npm pack' + +*.tgz + +# Yarn Integrity file + +.yarn-integrity + +# dotenv environment variable files + +.env +.env.development.local +.env.test.local +.env.production.local +.env.local + +# parcel-bundler cache (https://parceljs.org/) + +.parcel-cache + +# Next.js build output + +.next +out + +# Nuxt.js build / generate output + +.nuxt +dist + +# Gatsby files + +# Comment in the public line in if your project uses Gatsby and not Next.js + +# https://nextjs.org/blog/next-9-1#public-directory-support + +# public + +# vuepress build output + +.vuepress/dist + +# vuepress v2.x temp and cache directory + +.temp + +# Docusaurus cache and generated files + +.docusaurus + +# Serverless directories + +.serverless/ + +# FuseBox cache + +.fusebox/ + +# DynamoDB Local files + +.dynamodb/ + +# TernJS port file + +.tern-port + +# Stores VSCode versions used for testing VSCode extensions + +.vscode-test + +# yarn v2 + +.yarn/cache +.yarn/unplugged +.yarn/build-state.yml +.yarn/install-state.gz +.pnp.* + +# IntelliJ based IDEs +.idea + +# Finder (MacOS) folder config +.DS_Store + +# Agda build directory +_build \ No newline at end of file diff --git a/README.md b/README.md new file mode 100644 index 0000000..63d4c5f --- /dev/null +++ b/README.md @@ -0,0 +1,9 @@ +# remark-agda + +## Contact + +Author: Michael Zhang + +License: GPL-3.0 + +Send questions to ~mzhang/public-inbox@lists.sr.ht \ No newline at end of file diff --git a/biome.json b/biome.json new file mode 100644 index 0000000..72ea95b --- /dev/null +++ b/biome.json @@ -0,0 +1,32 @@ +{ + "$schema": "https://biomejs.dev/schemas/1.9.0/schema.json", + "vcs": { + "enabled": false, + "clientKind": "git", + "useIgnoreFile": false + }, + "files": { + "ignoreUnknown": false, + "ignore": [] + }, + "formatter": { + "enabled": true, + "indentStyle": "space", + "indentWidth": 2, + "lineWidth": 80 + }, + "organizeImports": { + "enabled": true + }, + "linter": { + "enabled": true, + "rules": { + "recommended": true + } + }, + "javascript": { + "formatter": { + "quoteStyle": "double" + } + } +} diff --git a/bun.lockb b/bun.lockb new file mode 100755 index 0000000..23e0969 Binary files /dev/null and b/bun.lockb differ diff --git a/package.json b/package.json new file mode 100644 index 0000000..37fbb11 --- /dev/null +++ b/package.json @@ -0,0 +1,22 @@ +{ + "name": "remark-agda", + "module": "src/index.ts", + "type": "module", + "devDependencies": { + "@biomejs/biome": "^1.9.0", + "@types/bun": "latest", + "rehype-stringify": "^10.0.0", + "remark-parse": "^11.0.0", + "remark-rehype": "^11.1.0", + "vfile": "^6.0.3" + }, + "peerDependencies": { + "typescript": "^5.0.0" + }, + "dependencies": { + "hast-util-from-html": "^2.0.2", + "unified": "^11.0.5", + "unist-util-visit": "^5.0.0" + }, + "trustedDependencies": ["@biomejs/biome"] +} diff --git a/remark-agda.agda-lib b/remark-agda.agda-lib new file mode 100644 index 0000000..cd69214 --- /dev/null +++ b/remark-agda.agda-lib @@ -0,0 +1,2 @@ +include: test +depend: standard-library \ No newline at end of file diff --git a/src/index.ts b/src/index.ts new file mode 100644 index 0000000..f792e9c --- /dev/null +++ b/src/index.ts @@ -0,0 +1,168 @@ +import { join, parse } from "node:path"; +import { tmpdir } from "node:os"; +import { spawnSync, spawn } from "node:child_process"; +import { + readdir, + mkdtemp, + exists, + copyFile, + readFile, + 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"; + +export interface RemarkAgdaOptions { + /** Place to output the HTML files */ + destDir: string; + + /** Function to transform HTML files */ + transformHtml?: (_: string) => string; + + /** Path to Agda */ + agdaBin?: string; + + /** Extra agda options */ + extraAgdaFlags?: string[]; +} + +const remarkAgda: Plugin<[RemarkAgdaOptions]> = ({ + agdaBin, + extraAgdaFlags, + destDir, + transformHtml, +}) => { + // const destDir = join(publicDir, "generated", "agda"); + mkdirSync(destDir, { recursive: true }); + + return async (tree, { history }) => { + if (history.length === 0) { + throw new Error( + "No history attribute found. Did you parse the VFile from a file?", + ); + } + + 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( + agdaBin ?? "agda", + [ + "--html", + `--html-dir=${agdaOutDir}`, + "--highlight-occurrences", + "--html-highlight=code", + ...(extraAgdaFlags ?? []), + path, + ], + {}, + ); + + if (childOutput.error || !(await exists(agdaOutFile))) { + throw new Error( + `Agda error: + + Stdout: + ${childOutput.stdout} + + Stderr: + ${childOutput.stderr}`, + { + cause: childOutput.error, + }, + ); + } + + // // TODO: Handle child output + // console.error("--AGDA OUTPUT--"); + // console.error(childOutput); + // console.error(childOutput.stdout?.toString()); + // console.error(childOutput.stderr?.toString()); + // console.error("--AGDA OUTPUT--"); + + const referencedFiles = new Set(); + + const writtenFiles = await readdir(agdaOutDir); + const promises = writtenFiles.map(async (file) => { + referencedFiles.add(file); + + const fullPath = join(agdaOutDir, file); + const fullDestPath = join(destDir, file); + + if (file.endsWith(".html")) { + // Transform the HTML optionally + const src = await readFile(fullPath, { encoding: "utf-8" }); + const transformedHtml = (transformHtml ?? ((html) => html))(src); + await writeFile(fullDestPath, transformedHtml); + } else { + // Copy the CSS file over + await copyFile(fullPath, fullDestPath); + } + }); + await Promise.all(promises); + + const htmlname = parse(path).base.replace(/\.lagda.md/, ".html"); + + const doc = await readFile(agdaOutFile); + + // This is the post-processed markdown with HTML code blocks replacing the Agda code blocks + const tree2 = fromMarkdown(doc); + + const collectedCodeBlocks: RootContent[] = []; + 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) { + // 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"; + } + } + }); + + if (!firstChild?.properties?.className?.includes("Agda")) return; + + const stringContents = toHtml(firstChild); + collectedCodeBlocks.push({ + contents: stringContents, + }); + }); + + let idx = 0; + visit(tree, "code", (node) => { + if (!(node.lang === null || node.lang === "agda")) return; + + node.type = "html"; + node.value = collectedCodeBlocks[idx].contents; + idx += 1; + }); + }; +}; + +export default remarkAgda; diff --git a/test/.gitignore b/test/.gitignore new file mode 100644 index 0000000..872aa27 --- /dev/null +++ b/test/.gitignore @@ -0,0 +1 @@ +results \ No newline at end of file diff --git a/test/Simple.lagda.md b/test/Simple.lagda.md new file mode 100644 index 0000000..68d0de7 --- /dev/null +++ b/test/Simple.lagda.md @@ -0,0 +1,27 @@ +``` +module Simple where + +open import Agda.Primitive +open import Relation.Binary.PropositionalEquality.Core + +variable + l : Level + +data ℕ : Set where + zero : ℕ + suc : ℕ → ℕ + +_+_ : ℕ → ℕ → ℕ +zero + b = b +suc a + b = suc (a + b) + ++-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) ++-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 diff --git a/test/index.test.ts b/test/index.test.ts new file mode 100644 index 0000000..519556c --- /dev/null +++ b/test/index.test.ts @@ -0,0 +1,38 @@ +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"; + +test("simple case", async () => { + const file = join(dirname(import.meta.path), "Simple.lagda.md"); + const vfile = new VFile({ path: file }); + + const result = await unified() + .use(remarkParse) + .use(remarkAgda, { + destDir: join(dirname(import.meta.path), "results"), + transformHtml: (src) => { + return ` + + + + + + + 
+          ${src}
+
+ + + `; + }, + }) + .use(remarkRehype) + .use(rehypeStringify) + .process(vfile); + console.log("result", result); +}); diff --git a/tsconfig.json b/tsconfig.json new file mode 100644 index 0000000..238655f --- /dev/null +++ b/tsconfig.json @@ -0,0 +1,27 @@ +{ + "compilerOptions": { + // Enable latest features + "lib": ["ESNext", "DOM"], + "target": "ESNext", + "module": "ESNext", + "moduleDetection": "force", + "jsx": "react-jsx", + "allowJs": true, + + // Bundler mode + "moduleResolution": "bundler", + "allowImportingTsExtensions": true, + "verbatimModuleSyntax": true, + "noEmit": true, + + // Best practices + "strict": true, + "skipLibCheck": true, + "noFallthroughCasesInSwitch": true, + + // Some stricter flags (disabled by default) + "noUnusedLocals": false, + "noUnusedParameters": false, + "noPropertyAccessFromIndexSignature": false + } +}