upgrade to astro 5.0

astro.config.ts

@@ -35,7 +35,7 @@ export default defineConfig({
     shikiConfig: { theme: "css-variables" },
     remarkPlugins: [
       () => remarkAgda({ outDir, base, publicDir }),
-      remarkMath,
+      [remarkMath, {}],
       [remarkAdmonitions, mkdocsConfig],
       remarkReadingTime,
       remarkTypst,

blog.agda-lib

@@ -1,2 +1,2 @@
-include: src/content/posts src
+include: src/posts src
 depend: standard-library cubical

package.json

@@ -12,18 +12,18 @@
     "format": "prettier -w ."
   },
   "dependencies": {
-    "@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",
+    "@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",
     "@justfork/rehype-autolink-headings": "^5.1.1",
-    "astro": "^3.6.5",
+    "astro": "^5.1.1",
     "astro-imagetools": "^0.9.0",
     "astro-remark-description": "^1.1.2",
     "classnames": "^2.5.1",
     "fork-awesome": "^1.2.0",
-    "katex": "^0.16.10",
+    "katex": "^0.16.18",
     "lodash-es": "^4.17.21",
     "mdast-util-to-string": "^4.0.0",
     "nanoid": "^4.0.2",
@@ -32,24 +32,24 @@
     "rehype-katex": "^6.0.3",
     "remark-emoji": "^4.0.1",
     "remark-github-beta-blockquote-admonitions": "^2.2.1",
-    "remark-math": "^5.1.1",
+    "remark-math": "^6.0.0",
     "remark-parse": "^10.0.2",
-    "sanitize-html": "^2.13.1",
-    "sharp": "^0.33.4"
+    "sanitize-html": "^2.14.0",
+    "sharp": "^0.33.5"
   },
   "devDependencies": {
-    "@biomejs/biome": "^1.8.2",
+    "@biomejs/biome": "^1.9.4",
     "@types/lodash-es": "^4.17.12",
     "@types/sanitize-html": "^2.13.0",
     "date-fns": "^2.30.0",
-    "hast-util-from-html": "^2.0.1",
-    "hast-util-to-html": "^9.0.1",
+    "hast-util-from-html": "^2.0.3",
+    "hast-util-to-html": "^9.0.4",
     "mdast": "^3.0.0",
-    "mdast-util-from-markdown": "^2.0.1",
-    "prettier": "^3.3.2",
+    "mdast-util-from-markdown": "^2.0.2",
+    "prettier": "^3.4.2",
     "prettier-plugin-astro": "^0.12.3",
     "rehype-slug": "^6.0.0",
-    "sass": "^1.77.6",
+    "sass": "^1.83.0",
     "shiki": "^0.14.7",
     "unified": "^11.0.5",
     "unist-util-visit": "^5.0.0"

src/components/PostList.astro

@@ -59,7 +59,7 @@ const sortedPosts = sortBy(allPosts, (post) => -post.data.date);
           <tr class="row">
             <td>
               <div class="title">
-                <a href={`${basePath}/${post.slug}/`} class="brand-colorlink">
+                <a href={`${basePath}/${post.id}/`} class="brand-colorlink">
                   {post.data.title}
                 </a>
               </div>

src/content.config.ts

@@ -1,7 +1,8 @@
 import { defineCollection, z } from "astro:content";
+import { glob, file } from "astro/loaders";
 
 const posts = defineCollection({
-  type: "content",
+  loader: glob({ pattern: ["**/*.md", "**/*.mdx"], base: "./src/posts" }),
 
   // Type-check frontmatter using a schema
   schema: ({ image }) =>

src/content/posts/_index.md

@@ -1,7 +0,0 @@
-+++
-title = "Blog"
-weight = 1
-
-[cascade]
-type = "posts"
-+++

src/env.d.ts

@@ -1,2 +0,0 @@
-/// <reference path="../.astro/types.d.ts" />
-/// <reference types="astro/client" />

src/pages/posts/[...id].astro

@@ -7,11 +7,12 @@ import Timestamp from "../../components/Timestamp.astro";
 import { getImage } from "astro:assets";
 import TocWrapper from "../../components/TocWrapper.astro";
 import TagList from "../../components/TagList.astro";
+import { render } from "astro:content";
 
 export async function getStaticPaths() {
   const posts = await getCollection("posts");
   return posts.map((post) => ({
-    params: { slug: post.slug },
+    params: { id: post.id },
     props: post,
   }));
 }
@@ -19,7 +20,7 @@ export async function getStaticPaths() {
 type Props = CollectionEntry<"posts">;
 
 const post = Astro.props;
-const { Content, remarkPluginFrontmatter, headings } = await post.render();
+const { Content, remarkPluginFrontmatter, headings } = await render(post);
 const { title, toc, heroImage: heroImagePath, heroAlt } = post.data;
 
 let heroImage = undefined;

src/posts/2022-08-01-uiuctf-2022-writeups/index.md

@@ -73,7 +73,7 @@ all of the objects except the two flag halves.
 
 [blender]: https://www.blender.org
 
-![Hiding blender objects](../../../assets/ctf/blender-objects.png)
+![Hiding blender objects](./blender-objects.png)
 
 This reveals two QR codes that can be combined into the flag.
 

src/posts/2022-10-27-dependent-types.md

@@ -1,6 +1,6 @@
 ---
 title: "Dependent Types from First Principles"
-slug: "dependent-types"
+id: "dependent-types"
 date: 2022-10-27
 tags: ["type-theory"]
 toc: true

src/posts/2023-04-21-proving-true-from-false.lagda.md

@@ -1,6 +1,6 @@
 ---
 title: "Formally proving true ≢ false in Homotopy Type Theory with Agda"
-slug: "proving-true-from-false"
+id: "proving-true-from-false"
 date: 2023-04-21
 tags: ["type-theory", "agda"]
 math: true

src/posts/2023-05-06-equivalences.md

@@ -1,6 +1,6 @@
 ---
 title: "Equivalences"
-slug: "equivalences"
+id: "equivalences"
 date: 2023-05-06
 tags:
   - type-theory

src/posts/2023-10-23-path-induction-gadt-perspective.lagda.md

@@ -1,6 +1,6 @@
 ---
 title: "Path induction: a GADT perspective"
-slug: 2023-10-23-path-induction-gadt-perspective
+id: 2023-10-23-path-induction-gadt-perspective
 date: 2023-10-23
 tags: ["type-theory", "pl-theory"]
 ---

src/posts/2024-06-26-agda-rendering.lagda.md

@@ -1,6 +1,6 @@
 ---
 title: "Agda syntax highlighting in my blog!"
-slug: 2024-06-26-agda-rendering
+id: 2024-06-26-agda-rendering
 date: 2024-06-27T04:25:15.332Z
 tags: ["meta", "agda"]
 ---

src/posts/2024-06-28-boolean-equivalences.lagda.md

@@ -1,6 +1,6 @@
 ---
 title: Boolean equivalences
-slug: 2024-06-28-boolean-equivalences
+id: 2024-06-28-boolean-equivalences
 date: 2024-06-28T21:37:04.299Z
 tags: ["agda", "type-theory", "hott"]
 ---

src/posts/2024-09-15-circle-is-a-suspension-over-booleans/index.lagda.md

@@ -1,6 +1,6 @@
 ---
 title: The circle is a suspension over booleans
-slug: 2024-09-15-circle-is-a-suspension-over-booleans
+id: 2024-09-15-circle-is-a-suspension-over-booleans
 date: 2024-09-15T23:02:32.058Z
 tags: [algebraic-topology, hott]
 draft: true