First commit

.github/workflows/github-pages.yml

@@ -0,0 +1,29 @@
+name: GitHub Pages
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+    branches: [main]
+
+jobs:
+  build:
+    name: Deploy
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v2
+      - uses: cachix/install-nix-action@v15
+      - uses: cachix/cachix-action@v10
+        with:
+          name: wolverian-agda-template
+          authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
+      - name: Build HTML
+        run: nix build --verbose --print-build-logs
+      - name: Copy HTML so the next step can read it
+        run: cp -vHR result html
+      - name: GitHub Pages
+        uses: crazy-max/[email protected]
+        with:
+          build_dir: html
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

.gitignore

@@ -0,0 +1,3 @@
+*.agdai
+/_build/
+/html/

Makefile

@@ -0,0 +1,55 @@
+SRC_DIR := src
+OUTPUT_DIR := html
+
+AGDA := agda
+AGDA_FLAGS := \
+	--html \
+	--html-highlight=auto \
+	--highlight-occurrences \
+	--html-dir=$(OUTPUT_DIR)
+
+PANDOC := pandoc
+PANDOC_FLAGS := \
+	--to=html5 \
+	--standalone \
+	--section-divs \
+	--katex \
+	--css=pandoc.css \
+	--css=style.css \
+	--include-in-header=header.html
+
+FONTS_SRC := $(wildcard fonts/*.otf)
+FONTS_DST := $(foreach font,$(FONTS_SRC),$(OUTPUT_DIR)/fonts/$(notdir $(font)))
+
+STYLES_SRC := $(wildcard styles/*.css)
+STYLES_DST := $(foreach style,$(STYLES_SRC),$(OUTPUT_DIR)/$(notdir $(style)))
+
+.PHONY: all
+all: \
+	$(OUTPUT_DIR)/index.html \
+	$(OUTPUT_DIR)/header.html \
+	$(OUTPUT_DIR)/UCC.html \
+	$(STYLES_DST) \
+	$(FONTS_DST)
+
+$(OUTPUT_DIR)/%.md: $(SRC_DIR)/%.lagda.md
+	$(AGDA) $(AGDA_FLAGS) $<
+
+$(OUTPUT_DIR)/%.html: $(OUTPUT_DIR)/%.md $(STYLES_DST) $(FONTS_DST)
+	$(PANDOC) $(PANDOC_FLAGS) -o $@ $<
+
+$(OUTPUT_DIR)/fonts/%.otf: fonts/%.otf
+	@mkdir -p $(OUTPUT_DIR)/fonts
+	cp $< $@
+
+$(OUTPUT_DIR)/%.css: styles/%.css
+	@mkdir -p $(OUTPUT_DIR)
+	cp $< $@
+
+$(OUTPUT_DIR)/header.html: header.html
+	@mkdir -p $(OUTPUT_DIR)
+	cp $< $@
+
+$(OUTPUT_DIR)/index.html: index.md
+	@mkdir -p $(OUTPUT_DIR)
+	$(PANDOC) $(PANDOC_FLAGS) -o $@ $<

README.md

@@ -0,0 +1,29 @@
+# Agda template
+
+## Prerequisites
+
+- Nix
+
+or
+
+- GNU `make`
+- Pandoc
+- Agda
+
+## Compile HTML
+
+Using Nix:
+
+```shellsession
+$ nix-build
+```
+
+Or, if you have the dependencies otherwise installed:
+
+```shellsession
+$ make all
+```
+
+## Continuous integration
+
+## License

agda-template.agda-lib

@@ -0,0 +1,2 @@
+depend: standard-library
+include: src

flake.nix

@@ -0,0 +1,38 @@
+{
+  inputs = {
+    nixpkgs.url = "github:nixos/nixpkgs";
+    flake-utils.url = "github:numtide/flake-utils";
+  };
+
+  outputs = { self, nixpkgs, flake-utils }:
+    flake-utils.lib.eachDefaultSystem (system:
+      let pkgs = nixpkgs.legacyPackages.${system};
+      in
+      rec {
+        defaultPackage = packages.wolverian-agda-template;
+        packages = {
+          wolverian-agda-template = pkgs.runCommand "wolverian-agda-template"
+            {
+              buildInputs = [
+                pkgs.gnumake
+                pkgs.pandoc
+                (pkgs.agda.withPackages (p: [ p.standard-library ]))
+              ];
+            }
+            ''
+              ln -s ${./fonts} fonts
+              ln -s ${./styles} styles
+              ln -s ${./index.md} index.md
+              ln -s ${./header.html} header.html
+              ln -s ${./Makefile} Makefile
+              ln -s ${./agda-template.agda-lib} agda-template.agda-lib
+              mkdir src && ln -s ${./src}/*.lagda.md src
+              ${pkgs.gnumake}/bin/make OUTPUT_DIR=$out
+            '';
+        };
+        checks = {
+          build = self.defaultPackage."${system}";
+        };
+      }
+    );
+}

header.html

@@ -0,0 +1 @@
+<script src="highlight-hover.js"></script>

src/AgdaTemplate.lagda.md

@@ -0,0 +1,5 @@
+# Agda template
+
+```
+data Example : Set where
+    Ok : Example

styles/pandoc.css

@@ -0,0 +1,164 @@
+html {
+  line-height: 1.5;
+  font-family: Georgia, serif;
+  font-size: 20px;
+  color: #1a1a1a;
+  background-color: #fdfdfd;
+}
+body {
+  margin: 0 auto;
+  max-width: 36em;
+  padding-left: 50px;
+  padding-right: 50px;
+  padding-top: 50px;
+  padding-bottom: 50px;
+  hyphens: auto;
+  overflow-wrap: break-word;
+  text-rendering: optimizeLegibility;
+  font-kerning: normal;
+}
+@media (max-width: 600px) {
+  body {
+    font-size: 0.9em;
+    padding: 1em;
+  }
+}
+@media print {
+  body {
+    background-color: transparent;
+    color: black;
+    font-size: 12pt;
+  }
+  p,
+  h2,
+  h3 {
+    orphans: 3;
+    widows: 3;
+  }
+  h2,
+  h3,
+  h4 {
+    page-break-after: avoid;
+  }
+}
+p {
+  margin: 1em 0;
+}
+a {
+  color: #1a1a1a;
+}
+a:visited {
+  color: #1a1a1a;
+}
+img {
+  max-width: 100%;
+}
+h1,
+h2,
+h3,
+h4,
+h5,
+h6 {
+  margin-top: 1.4em;
+}
+h5,
+h6 {
+  font-size: 1em;
+  font-style: italic;
+}
+h6 {
+  font-weight: normal;
+}
+ol,
+ul {
+  padding-left: 1.7em;
+  margin-top: 1em;
+}
+li > ol,
+li > ul {
+  margin-top: 0;
+}
+blockquote {
+  margin: 1em 0 1em 1.7em;
+  padding-left: 1em;
+  border-left: 2px solid #e6e6e6;
+  color: #606060;
+}
+code {
+  font-family: Menlo, Monaco, "Lucida Console", Consolas, monospace;
+  font-size: 85%;
+  margin: 0;
+}
+pre {
+  margin: 1em 0;
+  overflow: auto;
+}
+pre code {
+  padding: 0;
+  overflow: visible;
+  overflow-wrap: normal;
+}
+.sourceCode {
+  background-color: transparent;
+  overflow: visible;
+}
+hr {
+  background-color: #1a1a1a;
+  border: none;
+  height: 1px;
+  margin: 1em 0;
+}
+table {
+  margin: 1em 0;
+  border-collapse: collapse;
+  width: 100%;
+  overflow-x: auto;
+  display: block;
+  font-variant-numeric: lining-nums tabular-nums;
+}
+table caption {
+  margin-bottom: 0.75em;
+}
+tbody {
+  margin-top: 0.5em;
+  border-top: 1px solid #1a1a1a;
+  border-bottom: 1px solid #1a1a1a;
+}
+th {
+  border-top: 1px solid #1a1a1a;
+  padding: 0.25em 0.5em 0.25em 0.5em;
+}
+td {
+  padding: 0.125em 0.5em 0.25em 0.5em;
+}
+header {
+  margin-bottom: 4em;
+  text-align: center;
+}
+#TOC li {
+  list-style: none;
+}
+#TOC a:not(:hover) {
+  text-decoration: none;
+}
+code {
+  white-space: pre-wrap;
+}
+span.smallcaps {
+  font-variant: small-caps;
+}
+span.underline {
+  text-decoration: underline;
+}
+div.column {
+  display: inline-block;
+  vertical-align: top;
+  width: 50%;
+}
+div.hanging-indent {
+  margin-left: 1.5em;
+  text-indent: -1.5em;
+}
+ul.task-list {
+  list-style: none;
+}