This commit is contained in:
parent
2973f40c00
commit
9f6665b2b1
5 changed files with 26 additions and 40 deletions
|
@ -32,7 +32,7 @@ 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");
|
||||
|
@ -109,10 +109,7 @@ const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => {
|
|||
}
|
||||
}
|
||||
|
||||
const htmlname = basename(resolve(outputFile)).replace(
|
||||
/(\.lagda)?\.md/,
|
||||
".html",
|
||||
);
|
||||
const htmlname = basename(resolve(outputFile)).replace(/(\.lagda)?\.md/, ".html");
|
||||
|
||||
const doc = readFileSync(outputFile);
|
||||
|
||||
|
@ -168,9 +165,7 @@ const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => {
|
|||
} 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?",
|
||||
);
|
||||
console.log("Mismatch in number of args. Perhaps there was an empty block?");
|
||||
}
|
||||
};
|
||||
};
|
||||
|
|
|
@ -5,7 +5,8 @@ import links from "../data/links";
|
|||
import { Image } from "astro:assets";
|
||||
import portrait from "../assets/self.png";
|
||||
|
||||
const target = Astro.url.pathname === "/" ? "/about/" : "/";
|
||||
// const target = Astro.url.pathname === "/" ? "/about/" : "/";
|
||||
const target = "/";
|
||||
---
|
||||
|
||||
<nav class="side-nav">
|
||||
|
@ -19,16 +20,9 @@ const target = Astro.url.pathname === "/" ? "/about/" : "/";
|
|||
<a href={target} data-astro-prefetch>Michael Zhang</a>
|
||||
</h1>
|
||||
</div>
|
||||
|
||||
<div class="links">
|
||||
{
|
||||
links.map((link) => {
|
||||
return (
|
||||
<a href={link.url} title={link.description}>
|
||||
{link.name}
|
||||
</a>
|
||||
);
|
||||
})
|
||||
}
|
||||
<a href="/about/">About</a>
|
||||
</div>
|
||||
</div>
|
||||
|
||||
|
|
|
@ -1,15 +1,5 @@
|
|||
I'm a computer science master's student at the [University of Minnesota][1], advised by [Favonia].
|
||||
My current research topic is in cubical type theory and formalization of the Serre spectral sequence.
|
||||
|
||||
I've also worked 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].
|
||||
My current research is in cubical type theory and synthetic homotopy theory.
|
||||
|
||||
[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/
|
||||
|
|
|
@ -11,6 +11,17 @@ Hi there! :wave:
|
|||
|
||||
<Intro />
|
||||
|
||||
I've also worked 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].
|
||||
|
||||
[Swoop Search]: https://swoopsrch.com/
|
||||
[aws]: https://aws.amazon.com/
|
||||
[sift]: https://www.sift.net/
|
||||
[easyctf]: https://www.easyctf.com/
|
||||
[pjsk]: https://sekai.team/
|
||||
|
||||
## Academic life
|
||||
|
||||
I'm currently doing a thesis project for my master's program, involving the mechanization of [spectral sequences] using [cubical] [Agda].
|
||||
|
|
|
@ -24,16 +24,16 @@
|
|||
text-align: center;
|
||||
font-size: 0.9rem;
|
||||
|
||||
display: grid;
|
||||
grid-template-columns: repeat(3, 1fr);
|
||||
row-gap: 6px;
|
||||
display: flex;
|
||||
flex-direction: column;
|
||||
/* gap: 6px; */
|
||||
|
||||
a {
|
||||
text-decoration: none;
|
||||
color: var(--link-color);
|
||||
text-transform: lowercase;
|
||||
border-radius: 4px;
|
||||
padding: 4px;
|
||||
/* text-transform: lowercase; */
|
||||
/* border-radius: 4px; */
|
||||
padding: 8px;
|
||||
|
||||
&:hover {
|
||||
background-color: var(--link-hover-color);
|
||||
|
@ -137,10 +137,6 @@
|
|||
h1.title {
|
||||
text-align: center;
|
||||
}
|
||||
|
||||
.links {
|
||||
// margin-bottom: 20px;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue