trying to get typst rendering working for svgs
Some checks failed
ci/woodpecker/push/woodpecker Pipeline failed

This commit is contained in:
Michael Zhang 2024-09-26 18:09:45 -05:00
parent 8667d33798
commit 7a1b2b9787
6 changed files with 131 additions and 17 deletions

BIN
bun.lockb

Binary file not shown.

View file

@ -15,7 +15,7 @@
"@astrojs/markdoc": "^0.11.1", "@astrojs/markdoc": "^0.11.1",
"@astrojs/markdown-remark": "^5.1.1", "@astrojs/markdown-remark": "^5.1.1",
"@astrojs/mdx": "^1.1.5", "@astrojs/mdx": "^1.1.5",
"@astrojs/rss": "^3.0.0", "@astrojs/rss": "^4.0.7",
"@astrojs/sitemap": "^3.1.6", "@astrojs/sitemap": "^3.1.6",
"@justfork/rehype-autolink-headings": "^5.1.1", "@justfork/rehype-autolink-headings": "^5.1.1",
"astro": "^3.6.5", "astro": "^3.6.5",

View file

@ -1,39 +1,55 @@
import type { RemarkPlugin } from "@astrojs/markdown-remark"; import type { RemarkPlugin } from "@astrojs/markdown-remark";
import { mkdtempSync, readFileSync, writeFileSync } from "node:fs"; import { mkdtempSync, readFileSync, writeFileSync } from "node:fs";
import { visit } from "unist-util-visit"; import { visit } from "unist-util-visit";
import { join } from "node:path"; import { join, resolve, dirname } from "node:path";
import { spawnSync } from "node:child_process"; import { spawnSync } from "node:child_process";
import { tmpdir } from "node:os"; import { tmpdir } from "node:os";
import { readdir, copyFile } from "node:fs/promises";
const remarkTypst: RemarkPlugin = () => { const remarkTypst: RemarkPlugin = () => {
const tmp = mkdtempSync(join(tmpdir(), "typst")); const tmp = mkdtempSync(join(tmpdir(), "typst"));
let ctr = 0; let ctr = 0;
return (tree) => { return async (tree, { history }) => {
const path: string = resolve(history[history.length - 1]!);
const dir = dirname(path);
// Copy all the .typ files in the dir
for (const file of await readdir(dir)) {
console.log("checking", file);
if (file.endsWith(".typ")) {
const src = resolve(join(dir, file));
const dst = resolve(join(tmp, file));
console.log("copying", src, dst);
await copyFile(src, dst);
}
}
visit( visit(
tree, tree,
(node) => node.type === "code" && node.lang === "typst", (node) => node.type === "code" && node.lang === "typst",
(node, index, parent) => { (node, index, parent) => {
const doc = join(tmp, `${ctr}.typ`); const doc = resolve(join(tmp, `${ctr}.typ`));
const docOut = join(tmp, `${ctr}.svg`); const docOut = resolve(join(tmp, `${ctr}.svg`));
ctr += 1; ctr += 1;
writeFileSync(doc, node.value); writeFileSync(doc, node.value);
const result = spawnSync( const result = spawnSync("typst", [
"typst", "compile",
[ "--format",
"compile", "svg",
"--format", doc,
"svg", docOut,
doc, ]);
],
{},
);
console.log("OUTPUT", result.stderr.toString()); console.log("OUTPUT", result.stderr.toString());
const svgOut = readFileSync(docOut); const svgOut = readFileSync(docOut);
node.type = "html"; node.type = "html";
node.value = svgOut.toString(); node.value = `
<div class="svg">
${svgOut.toString()}
</div>
`;
}, },
); );
}; };

View file

@ -0,0 +1,11 @@
#import "@preview/fletcher:0.5.1" as fletcher: diagram, node, edge
#let arrow(left, right, leftcolor: red, rightcolor: blue) = diagram(cell-size: 1cm, $
#text(fill: leftcolor)[#left]
edge(
marks: #(none, (inherit: "head", stroke: rightcolor)),
stroke: #stroke(paint: gradient.linear(leftcolor, rightcolor))
)
&
#text(fill: rightcolor)[#right]
$)

View file

@ -0,0 +1,76 @@
---
title: Glue
slug: 2024-09-26-glue
date: 2024-09-26T21:24:18.030Z
tags: [hott, cubical, agda, type-theory]
draft: true
---
<details>
<summary>Imports for Agda</summary>
```
{-# OPTIONS --cubical #-}
module 2024-09-26-glue.index where
open import Cubical.Foundations.Prelude
```
</details>
The core idea behind cubical type theory is that we have powerful path primitives that give us the ability to just bridge arbitrary things together.
The $\mathsf{PathP}$ primitive gives us a way to connect elements of different types.
For example, let's create some custom boolean type and assume we have some path between it and the standard booleans:
```
module _ where
data Bool : Type where
false : Bool
true : Bool
data Direction : Type where
left : Direction
right : Direction
postulate
myFunnyPath1 : Bool ≡ Direction
```
At the point $\mathsf{i0}$, this is _definitionally_ equal to $\mathsf{Bool}$,
and at $\mathsf{i1}$, this is _definitionally_ equal to $\mathsf{Direction}$.
```
_ : myFunnyPath1 i0 ≡ Bool
_ = refl
_ : myFunnyPath1 i1 ≡ Direction
_ = refl
```
These are known as the _boundary conditions_ on the path $\mathsf{myFunnyPath1}$.
Not only this, we can provide paths between the elements of this type too:
```
postulate
myFunnyPath2 : PathP (λ i → myFunnyPath1 i) false left
```
There's definitely something funny going on here. The typical transport operations in homotopy type theory are defined using path induction, which is inherent from the inductive structure of paths.
But how do we perform path induction on this kind of path?
Cubical type theory's approach is to flip this around and make _transport_ the primitive operation on top of which path induction can be defined.
$$
\mathsf{transp} : (A : \mathbb{I} \rightarrow \mathcal{U}) \rightarrow (r : \mathbb{I}) \rightarrow A(\mathsf{i0}) \rightarrow A(\mathsf{i1})
$$
Computationally, you could imagine how the path above would be transported:
```typst
#set page(width: auto, height: auto, margin: 10pt)
#import "arrow.typ": arrow
#arrow($C$, $D$, leftcolor: green)
```

View file

@ -108,6 +108,17 @@
border: 1px solid var(--hr-color); border: 1px solid var(--hr-color);
} }
.svg {
display: flex;
flex-direction: column;
align-items: center;
svg {
width: auto;
height: auto;
}
}
details { details {
border: 1px solid var(--hr-color); border: 1px solid var(--hr-color);
border-radius: 8px; border-radius: 8px;