From 495f9db0606b0ed09e6fac59dc32de4cdc8c0087 Mon Sep 17 00:00:00 2001
From: Thomas Letan <lthms@soap.coffee>
Date: Sun, 28 Mar 2021 00:03:41 +0100
Subject: 2021 Spring redesign

---
 site/cleopatra.org                             |  62 +-
 site/cleopatra/commands.org                    |  36 ++
 site/cleopatra/coq.org                         |  60 +-
 site/cleopatra/dependencies.org                |  89 +++
 site/cleopatra/literate-programming.org        |  27 +-
 site/cleopatra/org.org                         | 183 +++---
 site/cleopatra/soupault.org                    | 811 ++++++++++++-------------
 site/cleopatra/theme.org                       | 722 ++++++++++++++--------
 site/coq.org                                   |  44 ++
 site/haskell.org                               |  13 +
 site/img/icons.svg                             |  39 ++
 site/img/merida.webp                           | Bin 36922 -> 0 bytes
 site/index.org                                 |  77 +--
 site/meta.org                                  |  23 +
 site/miscellaneous.org                         |  14 +
 site/news/index.html                           |  15 +
 site/opinions/MonadTransformers.org            |  13 +-
 site/opinions/index.org                        |   6 +-
 site/posts/AlgebraicDatatypes.v                |   6 +-
 site/posts/ClightIntroduction.v                |   6 +-
 site/posts/Coqffi.org                          |   7 +-
 site/posts/CoqffiEcho.org                      |  10 +-
 site/posts/CoqffiIntro.org                     |  10 +-
 site/posts/ExtensibleTypeSafeErrorHandling.org |   9 +-
 site/posts/Ltac.org                            |  18 +-
 site/posts/LtacMetaprogramming.v               |   3 +
 site/posts/LtacPatternMatching.v               |  10 +-
 site/posts/MixingLtacAndGallina.v              |   5 +-
 site/posts/RewritingInCoq.v                    |   6 +-
 site/posts/StronglySpecifiedFunctions.org      |   7 +-
 site/posts/StronglySpecifiedFunctionsProgram.v |  11 +-
 site/posts/StronglySpecifiedFunctionsRefine.v  |  20 +-
 site/posts/Thanks.org                          |  40 +-
 33 files changed, 1392 insertions(+), 1010 deletions(-)
 create mode 100644 site/cleopatra/commands.org
 create mode 100644 site/cleopatra/dependencies.org
 create mode 100644 site/coq.org
 create mode 100644 site/haskell.org
 create mode 100644 site/img/icons.svg
 delete mode 100644 site/img/merida.webp
 create mode 100644 site/meta.org
 create mode 100644 site/miscellaneous.org

(limited to 'site')

diff --git a/site/cleopatra.org b/site/cleopatra.org
index 77e8ff1..0831621 100644
--- a/site/cleopatra.org
+++ b/site/cleopatra.org
@@ -1,46 +1,44 @@
-#+BEGIN_EXPORT html
-<h1>A Series on Generating this Static Website</h1>
-#+END_EXPORT
+#+TITLE: A Series on Generating this Static Website
 
-The generation of this website is far from being trivial, and requires the
-combination of —probably too— many tools. For instance, my write-ups about Coq
-are actually Coq files, and I use ~coqdoc~ to generate the HTML pages you read.
-The theme is not written in CSS, but in SASS that needs to be compiled.  Even
-more, the whole website is postprocessed using ~soupault~.
+#+SERIES: ./meta.html
+#+SERIES_PREV: ./posts/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]].
 
-At some point, I felt like the whole process 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:bootstrap]. But the so-called
-generation processes I had written for *~cleopatra~* the first basically “just
-worked” with *~cleopatra~* the second.
+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.
 
 So, coming back to this series, it is just the very reason why I started using
 *~cleopatra~* in the first place: the generation processes used by this website,
 written as literate programs.
 
-#+BEGIN_EXPORT html
-<article class="index">
-#+END_EXPORT
+- [[./cleopatra/dependencies.org][Installing Dependencies]] ::
 
-- [[./cleopatra/theme.org][Theming and Templating]] ::
+- [[file:cleopatra/coq.org][Authoring Contents with Coq ~(TODO)~]] ::
 
-- [[file:cleopatra/coq.org][Authoring Contents As Coq Documents ~(TODO)~]] ::
+- [[./cleopatra/org.org][Authoring Contents with ~org-mode~ ~(TODO)~]] ::
 
-- [[./cleopatra/literate-programming.org][Authoring Literate Programs]] ::
+- [[./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
@@ -48,7 +46,7 @@ written as literate programs.
   programming projects present in the ~posts/~ directory of this
   website.
 
-- [[./cleopatra/org.org][Authoring Contents As Org Documents ~(TODO)~]] ::
+- [[./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
@@ -57,11 +55,3 @@ written as literate programs.
 
 *Appendix:* In case you are curious, you can have a look at
 [[./posts/CleopatraV1.html][the first implementaiton of *~cleopatra~*]].
-
-#+BEGIN_EXPORT html
-</article>
-#+END_EXPORT
-
-[fn:bootstrap] 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.”
diff --git a/site/cleopatra/commands.org b/site/cleopatra/commands.org
new file mode 100644
index 0000000..fbf0430
--- /dev/null
+++ b/site/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/cleopatra/coq.org b/site/cleopatra/coq.org
index 64d1e9d..81f3d27 100644
--- a/site/cleopatra/coq.org
+++ b/site/cleopatra/coq.org
@@ -1,3 +1,15 @@
+#+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
@@ -13,7 +25,6 @@ COQ_ARTIFACTS := $(COQ_POSTS:.v=.vo) \
 
 coq-build : ${COQ_HTML}
 
-theme-build : site/style/coq.sass
 soupault-build : coq-build
 
 ARTIFACTS += ${COQ_ARTIFACTS} .lia.cache
@@ -28,52 +39,9 @@ COQDOCARG := --no-index --charset utf8 --short \
              --external "https://compcert.org/doc/html" compcert \
              --external "https://lysxia.github.io/coq-simple-io" SimpleIO
 
-%.html : %.v coq.mk
-	@cleopatra echo Exporting "$*.v"
+%.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
-
-#+BEGIN_SRC sass :tangle site/style/coq.sass
-div.code
-    padding-left : 1.5rem
-    padding-left : 1.5rem
-    white-space: nowrap
-    line-height : 140%
-
-div.code,
-span.inlinecode
-    font-family : 'Fira Code', monospace
-    color : $monospace-color
-    font-size : 80%
-    overflow-x : auto
-
-div.doc
-    max-width : $content-width
-    line-height : 140%
-
-    /* dirty patch to get the code in full page width */
-    pre
-        width : calc(100vw - 2*var(--side-margin))
-
-.paragraph
-    margin-bottom : .8em
-#+END_SRC
-
-#+BEGIN_SRC sass :tangle site/style/coq.sass
-.code
-    a[href]
-        color : inherit
-        text-decoration : none
-        background : #f7f7f7
-        padding : .1rem .15rem .1rem .15rem
-        border-radius : 15%
-
-        .url-mark
-            display: none
-#+END_SRC
-
-# Local Variables:
-# org-src-preserve-indentation: t
-# End:
diff --git a/site/cleopatra/dependencies.org b/site/cleopatra/dependencies.org
new file mode 100644
index 0000000..5a79741
--- /dev/null
+++ b/site/cleopatra/dependencies.org
@@ -0,0 +1,89 @@
+#+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.1 |
+  | coq-compcert |     3.8 |
+
+  #+caption: Dependencies for the ~coqffi~ series
+  #+name: lp-deps
+  | Package       |     Version |
+  |---------------+-------------|
+  | dune          |       2.8.4 |
+  | coq-coqffi    | 1.0.0~beta5 |
+  | coq-simple-io |       1.5.0 |
+
+  #+caption: Soupault
+  #+name: soupault-deps
+  | Package  | Version |
+  |----------+---------|
+  | soupault |   2.5.0 |
+
+  #+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.11.2
+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.0 |
+  | minify        |   7.0.1 |
+  | 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
+  #+end_src
diff --git a/site/cleopatra/literate-programming.org b/site/cleopatra/literate-programming.org
index be25097..63e0b02 100644
--- a/site/cleopatra/literate-programming.org
+++ b/site/cleopatra/literate-programming.org
@@ -1,6 +1,8 @@
-#+BEGIN_EXPORT html
-<h1>Literate Programming Projects</h1>
-#+END_EXPORT
+#+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
@@ -12,18 +14,27 @@ 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
-(cleopatra:configure) ; opinionated configuration provided by cleopatra
+;; 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))) ; allow the execution of shell block code
+ '((shell . t)))
 
- ;; scan the posts/ directory and tangled it into lp/
+;; scan the posts/ directory and tangled it into lp/
 (setq org-publish-project-alist
       '(("lp"
          :base-directory "site/posts"
@@ -46,6 +57,8 @@ literate-programming-prebuild :
 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
@@ -54,7 +67,7 @@ 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
+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"
diff --git a/site/cleopatra/org.org b/site/cleopatra/org.org
index acfd432..829272b 100644
--- a/site/cleopatra/org.org
+++ b/site/cleopatra/org.org
@@ -1,54 +1,30 @@
-* Author Guidelines
-
-* Under the Hood
+#+TITLE: Authoring Content with ~org-mode~
 
-#+BEGIN_SRC emacs-lisp :tangle scripts/packages.el
-(use-package lua-mode :ensure t :defer t)
-(use-package rust-mode :ensure t :defer t)
-(use-package sass-mode :ensure t :defer t)
-(use-package haskell-mode :ensure t :defer t)
-(use-package toml-mode :ensure t :defer t)
-(use-package json-mode :ensure t :defer t)
-(use-package proof-general :ensure t :defer t)
-(use-package tuareg :ensure t :defer t)
-#+END_SRC
-
-#+BEGIN_SRC emacs-lisp :tangle scripts/export-org.el
-(cleopatra:configure)
+#+SERIES: ../cleopatra.html
+#+SERIES_PREV: ./coq.html
+#+SERIES_NEXT: ./literate-programming.html
 
-(setq org-html-doctype "html5")
-(setq org-html-html5-fancy t)
-
-(org-babel-do-load-languages
- 'org-babel-load-languages
- '((shell . t)
-   (dot . t)))
+#+BEGIN_EXPORT html
+<nav id="generate-toc"></nav>
+<div id="history">site/cleopatra/org.org</div>
+#+END_EXPORT
 
-(setq org-html-htmlize-output-type nil)
-(setq org-export-with-toc nil)
-
-(add-to-list 'org-entities-user
-             '("im" "\\(" nil "<span class=\"imath\">" "" "" ""))
-(add-to-list 'org-entities-user
-             '("mi" "\\)" nil "</span>" "" "" ""))
+* Author Guidelines
 
-(org-html-export-to-html nil nil nil t)
-#+END_SRC
+* Implementation
 
-#+BEGIN_SRC makefile :tangle org.mk
+#+begin_src makefile :tangle org.mk
 EMACS := cleopatra-emacs
 
-ORG_POSTS := $(shell find site/ -name "*.org")
-ORG_HTML := $(ORG_POSTS:.org=.html)
+ORG_IN := $(shell find site/ -name "*.org")
+ORG_OUT := $(ORG_IN:.org=.html)
 
 org-prebuild : .emacs
-org-build : ${ORG_HTML}
+org-build : ${ORG_OUT}
 
-theme-build : site/style/org.sass
 soupault-build : org-build
-org-build : literate-programming-build
 
-ARTIFACTS += ${ORG_HTML}
+ARTIFACTS += ${ORG_OUT}
 CONFIGURE += .emacs
 
 EXPORT := --batch \
@@ -68,44 +44,91 @@ INIT := --batch --load="${ROOT}/scripts/packages.el" \
          .emacs org.mk
 	@cleopatra echo Exporting "$*.org"
 	@${EMACS} $< ${EXPORT}
-#+END_SRC
-
-#+BEGIN_SRC sass :tangle site/style/org.sass
-#text-footnotes
-    max-width : 35rem
-
-.footpara
-    display: inline
-    margin-left: .2em
-
-.section-number-2:after,
-.section-number-3:after
-    content: ". "
-
-.section-number-4,
-.section-number-5,
-.section-number-6
-    display: none
-
-dl
-    dd p
-        margin-top: 0
-
-.footnotes
-    font-size : 1rem
-
-.org-literate-programming
-    .org-src-tangled-to:before
-        content: "\f054"
-        font : normal normal normal 11px/1 ForkAwesome
-
-    .org-src-tangled-to,
-        padding-left : 2rem
-
-    .org-src-tangled-to,
-    .org-src-name
-        font-family : 'Fira Code', monospace
-        font-size : 70%
-        font-weight: bold
-        color : #444
-#+END_SRC
+#+end_src
+
+#+begin_src emacs-lisp :tangle scripts/packages.el
+(use-package ox-tufte :ensure t)
+#+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)))
+
+(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/cleopatra/soupault.org b/site/cleopatra/soupault.org
index 452f442..92042c2 100644
--- a/site/cleopatra/soupault.org
+++ b/site/cleopatra/soupault.org
@@ -1,209 +1,136 @@
-#+BEGIN_EXPORT html
-<h1><code>soupault</code> Configuration</h1>
-#+END_EXPORT
+#+TITLE: ~soupault~
 
-#+NAME: build-dir
-#+BEGIN_SRC text :exports none
-build
-#+END_SRC
+#+SERIES: ../cleopatra.html
+#+SERIES_PREV: ./theme.html
+#+SERIES_NEXT: ./commands.html
 
-#+NAME: prefix
-#+BEGIN_SRC text :exports none
-~lthms
-#+END_SRC
+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
 
-In a nutshell, the purpose of ~soupault~ is to post-process HTML files
-generated by the generation processes of *~cleopatra~*
+* Installation
 
-The rest of this document proceeds as follows. We first describe the general
-settings of ~soupault~. Then, we enumerate the widgets enabled for this website.
-Finally, we provide a proper definition for ~soupault~ the *~cleopatra~*
-generation process.
+  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~*.
 
-#+TOC: headlines 2
+  #+begin_src makefile :tangle soupault.mk
+OCAML_VERSION := 4.11.2
+OCAML := ocaml-base-compiler.${OCAML_VERSION}
 
-* ~soupault~ General Settings
+CONFIGURE += _opam rss.json
+ARTIFACTS += out
 
-The general ~settings~ section of ~soupault.conf~ is fairly basic, and there is
-little to say that the
-[[https://soupault.neocities.org/reference-manual/#getting-started][“Getting
-Started”]] already discuss in length.
+soupault-prebuild : _opam/init
+  #+end_src
 
-We emphasize three things:
+  Using ~soupault~ is as simple as calling it, without any particular
+  command-line arguments.
+
+  #+begin_src makefile :tangle soupault.mk
+soupault-build : package-lock.json style.min.css
+	@cleopatra echo "Executing" "soupault"
+	@soupault
+  #+end_src
 
-- The ~build_dir~ is set to src_text[:exports code :noweb yes]{<<build-dir>>/<<prefix>>}
-  in place of simply src_text[:exports code :noweb yes]{<<build-dir>>}.
-- The ~ignore_extensions~ shall be updated to take into account artifacts
-  produces by other *~cleopatra~* generation processes.
-- We disable the “clean URLs” feature of ~soupault. This option renames
-  a HTML files ~foo/bar.html~ into ~foo/bar/index.html~, which means when served
-  by a HTTP server, the ~foo/bar~ URL will work. The issue we have with this
-  feature is that the internal links within your websiste needs to take their
-  /final/ URL into account, rather than their actual name. If one day ~soupault~
-  starts rewriting internal URLs when ~clean_url~ is enabled, we might
-  reconsider using it.
+  We now describe our configuration file for ~soupault~.
+
+* Configuration
+
+  #+name: base-dir
+  #+begin_src verbatim :noweb yes :exports none
+~lthms
+  #+end_src
 
-#+BEGIN_SRC toml :tangle soupault.conf :noweb yes
+** 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
-verbose = false
-debug = false
 site_dir = "site"
-build_dir = "<<build-dir>>/<<prefix>>"
-
+build_dir = "out/<<base-dir>>"
+doctype = "<!DOCTYPE html>"
+clean_urls = false
+generator_mode = true
+complete_page_selector = "html"
+default_content_selector = "main"
 page_file_extensions = ["html"]
 ignore_extensions = [
-  "draft", "vo", "vok", "vos", "glob",
-  "html~", "org", "aux", "sass",
+  "v", "vo", "vok", "vos", "glob",
+  "html~", "org"
 ]
-
-generator_mode = true
-complete_page_selector = "html"
 default_template_file = "templates/main.html"
-default_content_selector = "main"
-doctype = "<!DOCTYPE html>"
-clean_urls = false
-#+END_SRC
-
-#+BEGIN_TODO
-The list of ignored extensions should be programmatically generated with the
-help of *~cleopatra~*.
-#+END_TODO
-
-* Widgets
+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.
+   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
+   #+begin_src toml :tangle soupault.conf
 [widgets.page-title]
 widget = "title"
 selector = "h1"
 default = "~lthms"
 prepend = "~lthms: "
-#+END_SRC
+   #+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.
+   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
+   #+NAME: soupault-version
+   #+begin_src bash :results verbatim output
 soupault --version | head -n 1 | tr -d '\n'
-#+END_SRC
+   #+end_src
 
-The configuration of the widget ---initially provided by ~soupault~--- becomes
-less subject to the obsolescence.
+   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
+   #+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
-
-** Generating 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_element"
-valid_html = true
-min_level = 2
-numbered_list = true
-#+END_SRC
-
-#+BEGIN_TODO
-We could propose a patch to ~soupault~'s upstream to add numbering in titles.
-#+END_TODO
-
-** Fixing Org Internal Links
-
-For some reason, Org prefix internal links to other Org documents with
-~file://~. To avoid that, we provide a simple plugin which removes ~file://~
-from the begining of a URL.
-
-#+BEGIN_TODO
-This plugin definition should be part of [[./Contents/Org.org][the ~org~
-generation process]], but that would require to aggregate “subconfig” into a
-larger one.
-#+END_TODO
-
-This plugin key component is the =fix_org_urls= function.
-
-- =fix_org_urls(LIST, ATTR)= ::
-  Enumerate the DOM elements of =LIST=, and check their =ATTR= attribute.
-
-#+BEGIN_SRC lua :tangle plugins/fix-org-urls.lua
-function fix_org_urls(list, attr)
-  index, link = next(list)
-
-  while index do
-    href = HTML.get_attribute(link, attr)
-
-    if href then
-      href = Regex.replace(href, "^file://", "")
-      HTML.set_attribute(link, attr, href)
-    end
-
-    index, link = next(list, index)
-  end
-end
-#+END_SRC
-
-We use this function to fix the URLs of tags known to be subject to Org strange
-behavior. For now, only ~<a>~ has been affected.
-
-#+BEGIN_SRC lua :tangle plugins/fix-org-urls.lua
-fix_org_urls(HTML.select(page, "a"), "href")
-fix_org_urls(HTML.select(page, "img"), "src")
-#+END_SRC
-
-The configuration of this plugin, and the associated widget, is straightforward.
-
-#+BEGIN_SRC toml :tangle soupault.conf :noweb tangle
-[widgets.fix-org-urls]
-widget = "fix-org-urls"
-#+END_SRC
+   #+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.
+   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.
+   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.
+   From a high-level perspective, the plugin structure is the following.
 
-#+BEGIN_SRC lua  :tangle plugins/urls-rewriting.lua :noweb no-export
-prefix_url = config["prefix_url"]
-<<validate_prefix>>
+   First, we validate the widget configuration.
 
-<<prefix_func>>
-<<prefix_calls>>
-#+END_SRC
-
-1. We validate the widget configuration.
-2. We propose a generic function to enumerate and rewrite tags which can have
-   internal URLs as attribute argument.
-3. We use this generic function for relevant tags.
+   #+BEGIN_SRC lua :tangle plugins/urls-rewriting.lua
+prefix_url = config["prefix_url"]
 
-#+NAME: validate_prefix
-#+BEGIN_SRC lua
 if not prefix_url then
   Plugin.fail("Missing mandatory field: `prefix_url'")
 end
@@ -215,10 +142,12 @@ end
 if not Regex.match(prefix_url, "(.*)/$") then
   prefix_url = prefix_url .. "/"
 end
-#+END_SRC
+   #+END_SRC
+
+   Then, we propose a generic function to enumerate and rewrite tags
+   which can have.
 
-#+NAME: prefix_func
-#+BEGIN_SRC lua
+   #+BEGIN_SRC lua :tangle plugins/urls-rewriting.lua
 function prefix_urls (links, attr, prefix_url)
   index, link = next(links)
 
@@ -236,33 +165,35 @@ function prefix_urls (links, attr, prefix_url)
     index, link = next(links, index)
   end
 end
-#+END_SRC
+   #+END_SRC
 
-#+NAME: prefix_calls
-#+BEGIN_SRC lua
+   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)
-#+END_SRC
+prefix_urls(HTML.select(page, "use"), "href", prefix_url)
+   #+END_SRC
 
-Again, configuring soupault to use this plugin is relatively straightforward.
-The only important thing to notice is the use of the ~after~ field, to ensure
-this plugin is run /after/ the plugin responsible for fixing Org documents URLs.
+   Again, configuring soupault to use this plugin is relatively
+   straightforward.
 
-#+BEGIN_SRC toml :tangle soupault.conf :noweb tangle
+   #+BEGIN_SRC toml :tangle soupault.conf :noweb yes
 [widgets.urls-rewriting]
 widget = "urls-rewriting"
-prefix_url = "<<prefix>>"
-after = "fix-org-urls"
-#+END_SRC
+prefix_url = "<<base-dir>>"
+after = "mark-external-urls"
+   #+END_SRC
 
 ** Marking External Links
 
-#+BEGIN_SRC lua :tangle plugins/external-urls.lua
+   #+BEGIN_SRC lua :tangle plugins/external-urls.lua
 function mark(name)
-  return '<i class="url-mark fa fa-' .. name ..
-         '" aria-hidden="true"></i>'
+  return '<span class="icon"><svg><use href="/img/icons.svg#'
+         .. name ..
+         '"></use></svg></span>'
 end
 
 links = HTML.select(page, "a")
@@ -274,85 +205,101 @@ while index do
 
   if href then
     if Regex.match(href, "^https?://github.com") then
-      icon = HTML.parse(mark('github'))
+      icon = HTML.parse(mark("github"))
       HTML.append_child(link, icon)
     elseif Regex.match(href, "^https?://") then
-      icon = HTML.parse(mark('external-link'))
+      icon = HTML.parse(mark("external-link"))
       HTML.append_child(link, icon)
     end
   end
 
   index, link = next(links, index)
 end
-#+END_SRC
-
-#+BEGIN_SRC sass :tangle site/style/plugins.sass
-.url-mark.fa
-    display: inline
-    font-size: 90%
-    width: 1em
-
-.url-mark.fa-github::before
-    content: "\00a0\f09b"
+   #+END_SRC
 
-.url-mark.fa-external-link::before
-    content: "\00a0\f08e"
-#+END_SRC
-
-#+BEGIN_SRC toml :tangle soupault.conf
+   #+BEGIN_SRC toml :tangle soupault.conf
 [widgets.mark-external-urls]
 after = "generate-history"
 widget = "external-urls"
-#+END_SRC
+   #+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 = "preprocess_element"
+selector = "#generate-toc"
+command = 'echo "<h2>Table of Contents</h2> $(cat)"'
+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.
+    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
+    For instance, considering the following HTML snippet
 
-#+BEGIN_SRC html
+    #+begin_src html
 <div id="history">
   site/posts/FooBar.org
 </div>
-#+END_SRC
+    #+end_src
 
-This plugin will replace the content of this ~<div>~ with the revisions table of
-~site/posts/FooBar.org~.
+    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
-—afterwards abstracted with the ~<<repo>>~ noweb reference— is
+    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 text
+    #+name: repo
+    #+begin_src verbatim :exports none
 https://code.soap.coffee/writing/lthms.git
-#+END_SRC
+    #+end_src
 
-#+BEGIN_SRC html :tangle templates/history.html :noweb tangle
-<details class="history">
+    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.
+    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>.
+    You can consult the source of this file in its current version
+    <a href="<<repo>>/tree/{{file}}">here</a>.
   </p>
 
-  <table>
+  <table class="fullwidth">
   {{#history}}
   <tr>
     <td class="date"
@@ -362,66 +309,44 @@ https://code.soap.coffee/writing/lthms.git
 {{#modified}}
         id="modified-at"
 {{/modified}}
-        >
-      {{date}}
-    </td>
+        >{{date}}</td>
     <td class="subject">{{subject}}</td>
     <td class="commit">
-      <a href="<<repo>>/commit/{{filename}}/?id={{hash}}">
-        {{abbr_hash}}
-      </a>
+      <a href="<<repo>>/commit/{{filename}}/?id={{hash}}">{{abbr_hash}}</a>
     </td>
   </tr>
   {{/history}}
   </table>
 </details>
-#+END_SRC
-
-#+BEGIN_SRC sass :tangle site/style/plugins.sass
-table
-    border-top : 2px solid black
-    border-bottom : 2px solid black
-    border-collapse : collapse
-    width : 35rem
-
-td
-    border-bottom : 1px solid black
-    padding : .5em
-
-#history .commit
-    font-size : smaller
-    font-family : 'Fira Code', monospace
-    width : 7em
-    text-align : center
-#+END_SRC
+    #+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.
+    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
+    #+begin_src toml :tangle soupault.conf
 [widgets.generate-history]
 widget = "preprocess_element"
 selector = "#history"
 command = 'scripts/history.sh templates/history.html'
-action = "replace_content"
-#+END_SRC
+action = "replace_element"
+    #+end_src
 
-This plugin proceeds as follows:
+    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~
+    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.
+    This translates in Bash like this.
 
-#+BEGIN_SRC bash :tangle scripts/history.sh :shebang "#!/usr/bin/bash"
+    #+begin_src bash :tangle scripts/history.sh :shebang "#!/usr/bin/bash"
 function main () {
   local file="${1}"
   local template="${2}"
@@ -431,26 +356,27 @@ function main () {
   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
+    #+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 \
@@ -459,33 +385,35 @@ function gitlog () {
       --pretty=format:'%s%n%h%n%H%n%cs%n' \
       "${file}"
 }
-#+END_SRC
+    #+end_src
 
-This function will generate a sequence of 8 lines containing all the
-relevant information we are looking for, for each commit, namely:
+    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
+    - 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:
+    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
+    #+begin_src bash :results verbatim :exports results :noweb yes
 <<gitlog>>
 gitlog "soupault.org" | head -n8
-#+END_SRC
+    #+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}~.
+    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
+    #+begin_src bash :tangle scripts/history.sh :noweb yes
 function parse_filename () {
   local line="${1}"
   local shrink='s/ *\(.*\) \+|.*/\1/'
@@ -493,18 +421,18 @@ function parse_filename () {
 
   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
+    #+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})"
@@ -562,11 +490,11 @@ function generate_json () {
 
   echo -n "]}"
 }
-#+END_SRC
+    #+end_src
 
-Generating the JSON object for a given commit is as simple as
+    Generating the JSON object for a given commit is as simple as
 
-#+BEGIN_SRC bash :tangle scripts/history.sh :noweb yes
+    #+begin_src bash :tangle scripts/history.sh :noweb yes
 function output_json_entry () {
   local subject="${1}"
   local abbr_hash="${2}"
@@ -585,66 +513,31 @@ function output_json_entry () {
   echo -n ",\"filename\":\"${file}\""
   echo -n "}"
 }
-#+END_SRC
+    #+end_src
 
-And we are done! We can safely call the =main= function to generate
-our revisions table.
+    And we are done! We can safely call the =main= function to generate
+    our revisions table.
 
-#+BEGIN_SRC bash :tangle scripts/history.sh
+    #+begin_src bash :tangle scripts/history.sh
 main "$(cat)" "${1}"
-#+END_SRC
+    #+end_src
 
 ** Rendering Equations Offline
 
 *** 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.
+    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.
+    Using this widgets requires being able to inject raw HTML in
+    input files.
 
 *** Implementation
 
-We will use [[https://katex.org][\im \KaTeX \mi]] to render equations offline. \im \KaTeX \mi
-availability on most systems is unlikely, but it is part of [[https://www.npmjs.com/package/katex][npm]], so we can
-define a minimal ~package.json~ file to fetch it automatically.
-
-#+BEGIN_SRC json :tangle package.json
-{
-  "private": true,
-  "devDependencies": {
-    "katex": "^0.11.1"
-  }
-}
-#+END_SRC
-
-We introduce a Makefile recipe to call ~npm install~. This command produces a
-file called ~package-lock.json~ that we add to ~GENFILES~ to ensure \im \KaTeX
-\mi will be available when ~soupault~ is called.
-
-If ~Soupault.org~ has been modified since the last generation, Babel will
-generate ~package.json~ again. However, if the modifications of ~Soupault.org~
-do not concern ~package.json~, then ~npm install~ will not modify
-~package-lock.json~ and its “last modified” time will not be updated. This means
-that the next time ~make~ will be used, it will replay this recipe again. As a
-consequence, we systematically ~touch~ ~packase-lock.json~ to satisfy ~make~.
-
-#+BEGIN_SRC makefile :tangle katex.mk
-package-lock.json : package.json
-	@cleopatra echo "Fetching" "npm packages"
-	@npm install &>> build.log
-	@touch $@
-
-CONFIGURE += package-lock.json node_modules/
-#+END_SRC
-
-Once installed and available, \im \KaTeX \mi is really simple to use. The
-following script reads (synchronously!) the standard input, renders it using \im
-\KaTeX \mi and outputs the resut to the standard output.
-
-#+BEGIN_SRC js :tangle scripts/katex.js
+    #+begin_src js :tangle scripts/render-equations.js
 var katex = require("katex");
 var fs = require("fs");
 var input = fs.readFileSync(0);
@@ -656,102 +549,160 @@ var html = katex.renderToString(String.raw`${input}`, {
 });
 
 console.log(html)
-#+END_SRC
+    #+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.
+    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
+    #+begin_src toml :tangle soupault.conf
 [widgets.inline-math]
 widget = "preprocess_element"
 selector = ".imath"
-command = "node scripts/katex.js"
+command = "node scripts/render-equations.js"
 action = "replace_content"
 
 [widgets.display-math]
 widget = "preprocess_element"
 selector = ".dmath"
-command = "DISPLAY=1 node scripts/katex.js"
+command = "DISPLAY=1 node scripts/render-equations.js"
 action = "replace_content"
-#+END_SRC
+    #+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"]
+}
 
-The \im\KaTeX\mi font is bigger than the serif font used for this
-website, so we reduce it a bit with a dedicated SASS rule.
+modified-at = {
+  selector = ["#modified-at"]
+}
 
-#+BEGIN_SRC sass :tangle site/style/plugins.sass
-.imath, .dmath
-  font-size : smaller
+created-at = {
+  selector = ["#created-at"]
+}
+   #+end_src
 
-.dmath
-  text-align : center
-#+END_SRC
+** Series Navigation
 
-* *~cleopatra~* Generation Process Definition
+   #+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")
 
-We introduce the ~soupault~ generation process, obviously based on the
-[[https://soupault.neocities.org/][~soupault~ HTML processor]]. The structure of
-a *~cleopatra~* generation process is always the same.
+      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 makefile :tangle soupault.mk :noweb no-export
-<<stages>>
-<<dependencies>>
-<<ad-hoc-cmds>>
-#+END_SRC
+   #+begin_src lua :tangle plugins/series.lua
+function generate_nav_items (cwd, cls, template)
+  local elements = HTML.select(page, cls)
 
-In the rest of this section, we define these three components.
+  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)
 
-** Build Stages
+    HTML.replace_content(
+      element,
+      generate_nav_item_from_title(title_str, url, template)
+    )
 
-From the perspective of *~cleopatra~*, it is a rather simple component, since
-the ~build~ stage is simply a call to ~soupault~, whose outputs are located in a
-single (configurable) directory.
+    i = i + 1
+  end
+end
+   #+end_src
 
-#+NAME: stages
-#+BEGIN_SRC makefile :noweb yes
-soupault-build :
-	@cleopatra echo Running  soupault
-	@soupault
+   #+begin_src lua :tangle plugins/series.lua
+cwd = Sys.dirname(page_file)
 
-ARTIFACTS += <<build-dir>>/
-#+END_SRC
+home_template = 'This article is part of the series “<a href="{{ url }}">{{ title }}</a>.”'
+nav_template = '<a href="{{ url }}">{{ title }}</a>'
 
-** Dependencies
+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
 
-Most of the generation processes (if not all of them) need to declare themselves
-as a prerequisite for ~soupault-build~. If they do not, they will likely be
-executed after ~soupault~ is called.
+#+begin_src toml :tangle soupault.conf
+[widgets.series]
+widget = "series"
+#+end_src
 
-This file defines an auxiliary SASS sheet that needs to be declared as a
-dependency of the build stage of the [[./Theme.org][~theme~ generation
-process]].
+** Injecting Minified CSS
 
-Finally, the offline rendering of equations requires \im \KaTeX \mi to be
-available, so we include the ~katex.mk~ file, and make ~package-lock.json~ (the
-proof that ~npm install~ has been executed) a prerequisite of ~soupault-build~.
+   #+begin_src lua :tangle plugins/css.lua
+style = HTML.select_one(page, "style")
 
-#+NAME: dependencies
-#+BEGIN_SRC makefile
-theme-build : site/style/plugins.sass
-include katex.mk
-soupault-build : package-lock.json
-#+END_SRC
+if style then
+  css = HTML.create_text(Sys.read_file("style.min.css"))
+  HTML.replace_content(style, css)
+end
+   #+end_src
 
-** Ad-hoc Commands
+   #+begin_src toml :tangle soupault.conf
+[widgets.css]
+widget = "css"
+   #+end_src
 
-Finally, this generation process introduces a dedicated (~PHONY~) command to
-start a HTTP server in order to navigate the generated website from a browser.
+** Cleaning-up
 
-#+NAME: ad-hoc-cmds
-#+BEGIN_SRC makefile :noweb yes
-serve :
-	@echo "   start  a python server"
-	@cd <<build-dir>>; python -m http.server 2>/dev/null
+   #+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
 
-.PHONY : serve
-#+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
 
-This command does not assume anything about the current state of generation of
-the project. In particular, it does not check whether or not the ~<<build-dir>>~
-directory exists. The responsibility to use ~make serve~ in a good setting lies
-with final users.
+#+begin_src toml :tangle soupault.conf
+[widgets.clean-up]
+widget = "clean-up"
+#+end_src
diff --git a/site/cleopatra/theme.org b/site/cleopatra/theme.org
index dce9520..9041be8 100644
--- a/site/cleopatra/theme.org
+++ b/site/cleopatra/theme.org
@@ -1,267 +1,471 @@
-#+BEGIN_EXPORT html
-<h1>Theming and Templating</h1>
-#+END_EXPORT
+#+TITLE: Layout and Style
 
-The purpose of this build process is to implement the default layout of this
-website. To that end, it provides a template file (~main.html~), and a
-collection of SASS files that *~cleopatra~* then compiles into a single CSS file
-using ~sassc~.
+#+SERIES: ../cleopatra.html
+#+SERIES_PREV: ./literate-programming.html
+#+SERIES_NEXT: ./soupault.html
 
-We first discuss the structure of the website, by defining the default HTML
-template =soupault= will use to generate the website. Then, we specify its
-minimal design, implemented in SASS. Finally, we discuss the necessary build
-instructions for *~cleopatra~*.
+#+BEGIN_EXPORT html
+<nav id="generate-toc"></nav>
+<div id="history">site/cleopatra/theme.org</div>
+#+END_EXPORT
 
-* Main HTML Template
+* 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.
+
+   #+begin_src css :tangle style.css
+:root {
+    --main-width: 30rem;
+    --gutter-width: 5rem;
+    --margin-width: 15rem;
+    --body-width: calc(var(--main-width) + var(--gutter-width) + var(--margin-width));
+}
+
+@media (max-width: 55rem) {
+    :root {
+        --body-width: var(--main-width);
+    }
+}
+   #+end_src
+
+   #+begin_src css :tangle style.css
+,* {
+    box-sizing: border-box;
+}
+
+.fullwidth {
+    width: var(--body-width);
+}
+
+html {
+    font-size: 1.1rem;
+}
+
+body {
+    line-height: 1.3;
+    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);
+}
+
+main nav {
+    font-style: italic;
+    font-size: smaller;
+    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%;
+}
+
+.sidenote,
+.marginnote {
+    font-size: smaller;
+    float: right;
+    clear: right;
+    margin-right: calc(-1 * (var(--margin-width) + var(--gutter-width)));
+    width: var(--margin-width);
+    position: relative;
+}
+
+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(--body-width);
+    overflow-x: auto;
+    overflow-y: hidden;
+    padding: 1rem 2rem;
+}
+
+main {
+    padding-top: 4.2rem;
+}
+
+h1 {
+    text-align: center;
+}
+
+h2, h3, h4 {
+    font-style: italic;
+}
+
+h1, h2, h3, h4 {
+    font-weight: normal;
+}
+
+dt {
+    font-weight: bold;
+}
+
+div.code,
+span.inlinecode,
+code,
+.doc pre,
+tt,
+.dmath,
+.imath {
+    font-family: monospace;
+    font-size: 80%;
+}
+
+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: 55rem) {
+    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 {
+        width: 100%;
+    }
+}
+   #+end_src
+
+** Colors
+
+   #+begin_src css :tangle style.css
+:root {
+    --bg: white;
+    --bg-plus: #f9f8f4;
+    --current-line: #fbfbfb;
+    --fade: #cfcecb;
+    --fg: #3c3c3c;
+    --fg-plus: #575757;
+    --doc: #ff4c99;
+    --warning: #bd745e;
+    --red: #b3534b;
+    --green: #6d9319;
+    --yellow: #d4b100;
+}
+   #+end_src
+
+   #+begin_src css :tangle style.css
+body {
+    font-family: serif;
+    color: var(--fg);
+    background: var(--bg);
+}
+
+a[href] {
+    color: inherit;
+    text-decoration-color: var(--doc);
+}
+
+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);
+}
+
+.sidenote-number:after,
+.sidenote:before,
+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
 
-#+BEGIN_SRC html  :tangle templates/main.html :noweb yes
+** Icons
+
+   #+begin_src css :tangle style.css
+.icon svg {
+    fill: var(--doc);
+    display: inline;
+    width: 1em;
+    height: .9em;
+    vertical-align: text-top;
+}
+
+.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
+	@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-tags>>
-    <title><!-- page title will be inserted here --></title>
-    <<syncloading_html>>
-    <<asyncloading_html>>
+    <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>>
+  <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>
+    </main>
+  </body>
 </html>
-#+END_SRC
-
-** ~<head>~
-
-#+NAME: meta-tags
-#+BEGIN_SRC html :noweb no-export
-<meta charset="utf-8">
-<meta name="viewport"
-      content="width=device-width, initial-scale=1.0">
-#+END_SRC
-
-*** Assets Loading
-
-#+NAME: syncloading_html
-#+BEGIN_SRC html
-<link href="https://soap.coffee/+vendors/normalize.css.8.0.1/normalize.css"
-      rel="stylesheet">
-<link rel="stylesheet" href="/style/main.css">
-<link rel="icon" type="image/ico" href="/img/merida.webp">
-#+END_SRC
-
-#+NAME: asyncloading_js
-#+BEGIN_SRC js
-let noscript = document.getElementById('asyncloading');
-noscript.insertAdjacentHTML('beforebegin', noscript.innerText);
-noscript.parentNode.removeChild(noscript);
-#+END_SRC
-
-#+NAME: asyncloading_html
-#+BEGIN_SRC html
-<noscript id="asyncloading">
-  <link href="https://soap.coffee/+vendors/fira-code.2+swap/font.css"
-        rel="stylesheet">
-  <link href="https://soap.coffee/+vendors/katex.0.11.1+swap/katex.css"
-        rel="stylesheet">
-  <link href="https://soap.coffee/+vendors/fork-awesome.1.1.7+swap/css/fork-awesome.min.css"
-        rel="stylesheet">
-</noscript>
-#+END_SRC
-
-** ~body~
-
-#+NAME: body
-#+BEGIN_SRC html :noweb no-export
-<body>
-  <header>
-    <a href="/">Technical Articles</a> /
-    <a href="/opinions">Opinions</a> /
-    <a href="/news">News</a> /
-    <a href="/projects">Projects</a>
-  </header>
-  <main>
-  <!-- page content will be inserted here -->
-  </main>
-  <footer>
-    <img src="https://soap.coffee/~lthms/img/merida.webp"
-         alt="Merida from the movie Ralph 2.0 from Disney is the
-              avatar I use most of the time on the Internet"
-         title="lthms’ avatar" />
-
-    <p>
-      Hi, I’m <strong>lthms</strong>, and this is my humble corner of the
-      Internet. You are very welcome here! If you are interested in
-      <em>functional programming</em>, <em>formal verification</em>, or <em>free
-      software projects in the making</em>, you may even enjoy your stay!
-    </p>
-
-    <p>
-      This website has been generated using a collection of <a
-      href="/posts/Thanks.html">awesome free software projects</a>. You can have
-      a look at <a href="https://code.soap.coffee/writing/lthms.git/">the source
-      of this website</a> or <a href="/cleopatra.html">how it is being
-      generated</a>, and if you run into an error, feel free to <a
-      href="mailto:lthms@soap.coffee">shoot me a friendly email</a>.
-    </p>
-  </footer>
-  <script>
-    <<asyncloading_js>>
-  </script>
-</body>
-#+END_SRC
-
-* Main SASS File
-
-First, we introduce a set of variables.
-
-#+BEGIN_SRC sass :tangle site/style/main.sass
-$content-width : 30rem
-$large-side-margin : 7rem
-$small-side-margin : 2rem
-$monospace-color : #FF006D
-#+END_SRC
-
-Then, we introduce a key CSS variable whose definition will change according to
-the current width of the page (something we cannot achieve with SASS variables,
-whose behavior is purely static).
-
-#+BEGIN_SRC sass :tangle site/style/main.sass
-\:root
-    @media screen and (min-width: calc(#{$content-width} + 2 * #{$large-side-margin}))
-        --side-margin : #{$large-side-margin}
-    @media screen and (max-width: calc(#{$content-width} + 2 * #{$large-side-margin}))
-        --side-margin : #{$small-side-margin}
-#+END_SRC
-
-Then, we style!
-
-#+BEGIN_SRC sass :tangle site/style/main.sass
-*
-    box-sizing : border-box
-
-html
-    width : 100%
-    height : 100%
-    font-size : 100%
-    font-weight : normal
-    color : #222
-
-a
-    color : black
-
-a:visited
-    color : #222
-
-body
-    font-family : serif
-    margin : 0 var(--side-margin) 0 calc(var(--side-margin) - 2rem) !important
-    padding : 2rem
-    @media screen and (min-width: calc(#{$content-width} + 2 * #{$large-side-margin}))
-        border-left : 1px solid #ccc
-
-main p,
-main h1,
-main h2,
-main h3,
-main h4,
-main h5,
-main h6,
-main ul,
-main dl,
-main ol,
-header,
-footer
-    max-width : $content-width
-    line-height : 140%
-
-main h1,
-main h2,
-main h3,
-main h4,
-main h5,
-main h6
-    font-weight : bold
-    color : #0c0016
-
-header a,
-footer p
-    font-size : 90%
-
-main
-    padding-top : 4rem
-    padding-bottom : 4rem
-
-    dl dd
-        margin-left : 0
-
-    dl dt
-        font-weight : bold
-
-    dl dt:not(:first-child)
-        padding-top : .5rem
-
-    details
-        font-size : 90%
-        filter : opacity(0.8)
-
-footer img
-    border-radius : 100%
-    max-width : 7rem
-    float : right
-    margin-left : 1rem
-    margin-bottom : 1rem
-
-pre
-    padding-left : 1.5rem
-    padding-right : 1.5rem
-    overflow-x : auto
-
-code,
-tt,
-pre
-    font-family : 'Fira Code', monospace
-    font-size : 80%
-    line-height : 140%
-    color : $monospace-color
-
-#gallery
-    display : flex
-    flex-wrap : wrap
-    align-content : flex-start
-
-    img
-        max-width : 20rem
-
-@import plugins
-@import org
-@import coq
-#+END_SRC
-
-* Build Instructions
-
-The build instruction are pretty straightforward. We start by how to compile the
-main CSS file.
-
-#+BEGIN_SRC makefile :tangle theme.mk
-SASS := $(wildcard site/style/*.sass)
-MAIN_SASS := site/style/main.sass
-CSS := $(MAIN_SASS:.sass=.css)
-
-${CSS} : ${SASS}
-	@cleopatra echo Compiling  "${CSS}"
-	@sassc --style=compressed --sass ${MAIN_SASS} ${CSS}
-#+END_SRC
-
-Since the HTML template does not need any particular processing, the
-=theme-build= phase is only responsible for generating the main CSS file.  The
-[[./soupault.org][=soupault= build phase]] needs to start after the CSS file is
-compiled (since it copies all relevant files to the ~build/~ directory), so we
-explicit this dependency.
-
-#+BEGIN_SRC makefile :tangle theme.mk
-theme-build : ${CSS}
-soupault-build : theme-build
-#+END_SRC
-
-Therefore, at the end of this generation process only one file has been
-generated.
-
-#+BEGIN_SRC makefile :tangle theme.mk
-ARTIFACTS += ${CSS}
-#+END_SRC
+  #+end_src
diff --git a/site/coq.org b/site/coq.org
new file mode 100644
index 0000000..d13d387
--- /dev/null
+++ b/site/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.
+
+- [[./posts/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.
+
+- [[./posts/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.
+
+- [[./posts/RewritingInCoq.html][Rewriting in Coq]] ::
+  The ~rewrite~ tactics are really useful, since they are not limited to the Coq
+  built-in equality relation.
+
+- [[./posts/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.
+
+- [[./posts/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.
+
+- [[./posts/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/haskell.org b/site/haskell.org
new file mode 100644
index 0000000..c18fbb7
--- /dev/null
+++ b/site/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.
+
+- [[./posts/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/img/icons.svg b/site/img/icons.svg
new file mode 100644
index 0000000..917a417
--- /dev/null
+++ b/site/img/icons.svg
@@ -0,0 +1,39 @@
+<svg version="1.1" xmlns="http://www.w3.org/2000/svg">
+  <symbol id="external-link" viewBox="0 0 511.626 511.627">
+    <path d="M392.857,292.354h-18.274c-2.669,0-4.859,0.855-6.563,2.573c-1.718,1.708-2.573,3.897-2.573,6.563v91.361
+             c0,12.563-4.47,23.315-13.415,32.262c-8.945,8.945-19.701,13.414-32.264,13.414H82.224c-12.562,0-23.317-4.469-32.264-13.414
+             c-8.945-8.946-13.417-19.698-13.417-32.262V155.31c0-12.562,4.471-23.313,13.417-32.259c8.947-8.947,19.702-13.418,32.264-13.418
+             h200.994c2.669,0,4.859-0.859,6.57-2.57c1.711-1.713,2.566-3.9,2.566-6.567V82.221c0-2.662-0.855-4.853-2.566-6.563
+             c-1.711-1.713-3.901-2.568-6.57-2.568H82.224c-22.648,0-42.016,8.042-58.102,24.125C8.042,113.297,0,132.665,0,155.313v237.542
+             c0,22.647,8.042,42.018,24.123,58.095c16.086,16.084,35.454,24.13,58.102,24.13h237.543c22.647,0,42.017-8.046,58.101-24.13
+             c16.085-16.077,24.127-35.447,24.127-58.095v-91.358c0-2.669-0.856-4.859-2.574-6.57
+             C397.709,293.209,395.519,292.354,392.857,292.354z"/>
+    <path d="M506.199,41.971c-3.617-3.617-7.905-5.424-12.85-5.424H347.171c-4.948,0-9.233,1.807-12.847,5.424
+             c-3.617,3.615-5.428,7.898-5.428,12.847s1.811,9.233,5.428,12.85l50.247,50.248L198.424,304.067
+             c-1.906,1.903-2.856,4.093-2.856,6.563c0,2.479,0.953,4.668,2.856,6.571l32.548,32.544c1.903,1.903,4.093,2.852,6.567,2.852
+             s4.665-0.948,6.567-2.852l186.148-186.148l50.251,50.248c3.614,3.617,7.898,5.426,12.847,5.426s9.233-1.809,12.851-5.426
+             c3.617-3.616,5.424-7.898,5.424-12.847V54.818C511.626,49.866,509.813,45.586,506.199,41.971z"/>
+  </symbol>
+  <symbol id="github" viewBox="0 0 438.549 438.549">
+    <path d="M409.132,114.573c-19.608-33.596-46.205-60.194-79.798-79.8C295.736,15.166,259.057,5.365,219.271,5.365
+             c-39.781,0-76.472,9.804-110.063,29.408c-33.596,19.605-60.192,46.204-79.8,79.8C9.803,148.168,0,184.854,0,224.63
+             c0,47.78,13.94,90.745,41.827,128.906c27.884,38.164,63.906,64.572,108.063,79.227c5.14,0.954,8.945,0.283,11.419-1.996
+             c2.475-2.282,3.711-5.14,3.711-8.562c0-0.571-0.049-5.708-0.144-15.417c-0.098-9.709-0.144-18.179-0.144-25.406l-6.567,1.136
+             c-4.187,0.767-9.469,1.092-15.846,1c-6.374-0.089-12.991-0.757-19.842-1.999c-6.854-1.231-13.229-4.086-19.13-8.559
+             c-5.898-4.473-10.085-10.328-12.56-17.556l-2.855-6.57c-1.903-4.374-4.899-9.233-8.992-14.559
+             c-4.093-5.331-8.232-8.945-12.419-10.848l-1.999-1.431c-1.332-0.951-2.568-2.098-3.711-3.429c-1.142-1.331-1.997-2.663-2.568-3.997
+             c-0.572-1.335-0.098-2.43,1.427-3.289c1.525-0.859,4.281-1.276,8.28-1.276l5.708,0.853c3.807,0.763,8.516,3.042,14.133,6.851
+             c5.614,3.806,10.229,8.754,13.846,14.842c4.38,7.806,9.657,13.754,15.846,17.847c6.184,4.093,12.419,6.136,18.699,6.136
+             c6.28,0,11.704-0.476,16.274-1.423c4.565-0.952,8.848-2.383,12.847-4.285c1.713-12.758,6.377-22.559,13.988-29.41
+             c-10.848-1.14-20.601-2.857-29.264-5.14c-8.658-2.286-17.605-5.996-26.835-11.14c-9.235-5.137-16.896-11.516-22.985-19.126
+             c-6.09-7.614-11.088-17.61-14.987-29.979c-3.901-12.374-5.852-26.648-5.852-42.826c0-23.035,7.52-42.637,22.557-58.817
+             c-7.044-17.318-6.379-36.732,1.997-58.24c5.52-1.715,13.706-0.428,24.554,3.853c10.85,4.283,18.794,7.952,23.84,10.994
+             c5.046,3.041,9.089,5.618,12.135,7.708c17.705-4.947,35.976-7.421,54.818-7.421s37.117,2.474,54.823,7.421l10.849-6.849
+             c7.419-4.57,16.18-8.758,26.262-12.565c10.088-3.805,17.802-4.853,23.134-3.138c8.562,21.509,9.325,40.922,2.279,58.24
+             c15.036,16.18,22.559,35.787,22.559,58.817c0,16.178-1.958,30.497-5.853,42.966c-3.9,12.471-8.941,22.457-15.125,29.979
+             c-6.191,7.521-13.901,13.85-23.131,18.986c-9.232,5.14-18.182,8.85-26.84,11.136c-8.662,2.286-18.415,4.004-29.263,5.146
+             c9.894,8.562,14.842,22.077,14.842,40.539v60.237c0,3.422,1.19,6.279,3.572,8.562c2.379,2.279,6.136,2.95,11.276,1.995
+             c44.163-14.653,80.185-41.062,108.068-79.226c27.88-38.161,41.825-81.126,41.825-128.906
+             C438.536,184.851,428.728,148.168,409.132,114.573z"/>
+  </symbol>
+</svg>
diff --git a/site/img/merida.webp b/site/img/merida.webp
deleted file mode 100644
index c0e6354..0000000
Binary files a/site/img/merida.webp and /dev/null differ
diff --git a/site/index.org b/site/index.org
index e1b61bc..e4a7e18 100644
--- a/site/index.org
+++ b/site/index.org
@@ -1,76 +1,27 @@
-#+OPTIONS: toc:nil num:nil
-
-#+BEGIN_EXPORT html
-<h1>Technical Articles</h1>
-#+END_EXPORT
+#+TITLE: Technical Articles
 
 Over the past years, I have tried to capitalize on my findings. What I have
 lacked in regularity I made up for in subject exoticism.
 
-If you like what you read, have a question or for any other reasons really, you
-can shoot an [[mailto:lthms@soap.coffee][email]], or start a discussion on
-whichever site you like (I personnaly enjoy
-[[https://lobste.rs/search?q=domain%3Asoap.coffee&what=stories&order=relevance][Lobste.rs]]
-very much).
+If you like what you read, have a question or for any other reasons
+really, you can shoot an [[mailto:lthms@soap.coffee][email]], or start a discussion on whichever
+site you like[fn::I personnaly enjoy [[https://lobste.rs/search?q=domain%3Asoap.coffee&what=stories&order=relevance][Lobste.rs]] very much].
 
 * About Coq
-:PROPERTIES:
-:CUSTOM_ID: coq
-:END:
-
-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.
-
-- [[./posts/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.
-
-- [[./posts/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.
-
-- [[./posts/RewritingInCoq.html][Rewriting in Coq]] ::
-  The ~rewrite~ tactics are really useful, since they are not limited to the Coq
-  built-in equality relation.
+  :PROPERTIES:
+  :CUSTOM_ID: coq
+  :END:
 
-- [[./posts/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.
-
-- [[./posts/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.
-
-- [[./posts/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.
+  #+include: ./coq.org
 
 * About Haskell
 
-Haskell is a pure, lazy, functional programming language with a very expressive
-type system.
-
-- [[./posts/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.
+  #+include: ./haskell.org
 
 * Miscellaneous
 
-- [[./posts/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.
+  #+include: ./miscellaneous.org
+
+* About this Website
+
+  #+include: ./meta.org
diff --git a/site/meta.org b/site/meta.org
new file mode 100644
index 0000000..d5ce4b4
--- /dev/null
+++ b/site/meta.org
@@ -0,0 +1,23 @@
+#+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.
+
+- [[./posts/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.
+
+- [[./cleopatra.org][A Series on Generating this Website]] ::
+  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.  As a result, 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.
diff --git a/site/miscellaneous.org b/site/miscellaneous.org
new file mode 100644
index 0000000..c348c28
--- /dev/null
+++ b/site/miscellaneous.org
@@ -0,0 +1,14 @@
+#+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.
+
+- [[./posts/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.
diff --git a/site/news/index.html b/site/news/index.html
index 5a0331e..43315c0 100644
--- a/site/news/index.html
+++ b/site/news/index.html
@@ -3,6 +3,21 @@
 <h2>2021</h2>
 
 <ul>
+  <li>
+    On <strong>March 4, 2021</strong>,
+    FreeSpec packages
+    (<code>coq-freespec-core.0.3</code>, <code>coq-freespec-ffi.0.3</code>
+    and
+    <code>coq-freespec-exec.0.3</code>) have finally been released.
+  </li>
+  <li>
+    On <strong>March 1st, 2021</strong>, <code>coq-coqffi.1.0.0~beta5</code>
+    has been released.
+  </li>
+  <li>
+    On <strong>February 24, 2021</strong>, <code>coq-coqffi.1.0.0~beta4</code>
+    has been released.
+  </li>
   <li>
     On <strong>January 27, 2021</strong>,
     <a href="https://github.com/lthms/FreeSpec">FreeSpec</a> has been
diff --git a/site/opinions/MonadTransformers.org b/site/opinions/MonadTransformers.org
index 7296f08..0424c7b 100644
--- a/site/opinions/MonadTransformers.org
+++ b/site/opinions/MonadTransformers.org
@@ -1,12 +1,12 @@
-#+BEGIN_EXPORT html
-<h1>Monad Transformers are a Great Abstraction</h1>
+#+TITLE: Monad Transformers are a Great Abstraction
+
+#+SERIES: ../opinions/index.html
 
+#+BEGIN_EXPORT html
 <p>This article has originally been published on <span
 id="original-created-at">July 15, 2017</span>.</p>
 #+END_EXPORT
 
-#+OPTIONS: toc:nil
-
 #+BEGIN_EXPORT html
 <div id="history">site/opinions/MonadTransformers.org</div>
 #+END_EXPORT
@@ -14,8 +14,8 @@ id="original-created-at">July 15, 2017</span>.</p>
 Monads are hard to get right. I think it took me around a year of Haskelling to
 feel like I understood them. The reason is, to my opinion, there is not such
 thing as /the/ Monad. It is even the contrary. When someone asks me how I would
-define Monads in only a few words, [[https://techn.ical.ist/@lthms/590439][I say Monad is a convenient formalism to
-chain specific computations]]. Once I’ve got that, I started noticing “monadic
+define Monads in only a few words, I say monads are a convenient formalism to
+chain specific computations. Once I’ve got that, I started noticing “monadic
 construction” everywhere, from the Rust ~?~ operator to the [[https://blog.drewolson.org/elixirs-secret-weapon/][Elixir ~with~
 keyword]].
 
@@ -46,7 +46,6 @@ issue with the Monad Transformers.
 #+BEGIN_SRC diff
 -type Builder = StateT Text IO
 +type Builder = StateT Text (ReaderT Language IO)
-
 #+END_SRC
 
 As you may have already understood, I wasn't using the “raw” ~State~ Monad, but
diff --git a/site/opinions/index.org b/site/opinions/index.org
index 0be267e..58b0407 100644
--- a/site/opinions/index.org
+++ b/site/opinions/index.org
@@ -1,8 +1,4 @@
-#+options: num:nil
-
-#+BEGIN_EXPORT html
-<h1>Opinions</h1>
-#+END_EXPORT
+#+TITLE: Opinions
 
 I may have some opinions on some topics, and sometimes I may want to share
 them. However, I strongly believe facts and opinions are two differents things,
diff --git a/site/posts/AlgebraicDatatypes.v b/site/posts/AlgebraicDatatypes.v
index 1b24520..f32551c 100644
--- a/site/posts/AlgebraicDatatypes.v
+++ b/site/posts/AlgebraicDatatypes.v
@@ -1,3 +1,7 @@
+(** #<nav><p class="series">../coq.html</p>
+     <p class="series-prev">./ClightIntroduction.html</p>
+     <p class="series-next">./Coqffi.html</p></nav># *)
+
 (** * Proving Algebraic Datatypes are “Algebraic” *)
 
 (** Several programming languages allow programmers to define (potentially
@@ -93,7 +97,7 @@ Inductive prod (A B : Type) : Type :=
 | pair : A -> B -> prod A B
 >>
 
-    #<div id="generate-toc"></div>#
+    #<nav id="generate-toc"></nav>#
 
     #<div id="history">site/posts/AlgebraicDatatypes.v</div># *)
 
diff --git a/site/posts/ClightIntroduction.v b/site/posts/ClightIntroduction.v
index 4bd9a52..85d084b 100644
--- a/site/posts/ClightIntroduction.v
+++ b/site/posts/ClightIntroduction.v
@@ -1,3 +1,7 @@
+(** #<nav><p class="series">../coq.html</p>
+     <p class="series-prev">./RewritingInCoq.html</p>
+     <p class="series-next">./AlgebraicDatatypes.html</p></nav># *)
+
 (** * A Study of Clight and its Semantics *)
 (* begin hide *)
 From Coq Require Import List.
@@ -12,7 +16,7 @@ Import ListNotations.
     challenged myself to study Clight and its semantics. This write-up is the
     result of this challenge, written as I was progressing.
 
-    #<div id="generate-toc"></div>#
+    #<nav id="generate-toc"></nav>#
 
     #<div id="history">site/posts/ClightIntroduction.v</div># *)
 
diff --git a/site/posts/Coqffi.org b/site/posts/Coqffi.org
index 3d8b867..f8d9695 100644
--- a/site/posts/Coqffi.org
+++ b/site/posts/Coqffi.org
@@ -1,6 +1,7 @@
-#+BEGIN_EXPORT html
-<h1>A Series on <code>coqffi</code></h1>
-#+END_EXPORT
+#+TITLE: A series on ~coqffi~
+
+#+SERIES: ../coq.html
+#+SERIES_PREV: AlgebraicDatatypes.html
 
 ~coqffi~ generates Coq FFI modules from compiled OCaml interface
 modules (~.cmi~). In practice, it greatly reduces the hassle to mix
diff --git a/site/posts/CoqffiEcho.org b/site/posts/CoqffiEcho.org
index 04fa253..81ae0e9 100644
--- a/site/posts/CoqffiEcho.org
+++ b/site/posts/CoqffiEcho.org
@@ -1,6 +1,7 @@
-#+BEGIN_EXPORT html
-<h1>Implementing an Echo Server in Coq with <code>coqffi</code></h1>
-#+END_EXPORT
+#+TITLE: Implementing an Echo Server in Coq with ~coqffi~
+
+#+SERIES: ./Coqffi.html
+#+SERIES_PREV: ./CoqffiIntro.html
 
 #+NAME: coqffi_output
 #+BEGIN_SRC sh :results output :exports none :var mod=""
@@ -21,9 +22,8 @@ Besides, this article is a literate program, and you can download
 [[/files/coqffi-tutorial.tar.gz][the resulting source tree]] if you
 want to try to read the source directly, or modify it to your taste.
 
-#+TOC: headlines 2
-
 #+BEGIN_EXPORT html
+<nav id="generate-toc"></nav>
 <div id="history">site/posts/CoqffiEcho.org</div>
 #+END_EXPORT
 
diff --git a/site/posts/CoqffiIntro.org b/site/posts/CoqffiIntro.org
index 053826b..411f3cf 100644
--- a/site/posts/CoqffiIntro.org
+++ b/site/posts/CoqffiIntro.org
@@ -1,6 +1,7 @@
-#+BEGIN_EXPORT html
-<h1><code>coqffi</code> in a Nutshell</h1>
-#+END_EXPORT
+#+TITLE: ~coqffi~ in a Nutshell
+
+#+SERIES: ./Coqffi.html
+#+SERIES_NEXT: ./CoqffiEcho.html
 
 For each entry of a ~cmi~ file (a /compiled/ ~mli~ file), ~coqffi~
 tries to generate an equivalent (from the extraction mechanism
@@ -10,9 +11,8 @@ perspective) Coq definition. In this article, we walk through how
 Note that we do not dive into the vernacular commands ~coqffi~
 generates. They are of no concern for users of ~coqffi~.
 
-#+TOC: headlines 2
-
 #+BEGIN_EXPORT html
+<nav id="generate-toc"></nav>
 <div id="history">site/posts/CoqffiIntro.org</div>
 #+END_EXPORT
 
diff --git a/site/posts/ExtensibleTypeSafeErrorHandling.org b/site/posts/ExtensibleTypeSafeErrorHandling.org
index cc276f0..e817e31 100644
--- a/site/posts/ExtensibleTypeSafeErrorHandling.org
+++ b/site/posts/ExtensibleTypeSafeErrorHandling.org
@@ -1,13 +1,14 @@
-#+BEGIN_EXPORT html
-<h1>Extensible Type-Safe Error Handling in Haskell</h1>
+#+TITLE: Extensible Type-Safe Error Handling in Haskell
+
+#+SERIES: ../haskell.html
 
+#+BEGIN_EXPORT html
 <p>This article has originally been published on <span
 id="original-created-at">February 04, 2018</span>.</p>
 #+END_EXPORT
 
-#+TOC: headlines 2
-
 #+BEGIN_EXPORT html
+<nav id="generate-toc"></nav>
 <div id="history">site/posts/ExtensibleTypeSafeErrorHandling.org</div>
 #+END_EXPORT
 
diff --git a/site/posts/Ltac.org b/site/posts/Ltac.org
index caba76c..37580cd 100644
--- a/site/posts/Ltac.org
+++ b/site/posts/Ltac.org
@@ -1,12 +1,16 @@
-#+BEGIN_EXPORT html
-<h1>A Series on Ltac</h1>
-#+END_EXPORT
+#+TITLE: A Series on Ltac
+
+#+SERIES: ../coq.html
+#+SERIES_PREV: ./StronglySpecifiedFunctions.html
+#+SERIES_NEXT: ./RewritingInCoq.html
 
 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.
+approach to write proofs, which tends to bias how it is introduced to
+new Coq users[fn::I know /I/ was introduced to Coq in a similar way in
+my 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.
 
 - [[./LtacMetaprogramming.html][Ltac is an Imperative Metaprogramming Language]] ::
   Ltac generates terms, therefore it is a metaprogramming language. It does it
diff --git a/site/posts/LtacMetaprogramming.v b/site/posts/LtacMetaprogramming.v
index 2a4fe50..6b086e3 100644
--- a/site/posts/LtacMetaprogramming.v
+++ b/site/posts/LtacMetaprogramming.v
@@ -1,3 +1,6 @@
+(** #<nav><p class="series">Ltac.html</p>
+     <p class="series-next">LtacPatternMatching.html</p></nav># *)
+
 (** * Ltac is an Imperative Metaprogramming Language *)
 
 (** #<div id="history">site/posts/LtacMetaprogramming.v</div># *)
diff --git a/site/posts/LtacPatternMatching.v b/site/posts/LtacPatternMatching.v
index d52d0bf..a0b8a4d 100644
--- a/site/posts/LtacPatternMatching.v
+++ b/site/posts/LtacPatternMatching.v
@@ -1,3 +1,7 @@
+(** #<nav><p class="series">Ltac.html</p>
+     <p class="series-prev">./LtacMetaprogramming.html</p>
+     <p class="series-next">./MixingLtacAndGallina.html</p></nav># *)
+
 (** * Pattern Matching on Types and Contexts  *)
 
 (** In the #<a href="LtacMetaprogramming.html">#previous article#</a># of our
@@ -11,7 +15,7 @@
     contexts. In this article, we give a short introduction on this feature of
     key importance. *)
 
-(** #<div id="generate-toc"></div>#
+(** #<nav id="generate-toc"></nav>#
 
     #<div id="history">site/posts/LtacPatternMatching.v</div># *)
 
@@ -137,8 +141,8 @@ Ltac not_param_type x :=
   | _ => idtac
   end.
 
-(** Both <<not_param_type (@nil nat)>> of type [list nat] and <<(@eq_refl nat
-    0)>> of type [0 = 0] fail, but <<not_param_type 0>> of type [nat]
+(** Both <<not_param_type (@nil nat)>> of type [list nat] and
+    <<(@eq_refl nat 0)>> of type [0 = 0] fail, but <<not_param_type 0>> of type [nat]
     succeeds. *)
 
 (** ** Pattern Matching on the Context with [goal] *)
diff --git a/site/posts/MixingLtacAndGallina.v b/site/posts/MixingLtacAndGallina.v
index 4e6b28d..d77cd8a 100644
--- a/site/posts/MixingLtacAndGallina.v
+++ b/site/posts/MixingLtacAndGallina.v
@@ -1,3 +1,6 @@
+(** #<nav><p class="series">Ltac.html</p>
+     <p class="series-prev">./LtacPatternMatching.html</p></nav># *)
+
 (** * Mixing Ltac and Gallina for Fun and Profit *)
 
 (** One of the most misleading introduction to Coq is to say that “Gallina is
@@ -20,7 +23,7 @@
     It turns out these features are more than handy when it comes to
     metaprogramming (that is, the generation of programs by programs). *)
 
-(** #<div id="generate-toc"></div>#
+(** #<nav id="generate-toc"></nav>#
 
     #<div id="history">site/posts/MixingLtacAndGallina.v</div># *)
 
diff --git a/site/posts/RewritingInCoq.v b/site/posts/RewritingInCoq.v
index 0020a3e..a285e09 100644
--- a/site/posts/RewritingInCoq.v
+++ b/site/posts/RewritingInCoq.v
@@ -1,3 +1,7 @@
+(** #<nav><p class="series">../coq.html</p>
+     <p class="series-prev">./Ltac.html</p>
+     <p class="series-next">./ClightIntroduction.html</p></nav># *)
+
 (** * Rewriting in Coq *)
 
 (** I have to confess something. In the codebase of SpecCert lies a shameful
@@ -9,7 +13,7 @@
     13, 2017</span> how it is possible to rewrite a term in a proof using a
     ad-hoc equivalence relation and, when necessary, a proper morphism. *)
 
-(** #<div id="generate-toc"></div>#
+(** #<nav id="generate-toc"></nav>#
 
     #<div id="history">site/posts/RewritingInCoq.v</div># *)
 
diff --git a/site/posts/StronglySpecifiedFunctions.org b/site/posts/StronglySpecifiedFunctions.org
index 805b944..83148c6 100644
--- a/site/posts/StronglySpecifiedFunctions.org
+++ b/site/posts/StronglySpecifiedFunctions.org
@@ -1,8 +1,7 @@
-#+OPTIONS: toc:nil num:nil
+#+TITLE: A Series on Strongly-Specified Functions in Coq
 
-#+BEGIN_EXPORT html
-<h1>A Series on Strongly-Specified Functions in Coq</h1>
-#+END_EXPORT
+#+SERIES: ../coq.html
+#+SERIES_NEXT: ./Ltac.html
 
 Using dependent types and the ~Prop~ sort, it becomes possible to specify
 functions whose arguments and results are constrained by properties.  Using such
diff --git a/site/posts/StronglySpecifiedFunctionsProgram.v b/site/posts/StronglySpecifiedFunctionsProgram.v
index 1b4ab5f..c5763ea 100644
--- a/site/posts/StronglySpecifiedFunctionsProgram.v
+++ b/site/posts/StronglySpecifiedFunctionsProgram.v
@@ -5,7 +5,7 @@
     to write strongly-specified functions in Coq. You can read the previous part
     #<a href="./StronglySpecifiedFunctionsRefine.html">here</a>#. # *)
 
-(** #<div id="generate-toc"></div>#
+(** #<nav id="generate-toc"></nav>#
 
     #<div id="history">site/posts/StronglySpecifiedFunctionsProgram.v</div># *)
 
@@ -341,7 +341,8 @@ Defined.
 (** val extract : 'a1 vector -> nat -> nat -> 'a1 vector **)
 let extract v e b =
   take (drop v b) (sub e b)
->> *)
+>>
+    *)
 
 (** I was pretty happy, so I tried some more. Each time, using [nth], I managed
     to write a precise post condition and to prove it holds true. For instance,
@@ -467,7 +468,8 @@ cannot be applied to the terms
  "b" : "Type"
 The 3rd term has type "Type" which should be coercible
 to "nat".
->> *)
+>>
+    *)
 
 #[program]
 Fixpoint map2 {a b c n}
@@ -520,4 +522,5 @@ cannot be applied to the terms
  "wildcard'" : "vector A n'"
 The 3rd term has type "vector A n'" which should be
 coercible to "nat".
->> *)
+>>
+    *)
diff --git a/site/posts/StronglySpecifiedFunctionsRefine.v b/site/posts/StronglySpecifiedFunctionsRefine.v
index 1d4ec2e..4ffb385 100644
--- a/site/posts/StronglySpecifiedFunctionsRefine.v
+++ b/site/posts/StronglySpecifiedFunctionsRefine.v
@@ -19,7 +19,7 @@
     return value is the list passed in argument in which the first
     element has been removed for example.
 
-    #<div id="generate-toc"></div>#
+    #<nav id="generate-toc"></nav>#
 
     #<div id="history">site/posts/StronglySpecifiedFunctionsRefine.v</div># *)
 
@@ -54,7 +54,8 @@ Import ListNotations.
 <<
 Definition predicate_b (args) :=
   if predicate_dec args then true else false.
->> *)
+>>
+    *)
 
 (** *** Defining the <<empty>> predicate *)
 
@@ -174,7 +175,8 @@ Definition pop {a} (l : list a) (h : ~ empty l)
   h : ~ empty l
   ============================
   list a
->> *)
+>>
+    *)
 
 (** Using the [refine] tactic naively, for instance this way:  *)
 
@@ -280,7 +282,8 @@ Definition pop {a} (l : list a | ~ empty l)
   equ : proj1_sig l = []
   ============================
   {l' : list a | exists a0 : a, proj1_sig l = a0 :: l'}
->> *)
+>>
+    *)
 
   + destruct l as [l nempty]; cbn in *.
     rewrite equ in nempty.
@@ -299,7 +302,8 @@ Definition pop {a} (l : list a | ~ empty l)
   equ : proj1_sig l = a0 :: rst
   ============================
   exists a1 : a, proj1_sig l = a1 :: rst
->> *)
+>>
+    *)
 
   + destruct l as [l nempty]; cbn in *.
     rewrite equ.
@@ -339,7 +343,8 @@ Definition push {a} (l : list a) (x : a)
 <<
 let push l a =
   Cons (a, l)
->> *)
+>>
+    *)
 
 (** ** Defining [head] *)
 
@@ -376,7 +381,8 @@ Defined.
 let head = function
 | Nil -> assert false (* absurd case *)
 | Cons (a, l0) -> a
->> *)
+>>
+    *)
 
 (** ** Conclusion & Moving Forward *)
 
diff --git a/site/posts/Thanks.org b/site/posts/Thanks.org
index ba76a88..c20f1e5 100644
--- a/site/posts/Thanks.org
+++ b/site/posts/Thanks.org
@@ -1,18 +1,15 @@
-#+BEGIN_EXPORT html
-<h1>Thanks!</h1>
-
-<article class="index">
-#+END_EXPORT
+#+TITLE: 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 “main” ones.
+#+SERIES: ../meta.html
+#+SERIES_NEXT: ../cleopatra.html
 
-#+OPTIONS: toc:nil num:nil
+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.
 
 #+BEGIN_EXPORT html
-<div id="generate-toc"></div>
-
+<nav id="generate-toc"></nav>
 <div id="history">site/posts/Thanks.org</div>
 #+END_EXPORT
 
@@ -35,9 +32,6 @@ least to try keeping up-to-date a curated description of the “main” ones.
 - [[https://soupault.neocities.org][soupault]] ::
   Soupault is a static website generator and HTML processor written by [[https://www.baturin.org/][Daniil
   Baturin]].
-- [[https://github.com/sass/sassc][~sassc~]] ::
-  ~sassc~ is a compiler for SASS files (actually, a wrapper around [[https://github.com/sass/libsass][~libsass~]]),
-  authored by [[https://github.com/akhleung][Aaron Leung]], [[https://github.com/hcatlin][Hampton Catlin]], [[https://github.com/mgreter][Marcel Greter]], and [[https://github.com/xzyfer][Michael Mifsud]].
 - [[https://cleopatra.soap.coffee][~cleopatra~]] ::
   ~cleopatra~ is a generic, extensible toolchain with facilities for
   literate programming projects using Org mode and more. I have
@@ -45,25 +39,9 @@ least to try keeping up-to-date a curated description of the “main” ones.
 
 * Frontend
 
-- [[https://forkaweso.me/Fork-Awesome/][Fork Awesome]] ::
-  Fork Awesome is a collection of icons for the web. It is a community fork of
-  [[https://fontawesome.com/][Font Awesome]].
 - [[https://katex.org][\im \KaTeX \mi]] ::
   \im \KaTeX \mi is the “fastest” math typesetting library for the web, and is
-  uses to render inline mathematics in my posts at build time. It has been
+  used to render inline mathematics in my posts at build time. It has been
   created by [[https://github.com/xymostech][Emily Eisenberg]] and
   [[https://sophiebits.com/][Sophie Alpert]], with the help of
   [[https://github.com/KaTeX/KaTeX/graphs/contributors][many contributors]].
-- [[https://github.com/tonsky/FiraCode][Fira Code]] ::
-  Fira Code is a monospaced font by [[https://github.com/tonsky][Nikita Prokopov]] inspired with Fira Mono by
-  the [[https://www.mozilla.org/en-US/][Mozilla Foundation]], with “programming ligatures” (/e.g./, =>>==, ====,
-  =!==, etc.), and it is used here for verbatim content (principally source
-  code).
-- [[https://github.com/productiontype/spectral][Spectral]] ::
-  Spectral is an original typeface designed by Production Type,
-  primarily intended for use inside Google’s Docs and Slides.  It is
-  used as the main font of this website.
-
-#+BEGIN_EXPORT html
-</article>
-#+END_EXPORT
-- 
cgit v1.2.3