diff --git a/.gitignore b/.gitignore index 829aa1c..f35db38 100644 --- a/.gitignore +++ b/.gitignore @@ -24,3 +24,6 @@ PragmataPro-Mono-Liga-Regular-Nerd-Font-Complete.woff2 *.agdai _build .direnv + + +/result diff --git a/.woodpecker.yml b/.woodpecker.yml index 75bc448..998d442 100644 --- a/.woodpecker.yml +++ b/.woodpecker.yml @@ -1,26 +1,18 @@ steps: build: - image: node:20 + image: git.mzhang.io/michael/blog-docker-builder:ksi5l9c786i4x6sq2crsjqlmcfidvvza + environment: + - ASTRO_TELEMETRY_DISABLED=1 commands: - - npm install -g pnpm - # - cd /tmp - # - rm -rf astro - # - git clone https://git.mzhang.io/michael/astro --depth 1 - # - cd astro - # - pnpm install - # - pnpm run build - # - cd /woodpecker/src/git.mzhang.io/michael/blog - - pnpm install - # - pnpm link /tmp/astro/packages/astro - # - pnpm link /tmp/astro/packages/markdown/remark - - pnpm run build + - mkdir /tmp + - bun install --frozen-lockfile + - bun run build when: - event: push deploy: - image: alpine + image: git.mzhang.io/michael/blog-docker-builder:ksi5l9c786i4x6sq2crsjqlmcfidvvza commands: - - apk add rsync openssh - echo "$${SSH_SECRET_KEY}" > SSH_SECRET_KEY - chmod 600 SSH_SECRET_KEY - mkdir -p ~/.ssh diff --git a/astro.config.ts b/astro.config.ts index f029fdf..b1aa992 100644 --- a/astro.config.ts +++ b/astro.config.ts @@ -14,6 +14,7 @@ import rehypeLinkHeadings from "@justfork/rehype-autolink-headings"; import rehypeSlug from "rehype-slug"; import markdoc from "@astrojs/markdoc"; +import remarkAgda from "./plugin/remark-agda"; // https://astro.build/config export default defineConfig({ @@ -25,6 +26,7 @@ export default defineConfig({ theme: "css-variables", }, remarkPlugins: [ + remarkAgda, remarkMath, remarkAdmonitions, remarkReadingTime, diff --git a/blog.agda-lib b/blog.agda-lib index b2eca72..bbf3295 100644 --- a/blog.agda-lib +++ b/blog.agda-lib @@ -1,2 +1,2 @@ include: src/content/posts src -depend: standard-library +depend: standard-library cubical diff --git a/bun.lockb b/bun.lockb new file mode 100755 index 0000000..6bda38a Binary files /dev/null and b/bun.lockb differ diff --git a/flake.nix b/flake.nix index eaeff5a..fb7a12e 100644 --- a/flake.nix +++ b/flake.nix @@ -4,16 +4,22 @@ let pkgs = import nixpkgs { inherit system; }; agda-pkg = agda.packages.x86_64-linux.default; - flakePkgs = { - agda = agda-pkg; - agda-bin = pkgs.callPackage ./nix/agda-bin.nix { agda = agda-pkg; }; - docker-builder = pkgs.callPackage ./nix/docker-builder.nix { }; + flakePkgs = rec { + agda-bin = pkgs.callPackage ./nix/agda-bin.nix { inherit agda-pkg; }; + docker-builder = pkgs.callPackage ./nix/docker-builder.nix { inherit agda-bin; }; }; in { packages = flake-utils.lib.flattenTree flakePkgs; devShell = pkgs.mkShell { - packages = with pkgs; [ nixfmt-rfc-style ]; + packages = with pkgs; [ + bun + woodpecker-cli + nixfmt-rfc-style + dive + nix-tree + vips + ]; }; }); } diff --git a/nix/agda-bin.nix b/nix/agda-bin.nix index 5c2ed45..e112e85 100644 --- a/nix/agda-bin.nix +++ b/nix/agda-bin.nix @@ -1,6 +1,23 @@ -{ agda, runCommand }: +{ agda-pkg, runCommand, writeShellScriptBin, writeTextFile, agdaPackages }: -runCommand "agda-bin" { } - '' - cp ${agda}/bin/agda $out - '' +let + libraryFile = + with agdaPackages; + writeTextFile { + name = "agda-libraries"; + text = '' + ${agdaPackages.cubical}/cubical.agda-lib + ${agdaPackages.standard-library}/standard-library.agda-lib + ''; + }; + + # Add an extra layer of indirection here to prevent all of GHC from being pulled in + wtf = runCommand "agda-bin" { } '' + cp ${agda-pkg}/bin/agda $out + ''; +in + +writeShellScriptBin "agda" '' + set -euo pipefail + exec ${wtf} --library-file=${libraryFile} $@ +'' diff --git a/nix/agda.nix b/nix/agda.nix deleted file mode 100644 index c072dc6..0000000 --- a/nix/agda.nix +++ /dev/null @@ -1,6 +0,0 @@ -{ haskellPackages }: - -haskellPackages.developPackage { - name = "agda"; - version = "2.6.4.3"; -} diff --git a/nix/docker-builder.nix b/nix/docker-builder.nix index fbeb4f2..b90c7af 100644 --- a/nix/docker-builder.nix +++ b/nix/docker-builder.nix @@ -1,3 +1,35 @@ -{ dockerTools }: +{ dockerTools +, buildEnv +, agda-bin +, corepack +, rsync +, openssh +, bash +, coreutils +, bun +, nodejs_20 +}: + +dockerTools.buildLayeredImage { + name = "blog-docker-builder"; + + contents = with dockerTools; [ + agda-bin + corepack + rsync + openssh + bash + coreutils + bun + nodejs_20 + usrBinEnv + caCertificates + ]; +} + +# copyToRoot = with dockerTools; buildEnv { +# name = "blog-docker-builder-image-root"; +# paths = [ +# ]; +# }; -dockerTools.buildImage { } diff --git a/package.json b/package.json index d094b25..39a4d2e 100644 --- a/package.json +++ b/package.json @@ -47,7 +47,6 @@ "prettier-plugin-astro": "^0.12.0", "rehype-slug": "^6.0.0", "sass": "^1.66.1", - "sharp": "^0.32.6", "shiki": "^0.14.5", "unified": "^11.0.2", "unist-util-visit": "^5.0.0" diff --git a/plugin/remark-agda.ts b/plugin/remark-agda.ts index e014761..f824894 100644 --- a/plugin/remark-agda.ts +++ b/plugin/remark-agda.ts @@ -33,6 +33,15 @@ const remarkAgda: RemarkPlugin = () => { {}, ); + // 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--") + // if (childOutput.status !== 0) + // throw new Error("Agda failed", childOutput.stderr) + const filename = parse(path).base.replace(/\.lagda.md/, ".md"); const htmlname = parse(path).base.replace(/\.lagda.md/, ".html"); const fullOutputPath = join(outDir, filename); diff --git a/scripts/upload-builder.sh b/scripts/upload-builder.sh new file mode 100755 index 0000000..bcb05a3 --- /dev/null +++ b/scripts/upload-builder.sh @@ -0,0 +1,12 @@ +#!/usr/bin/env bash + +set -euo pipefail + +nix build .#docker-builder +IMAGE_NAME=$(docker load -q -i ./result | cut -d':' -f2,3 | xargs) +REMOTE_IMAGE_NAME="git.mzhang.io/michael/$IMAGE_NAME" +docker image tag "$IMAGE_NAME" "$REMOTE_IMAGE_NAME" +docker push "$REMOTE_IMAGE_NAME" + +set -x +sed -i -E "s~(.*image: )blog-docker-builder:?.*~\1$REMOTE_IMAGE_NAME~" .woodpecker.yml diff --git a/utils/agda.Dockerfile b/utils/agda.Dockerfile deleted file mode 100644 index 88a6f98..0000000 --- a/utils/agda.Dockerfile +++ /dev/null @@ -1,23 +0,0 @@ -# FROM haskell:9-slim-buster -# RUN cabal update -# RUN cabal install --global Agda-2.6.4 -# -# FROM debian:buster-slim -# COPY --from=0 /root/.cabal/bin/agda /usr/bin/agda -# COPY --from=0 /root/.cabal/store/ghc-9.6.3/Agda-2.6.4-c592e701b6d172f37cf6e17790bc1993481dac7a9e29753b34c448a31924a9ab/share/lib /root/.cabal/store/ghc-9.6.3/Agda-2.6.4-c592e701b6d172f37cf6e17790bc1993481dac7a9e29753b34c448a31924a9ab/share/lib -# CMD ["agda", "--interactive"] - -FROM alpine AS base -ENV PATH /root/.local/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin -RUN apk add --update curl alpine-sdk ncurses-dev gmp-dev zlib-dev - -FROM base AS agda-build -RUN curl -sSL https://get.haskellstack.org/ | sh -RUN stack install ghc-9.4.7 -RUN git clone --depth 1 --single-branch --branch v2.6.4 https://github.com/agda/agda -WORKDIR /agda -RUN stack --stack-yaml stack-9.4.7.yaml install - -FROM base -COPY --from=agda-build /root/.local/bin/agda /usr/bin/agda -COPY --from=agda-build /agda/.stack-work/install/x86_64-linux-musl/099dc152e5f5edaf6e084b385953a851d037c26c20471a6eefaa57c4704a9540/9.4.7/share/x86_64-linux-ghc-9.4.7/Agda-2.6.4/lib /agda/.stack-work/install/x86_64-linux-musl/099dc152e5f5edaf6e084b385953a851d037c26c20471a6eefaa57c4704a9540/9.4.7/share/x86_64-linux-ghc-9.4.7/Agda-2.6.4/lib diff --git a/utils/builder.Dockerfile b/utils/builder.Dockerfile deleted file mode 100644 index 6d12c02..0000000 --- a/utils/builder.Dockerfile +++ /dev/null @@ -1,27 +0,0 @@ -FROM git.mzhang.io/michael/agda:2.6.4-x86_64 - -FROM node:18-alpine AS node -RUN apk add --update git -RUN npm install -g pnpm - -FROM node AS astro-build -WORKDIR /tmp -RUN git clone https://git.mzhang.io/michael/astro --depth 1 -WORKDIR /tmp/astro -RUN pnpm install -RUN pnpm run build -RUN rm -rf node_modules - - -FROM node -COPY --from=0 /usr/bin/agda /usr/bin/agda -COPY --from=0 /agda/.stack-work/install/x86_64-linux-musl/099dc152e5f5edaf6e084b385953a851d037c26c20471a6eefaa57c4704a9540/9.4.7/share/x86_64-linux-ghc-9.4.7/Agda-2.6.4/lib /agda/.stack-work/install/x86_64-linux-musl/099dc152e5f5edaf6e084b385953a851d037c26c20471a6eefaa57c4704a9540/9.4.7/share/x86_64-linux-ghc-9.4.7/Agda-2.6.4/lib - -COPY --from=astro-build /tmp/astro /tmp/astro -WORKDIR /tmp/astro/packages/astro -RUN pnpm link --global -WORKDIR /tmp/astro/packages/markdown/remark -RUN pnpm link --global - -WORKDIR / -