From 05617fad8255248ee8ac8796e40a99529e1c8e8c Mon Sep 17 00:00:00 2001
From: Thomas Letan <lthms@soap.coffee>
Date: Sun, 23 Oct 2022 13:13:09 +0200
Subject: Website reorg

---
 site/posts/AlgebraicDatatypes.v                |   2 +-
 site/posts/ClightIntroduction.v                |   2 +-
 site/posts/Coqffi.org                          |   2 +-
 site/posts/DiscoveringCommonLisp.org           |   2 +-
 site/posts/ExtensibleTypeSafeErrorHandling.org |   2 +-
 site/posts/Ltac.org                            |   2 +-
 site/posts/RankNTypesInOCaml.org               |   2 +-
 site/posts/RewritingInCoq.v                    |   2 +-
 site/posts/StronglySpecifiedFunctions.org      |   2 +-
 site/posts/Thanks.org                          |   8 +-
 site/posts/cleopatra.org                       |  66 +++
 site/posts/cleopatra/commands.org              |  36 ++
 site/posts/cleopatra/coq.org                   |  47 ++
 site/posts/cleopatra/dependencies.org          |  95 ++++
 site/posts/cleopatra/literate-programming.org  |  82 +++
 site/posts/cleopatra/org.org                   | 144 +++++
 site/posts/cleopatra/soupault.org              | 702 +++++++++++++++++++++++++
 site/posts/cleopatra/theme.org                 | 573 ++++++++++++++++++++
 site/posts/coq.org                             |  44 ++
 site/posts/haskell.org                         |  13 +
 site/posts/index.org                           |  28 +
 site/posts/meta.org                            |  16 +
 site/posts/miscellaneous.org                   |  20 +
 23 files changed, 1877 insertions(+), 15 deletions(-)
 create mode 100644 site/posts/cleopatra.org
 create mode 100644 site/posts/cleopatra/commands.org
 create mode 100644 site/posts/cleopatra/coq.org
 create mode 100644 site/posts/cleopatra/dependencies.org
 create mode 100644 site/posts/cleopatra/literate-programming.org
 create mode 100644 site/posts/cleopatra/org.org
 create mode 100644 site/posts/cleopatra/soupault.org
 create mode 100644 site/posts/cleopatra/theme.org
 create mode 100644 site/posts/coq.org
 create mode 100644 site/posts/haskell.org
 create mode 100644 site/posts/index.org
 create mode 100644 site/posts/meta.org
 create mode 100644 site/posts/miscellaneous.org

(limited to 'site/posts')

diff --git a/site/posts/AlgebraicDatatypes.v b/site/posts/AlgebraicDatatypes.v
index f32551c..77ecc3c 100644
--- a/site/posts/AlgebraicDatatypes.v
+++ b/site/posts/AlgebraicDatatypes.v
@@ -1,4 +1,4 @@
-(** #<nav><p class="series">../coq.html</p>
+(** #<nav><p class="series">./coq.html</p>
      <p class="series-prev">./ClightIntroduction.html</p>
      <p class="series-next">./Coqffi.html</p></nav># *)
 
diff --git a/site/posts/ClightIntroduction.v b/site/posts/ClightIntroduction.v
index 85d084b..755d505 100644
--- a/site/posts/ClightIntroduction.v
+++ b/site/posts/ClightIntroduction.v
@@ -1,4 +1,4 @@
-(** #<nav><p class="series">../coq.html</p>
+(** #<nav><p class="series">./coq.html</p>
      <p class="series-prev">./RewritingInCoq.html</p>
      <p class="series-next">./AlgebraicDatatypes.html</p></nav># *)
 
diff --git a/site/posts/Coqffi.org b/site/posts/Coqffi.org
index f8d9695..6116612 100644
--- a/site/posts/Coqffi.org
+++ b/site/posts/Coqffi.org
@@ -1,6 +1,6 @@
 #+TITLE: A series on ~coqffi~
 
-#+SERIES: ../coq.html
+#+SERIES: ./coq.html
 #+SERIES_PREV: AlgebraicDatatypes.html
 
 ~coqffi~ generates Coq FFI modules from compiled OCaml interface
diff --git a/site/posts/DiscoveringCommonLisp.org b/site/posts/DiscoveringCommonLisp.org
index 307a315..f31f280 100644
--- a/site/posts/DiscoveringCommonLisp.org
+++ b/site/posts/DiscoveringCommonLisp.org
@@ -1,6 +1,6 @@
 #+TITLE: Discovering Common Lisp with ~trivial-gamekit~
 
-#+SERIES: ../miscellaneous.html
+#+SERIES: ./miscellaneous.html
 #+SERIES_NEXT: ./RankNTypesInOCaml.html
 
 #+BEGIN_EXPORT html
diff --git a/site/posts/ExtensibleTypeSafeErrorHandling.org b/site/posts/ExtensibleTypeSafeErrorHandling.org
index e817e31..67ad3b1 100644
--- a/site/posts/ExtensibleTypeSafeErrorHandling.org
+++ b/site/posts/ExtensibleTypeSafeErrorHandling.org
@@ -1,6 +1,6 @@
 #+TITLE: Extensible Type-Safe Error Handling in Haskell
 
-#+SERIES: ../haskell.html
+#+SERIES: ./haskell.html
 
 #+BEGIN_EXPORT html
 <p>This article has originally been published on <span
diff --git a/site/posts/Ltac.org b/site/posts/Ltac.org
index 37580cd..3dffb66 100644
--- a/site/posts/Ltac.org
+++ b/site/posts/Ltac.org
@@ -1,6 +1,6 @@
 #+TITLE: A Series on Ltac
 
-#+SERIES: ../coq.html
+#+SERIES: ./coq.html
 #+SERIES_PREV: ./StronglySpecifiedFunctions.html
 #+SERIES_NEXT: ./RewritingInCoq.html
 
diff --git a/site/posts/RankNTypesInOCaml.org b/site/posts/RankNTypesInOCaml.org
index fb21e4b..a8ffb3b 100644
--- a/site/posts/RankNTypesInOCaml.org
+++ b/site/posts/RankNTypesInOCaml.org
@@ -1,6 +1,6 @@
 #+TITLE: Writing a Function Whose Argument is a Polymorphic Function in OCaml
 
-#+SERIES: ../miscellaneous.html
+#+SERIES: ./miscellaneous.html
 #+SERIES_PREV: ./DiscoveringCommonLisp.html
 
 #+BEGIN_EXPORT html
diff --git a/site/posts/RewritingInCoq.v b/site/posts/RewritingInCoq.v
index a285e09..f58e9e0 100644
--- a/site/posts/RewritingInCoq.v
+++ b/site/posts/RewritingInCoq.v
@@ -1,4 +1,4 @@
-(** #<nav><p class="series">../coq.html</p>
+(** #<nav><p class="series">./coq.html</p>
      <p class="series-prev">./Ltac.html</p>
      <p class="series-next">./ClightIntroduction.html</p></nav># *)
 
diff --git a/site/posts/StronglySpecifiedFunctions.org b/site/posts/StronglySpecifiedFunctions.org
index 83148c6..4a608c7 100644
--- a/site/posts/StronglySpecifiedFunctions.org
+++ b/site/posts/StronglySpecifiedFunctions.org
@@ -1,6 +1,6 @@
 #+TITLE: A Series on Strongly-Specified Functions in Coq
 
-#+SERIES: ../coq.html
+#+SERIES: ./coq.html
 #+SERIES_NEXT: ./Ltac.html
 
 Using dependent types and the ~Prop~ sort, it becomes possible to specify
diff --git a/site/posts/Thanks.org b/site/posts/Thanks.org
index 22e2d57..ae23b7b 100644
--- a/site/posts/Thanks.org
+++ b/site/posts/Thanks.org
@@ -1,7 +1,7 @@
 #+TITLE: Thanks!
 
-#+SERIES: ../meta.html
-#+SERIES_NEXT: ../cleopatra.html
+#+SERIES: ./meta.html
+#+SERIES_NEXT: ./cleopatra.html
 
 This website could not exist without many awesome free software
 projects. Although I could not list them all even if I wanted, my
@@ -32,10 +32,6 @@ the most significant ones.
 - [[https://soupault.app][soupault]] ::
   Soupault is a static website generator and HTML processor written by [[https://www.baturin.org/][Daniil
   Baturin]].
-- [[https://cleopatra.soap.coffee][~cleopatra~]] ::
-  ~cleopatra~ is a generic, extensible toolchain with facilities for
-  literate programming projects using Org mode and more. I have
-  written it for this very website.
 
 * Frontend
 
diff --git a/site/posts/cleopatra.org b/site/posts/cleopatra.org
new file mode 100644
index 0000000..6081708
--- /dev/null
+++ b/site/posts/cleopatra.org
@@ -0,0 +1,66 @@
+#+TITLE: An Unfinished Series on How This Static Website Used to be Generated
+
+#+SERIES: ./meta.html
+#+SERIES_PREV: ./Thanks.html
+
+At some point, I felt like the whole process of generating this
+website was interesting enough so that it would deserve a write-up of
+its own, but the risk was that such a piece of text would quickly
+become out-dated. This is reminescent of documenting any software
+project, and I was aware at that time of a dedicated paradigm to
+prevent these kind of issues: [[http://www.literateprogramming.com/][literate programming]].
+
+I spent quite some time turning my custom toolchain into a literate
+program, so that its actual code source would actually be the
+write-ups I wanted to add to my website. This was an interesting
+challenge, since it meant *~cleopatra~* would have to generate itself
+before it could build my website. In other words, *~cleopatra~*
+achieves the bootstsrapping challenge!
+
+I really enjoyed this first experiment with literate programming, and
+I started using *~cleopatra~* for other projects of mine where
+literate programming felt like an interesting choice. In doing so, it
+quickly became clear *~cleopatra~* was cumbersome to set-up for a new
+project. At the end, [[https://cleopatra.soap.coffee][I ended up rewriting it]] to overcome the specific
+issues posed by its initial design[fn::For the record, this second
+version is also implemented using literate programming, and if I was
+first using the first version to build it, I quickly “made the
+bootstrap jump.”]. But the so-called generation processes I had
+written for *~cleopatra~* the first basically “just worked” with
+*~cleopatra~* the second.
+
+Now, I don’t use *~cleopatra~* anymore. Literate programming is a fun
+paradigm, but I never took the time to actually document in depth most
+of the bits on how this website is built. So I took the various
+scripts extracted by *~cleopatra~*, and recreated a straightforward
+~makefile~ file on top of it. The nice thing is, it now takes way less
+time to build!
+
+Anyway, coming back to this series, it is just the very reason why I
+started using *~cleopatra~* in the first place: the generation
+processes I was using to generate this website, written as literate
+programs. If you are curious, you can have a look.
+
+- [[./cleopatra/dependencies.org][Installing Dependencies]] ::
+
+- [[file:cleopatra/coq.org][Authoring Contents with Coq ~(TODO)~]] ::
+
+- [[./cleopatra/org.org][Authoring Contents with ~org-mode~ ~(TODO)~]] ::
+
+- [[./cleopatra/literate-programming.org][Literate Programming Projects]] ::
+  Literate programming is an interesting exercice, and it is
+  particularly well-suited for blog posts, since at the very least it
+  provides the tool to enforce the code presented to readers is
+  correct. We use Emacs and ~org-mode~ to tangle the literate
+  programming projects present in the ~posts/~ directory of this
+  website.
+
+- [[./cleopatra/theme.org][Layout and Style]] ::
+
+- [[./cleopatra/soupault.org][Processing HTML with ~soupault~]] ::
+  ~soupault~ is a HTML processor, and it can be used as a static website
+  generator. We leverage *~soupault~* to provide a unified look and feel to a
+  website generated with diverse tools.
+
+*Appendix:* In case you are curious, you can have a look at
+[[./posts/CleopatraV1.html][the first implementaiton of *~cleopatra~*]].
diff --git a/site/posts/cleopatra/commands.org b/site/posts/cleopatra/commands.org
new file mode 100644
index 0000000..fbf0430
--- /dev/null
+++ b/site/posts/cleopatra/commands.org
@@ -0,0 +1,36 @@
+#+TITLE: Adhoc *~cleopatra~* commands
+
+#+SERIES: ../cleopatra.html
+#+SERIES_PREV: ./soupault.html
+
+In this generation process, we provide adhoc commands to ease the
+authoring experience.  A given command ~<cmd>~ is implemented as a
+~makefile~ rule, and can be called with ~cleopatra <cmd>~.
+
+#+BEGIN_EXPORT html
+<nav id="generate-toc"></nav>
+<div id="history">site/cleopatra/commands.org</div>
+#+END_EXPORT
+
+* ~serve~
+
+  This command spawns a simple HTTP server which allows us to navigate
+  the website more easily.
+
+  #+begin_src makefile :tangle commands.mk
+serve :
+	@cleopatra echo Spwaning "HTTP server"
+	@cd out && python -m http.server
+  #+end_src
+
+* ~update~
+
+  This commands updates the various dependencies locally installed to
+  build this website, such as ~soupault~ for instance.
+
+  #+begin_src makefile :tangle commands.mk
+update :
+	@cleopatra echo "Updating" "OCaml dependencies"
+	@opam update
+	@opam upgrade -y
+  #+end_src
diff --git a/site/posts/cleopatra/coq.org b/site/posts/cleopatra/coq.org
new file mode 100644
index 0000000..81f3d27
--- /dev/null
+++ b/site/posts/cleopatra/coq.org
@@ -0,0 +1,47 @@
+#+TITLE: Authoring Content with Coq
+
+#+SERIES: ../cleopatra.html
+#+SERIES_PREV: ./dependencies.html
+#+SERIES_NEXT: ./org.html
+
+#+BEGIN_EXPORT html
+<nav id="generate-toc"></nav>
+<div id="history">site/cleopatra/coq.org</div>
+#+END_EXPORT
+
+
+* Author Guidelines
+
+* Under the Hood
+
+#+BEGIN_SRC makefile :tangle coq.mk
+COQ_POSTS := $(shell find site/ -name "*.v")
+COQ_HTML := $(COQ_POSTS:.v=.html)
+COQ_ARTIFACTS := $(COQ_POSTS:.v=.vo) \
+  $(COQ_POSTS:.v=.vok) \
+  $(COQ_POSTS:.v=.vos) \
+  $(COQ_POSTS:.v=.glob) \
+  $(join $(dir ${COQ_POSTS}),$(addprefix ".",$(notdir $(COQ_POSTS:.v=.aux))))
+
+coq-build : ${COQ_HTML}
+
+soupault-build : coq-build
+
+ARTIFACTS += ${COQ_ARTIFACTS} .lia.cache
+ARTIFACTS += ${COQ_HTML}
+
+COQLIB := "https://coq.inria.fr/distrib/current/stdlib/"
+COQCARG := -async-proofs-cache force \
+           -w -custom-entry-overriden
+COQDOCARG := --no-index --charset utf8 --short \
+             --body-only --coqlib "${COQLIB}" \
+             --external "https://coq-community.org/coq-ext-lib/v0.11.2/" ExtLib \
+             --external "https://compcert.org/doc/html" compcert \
+             --external "https://lysxia.github.io/coq-simple-io" SimpleIO
+
+%.html : %.v coq.mk _opam/init
+	@cleopatra echo Exporting  "$*.v"
+	@coqc ${COQCARG} $<
+	@coqdoc ${COQDOCARG} -d $(shell dirname $<) $<
+	@rm -f $(shell dirname $<)/coqdoc.css
+#+END_SRC
diff --git a/site/posts/cleopatra/dependencies.org b/site/posts/cleopatra/dependencies.org
new file mode 100644
index 0000000..7858df4
--- /dev/null
+++ b/site/posts/cleopatra/dependencies.org
@@ -0,0 +1,95 @@
+#+TITLE: Installing Dependencies
+
+#+SERIES: ../cleopatra.html
+#+SERIES_NEXT: ./coq.html
+
+* OCaml and Coq
+
+  #+caption: Dependencies for Coq articles
+  #+name: coq-deps
+  | Package      | Version |
+  |--------------+---------|
+  | coq          |  8.13.2 |
+  | coq-compcert |     3.8 |
+
+  #+caption: Dependencies for the ~coqffi~ series
+  #+name: lp-deps
+  | Package       |     Version |
+  |---------------+-------------|
+  | dune          |       2.9.0 |
+  | coq-coqffi    | 1.0.0~beta7 |
+  | coq-simple-io |       1.5.0 |
+
+  #+caption: Soupault
+  #+name: soupault-deps
+  | Package  | Version |
+  |----------+---------|
+  | soupault |   4.0.1 |
+
+  #+name: deps-listing
+  #+begin_src emacs-lisp :noweb yes :var coq-deps=coq-deps :var lp-deps=lp-deps :var soupault-deps=soupault-deps :results value raw :exports none
+;; We use this Emacs Lisp snippet to generate the list of dependencies
+;; we have to install with Opam
+(defun fmt-deps (d)
+  (mapconcat (lambda (d) (format "%s" d)) d "."))
+
+(string-join
+ (append (mapcar 'fmt-deps lp-deps)
+         (mapcar 'fmt-deps soupault-deps)
+         (mapcar 'fmt-deps coq-deps))
+ " ")
+  #+end_src
+
+  #+begin_src makefile :tangle dependencies.mk :noweb yes
+OCAML_VERSION := 4.12.0
+OCAML := ocaml-base-compiler.${OCAML_VERSION}
+
+_opam/init :
+	@cleopatra echo "Creating" "a local Opam switch"
+	@opam switch create . ${OCAML} --repos default,coq-released || true
+	@cleopatra echo "Installing" "OCaml dependencies"
+	@opam install <<deps-listing()>> -y
+	@touch $@
+
+CONFIGURE += _opam
+  #+end_src
+
+* Frontend
+
+  #+caption: Frontend dependencies
+  #+name: frontend-deps
+  | Package       | Version |
+  |---------------+---------|
+  | katex         | 0.13.13 |
+  | minify        |   7.0.2 |
+  | normalize.css |   8.0.1 |
+
+  #+name: frontend-listing
+  #+begin_src emacs-lisp :var frontend-deps=frontend-deps :exports none
+;; We use this Emacs Lisp snippet to generate the list of dependencies
+;; we have to install with npm
+(defun fmt-deps (d)
+  (format "  \"%s\": \"^%s\"" (nth 0 d) (nth 1 d)))
+
+(string-join (mapcar 'fmt-deps frontend-deps) ",\n")
+  #+end_src
+
+  #+begin_src json :tangle package.json :noweb yes
+{
+  "dependencies": {
+    <<frontend-listing()>>
+  }
+}
+  #+end_src
+
+  #+begin_src makefile :tangle dependencies.mk :noweb yes
+package-lock.json : package.json
+	@cleopatra echo "Installing" "frontend dependencies"
+	@npm install
+
+CONFIGURE += package-lock.json
+  #+end_src
+
+  #+begin_src makefile :tangle dependencies.mk :noweb yes
+dependencies-prebuild : _opam/init package-lock.json
+  #+end_src
diff --git a/site/posts/cleopatra/literate-programming.org b/site/posts/cleopatra/literate-programming.org
new file mode 100644
index 0000000..63e0b02
--- /dev/null
+++ b/site/posts/cleopatra/literate-programming.org
@@ -0,0 +1,82 @@
+#+TITLE: Literate Programming Projects
+
+#+SERIES: ../cleopatra.html
+#+SERIES_PREV: ./org.html
+#+SERIES_NEXT: ./theme.html
+
+Literate programming is an interesting exercice. It forces programmers
+to think about how to present their code for other people to
+understand it. It poses several significant challenges, in particular
+in terms of code refactoring. If a given piece of code is too much
+entangled with proses explaining it, rewriting it becomes cumbersome.
+
+That being said, literate programming is particularly well-suited for
+blog posts, since at the very least it provides the tool to enforce
+the code presented to readers is correct.
+
+#+BEGIN_EXPORT html
+<nav id="generate-toc"></nav>
+<div id="history">site/cleopatra/literate-programming.org</div>
+#+END_EXPORT
+
+* Tangling
+
+We use Emacs and ~org-mode~ to tangle the literate programming
+projects present in the ~posts/~ directory of this website. This is
+done with the following emacs lisp script.
+
+#+BEGIN_SRC emacs-lisp :tangle export-lp.el
+;; opinionated configuration provided by cleopatra
+(cleopatra:configure)
+
+;; allow the execution of shell block code
+(org-babel-do-load-languages
+ 'org-babel-load-languages
+ '((shell . t)))
+
+;; scan the posts/ directory and tangled it into lp/
+(setq org-publish-project-alist
+      '(("lp"
+         :base-directory "site/posts"
+         :publishing-directory "lp"
+         :recursive t
+         :publishing-function cleopatra:tangle-publish)))
+
+(org-publish-all)
+#+END_SRC
+
+Tangling literate programming is done in the =prebuild= phase of
+*~cleopatra~*.
+
+#+BEGIN_SRC makefile :tangle literate-programming.mk
+literate-programming-prebuild :
+	@cleopatra echo "Tangling" "literate programming project"
+	@cleopatra exec -- cleopatra-run-elisp export-lp.el \
+	    >> build.log 2>&1
+
+ARTIFACTS += lp/ site/posts/deps.svg
+#+END_SRC
+
+* Building
+
+In the =build= phase, we actually try to compile the tangled projects.
+As of now, there is only one literate program: [[../posts/CoqffiEcho.org][the Echo server
+implemented in Coq]] which demonstrates how ~coqffi~ can be used to
+implement realistic software projects.
+
+#+BEGIN_SRC makefile :tangle literate-programming.mk
+COQFFI_ARCHIVE := site/files/coqffi-tutorial.tar.gz
+
+coqffi-tutorial-build : literate-programming-prebuild _opam/init
+	@cleopatra echo "Building" "coqffi tutorial"
+	@cd lp/coqffi-tutorial; dune build --display quiet
+	@cleopatra echo "Archiving" "coqffi tutorial"
+	@rm -f ${COQFFI_ARCHIVE}
+	@tar --exclude="_build" -C lp/ -czvf ${COQFFI_ARCHIVE} coqffi-tutorial \
+	      2>&1 >> build.log
+
+site/posts/CoqffiEcho.html : coqffi-tutorial-build
+literate-programming-build : coqffi-tutorial-build
+
+ARTIFACTS += ${COQFFI_ARCHIVE}
+#+END_SRC
diff --git a/site/posts/cleopatra/org.org b/site/posts/cleopatra/org.org
new file mode 100644
index 0000000..9f5a77c
--- /dev/null
+++ b/site/posts/cleopatra/org.org
@@ -0,0 +1,144 @@
+#+TITLE: Authoring Content with ~org-mode~
+
+#+SERIES: ../cleopatra.html
+#+SERIES_PREV: ./coq.html
+#+SERIES_NEXT: ./literate-programming.html
+
+#+BEGIN_EXPORT html
+<nav id="generate-toc"></nav>
+<div id="history">site/cleopatra/org.org</div>
+#+END_EXPORT
+
+* Author Guidelines
+
+* Implementation
+
+#+begin_src makefile :tangle org.mk
+EMACS := cleopatra-emacs
+
+ORG_IN := $(shell find site/ -name "*.org")
+ORG_OUT := $(ORG_IN:.org=.html)
+
+org-prebuild : .emacs
+org-build : ${ORG_OUT}
+
+soupault-build : org-build
+
+ARTIFACTS += ${ORG_OUT}
+CONFIGURE += .emacs
+
+EXPORT := --batch \
+          --load="${ROOT}/scripts/packages.el" \
+          --load="${ROOT}/scripts/export-org.el" \
+          2>> build.log
+
+INIT := --batch --load="${ROOT}/scripts/packages.el" \
+        2>> build.log
+
+.emacs : scripts/packages.el
+	@cleopatra echo Initiating  "Emacs configuration"
+	@${EMACS} ${INIT}
+	@touch .emacs
+
+%.html : %.org scripts/packages.el scripts/export-org.el \
+         .emacs org.mk
+	@cleopatra echo Exporting "$*.org"
+	@${EMACS} $< ${EXPORT}
+#+end_src
+
+#+begin_src emacs-lisp :tangle scripts/packages.el
+(use-package ox-tufte :ensure t)
+#+end_src
+
+We also use the OCaml backend for ~org-babel~ to ensure our OCaml
+snippets are well-typed, among other things.
+
+#+begin_src emacs-lisp :tangle scripts/packages.el
+(use-package tuareg :ensure t
+  :config
+  (require 'ob-ocaml))
+#+end_src
+
+#+begin_src emacs-lisp :tangle scripts/export-org.el
+(cleopatra:configure)
+
+(org-babel-do-load-languages
+ 'org-babel-load-languages
+ '((dot . t)
+   (shell . t)
+   (ocaml . t)))
+
+(setq org-export-with-toc nil
+      org-html-htmlize-output-type nil
+      org-export-with-section-numbers nil)
+
+(add-to-list 'org-entities-user
+             '("im" "\\(" nil "<span class=\"imath\">" "" "" ""))
+(add-to-list 'org-entities-user
+             '("mi" "\\)" nil "</span>" "" "" ""))
+
+(defun with-keyword (keyword k)
+  "Look-up for keyword KEYWORD, and call continuation K with its value."
+  (pcase (org-collect-keywords `(,keyword))
+    (`((,keyword . ,kw))
+     (when kw (funcall k (string-join kw " "))))))
+
+(defun get-keyword (keyword)
+  "Look-up for keyword KEYWORD, and returns its value"
+  (with-keyword keyword (lambda (x) x)))
+
+(defun get-org-title (path)
+  "Fetch the title of an Org file whose path is PATH."
+  (with-temp-buffer
+    (find-file-read-only path)
+    (get-keyword "TITLE")))
+
+(defun insert-title ()
+  "Insert the title of the article."
+  (with-keyword
+   "TITLE"
+   (lambda (title)
+     (insert
+      (format "\n\n@@html:<h1>@@ %s @@html:</h1>@@\n\n" title)))))
+
+(defun insert-series ()
+  "Insert the series root link."
+  (with-keyword
+   "SERIES"
+   (lambda (series)
+     (insert "\n\n#+attr_html: :class series\n")
+     (insert series))))
+
+(defun insert-series-prev ()
+  "Insert the series previous article link."
+  (with-keyword
+   "SERIES_PREV"
+   (lambda (series-prev)
+     (insert "\n\n#+attr_html: :class series-prev\n")
+     (insert series-prev))))
+
+(defun insert-series-next ()
+  "Insert the series next article link."
+  (with-keyword
+   "SERIES_NEXT"
+   (lambda (series-next)
+     (insert "\n\n#+attr_html: :class series-next\n")
+     (insert series-next))))
+
+(defun insert-nav ()
+  "Insert the navigation links."
+  (when (get-keyword "SERIES")
+    (insert "\n\n#+begin_nav\n")
+    (insert-series)
+    (insert-series-prev)
+    (insert-series-next)
+    (insert "\n\n#+end_nav\n")))
+
+(beginning-of-buffer)
+(insert-nav)
+(insert-title)
+
+(let ((outfile (org-export-output-file-name ".html"))
+      (org-html-footnotes-section "<!-- %s --><!-- %s -->"))
+  (org-export-to-file 'tufte-html outfile nil nil nil t))
+#+end_src
diff --git a/site/posts/cleopatra/soupault.org b/site/posts/cleopatra/soupault.org
new file mode 100644
index 0000000..3fdb8d6
--- /dev/null
+++ b/site/posts/cleopatra/soupault.org
@@ -0,0 +1,702 @@
+#+TITLE: ~soupault~
+
+#+SERIES: ../cleopatra.html
+#+SERIES_PREV: ./theme.html
+#+SERIES_NEXT: ./commands.html
+
+We use ~soupault~ to build this website[fn::~soupault~ is an awesome
+free software project, with a unique approach to static website
+generation. You should definitely [[https://soupault.app][check out their website]]!].
+
+#+begin_export html
+<nav id="generate-toc"></nav>
+#+end_export
+
+* Installation
+
+  We install ~soupault~ in a local switch. We use a witness file
+  ~_opam/.init~ to determine whether or not our switch has always been
+  created during a previous invocation of *~cleopatra~*.
+
+  #+begin_src makefile :tangle soupault.mk
+CONFIGURE += _opam rss.json
+ARTIFACTS += out
+
+soupault-prebuild : _opam/init
+  #+end_src
+
+  Using ~soupault~ is as simple as calling it, without any particular
+  command-line arguments.
+
+  #+begin_src makefile :tangle soupault.mk
+soupault-build : dependencies-prebuild style.min.css
+	@cleopatra echo "Executing" "soupault"
+	@soupault
+  #+end_src
+
+  We now describe our configuration file for ~soupault~.
+
+* Configuration
+
+  #+name: base-dir
+  #+begin_src verbatim :noweb yes :exports none
+~lthms
+  #+end_src
+
+** Global Settings
+
+   The options of the ~[settings]~ section of a ~soupault~
+   configuration are often self-explanatory, and we do not spend too
+   much time to detaul them.
+
+   #+begin_src toml :tangle soupault.conf :noweb yes
+[settings]
+strict = true
+site_dir = "site"
+build_dir = "out/<<base-dir>>"
+doctype = "<!DOCTYPE html>"
+clean_urls = false
+generator_mode = true
+complete_page_selector = "html"
+default_content_selector = "main"
+default_content_action = "append_child"
+page_file_extensions = ["html"]
+ignore_extensions = [
+  "v", "vo", "vok", "vos", "glob",
+  "html~", "org"
+]
+default_template_file = "templates/main.html"
+pretty_print_html = false
+   #+end_src
+
+** Setting Page Title
+
+   We use the “page title” widget to set the title of the webpage
+   based on the first (and hopefully the only) ~<h1>~ tag of the
+   page.
+
+   #+begin_src toml :tangle soupault.conf
+[widgets.page-title]
+widget = "title"
+selector = "h1"
+default = "~lthms"
+prepend = "~lthms: "
+   #+end_src
+
+** Acknowledging ~soupault~
+
+   When creating a new ~soupault~ project (using ~soupault --init~),
+   the default configuration file suggests advertising the use of
+   ~soupault~. Rather than hard-coding the used version of ~soupault~
+   (which is error-prone), we rather determine the version of
+   ~soupault~ with the following script.
+
+   #+NAME: soupault-version
+   #+begin_src bash :results verbatim output
+soupault --version | head -n 1 | tr -d '\n'
+   #+end_src
+
+   The configuration of the widget ---initially provided by
+   ~soupault~--- becomes less subject to the obsolescence[fn::That
+   is, as long as ~soupault~ does not change the output of its
+   ~--version~ option.].
+
+   #+begin_src toml :tangle soupault.conf :noweb yes
+[widgets.generator-meta]
+widget = "insert_html"
+html = """<meta name="generator" content="<<soupault-version()>>">"""
+selector = "head"
+   #+end_src
+
+** Prefixing Internal URLs
+
+   On the one hand, internal links can be absolute, meaning they
+   start with a leading ~/~, and therefore are relative to the
+   website root. On the other hand, website (especially static
+   website) can be placed in larger context. For instance, my
+   personal website lives inside the ~~lthms~ directory of the
+   ~soap.coffee~ domain[fn::To my experience in hosting webapps and
+   websites, this set-up is way harder to get right than I initially
+   expect.].
+
+   The purpose of this plugin is to rewrite internal URLs which are relative to the
+   root, in order to properly prefix them.
+
+   From a high-level perspective, the plugin structure is the following.
+
+   First, we validate the widget configuration.
+
+   #+BEGIN_SRC lua :tangle plugins/urls-rewriting.lua
+prefix_url = config["prefix_url"]
+
+if not prefix_url then
+  Plugin.fail("Missing mandatory field: `prefix_url'")
+end
+
+if not Regex.match(prefix_url, "^/(.*)") then
+  prefix_url = "/" .. prefix_url
+end
+
+if not Regex.match(prefix_url, "(.*)/$") then
+  prefix_url = prefix_url .. "/"
+end
+   #+END_SRC
+
+   Then, we propose a generic function to enumerate and rewrite tags
+   which can have.
+
+   #+BEGIN_SRC lua :tangle plugins/urls-rewriting.lua
+function prefix_urls (links, attr, prefix_url)
+  index, link = next(links)
+
+  while index do
+    href = HTML.get_attribute(link, attr)
+
+    if href then
+      if Regex.match(href, "^/") then
+        href = Regex.replace(href, "^/*", "")
+        href = prefix_url .. href
+      end
+
+      HTML.set_attribute(link, attr, href)
+    end
+    index, link = next(links, index)
+  end
+end
+   #+END_SRC
+
+   Finally, we use this generic function for relevant tags.
+
+   #+BEGIN_SRC lua  :tangle plugins/urls-rewriting.lua
+prefix_urls(HTML.select(page, "a"), "href", prefix_url)
+prefix_urls(HTML.select(page, "link"), "href", prefix_url)
+prefix_urls(HTML.select(page, "img"), "src", prefix_url)
+prefix_urls(HTML.select(page, "script"), "src", prefix_url)
+prefix_urls(HTML.select(page, "use"), "href", prefix_url)
+   #+END_SRC
+
+   Again, configuring soupault to use this plugin is relatively
+   straightforward.
+
+   #+BEGIN_SRC toml :tangle soupault.conf :noweb yes
+[widgets.urls-rewriting]
+widget = "urls-rewriting"
+prefix_url = "<<base-dir>>"
+after = "mark-external-urls"
+   #+END_SRC
+
+** Marking External Links
+
+   #+BEGIN_SRC lua :tangle plugins/external-urls.lua
+function mark(name)
+  return '<span class="icon"><svg><use href="/img/icons.svg#'
+         .. name ..
+         '"></use></svg></span>'
+end
+
+links = HTML.select(page, "a")
+
+index, link = next(links)
+
+while index do
+  href = HTML.get_attribute(link, "href")
+
+  if href then
+    if Regex.match(href, "^https?://github.com") then
+      icon = HTML.parse(mark("github"))
+      HTML.append_child(link, icon)
+    elseif Regex.match(href, "^https?://") then
+      icon = HTML.parse(mark("external-link"))
+      HTML.append_child(link, icon)
+    end
+  end
+
+  index, link = next(links, index)
+end
+   #+END_SRC
+
+   #+BEGIN_SRC toml :tangle soupault.conf
+[widgets.mark-external-urls]
+after = "generate-history"
+widget = "external-urls"
+   #+END_SRC
+
+** Generating a Table of Contents
+
+   The ~toc~ widget allows for generating a table of contents for
+   HTML files which contains a node matching a given ~selector~ (in
+   the case of this document, ~#generate-toc~).
+
+   #+begin_src toml :tangle soupault.conf
+[widgets.table-of-contents]
+widget = "toc"
+selector = "#generate-toc"
+action = "replace_content"
+valid_html = true
+min_level = 2
+max_level = 3
+numbered_list = false
+heading_links = true
+heading_link_text = " §"
+heading_links_append = true
+heading_link_class = "anchor-link"
+
+[widgets.append-toc-title]
+widget = "insert_html"
+selector = "#generate-toc"
+action = "prepend_child"
+html = '<h2>Table of Contents</h2>'
+after = "table-of-contents"
+   #+end_src
+
+** Generating Per-File Revisions Tables
+
+*** Users Instructions
+
+    This widgets allows to generate a so-called “revisions table” of
+    the filename contained in a DOM element of id ~history~, based on
+    its history. Paths should be relative to the directory from which
+    you start the build process (typically, the root of your
+    repository). The revisions table notably provides hyperlinks to a
+    ~git~ webview for each commit.
+
+    For instance, considering the following HTML snippet
+
+    #+begin_src html
+<div id="history">
+  site/posts/FooBar.org
+</div>
+    #+end_src
+
+    This plugin will replace the content of this ~<div>~ with the
+    revisions table of ~site/posts/FooBar.org~.
+
+*** Customization
+
+    The base of the URL webview for the document you are currently
+    reading is src_verbatim[:noweb yes :exports code]{<<repo>>}.
+
+    #+name: repo
+    #+begin_src verbatim :exports none
+https://src.soap.coffee/soap.coffee/lthms.git
+    #+end_src
+
+    The template used to generate the revision table is the following.
+
+    #+begin_src html :tangle templates/history.html :noweb yes
+<details id="history">
+  <summary>Revisions</summary>
+  <p>
+    This revisions table has been automatically generated
+    from <a href="<<repo>>">the
+    <code>git</code> history of this website repository</a>, and the
+    change descriptions may not always be as useful as they should.
+  </p>
+
+  <p>
+    You can consult the source of this file in its current version
+    <a href="<<repo>>/tree/{{file}}">here</a>.
+  </p>
+
+  <table class="fullwidth">
+  {{#history}}
+  <tr>
+    <td class="date"
+{{#created}}
+        id="created-at"
+{{/created}}
+{{#modified}}
+        id="modified-at"
+{{/modified}}
+        >{{date}}</td>
+    <td class="subject">{{subject}}</td>
+    <td class="commit">
+      <a href="<<repo>>/commit/{{filename}}/?id={{hash}}">{{abbr_hash}}</a>
+    </td>
+  </tr>
+  {{/history}}
+  </table>
+</details>
+    #+end_src
+
+*** Implementation
+
+    We use the built-in [[https://soupault.neocities.org/reference-manual/#widgets-preprocess-element][=preprocess_element=]] to implement, which
+    means we need a script which gets its input from the standard
+    input, and echoes its output to the standard input.
+
+    #+begin_src toml :tangle soupault.conf
+[widgets.generate-history]
+widget = "preprocess_element"
+selector = "#history"
+command = 'scripts/history.sh templates/history.html'
+action = "replace_element"
+    #+end_src
+
+    This plugin proceeds as follows:
+
+    1. Using an ad-hoc script, it generates a JSON containing for each revision
+       - The subject, date, hash, and abbreviated hash of the related commit
+       - The name of the file at the time of this commit
+    2. This JSON is passed to a mustache engine (~haskell-mustache~) with a
+       proper template
+    3. The content of the selected DOM element is replaced with the output of
+       ~haskell-mustache~
+
+    This translates in Bash like this.
+
+    #+begin_src bash :tangle scripts/history.sh :shebang "#!/usr/bin/bash"
+function main () {
+  local file="${1}"
+  local template="${2}"
+
+  tmp_file=$(mktemp)
+  generate_json ${file} > ${tmp_file}
+  haskell-mustache ${template} ${tmp_file}
+  rm ${tmp_file}
+}
+    #+end_src
+
+    Generating the expected JSON is therefore as simple as:
+
+    - Fetching the logs
+    - Reading 8 line from the logs, parse the filename from the 6th
+      line
+    - Outputing the JSON
+
+    We will use ~git~ to get the information we need. By default,
+    ~git~ subcommands use a pager when its output is likely to be
+    long. This typically includes ~git-log~. To disable this
+    behavior, ~git~ exposes the ~--no-pager~ command.  Besides, we
+    also need ~--follow~ and ~--stat~ to deal with file
+    renaming. Without this option, ~git-log~ stops when the file
+    first appears in the repository, even if this “creation” is
+    actually a renaming. Therefore, the ~git~ command line we use to
+    collect our history is
+
+    #+name: gitlog
+    #+begin_src bash :tangle scripts/history.sh :noweb yes
+function gitlog () {
+  local file="${1}"
+  git --no-pager log \
+      --follow \
+      --stat=10000 \
+      --pretty=format:'%s%n%h%n%H%n%cs%n' \
+      "${file}"
+}
+    #+end_src
+
+    This function will generate a sequence of 8 lines containing all
+    the relevant information we are looking for, for each commit,
+    namely:
+
+    - Subject
+    - Abbreviated hash
+    - Full hash
+    - Date
+    - Empty line
+    - Change summary
+    - Shortlog
+    - Empty line
+
+    For instance, the =gitlog= function will output the following
+    lines for the last commit of this very file:
+
+    #+begin_src bash :results verbatim :exports results :noweb yes
+<<gitlog>>
+gitlog "soupault.org" | head -n8
+    #+end_src
+
+    Among other things, the 6th line contains the filename. We need
+    to extract it, and we do that with ~sed~. In case of file
+    renaming, we need to parse something of the form ~both/to/{old =>
+    new}~.
+
+    #+begin_src bash :tangle scripts/history.sh :noweb yes
+function parse_filename () {
+  local line="${1}"
+  local shrink='s/ *\(.*\) \+|.*/\1/'
+  local unfold='s/\(.*\){\(.*\) => \(.*\)}/\1\3/'
+
+  echo ${line} | sed -e "${shrink}" | sed -e "${unfold}"
+}
+    #+end_src
+
+    The next step is to process the logs to generate the expected
+    JSON. We have to deal with the fact that JSON does not allow the
+    last item of an array to be concluded by ",". Besides, we also
+    want to indicate which commit is responsible for the creation of
+    the file.  To do that, we use two variables: =idx= and
+    =last_entry=. When =idx= is equal to 0, we know it is the latest
+    commit. When =idx= is equal to =last_entry=, we know we are
+    looking at the oldest commit for that file.
+
+    #+begin_src bash :tangle scripts/history.sh :noweb yes
+function generate_json () {
+  local input="${1}"
+  local logs="$(gitlog ${input})"
+
+  if [ ! $? -eq 0 ]; then
+      exit 1
+  fi
+
+  let "idx=0"
+  let "last_entry=$(echo "${logs}" | wc -l) / 8"
+
+  local subject=""
+  local abbr_hash=""
+  local hash=""
+  local date=""
+  local file=""
+  local created="true"
+  local modified="false"
+
+  echo -n "{"
+  echo -n "\"file\": \"${input}\""
+  echo -n ",\"history\": ["
+
+  while read -r subject; do
+    read -r abbr_hash
+    read -r hash
+    read -r date
+    read -r # empty line
+    read -r file
+    read -r # short log
+    read -r # empty line
+
+    if [ ${idx} -ne 0 ]; then
+      echo -n ","
+    fi
+
+    if [ ${idx} -eq ${last_entry} ]; then
+      created="true"
+      modified="false"
+    else
+      created="false"
+      modified="true"
+    fi
+
+    output_json_entry "${subject}" \
+                      "${abbr_hash}" \
+                      "${hash}" \
+                      "${date}" \
+                      "$(parse_filename "${file}")" \
+                      "${created}" \
+                      "${modified}"
+
+    let idx++
+  done < <(echo "${logs}")
+
+  echo -n "]}"
+}
+    #+end_src
+
+    Generating the JSON object for a given commit is as simple as
+
+    #+begin_src bash :tangle scripts/history.sh :noweb yes
+function output_json_entry () {
+  local subject="${1}"
+  local abbr_hash="${2}"
+  local hash="${3}"
+  local date="${4}"
+  local file="${5}"
+  local created="${6}"
+  local last_entry="${7}"
+
+  echo -n "{\"subject\": \"${subject}\""
+  echo -n ",\"created\":${created}"
+  echo -n ",\"modified\":${modified}"
+  echo -n ",\"abbr_hash\":\"${abbr_hash}\""
+  echo -n ",\"hash\":\"${hash}\""
+  echo -n ",\"date\":\"${date}\""
+  echo -n ",\"filename\":\"${file}\""
+  echo -n "}"
+}
+    #+end_src
+
+    And we are done! We can safely call the =main= function to generate
+    our revisions table.
+
+    #+begin_src bash :tangle scripts/history.sh
+main "$(cat)" "${1}"
+    #+end_src
+
+** Rendering Equations Offline
+   :PROPERTIES:
+   :CUSTOM_ID: katex
+   :END:
+
+*** Users instructions
+
+    Inline equations written in the DOM under the class
+    src_css{.imath} and using the \im \LaTeX \mi syntax can be
+    rendered once and for all by ~soupault~. User For instance,
+    ~<span class="imath">\LaTeX</span>~ is rendered \im \LaTeX \mi as
+    expected.
+
+    Using this widgets requires being able to inject raw HTML in
+    input files.
+
+*** Implementation
+
+    #+begin_src js :tangle scripts/render-equations.js
+var katex = require("katex");
+var fs = require("fs");
+var input = fs.readFileSync(0);
+var displayMode = process.env.DISPLAY != undefined;
+
+var html = katex.renderToString(String.raw`${input}`, {
+    throwOnError : false,
+    displayModed : displayMode
+});
+
+console.log(html)
+    #+end_src
+
+    We reuse once again the =preprocess_element= widget. The selector
+    is ~.imath~ (~i~ stands for inline in this context), and we
+    replace the previous content with the result of our script.
+
+    #+begin_src toml :tangle soupault.conf
+[widgets.inline-math]
+widget = "preprocess_element"
+selector = ".imath"
+command = "node scripts/render-equations.js"
+action = "replace_content"
+
+[widgets.display-math]
+widget = "preprocess_element"
+selector = ".dmath"
+command = "DISPLAY=1 node scripts/render-equations.js"
+action = "replace_content"
+    #+end_src
+
+** RSS Feed
+
+   #+begin_src toml :tangle soupault.conf
+[index]
+index = true
+dump_json = "rss.json"
+extract_after_widgets = ["urls-rewriting"]
+
+[index.fields]
+title = { selector = ["h1"] }
+modified-at = { selector = ["#modified-at"] }
+created-at = { selector = ["#created-at"] }
+   #+end_src
+
+** Series Navigation
+
+   #+begin_src lua :tangle plugins/series.lua
+function get_title_from_path (path)
+   if Sys.is_file(path) then
+      local content_raw = Sys.read_file(path)
+      local content_dom = HTML.parse(content_raw)
+      local title = HTML.select_one(content_dom, "h1")
+
+      if title then
+         return String.trim(HTML.inner_html(title))
+      else
+         Plugin.fail(path .. ' has no <h1> tag')
+      end
+   else
+      Plugin.fail(path .. ' is not a file')
+   end
+end
+   #+end_src
+
+   #+begin_src lua :tangle plugins/series.lua
+function generate_nav_item_from_title (title, url, template)
+    local env = {}
+    env["url"] = url
+    env["title"] = title
+    local new_content = String.render_template(template, env)
+    return HTML.parse(new_content)
+end
+   #+end_src
+
+   #+begin_src lua :tangle plugins/series.lua
+function generate_nav_items (cwd, cls, template)
+  local elements = HTML.select(page, cls)
+
+  local i = 1
+  while elements[i] do
+    local element = elements[i]
+    local url = HTML.strip_tags(element)
+    local path = Sys.join_path(cwd, url)
+    local title_str = get_title_from_path(path)
+
+    HTML.replace_content(
+      element,
+      generate_nav_item_from_title(title_str, url, template)
+    )
+
+    i = i + 1
+  end
+end
+   #+end_src
+
+   #+begin_src lua :tangle plugins/series.lua
+cwd = Sys.dirname(page_file)
+
+home_template = 'This article is part of the series “<a href="{{ url }}">{{ title }}</a>.”'
+nav_template = '<a href="{{ url }}">{{ title }}</a>'
+
+generate_nav_items(cwd, ".series", home_template)
+generate_nav_items(cwd, ".series-prev", nav_template)
+generate_nav_items(cwd, ".series-next", nav_template)
+   #+end_src
+
+#+begin_src toml :tangle soupault.conf
+[widgets.series]
+widget = "series"
+#+end_src
+
+** Injecting Minified CSS
+
+   #+begin_src lua :tangle plugins/css.lua
+style = HTML.select_one(page, "style")
+
+if style then
+  css = HTML.create_text(Sys.read_file("style.min.css"))
+  HTML.replace_content(style, css)
+end
+   #+end_src
+
+   #+begin_src toml :tangle soupault.conf
+[widgets.css]
+widget = "css"
+   #+end_src
+
+** Cleaning-up
+
+   #+begin_src lua :tangle plugins/clean-up.lua
+function remove_if_empty(html)
+   if String.trim(HTML.inner_html(html)) == "" then
+      HTML.delete(html)
+   end
+end
+   #+end_src
+
+   #+begin_src lua :tangle plugins/clean-up.lua
+function remove_all_if_empty(cls)
+   local elements = HTML.select(page, cls)
+
+   local i = 1
+   while elements[i] do
+      local element = elements[i]
+      remove_if_empty(element)
+      i = i + 1
+   end
+end
+   #+end_src
+
+   #+begin_src lua :tangle plugins/clean-up.lua
+remove_all_if_empty("p") -- introduced by org-mode
+remove_all_if_empty("div.code") -- introduced by coqdoc
+   #+end_src
+
+#+begin_src toml :tangle soupault.conf
+[widgets.clean-up]
+widget = "clean-up"
+#+end_src
diff --git a/site/posts/cleopatra/theme.org b/site/posts/cleopatra/theme.org
new file mode 100644
index 0000000..9b1a129
--- /dev/null
+++ b/site/posts/cleopatra/theme.org
@@ -0,0 +1,573 @@
+#+TITLE: Layout and Style
+
+#+SERIES: ../cleopatra.html
+#+SERIES_PREV: ./literate-programming.html
+#+SERIES_NEXT: ./soupault.html
+
+#+BEGIN_EXPORT html
+<nav id="generate-toc"></nav>
+<div id="history">site/cleopatra/theme.org</div>
+#+END_EXPORT
+
+* Setup
+
+  As often when it comes to frontend development, we will use several
+  tools hosted in the ~npm~ packages repository.  ~npm~ is infamous
+  for downloading lots of files and to store it in the ~node_modules/~
+  directory.  We configure *~cleopatra~* accordingly.
+
+  #+begin_src makefile :tangle theme.mk
+CONFIGURE += package.json package-lock.json node_modules
+  #+end_src
+
+* Base CSS
+
+  We know construct piece by piece the “base” CSS layout which we will
+  inject inside a ~<style>~ tag in each web page.
+
+** Layout
+
+   Our goal is to have a three columns layout: one aside menu, with
+   the top-level navigation links (technical articles, news, etc.) and
+   the table of contents of the current pages if relevant, one main
+   area for the webpage content, and a margin column with side notes
+   and margin notes.
+
+   #+caption: Widths of page components (in ~rem~)
+   #+name: widths
+   | Content | 35 |
+   | Gutter  |  3 |
+   | Margin  | 13 |
+
+   #+name: main-width
+   #+begin_src emacs-lisp :exports none :noweb yes :var widths=widths[,1]
+(nth 0 widths)
+   #+end_src
+
+   #+name: gutter-width
+   #+begin_src emacs-lisp :exports none :noweb yes :var widths=widths[,1]
+(nth 1 widths)
+   #+end_src
+
+   #+name: margin-width
+   #+begin_src emacs-lisp :exports none :noweb yes :var widths=widths[,1]
+(nth 2 widths)
+   #+end_src
+
+   #+begin_src css :tangle style.css :noweb yes
+:root {
+    --main-width: <<main-width()>>rem;
+    --gutter-width: <<gutter-width()>>rem;
+    --margin-width: <<margin-width()>>rem;
+    --code-width: calc(var(--main-width) + var(--gutter-width) + var(--margin-width));
+    --body-width: calc(var(--main-width) + 2 * (var(--gutter-width) + var(--margin-width)));
+}
+   #+end_src
+
+   According to CSS’ own [[https://www.w3.org/TR/css-variables-1/#using-variables][specification]], you cannot use ~var()~ inside
+   media queries.  As a consequnece, for our theme to be responsive,
+   the full width of the page content (\im 2 \times (that is,
+   \mathrm{margin\_width} + \mathrm{gutter\_width}) +
+   \mathrm{content\_width} \mi or call_body-width[:results raw]()rem)
+   has to be hard-coded[fn::Fortunately, this is a literate
+   program. This value is actually programmatically computed, so that
+   we do not have to worry about forgetting to update it].
+
+   #+name: body-width
+   #+begin_src bash :exports none :noweb yes
+echo $((2 * (<<margin-width()>> + <<gutter-width()>>) + <<main-width()>>))
+   #+end_src
+
+   #+begin_src css :tangle style.css :noweb yes
+@media (max-width: <<body-width()>>rem) {
+    :root {
+        --body-width: var(--main-width);
+        --code-width: var(--main-width);
+    }
+}
+   #+end_src
+
+   And now, we are free to actually implement the layout.
+
+   #+begin_src css :tangle style.css :noweb yes
+,* {
+    box-sizing: border-box;
+}
+
+.fullwidth {
+    width: var(--body-width);
+}
+
+@media (min-width: <<body-width()>>rem) {
+    .fullwidth {
+        margin-left: calc(-1 * (var(--margin-width) + var(--gutter-width)));
+    }
+}
+
+html {
+    font-size: 1rem;
+}
+
+body {
+    line-height: 1.4;
+    max-width: var(--body-width);
+    margin-left: auto;
+    margin-right: auto;
+}
+
+aside {
+    background: var(--bg);
+    z-index: 9999;
+    width: var(--body-width);
+    align-self: flex-start;
+    position: sticky;
+    top: 0;
+}
+
+aside nav {
+    text-align: center;
+    border-bottom: 1px solid var(--fade);
+}
+
+aside nav ul {
+    list-style: none;
+    padding: 1rem 0;
+    margin: 0;
+}
+
+aside nav li {
+    display: inline;
+}
+
+aside nav li:not(:first-of-type)::before {
+    content: " · ";
+}
+
+main {
+    counter-reset: sidenote-counter;
+    max-width: var(--main-width);
+    margin: auto;
+}
+
+main nav {
+    font-style: italic;
+    color: var(--fg-plus);
+    background: var(--current-line);
+    padding: .5rem 1rem;
+}
+
+main nav .series-next {
+    text-align: right;
+}
+
+main nav p.series-next::after {
+    content: " →";
+}
+
+main nav p.series-prev::before {
+    content: "← ";
+}
+
+img {
+    max-width: 100%;
+}
+
+#whoami.marginnote {
+    color: var(--fg);
+    margin-bottom: 2em;
+}
+
+img.avatar {
+    border-radius: 20px;
+    display: block;
+    max-width: 90%;
+    margin: auto;
+}
+
+dd {
+    margin-left: 0;
+    margin-bottom: 0.5rem;
+}
+
+.sidenote,
+.marginnote {
+    font-size: smaller;
+    position: relative;
+    width: var(--margin-width);
+}
+
+.sidenote {
+    margin-right: calc(-1 * (var(--margin-width) + var(--gutter-width)));
+    float: right;
+    clear: right;
+}
+
+.marginnote {
+    float: left;
+    clear: left;
+    margin-left: calc(-1 * (var(--margin-width) + var(--gutter-width)));
+}
+
+input.margin-toggle {
+    display: none;
+}
+
+label.sidenote-number {
+    display: inline;
+}
+
+label.margin-toggle:not(.sidenote-number) {
+    display: none;
+}
+
+.sidenote-number:after,
+.sidenote:before {
+    position: relative;
+    vertical-align: baseline;
+}
+
+.sidenote-number {
+    counter-increment: sidenote-counter;
+}
+
+.sidenote-number::after {
+    content: "(" counter(sidenote-counter, lower-greek) ")";
+    font-size: 60%;
+    top: -0.4rem;
+    left: 0.1rem;
+}
+
+.sidenote::before {
+    content: "(" counter(sidenote-counter, lower-greek) ")";
+    font-size: 70%;
+    top: -0.5rem;
+    right: 0.1rem;
+}
+
+div.code,
+pre {
+    width: var(--code-width);
+    overflow-x: auto;
+    overflow-y: hidden;
+    padding: 1rem 2rem;
+}
+
+main {
+    padding-top: 4.2rem;
+    padding-bottom: 4.2rem;
+}
+
+h1 {
+    text-align: center;
+}
+
+h2, h3, h4 {
+    font-style: italic;
+}
+
+h1, h2, h3, h4 {
+    color: var(--doc);
+    font-family: serif;
+    font-weight: normal;
+}
+
+dt {
+    font-weight: bold;
+}
+
+div.code,
+span.inlinecode,
+pre,
+tt,
+.dmath,
+.imath {
+    font-family: monospace;
+    font-size: 85%;
+}
+
+details {
+    margin: 1.5rem 0;
+}
+
+table {
+    border-top: 2px solid var(--fg);
+    border-bottom: 2px solid var(--fg);
+    border-collapse: collapse;
+    width: 100%;
+    margin: 1.5rem 0;
+}
+
+th {
+    font-weight: normal;
+    text-transform: uppercase;
+}
+
+td,
+th {
+    border-top: 1px solid var(--fade);
+    height: 2em;
+    padding: 0 1em;
+}
+
+td.date,
+td.commit {
+    text-align: center;
+    font-size: 0.75em;
+    font-family: monospace;
+}
+
+/* max-width has to be equal to --body-width */
+@media (max-width: <<body-width()>>rem) {
+    body {
+        padding: 2rem;
+        margin: auto;
+        display: block;
+    }
+
+    aside {
+        width: var(--main-width);
+        margin: auto;
+    }
+
+    label.margin-toggle:not(.sidenote-number) {
+        display: inline;
+    }
+
+    .sidenote,
+    .marginnote {
+        display: none;
+    }
+
+    .margin-toggle:checked + .sidenote,
+    .margin-toggle:checked + .marginnote {
+        display: block;
+        float: left;
+        left: 1rem;
+        clear: both;
+        width: 95%;
+        margin: 1rem 2.5%;
+        vertical-align: baseline;
+        position: relative;
+    }
+
+    label {
+        cursor: pointer;
+    }
+
+    pre, aside, div.code {
+        width: 100%;
+    }
+}
+   #+end_src
+
+** Colors
+
+   #+begin_src css :tangle style.css
+:root {
+    --bg: white;
+    --bg-plus: #f7f7f7;
+    --current-line: #fbfbfb;
+    --fade: #cfcecb;
+    --fg: #3c3c3c;
+    --fg-plus: #575757;
+    --doc: black;
+    --warning: #bd745e;
+    --red: #b3534b;
+    --green: #6d9319;
+    --yellow: #d4b100;
+}
+   #+end_src
+
+   #+begin_src css :tangle style.css
+body {
+    font-family: sans-serif;
+    color: var(--fg);
+    background: var(--bg);
+}
+
+h2 a.anchor-link,
+h3 a.anchor-link,
+h4 a.anchor-link {
+    display: none;
+    font-style: normal;
+    text-decoration: none;
+    font-family: monospace;
+    font-size: smaller;
+    color: var(--doc);
+}
+
+[id] {
+    scroll-margin-top: 4rem;
+}
+
+h2:hover a.anchor-link,
+h3:hover a.anchor-link,
+h4:hover a.anchor-link {
+    display: inline;
+}
+
+.sidenote,
+.marginnote {
+    color: var(--fg-plus);
+}
+
+pre,
+code,
+div.code,
+span.inlinecode,
+tt {
+    color: var(--doc);
+}
+   #+end_src
+
+** Coq
+
+   #+begin_src css :tangle style.css
+div.code {
+    white-space: nowrap;
+}
+
+div.code,
+span.inlinecode {
+    font-family : monospace;
+}
+
+.paragraph {
+    margin-bottom : .8em;
+}
+
+.code a[href] {
+    color : inherit;
+    text-decoration : none;
+    background : var(--bg-plus);
+    padding : .1rem .15rem .1rem .15rem;
+    border-radius : 15%;
+}
+
+.code .icon {
+    display: none;
+}
+#+END_SRC
+
+** Icons
+
+   #+begin_src css :tangle style.css
+.icon svg {
+    display: inline;
+    width: 1em;
+    height: .9em;
+    vertical-align: text-top;
+}
+
+a[href], .margin-toggle {
+    color: #0000ee;
+}
+
+a[href] .icon svg {
+    fill: #0000ee;
+}
+
+a[href]:visited {
+    color: #25008b;
+}
+
+a[href]:visited .icon svg {
+    fill: #25008b;
+}
+
+.url-mark.fa {
+    display: inline;
+    font-size: 90%;
+    width: 1em;
+}
+
+.url-mark.fa-github::before {
+    content: "\00a0\f09b";
+}
+
+.url-mark.fa-external-link::before {
+    content: "\00a0\f08e";
+}
+   #+end_src
+
+** Minify CSS
+
+   #+begin_src shell :shebang #!/bin/bash :tangle scripts/css.sh
+minify="$(npm bin)/minify"
+normalize="$(npm root)/normalize.css/normalize.css"
+style="style.css"
+
+# minify add a newline character at the end of its input
+# we remove it using `head'
+echo "
+@charset \"UTF-8\";
+$(cat ${normalize})
+$(cat ${style})
+" | ${minify} --css | head -c -1 > style.min.css
+   #+end_src
+
+   #+begin_src makefile :tangle theme.mk
+style.min.css : style.css dependencies-prebuild
+	@cleopatra echo "Minifying" "CSS"
+	@scripts/css.sh
+
+ARTIFACTS += style.min.css
+
+theme-build : style.min.css
+   #+end_src
+
+* HTML Templates
+
+  It would be best if we had a preprocessing step to inject the
+  minified style, rather than using ~soupault~ to do the work once per
+  page.
+
+  #+begin_src html :tangle templates/main.html :noweb yes
+<html lang="en">
+  <head>
+    <meta charset="utf-8">
+    <meta name="viewport" content="width=device-width, initial-scale=1.0">
+    <style></style>
+    <link href="https://soap.coffee/+vendors/katex.0.11.1+swap/katex.css" rel="stylesheet" media="none" onload="if(media!='all')media='all'">
+    <title></title>
+  </head>
+  <body>
+    <aside>
+      <nav>
+        <ul>
+          <li>
+            <a href="/">Technical Posts</a>
+          </li>
+          <li>
+            <a href="/opinions">Opinions</a>
+          </li>
+          <li>
+            <a href="/news">News</a>
+          </li>
+        </ul>
+      </nav>
+    </aside>
+    <main>
+      <span id="whoami" class="marginnote">
+        <img class="avatar" src="/img/vampy.jpg" />
+
+        <p>
+          Hi, I’m <strong>lthms</strong>.
+        </p>
+
+        <p>
+          I don’t like syntax highlighting, but I like
+          types and functional programming languages.
+          He/him.
+        </p>
+
+        <p>
+          Interested in starting a discussion? Don’t hesitate to <a
+          href="mailto:~lthms/public-inbox@lists.sr.ht">shoot me an
+          email</a>.
+        </p>
+      </span>
+    </main>
+  </body>
+</html>
+  #+end_src
diff --git a/site/posts/coq.org b/site/posts/coq.org
new file mode 100644
index 0000000..b8b6818
--- /dev/null
+++ b/site/posts/coq.org
@@ -0,0 +1,44 @@
+#+SERIES: ./index.html
+#+SERIES_NEXT: haskell.html
+
+#+TITLE: About Coq
+
+Coq is a formal proof management system which provides a pure
+functional language with nice dependent types together with an
+environment for writing machine-checked proofs.
+
+- [[./StronglySpecifiedFunctions.org][A Series on Strongly-Specified Funcions in Coq]] ::
+  Using dependent types and the ~Prop~ sort, it becomes possible to specify
+  functions whose arguments and results are constrained by properties.
+  Using such a “strongly-specified” function requires to provide a proof that
+  the supplied arguments satisfy the expected properties, and allows for soundly
+  assuming the results are correct too. However, implementing dependently-typed
+  functions can be challenging.
+
+- [[./Ltac.org][A Series on Ltac]] ::
+  Ltac is the “tactic language” of Coq. It is commonly advertised as the common
+  approach to write proofs, which tends to bias how it is introduced to new Coq
+  users (/e.g./, in Master courses). In this series, we present Ltac as the
+  metaprogramming tool it is, since fundamentally it is an imperative language
+  which allows for constructing Coq terms interactively and incrementally.
+
+- [[./RewritingInCoq.html][Rewriting in Coq]] ::
+  The ~rewrite~ tactics are really useful, since they are not limited to the Coq
+  built-in equality relation.
+
+- [[./ClightIntroduction.html][A Study of Clight and its Semantics]] ::
+  Clight is a “simplified” C AST used by CompCert, the certified C compiler. In
+  this write-up, we prove a straighforward functional property of a small C
+  function, as an exercise to discover the Clight semantics.
+
+- [[./AlgebraicDatatypes.html][Proving Algebraic Datatypes are “Algebraic”]] ::
+  The set of types which can be defined in a language together with ~+~ and ~*~
+  form an “algebraic structure” in the mathematical sense, hence the name. It
+  means the definitions of ~+~ and ~*~ have to satisfy properties such as
+  commutativity or the existence of neutral elements.
+
+- [[./Coqffi.org][A Series on ~coqffi~]] ::
+  ~coqffi~ generates Coq FFI modules from compiled OCaml interface
+  modules (~.cmi~). In practice, it greatly reduces the hassle to
+  together OCaml and Coq modules within the same codebase, especially
+  when used together with the ~dune~ build system.
diff --git a/site/posts/haskell.org b/site/posts/haskell.org
new file mode 100644
index 0000000..cf06b89
--- /dev/null
+++ b/site/posts/haskell.org
@@ -0,0 +1,13 @@
+#+SERIES: index.html
+#+SERIES_PREV: coq.html
+#+SERIES_NEXT: miscellaneous.html
+
+#+TITLE: About Haskell
+
+Haskell is a pure, lazy, functional programming language with a very
+expressive type system.
+
+- [[./ExtensibleTypeSafeErrorHandling.html][Extensible, Type-Safe Error Handling In Haskell]] ::
+  Ever heard of “extensible effects?” By applying the same principle, but for
+  error handling, the result is nice, type-safe API for Haskell, with a lot of
+  GHC magic under the hood.
diff --git a/site/posts/index.org b/site/posts/index.org
new file mode 100644
index 0000000..bc53280
--- /dev/null
+++ b/site/posts/index.org
@@ -0,0 +1,28 @@
+#+TITLE: Technical Articles
+
+Over the past years, I have tried to capitalize on my findings. More
+often than not, I have lacked in regularity, but I hope I have made up
+for it in exoticism.
+
+#+begin_export html
+<nav id="generate-toc"></nav>
+#+end_export
+
+* About Coq
+  :PROPERTIES:
+  :CUSTOM_ID: coq
+  :END:
+
+  #+include: ./coq.org
+
+* About Haskell
+
+  #+include: ./haskell.org
+
+* Miscellaneous
+
+  #+include: ./miscellaneous.org
+
+* About this Website
+
+  #+include: ./meta.org
diff --git a/site/posts/meta.org b/site/posts/meta.org
new file mode 100644
index 0000000..f6c1de5
--- /dev/null
+++ b/site/posts/meta.org
@@ -0,0 +1,16 @@
+#+TITLE: About this Website
+
+#+SERIES: ./index.html
+#+SERIES_PREV: miscellaneous.html
+
+The generation of this website is far from being trivial, and requires
+the combination of —probably too— many tools. For instance, even if I
+mostly use Org mode for authoring content, most of my write-ups about
+Coq are actually Coq files, and I use ~coqdoc~ to generate the HTML
+pages you read.
+
+- [[./Thanks.org][Thanks!]] ::
+  This website could not exist without many awesome free software
+  projects. Although I could not list them all even if I wanted, my
+  desire is at least to try keeping up-to-date a curated description
+  of the most significant ones.
diff --git a/site/posts/miscellaneous.org b/site/posts/miscellaneous.org
new file mode 100644
index 0000000..7458cb3
--- /dev/null
+++ b/site/posts/miscellaneous.org
@@ -0,0 +1,20 @@
+#+SERIES: index.html
+#+SERIES_PREV: haskell.html
+#+SERIES_NEXT: meta.html
+
+#+TITLE: Miscellaneous
+
+Over the years, I have made a habit of learning new programming
+languages, out of curiosity, and I intend to continue this way for the
+time being.
+
+- [[./DiscoveringCommonLisp.html][Discovering Common Lisp with ~trivial-gamekit~]] ::
+  Common Lisp is a venerable programming languages like no other I
+  know.  From the creation of a Lisp package up to the creation of a
+  standalone executable, we explore the shore of this strange beast.
+
+- [[./RankNTypesInOCaml.html][Writing a Function Whose Argument is a Polymorphic Function in OCaml]] ::
+  In OCaml, it is not possible to write a function whose argument is a
+  polymorphic function. Trying to write such a function results in the
+  type-checker complaining back at you. The trick to be able to write
+  such a function is to use records.
-- 
cgit v1.2.3