Compare commits
1 commit
master
...
color-upda
Author | SHA1 | Date | |
---|---|---|---|
ebba251502 |
|
@ -1,4 +1,3 @@
|
|||
public
|
||||
package-lock.json
|
||||
src/styles/fork-awesome
|
||||
pnpm-lock.yaml
|
||||
src/styles/fork-awesome
|
3
.vscode/settings.json
vendored
|
@ -1,3 +0,0 @@
|
|||
{
|
||||
"npm.packageManager": "pnpm"
|
||||
}
|
26
.woodpecker.yml
Normal file
|
@ -0,0 +1,26 @@
|
|||
steps:
|
||||
build:
|
||||
image: git.mzhang.io/michael/blog-docker-builder:x0m1c7r2qzc3qbyw8sfv5flfv75xiqdz
|
||||
environment:
|
||||
- ASTRO_TELEMETRY_DISABLED=1
|
||||
commands:
|
||||
- mkdir /tmp
|
||||
- rm -rf node_modules
|
||||
- npm i -g pnpm@9.4.0
|
||||
- npx pnpm install --frozen-lockfile
|
||||
- npx pnpm run build
|
||||
when:
|
||||
- event: push
|
||||
|
||||
deploy:
|
||||
image: git.mzhang.io/michael/blog-docker-builder:x0m1c7r2qzc3qbyw8sfv5flfv75xiqdz
|
||||
commands:
|
||||
- echo "$${SSH_SECRET_KEY}" > SSH_SECRET_KEY
|
||||
- chmod 600 SSH_SECRET_KEY
|
||||
- mkdir -p ~/.ssh
|
||||
- echo "mzhang.io ssh-ed25519 AAAAC3NzaC1lZDI1NTE5AAAAIO+RKFYjD8UjqhfOHFHNyijkbGzC4fJEIIhrBwHj+FsQ" >> known_hosts
|
||||
- rsync -azrP -e "ssh -i SSH_SECRET_KEY -o UserKnownHostsFile=known_hosts" dist/ blogDeploy@mzhang.io:/home/blogDeploy/public
|
||||
secrets: [SSH_SECRET_KEY]
|
||||
when:
|
||||
- branch: master
|
||||
event: push
|
|
@ -1,27 +0,0 @@
|
|||
steps:
|
||||
build:
|
||||
image: git.mzhang.io/michael/blog-docker-builder:6gzd1rhcl41y02yw4z9kpjgrhxifqyfs
|
||||
environment:
|
||||
- ASTRO_TELEMETRY_DISABLED=1
|
||||
commands:
|
||||
- mkdir /tmp
|
||||
- rm -rf node_modules
|
||||
- npm i -g pnpm@9.4.0
|
||||
- npx pnpm install --frozen-lockfile
|
||||
- npx pnpm run build
|
||||
when:
|
||||
- event: push
|
||||
|
||||
deploy:
|
||||
image: git.mzhang.io/michael/blog-docker-builder:6gzd1rhcl41y02yw4z9kpjgrhxifqyfs
|
||||
commands:
|
||||
- mc alias set $AWS_DEFAULT_REGION $AWS_ENDPOINT_URL $AWS_ACCESS_KEY_ID $AWS_SECRET_ACCESS_KEY --api S3v4
|
||||
- mc mirror --overwrite ./dist/ $AWS_DEFAULT_REGION/mzhang-io-website/
|
||||
secrets:
|
||||
- AWS_ACCESS_KEY_ID
|
||||
- AWS_DEFAULT_REGION
|
||||
- AWS_ENDPOINT_URL
|
||||
- AWS_SECRET_ACCESS_KEY
|
||||
when:
|
||||
- branch: master
|
||||
event: push
|
|
@ -2,4 +2,4 @@
|
|||
|
||||
https://mzhang.io
|
||||
|
||||
License: GPL-3.0 code / CC-BY-SA-4.0 contents
|
||||
License: GPL-3.0 / CC-BY-SA-4.0
|
||||
|
|
|
@ -22,7 +22,6 @@ const publicDir = "public";
|
|||
// https://astro.build/config
|
||||
export default defineConfig({
|
||||
site: "https://mzhang.io",
|
||||
prefetch: true,
|
||||
integrations: [mdx(), sitemap(), markdoc()],
|
||||
|
||||
outDir,
|
||||
|
@ -35,7 +34,7 @@ export default defineConfig({
|
|||
shikiConfig: { theme: "css-variables" },
|
||||
remarkPlugins: [
|
||||
() => remarkAgda({ outDir, base, publicDir }),
|
||||
[remarkMath, {}],
|
||||
remarkMath,
|
||||
[remarkAdmonitions, mkdocsConfig],
|
||||
remarkReadingTime,
|
||||
remarkTypst,
|
||||
|
|
|
@ -1,2 +1,2 @@
|
|||
include: src/posts src
|
||||
include: src/content/posts src
|
||||
depend: standard-library cubical
|
||||
|
|
BIN
bun.lockb
44
flake.lock
|
@ -3,16 +3,14 @@
|
|||
"agda": {
|
||||
"inputs": {
|
||||
"flake-parts": "flake-parts",
|
||||
"nixpkgs": [
|
||||
"nixpkgs"
|
||||
]
|
||||
"nixpkgs": "nixpkgs"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1729253305,
|
||||
"narHash": "sha256-S7/C8VGMrXeGhFeYXx1cVBjZlNVB5L1o/SkW0hFm0Jc=",
|
||||
"lastModified": 1719426791,
|
||||
"narHash": "sha256-jiPGzJM+XMwb1OwyxpbY6jV0Lzr5yLKnPSMZbueFNRM=",
|
||||
"owner": "agda",
|
||||
"repo": "agda",
|
||||
"rev": "3425ed5543d2e6f98094b834fedcdec3a2fb67a6",
|
||||
"rev": "777b07f573c7526d677c18c25e44b24a849bc03b",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
|
@ -44,11 +42,11 @@
|
|||
"systems": "systems"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1726560853,
|
||||
"narHash": "sha256-X6rJYSESBVr3hBoH0WbKE5KvhPU5bloyZ2L4K60/fPQ=",
|
||||
"lastModified": 1710146030,
|
||||
"narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
|
||||
"owner": "numtide",
|
||||
"repo": "flake-utils",
|
||||
"rev": "c1dfcf08411b08f6b8615f7d8971a2bfa81d5e8a",
|
||||
"rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
|
@ -58,16 +56,18 @@
|
|||
},
|
||||
"nixpkgs": {
|
||||
"locked": {
|
||||
"lastModified": 1729265718,
|
||||
"narHash": "sha256-4HQI+6LsO3kpWTYuVGIzhJs1cetFcwT7quWCk/6rqeo=",
|
||||
"lastModified": 1702346276,
|
||||
"narHash": "sha256-eAQgwIWApFQ40ipeOjVSoK4TEHVd6nbSd9fApiHIw5A=",
|
||||
"owner": "NixOS",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "ccc0c2126893dd20963580b6478d1a10a4512185",
|
||||
"rev": "cf28ee258fd5f9a52de6b9865cdb93a1f96d09b7",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"id": "nixpkgs",
|
||||
"type": "indirect"
|
||||
"owner": "NixOS",
|
||||
"ref": "nixos-23.11",
|
||||
"repo": "nixpkgs",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"nixpkgs-lib": {
|
||||
|
@ -88,11 +88,25 @@
|
|||
"type": "github"
|
||||
}
|
||||
},
|
||||
"nixpkgs_2": {
|
||||
"locked": {
|
||||
"lastModified": 1718089647,
|
||||
"narHash": "sha256-COO4Xk2EzlZ3x9KCiJildlAA6cYDSPlnY8ms7pKl2Iw=",
|
||||
"owner": "NixOS",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "f7207adcc68d9cafa29e3cd252a18743ae512c6a",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"id": "nixpkgs",
|
||||
"type": "indirect"
|
||||
}
|
||||
},
|
||||
"root": {
|
||||
"inputs": {
|
||||
"agda": "agda",
|
||||
"flake-utils": "flake-utils",
|
||||
"nixpkgs": "nixpkgs"
|
||||
"nixpkgs": "nixpkgs_2"
|
||||
}
|
||||
},
|
||||
"systems": {
|
||||
|
|
|
@ -1,13 +1,12 @@
|
|||
{
|
||||
inputs.agda.url = "github:agda/agda";
|
||||
inputs.agda.inputs.nixpkgs.follows = "nixpkgs";
|
||||
outputs = { self, nixpkgs, flake-utils, agda, }:
|
||||
flake-utils.lib.eachDefaultSystem (system:
|
||||
let
|
||||
pkgs = import nixpkgs { inherit system; overlays = [ agda.overlays.default ]; };
|
||||
pkgs = import nixpkgs { inherit system; };
|
||||
agda-pkg = agda.packages.x86_64-linux.default;
|
||||
flakePkgs = rec {
|
||||
agda-bin = pkgs.callPackage ./nix/agda-bin.nix { agda-pkg = pkgs.haskellPackages.Agda.bin; };
|
||||
agda-bin = pkgs.callPackage ./nix/agda-bin.nix { inherit agda-pkg; };
|
||||
docker-builder =
|
||||
pkgs.callPackage ./nix/docker-builder.nix { inherit agda-bin; };
|
||||
};
|
||||
|
@ -19,9 +18,13 @@
|
|||
packages = with pkgs;
|
||||
with flakePkgs; [
|
||||
bun
|
||||
woodpecker-cli
|
||||
nixfmt-rfc-style
|
||||
dive
|
||||
nix-tree
|
||||
vips
|
||||
shellcheck
|
||||
agda-bin
|
||||
|
||||
nodejs_20
|
||||
corepack
|
||||
|
|
|
@ -6,8 +6,8 @@ let
|
|||
writeTextFile {
|
||||
name = "agda-libraries";
|
||||
text = ''
|
||||
${agdaPackages.cubical.src}/cubical.agda-lib
|
||||
${agdaPackages.standard-library.src}/standard-library.agda-lib
|
||||
${agdaPackages.cubical}/cubical.agda-lib
|
||||
${agdaPackages.standard-library}/standard-library.agda-lib
|
||||
'';
|
||||
};
|
||||
|
||||
|
|
|
@ -1,15 +1,13 @@
|
|||
{ dockerTools
|
||||
, agda-bin
|
||||
, bash
|
||||
, corepack
|
||||
, coreutils
|
||||
, gitMinimal
|
||||
, gnused
|
||||
, minio-client
|
||||
, nodejs_20
|
||||
, openssh
|
||||
, pkgsLinux
|
||||
, rsync
|
||||
, openssh
|
||||
, bash
|
||||
, coreutils
|
||||
, nodejs_20
|
||||
, gnused
|
||||
, pkgsLinux
|
||||
}:
|
||||
|
||||
dockerTools.buildLayeredImage {
|
||||
|
@ -17,18 +15,16 @@ dockerTools.buildLayeredImage {
|
|||
|
||||
contents = with dockerTools; [
|
||||
agda-bin
|
||||
bash
|
||||
caCertificates
|
||||
corepack
|
||||
coreutils
|
||||
fakeNss
|
||||
gitMinimal
|
||||
gnused
|
||||
minio-client
|
||||
nodejs_20
|
||||
openssh
|
||||
rsync
|
||||
openssh
|
||||
bash
|
||||
coreutils
|
||||
nodejs_20
|
||||
gnused
|
||||
usrBinEnv
|
||||
caCertificates
|
||||
fakeNss
|
||||
];
|
||||
|
||||
# fakeRootCommands = ''
|
||||
|
|
32
package.json
|
@ -12,18 +12,18 @@
|
|||
"format": "prettier -w ."
|
||||
},
|
||||
"dependencies": {
|
||||
"@astrojs/markdoc": "^0.12.4",
|
||||
"@astrojs/markdown-remark": "^6.0.1",
|
||||
"@astrojs/mdx": "^4.0.3",
|
||||
"@astrojs/rss": "^4.0.10",
|
||||
"@astrojs/sitemap": "^3.2.1",
|
||||
"@astrojs/markdoc": "^0.11.1",
|
||||
"@astrojs/markdown-remark": "^5.1.1",
|
||||
"@astrojs/mdx": "^1.1.5",
|
||||
"@astrojs/rss": "^3.0.0",
|
||||
"@astrojs/sitemap": "^3.1.6",
|
||||
"@justfork/rehype-autolink-headings": "^5.1.1",
|
||||
"astro": "^5.1.1",
|
||||
"astro": "^3.6.5",
|
||||
"astro-imagetools": "^0.9.0",
|
||||
"astro-remark-description": "^1.1.2",
|
||||
"classnames": "^2.5.1",
|
||||
"fork-awesome": "^1.2.0",
|
||||
"katex": "^0.16.18",
|
||||
"katex": "^0.16.10",
|
||||
"lodash-es": "^4.17.21",
|
||||
"mdast-util-to-string": "^4.0.0",
|
||||
"nanoid": "^4.0.2",
|
||||
|
@ -32,24 +32,22 @@
|
|||
"rehype-katex": "^6.0.3",
|
||||
"remark-emoji": "^4.0.1",
|
||||
"remark-github-beta-blockquote-admonitions": "^2.2.1",
|
||||
"remark-math": "^6.0.0",
|
||||
"remark-math": "^5.1.1",
|
||||
"remark-parse": "^10.0.2",
|
||||
"sanitize-html": "^2.14.0",
|
||||
"sharp": "^0.33.5"
|
||||
"sharp": "^0.33.4"
|
||||
},
|
||||
"devDependencies": {
|
||||
"@biomejs/biome": "^1.9.4",
|
||||
"@biomejs/biome": "^1.8.2",
|
||||
"@types/lodash-es": "^4.17.12",
|
||||
"@types/sanitize-html": "^2.13.0",
|
||||
"date-fns": "^2.30.0",
|
||||
"hast-util-from-html": "^2.0.3",
|
||||
"hast-util-to-html": "^9.0.4",
|
||||
"hast-util-from-html": "^2.0.1",
|
||||
"hast-util-to-html": "^9.0.1",
|
||||
"mdast": "^3.0.0",
|
||||
"mdast-util-from-markdown": "^2.0.2",
|
||||
"prettier": "^3.4.2",
|
||||
"mdast-util-from-markdown": "^2.0.1",
|
||||
"prettier": "^3.3.2",
|
||||
"prettier-plugin-astro": "^0.12.3",
|
||||
"rehype-slug": "^6.0.0",
|
||||
"sass": "^1.83.0",
|
||||
"sass": "^1.77.6",
|
||||
"shiki": "^0.14.7",
|
||||
"unified": "^11.0.5",
|
||||
"unist-util-visit": "^5.0.0"
|
||||
|
|
|
@ -89,7 +89,9 @@ export const mkdocsConfig: Partial<Config> = {
|
|||
titleFilter: (title) => Boolean(title.match(TITLE_PATTERN)),
|
||||
|
||||
titleTextMap: (title: string) => {
|
||||
console.log("title", title);
|
||||
const match = title.match(TITLE_PATTERN);
|
||||
console.log("matches", match);
|
||||
const displayTitle = match?.[1] ?? "";
|
||||
const checkedTitle = displayTitle;
|
||||
return { displayTitle, checkedTitle };
|
||||
|
|
|
@ -14,7 +14,7 @@ import {
|
|||
writeFileSync,
|
||||
} from "node:fs";
|
||||
import { tmpdir } from "node:os";
|
||||
import { join, parse, resolve, basename } from "node:path";
|
||||
import { join, parse } from "node:path";
|
||||
import { visit } from "unist-util-visit";
|
||||
import type { RemarkPlugin } from "@astrojs/markdown-remark";
|
||||
|
||||
|
@ -32,10 +32,12 @@ const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => {
|
|||
const path: string = history[history.length - 1]!;
|
||||
if (!(path.endsWith(".lagda.md") || path.endsWith(".agda"))) return;
|
||||
|
||||
// console.log("AGDA:processing path", path);
|
||||
console.log("AGDA:processing path", path);
|
||||
|
||||
const tempDir = mkdtempSync(join(tmpdir(), "agdaRender."));
|
||||
const agdaOutDir = join(tempDir, "output");
|
||||
const agdaOutFilename = parse(path).base.replace(/\.lagda.md/, ".md");
|
||||
const agdaOutFile = join(agdaOutDir, agdaOutFilename);
|
||||
mkdirSync(agdaOutDir, { recursive: true });
|
||||
|
||||
const childOutput = spawnSync(
|
||||
|
@ -50,28 +52,21 @@ const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => {
|
|||
{},
|
||||
);
|
||||
|
||||
// Locate output file
|
||||
const directory = readdirSync(agdaOutDir);
|
||||
const outputFilename = directory.find((name) => name.endsWith(".md"));
|
||||
|
||||
if (childOutput.status !== 0 || outputFilename === undefined) {
|
||||
if (childOutput.error || !existsSync(agdaOutFile)) {
|
||||
throw new Error(
|
||||
`Agda output:
|
||||
`Agda error:
|
||||
|
||||
Stdout:
|
||||
${childOutput.stdout}
|
||||
|
||||
Stderr:
|
||||
${childOutput.stderr}
|
||||
`,
|
||||
${childOutput.stderr}`,
|
||||
{
|
||||
cause: childOutput.error,
|
||||
},
|
||||
);
|
||||
}
|
||||
|
||||
const outputFile = join(agdaOutDir, outputFilename);
|
||||
|
||||
// // TODO: Handle child output
|
||||
// console.error("--AGDA OUTPUT--");
|
||||
// console.error(childOutput);
|
||||
|
@ -94,7 +89,6 @@ const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => {
|
|||
<!DOCTYPE html>
|
||||
<html>
|
||||
<head>
|
||||
<meta charset="utf-8" />
|
||||
<link rel="stylesheet" href="${base}generated/agda/Agda.css" />
|
||||
</head>
|
||||
<body>
|
||||
|
@ -110,9 +104,9 @@ const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => {
|
|||
}
|
||||
}
|
||||
|
||||
const htmlname = basename(resolve(outputFile)).replace(/(\.lagda)?\.md/, ".html");
|
||||
const htmlname = parse(path).base.replace(/\.lagda.md/, ".html");
|
||||
|
||||
const doc = readFileSync(outputFile);
|
||||
const doc = readFileSync(agdaOutFile);
|
||||
|
||||
// This is the post-processed markdown with HTML code blocks replacing the Agda code blocks
|
||||
const tree2 = fromMarkdown(doc);
|
||||
|
@ -131,9 +125,7 @@ const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => {
|
|||
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 (href === htmlname) node.properties.href = `#${hash}`;
|
||||
|
||||
if (referencedFiles.has(href)) {
|
||||
node.properties.href = `${base}generated/agda/${href}${hash ? `#${hash}` : ""}`;
|
||||
|
@ -151,23 +143,13 @@ const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => {
|
|||
});
|
||||
|
||||
let idx = 0;
|
||||
try {
|
||||
visit(tree, "code", (node) => {
|
||||
if (!(node.lang === null || node.lang === "agda")) return;
|
||||
visit(tree, "code", (node) => {
|
||||
if (!(node.lang === null || node.lang === "agda")) return;
|
||||
|
||||
if (idx > collectedCodeBlocks.length) {
|
||||
throw new Error("failed");
|
||||
}
|
||||
|
||||
node.type = "html";
|
||||
node.value = collectedCodeBlocks[idx].contents;
|
||||
idx += 1;
|
||||
});
|
||||
} catch (e) {
|
||||
// TODO: Figure out a way to handle this correctly
|
||||
// Possibly by diffing?
|
||||
console.log("Mismatch in number of args. Perhaps there was an empty block?");
|
||||
}
|
||||
node.type = "html";
|
||||
node.value = collectedCodeBlocks[idx].contents;
|
||||
idx += 1;
|
||||
});
|
||||
};
|
||||
};
|
||||
|
||||
|
|
|
@ -1,10 +1,10 @@
|
|||
import getReadingTime from "reading-time";
|
||||
import { toString as mdastToString } from "mdast-util-to-string";
|
||||
import { toString } from "mdast-util-to-string";
|
||||
import type { RemarkPlugin } from "@astrojs/markdown-remark";
|
||||
|
||||
const remarkReadingTime: RemarkPlugin = () => {
|
||||
return (tree, { data }) => {
|
||||
const textOnPage = mdastToString(tree);
|
||||
const textOnPage = toString(tree);
|
||||
const readingTime = getReadingTime(textOnPage);
|
||||
|
||||
// readingTime.text will give us minutes read as a friendly string,
|
||||
|
|
5200
pnpm-lock.yaml
Before Width: | Height: | Size: 136 KiB |
|
@ -1,3 +1,2 @@
|
|||
User-agent: *
|
||||
Allow: /
|
||||
Disallow: /drafts
|
||||
Allow: /
|
Before Width: | Height: | Size: 24 KiB After Width: | Height: | Size: 24 KiB |
|
@ -1,27 +1,16 @@
|
|||
---
|
||||
import "../styles/footer.scss";
|
||||
import { execSync } from "node:child_process";
|
||||
|
||||
const dateUpdated = new Date();
|
||||
const gitRevShort = execSync("git rev-parse --short HEAD").toString().trim();
|
||||
const gitRev = execSync("git rev-parse HEAD").toString().trim();
|
||||
---
|
||||
|
||||
<footer>
|
||||
<p>
|
||||
Blog theme and contents written by Michael Zhang with the <a
|
||||
href="https://astro.build/"
|
||||
target="_blank"
|
||||
rel="noreferrer noopener">Astro</a
|
||||
> framework.
|
||||
<br />
|
||||
Last updated {dateUpdated.toLocaleString(undefined, { dateStyle: "full" })} at commit
|
||||
<a
|
||||
href={`https://git.mzhang.io/michael/blog/commit/${gitRev}`}
|
||||
class="colorlink"
|
||||
target="_blank">{gitRevShort}</a
|
||||
Blog code licensed under <a href="https://www.gnu.org/licenses/gpl-3.0.txt" target="_blank"
|
||||
>GPL-3.0</a
|
||||
>. Post contents licensed under <a
|
||||
href="https://creativecommons.org/licenses/by-sa/4.0/legalcode.txt">CC BY-SA 4.0</a
|
||||
>.
|
||||
<br />
|
||||
<a href="https://git.mzhang.io/michael/blog" class="colorlink" target="_blank">Source code</a>.
|
||||
Written by Michael Zhang.
|
||||
<a href="https://git.mzhang.io/michael/blog" class="colorlink" target="_blank">Source</a>.
|
||||
</p>
|
||||
</footer>
|
||||
|
|
|
@ -4,31 +4,31 @@ import { Content as ShortBio } from "../content/partials/shortBio.md";
|
|||
import links from "../data/links";
|
||||
import { Image } from "astro:assets";
|
||||
import portrait from "../assets/self.png";
|
||||
|
||||
// const target = Astro.url.pathname === "/" ? "/about/" : "/";
|
||||
const target = "/";
|
||||
---
|
||||
|
||||
<nav class="side-nav">
|
||||
<div class="side-nav-content">
|
||||
<a href={target} class="portrait" data-astro-prefetch>
|
||||
<Image src={portrait} alt="portrait" class="portrait" width={350} height={350} loading="eager" />
|
||||
<a href="/" class="portrait">
|
||||
<Image src={portrait} alt="portrait" class="portrait" />
|
||||
</a>
|
||||
<div class="me">
|
||||
<div class="titleContainer">
|
||||
<h1 class="title">
|
||||
<a href={target} data-astro-prefetch>Michael Zhang</a>
|
||||
</h1>
|
||||
</div>
|
||||
|
||||
<h1 class="title">Michael Zhang</h1>
|
||||
<div class="links">
|
||||
<a href="/about/">About</a>
|
||||
{
|
||||
links.map((link) => {
|
||||
return (
|
||||
<a href={link.url} title={link.description}>
|
||||
{link.name}
|
||||
</a>
|
||||
);
|
||||
})
|
||||
}
|
||||
</div>
|
||||
</div>
|
||||
|
||||
<div class="bio">
|
||||
<ShortBio />
|
||||
<a href="/about/">More »</a>
|
||||
<a href="/about">More »</a>
|
||||
</div>
|
||||
</div>
|
||||
</nav>
|
||||
|
|
|
@ -59,7 +59,7 @@ const sortedPosts = sortBy(allPosts, (post) => -post.data.date);
|
|||
<tr class="row">
|
||||
<td>
|
||||
<div class="title">
|
||||
<a href={`${basePath}/${post.id}/`} class="brand-colorlink">
|
||||
<a href={`${basePath}/${post.slug}/`} class="brand-colorlink">
|
||||
{post.data.title}
|
||||
</a>
|
||||
</div>
|
||||
|
@ -79,7 +79,7 @@ const sortedPosts = sortBy(allPosts, (post) => -post.data.date);
|
|||
<style lang="scss">
|
||||
.postListing {
|
||||
width: 100%;
|
||||
border-spacing: 0px 24px;
|
||||
border-spacing: 6px 24px;
|
||||
|
||||
:global(.timestamp) {
|
||||
font-family: var(--monofont);
|
||||
|
|
|
@ -8,7 +8,7 @@ const { extraFront, tags, extraBack } = Astro.props;
|
|||
{extraFront}
|
||||
{
|
||||
tags.toSorted().map((tag: string) => (
|
||||
<a href={`/tags/${tag}/`} class="tag">
|
||||
<a href={`/tags/${tag}`} class="tag">
|
||||
<i class="fa fa-tag" aria-hidden="true" />
|
||||
<span class="text">#{tag}</span>
|
||||
</a>
|
||||
|
|
|
@ -1,5 +1,5 @@
|
|||
// Place any global data in this file.
|
||||
// You can import this data from anywhere in your site by using the `import` keyword.
|
||||
|
||||
export const SITE_TITLE = "Michael's Blog";
|
||||
export const SITE_DESCRIPTION = "Michael's Blog";
|
||||
export const SITE_TITLE = "Astro Blog";
|
||||
export const SITE_DESCRIPTION = "Welcome to my website!";
|
||||
|
|
|
@ -1,8 +1,7 @@
|
|||
import { defineCollection, z } from "astro:content";
|
||||
import { glob, file } from "astro/loaders";
|
||||
|
||||
const posts = defineCollection({
|
||||
loader: glob({ pattern: ["**/*.md", "**/*.mdx"], base: "./src/posts" }),
|
||||
type: "content",
|
||||
|
||||
// Type-check frontmatter using a schema
|
||||
schema: ({ image }) =>
|
|
@ -1,5 +1,15 @@
|
|||
I'm a computer science master's student at the [University of Minnesota][1], advised by [Favonia].
|
||||
My current research is in programming languages and formal methods, specifically cubical type theory and synthetic homotopy theory.
|
||||
My current research is cubical type theory and its applications to formalizing some results in algebraic topology.
|
||||
|
||||
I also work as a researcher for [SIFT], specializing in compilers and binary analysis. Previously I worked as a software engineer at [Swoop Search] and [AWS].
|
||||
|
||||
Before that, I was a CTF hobbyist. I created [EasyCTF], a cybersecurity competition for high schoolers.
|
||||
I also briefly played with the CTF team [Project Sekai][pjsk].
|
||||
|
||||
[1]: https://twin-cities.umn.edu/
|
||||
[Swoop Search]: https://swoopsrch.com/
|
||||
[aws]: https://aws.amazon.com/
|
||||
[sift]: https://www.sift.net/
|
||||
[favonia]: https://favonia.org/
|
||||
[easyctf]: https://www.easyctf.com/
|
||||
[pjsk]: https://sekai.team/
|
||||
|
|
|
@ -85,6 +85,6 @@ then calling something like `instance.verify()` should run all those validators
|
|||
|
||||
## Conclusion
|
||||
|
||||
This project is a work in progress! You can see how far I am [on Github](https://github.com/mzhang28/wtforms).
|
||||
This project is a work in progress! You can see how far I am [on Github](https://github.com/iptq/wtforms).
|
||||
|
||||
[1]: https://docs.rs/serde
|
|
@ -73,7 +73,7 @@ all of the objects except the two flag halves.
|
|||
|
||||
[blender]: https://www.blender.org
|
||||
|
||||
![Hiding blender objects](./blender-objects.png)
|
||||
![Hiding blender objects](../../../assets/ctf/blender-objects.png)
|
||||
|
||||
This reveals two QR codes that can be combined into the flag.
|
||||
|
|
@ -1,6 +1,6 @@
|
|||
---
|
||||
title: "Dependent Types from First Principles"
|
||||
id: "dependent-types"
|
||||
slug: "dependent-types"
|
||||
date: 2022-10-27
|
||||
tags: ["type-theory"]
|
||||
toc: true
|
|
@ -1,6 +1,6 @@
|
|||
---
|
||||
title: "Formally proving true ≢ false in Homotopy Type Theory with Agda"
|
||||
id: "proving-true-from-false"
|
||||
slug: "proving-true-from-false"
|
||||
date: 2023-04-21
|
||||
tags: ["type-theory", "agda"]
|
||||
math: true
|
|
@ -1,6 +1,6 @@
|
|||
---
|
||||
title: "Equivalences"
|
||||
id: "equivalences"
|
||||
slug: "equivalences"
|
||||
date: 2023-05-06
|
||||
tags:
|
||||
- type-theory
|
Before Width: | Height: | Size: 984 KiB After Width: | Height: | Size: 984 KiB |
Before Width: | Height: | Size: 62 KiB After Width: | Height: | Size: 62 KiB |
Before Width: | Height: | Size: 25 KiB After Width: | Height: | Size: 25 KiB |
Before Width: | Height: | Size: 190 KiB After Width: | Height: | Size: 190 KiB |
Before Width: | Height: | Size: 630 KiB After Width: | Height: | Size: 630 KiB |
Before Width: | Height: | Size: 1.8 MiB After Width: | Height: | Size: 1.8 MiB |
|
@ -1,6 +1,6 @@
|
|||
---
|
||||
title: "Path induction: a GADT perspective"
|
||||
id: 2023-10-23-path-induction-gadt-perspective
|
||||
slug: 2023-10-23-path-induction-gadt-perspective
|
||||
date: 2023-10-23
|
||||
tags: ["type-theory", "pl-theory"]
|
||||
---
|
Before Width: | Height: | Size: 704 KiB After Width: | Height: | Size: 704 KiB |
Before Width: | Height: | Size: 25 KiB After Width: | Height: | Size: 25 KiB |
Before Width: | Height: | Size: 37 KiB After Width: | Height: | Size: 37 KiB |
Before Width: | Height: | Size: 37 KiB After Width: | Height: | Size: 37 KiB |
Before Width: | Height: | Size: 46 KiB After Width: | Height: | Size: 46 KiB |
Before Width: | Height: | Size: 44 KiB After Width: | Height: | Size: 44 KiB |
Before Width: | Height: | Size: 34 KiB After Width: | Height: | Size: 34 KiB |
Before Width: | Height: | Size: 44 KiB After Width: | Height: | Size: 44 KiB |
Before Width: | Height: | Size: 99 KiB After Width: | Height: | Size: 99 KiB |
Before Width: | Height: | Size: 478 KiB After Width: | Height: | Size: 478 KiB |
Before Width: | Height: | Size: 28 KiB After Width: | Height: | Size: 28 KiB |
Before Width: | Height: | Size: 2.4 MiB After Width: | Height: | Size: 2.4 MiB |
|
@ -1,6 +1,6 @@
|
|||
---
|
||||
title: "Agda syntax highlighting in my blog!"
|
||||
id: 2024-06-26-agda-rendering
|
||||
slug: 2024-06-26-agda-rendering
|
||||
date: 2024-06-27T04:25:15.332Z
|
||||
tags: ["meta", "agda"]
|
||||
---
|
|
@ -1,6 +1,6 @@
|
|||
---
|
||||
title: Boolean equivalences
|
||||
id: 2024-06-28-boolean-equivalences
|
||||
title: "Boolean equivalences in HoTT"
|
||||
slug: 2024-06-28-boolean-equivalences
|
||||
date: 2024-06-28T21:37:04.299Z
|
||||
tags: ["agda", "type-theory", "hott"]
|
||||
---
|
||||
|
@ -32,7 +32,7 @@ open Σ
|
|||
|
||||
With just that notation, the problem may not be clear.
|
||||
$2$ represents the set with only two elements in it, which is the booleans. The
|
||||
elements of $2$ are $\mathsf{true}$ and $\mathsf{false}$.
|
||||
elements of $2$ are $\textrm{true}$ and $\textrm{false}$.
|
||||
|
||||
```
|
||||
data 𝟚 : Set where
|
||||
|
@ -53,8 +53,8 @@ shown by Theorem 4.1.3 in the [HoTT book][book].
|
|||
[1]: https://en.wikipedia.org/wiki/Homotopy#Homotopy_equivalence
|
||||
|
||||
- there exists a $g : B \rightarrow A$
|
||||
- $f \circ g$ is homotopic to the identity map $\mathsf{id}_B : B \rightarrow B$
|
||||
- $g \circ f$ is homotopic to the identity map $\mathsf{id}_A : A \rightarrow A$
|
||||
- $f \circ g$ is homotopic to the identity map $\textrm{id}_B : B \rightarrow B$
|
||||
- $g \circ f$ is homotopic to the identity map $\textrm{id}_A : A \rightarrow A$
|
||||
|
||||
We can write this in Agda like this:
|
||||
|
||||
|
@ -92,7 +92,7 @@ function along with proof of its equivalence properties using a dependent
|
|||
pair[^dependent-pair]:
|
||||
|
||||
[^dependent-pair]: A dependent pair (or $\Sigma$-type) is like a regular pair $\langle x, y\rangle$, but where $y$ can depend on $x$.
|
||||
For example, $\langle x , \mathsf{isPrime}(x) \rangle$.
|
||||
For example, $\langle x , \textrm{isPrime}(x) \rangle$.
|
||||
In this case it's useful since we can carry the equivalence information along with the function itself.
|
||||
This type is rather core to Martin-Löf Type Theory, you can read more about it [here][dependent-pair].
|
||||
|
||||
|
@ -184,8 +184,8 @@ Now we need another function in the other direction. We can't case-split on
|
|||
functions, but we can certainly case-split on their output. Specifically, we can
|
||||
differentiate `id` from `neg` by their behavior when being called on `true`:
|
||||
|
||||
- $\mathsf{id}(\mathsf{true}) :\equiv \mathsf{true}$
|
||||
- $\mathsf{neg}(\mathsf{true}) :\equiv \mathsf{false}$
|
||||
- $\textrm{id}(\textrm{true}) :\equiv \textrm{true}$
|
||||
- $\textrm{neg}(\textrm{true}) :\equiv \textrm{false}$
|
||||
|
||||
```
|
||||
g : (𝟚 ≃ 𝟚) → 𝟚
|
||||
|
@ -207,7 +207,7 @@ everything to true, since it can't possibly have an inverse.
|
|||
|
||||
We'll come back to this later.
|
||||
|
||||
First, let's show that $g \circ f \sim \mathsf{id}$. This one is easy, we can
|
||||
First, let's show that $g \circ f \sim \textrm{id}$. This one is easy, we can
|
||||
just case-split. Each of the cases reduces to something that is definitionally
|
||||
equal, so we can use `refl`.
|
||||
|
||||
|
@ -217,7 +217,7 @@ g∘f true = refl
|
|||
g∘f false = refl
|
||||
```
|
||||
|
||||
Now comes the complicated case: proving $f \circ g \sim \mathsf{id}$.
|
||||
Now comes the complicated case: proving $f \circ g \sim \textrm{id}$.
|
||||
|
||||
> [!admonition: NOTE]
|
||||
> Since Agda's comment syntax is `--`, the horizontal lines in the code below
|
||||
|
@ -235,9 +235,9 @@ module f∘g-case where
|
|||
f∘g eqv = goal eqv
|
||||
```
|
||||
|
||||
Now our goal is to show that for any equivalence $\mathsf{eqv} : 2 \simeq 2$,
|
||||
Now our goal is to show that for any equivalence $\textrm{eqv} : 2 \simeq 2$,
|
||||
applying $f ∘ g$ to it is the same as not doing anything. We can evaluate the
|
||||
$g(\mathsf{eqv})$ a little bit to give us a more detailed goal:
|
||||
$g(\textrm{eqv})$ a little bit to give us a more detailed goal:
|
||||
|
||||
```
|
||||
goal2 :
|
||||
|
@ -273,27 +273,27 @@ a syntax known as [with-abstraction]:
|
|||
|
||||
We can now case-split on $b$, which is the output of calling $f$ on the
|
||||
equivalence returned by $g$. This means that for the `true` case, we need to
|
||||
show that $f(b) = \mathsf{booleqv}$ (which is based on `id`) is equivalent to
|
||||
show that $f(b) = \textrm{bool-eqv}$ (which is based on `id`) is equivalent to
|
||||
the equivalence that generated the `true`.
|
||||
|
||||
Let's start with the `id` case; we just need to show that for every equivalence
|
||||
$e$ where running the equivalence function on `true` also returned `true`, $e
|
||||
\equiv f(\mathsf{true})$.
|
||||
\equiv f(\textrm{true})$.
|
||||
|
||||
Unfortunately, we don't know if this is true unless our equivalences are _mere
|
||||
propositions_, meaning if two functions are identical, then so are their
|
||||
equivalences.
|
||||
|
||||
$$
|
||||
\mathsf{isProp}(P) :\equiv \prod_{x, y \, : \, P}(x \equiv y)
|
||||
\textrm{isProp}(P) :\equiv \prod_{x, y: P}(x \equiv y)
|
||||
$$
|
||||
|
||||
<small>Definition 3.3.1 from the [HoTT book][book]</small>
|
||||
|
||||
Applying this to $\mathsf{isEquiv}(f)$, we get the property:
|
||||
Applying this to $\textrm{isEquiv}(f)$, we get the property:
|
||||
|
||||
$$
|
||||
\sum_{f : A → B} \left( \prod_{e_1, e_2 \, : \, \mathsf{isEquiv}(f)} e_1 \equiv e_2 \right)
|
||||
\sum_{f : A → B} \left( \prod_{e_1, e_2 : \textrm{isEquiv}(f)} e_1 \equiv e_2 \right)
|
||||
$$
|
||||
|
||||
This proof is shown later in the book, so I will use it here directly without proof[^equiv-isProp]:
|
||||
|
@ -314,7 +314,7 @@ equivalences must not map both values to a single one.
|
|||
This way, we can pin the behavior of the function on all inputs by just using
|
||||
its behavior on `true`, since its output on `false` must be _different_.
|
||||
|
||||
We can use a proof that [$\mathsf{true} \not\equiv \mathsf{false}$][true-not-false] that I've shown previously.
|
||||
We can use a proof that [$\textrm{true} \not\equiv \textrm{false}$][true-not-false] that I've shown previously.
|
||||
|
||||
[true-not-false]: https://mzhang.io/posts/proving-true-from-false/
|
||||
|
7
src/content/posts/_index.md
Normal file
|
@ -0,0 +1,7 @@
|
|||
+++
|
||||
title = "Blog"
|
||||
weight = 1
|
||||
|
||||
[cascade]
|
||||
type = "posts"
|
||||
+++
|
|
@ -6,18 +6,24 @@ export interface Link {
|
|||
}
|
||||
|
||||
const links: Link[] = [
|
||||
{
|
||||
name: "projects",
|
||||
url: "https://git.mzhang.io/michael",
|
||||
icon: "gitea",
|
||||
description: "Check out my public open source projects on Forgejo",
|
||||
},
|
||||
{
|
||||
name: "Matrix",
|
||||
url: "https://matrix.to/#/@michael:chat.mzhang.io",
|
||||
icon: "matrix-org",
|
||||
description: "Come chat with me on Matrix",
|
||||
},
|
||||
{
|
||||
name: "Git",
|
||||
url: "https://git.mzhang.io",
|
||||
icon: "gitea",
|
||||
description: "Check out my public open source projects on Forgejo",
|
||||
},
|
||||
{
|
||||
name: "GitHub",
|
||||
url: "https://github.com/iptq",
|
||||
icon: "github",
|
||||
description: "See a history of my old projects on GitHub",
|
||||
},
|
||||
{
|
||||
name: "Mastodon",
|
||||
url: "https://fosstodon.org/@mzhang",
|
||||
|
@ -36,12 +42,6 @@ const links: Link[] = [
|
|||
icon: "linkedin",
|
||||
description: "Connect with me on LinkedIn",
|
||||
},
|
||||
{
|
||||
name: "GitHub",
|
||||
url: "https://github.com/mzhang28",
|
||||
icon: "github",
|
||||
description: "See a history of my old projects on GitHub",
|
||||
},
|
||||
];
|
||||
|
||||
export default links;
|
||||
|
|