6 files changed, 104 insertions, 16 deletions
diff --git a/site/posts/StronglySpecifiedFunctions.v b/site/posts/StronglySpecifiedFunctions.v
index fa5df95..ac55b7e 100644
--- a/site/posts/StronglySpecifiedFunctions.v
+++ b/site/posts/StronglySpecifiedFunctions.v
@@ -3,7 +3,7 @@
     This is the first article (initially published on #<span
     class="time">January 11, 2015</span>#) of a series of two on how to write
     strongly-specified functions in Coq. You can read the next part #<a
-    href="/posts/StronglySpecifiedFunctionsProgram">here</a>#. *)
+    href="./StronglySpecifiedFunctionsProgram.html">here</a>#. *)
 
 (** I started to play with Coq, the interactive theorem prover
     developed by Inria, a few weeks ago. It is a very powerful tool,
diff --git a/site/posts/StronglySpecifiedFunctionsProgram.v b/site/posts/StronglySpecifiedFunctionsProgram.v
index 33200c8..2a998aa 100644
--- a/site/posts/StronglySpecifiedFunctionsProgram.v
+++ b/site/posts/StronglySpecifiedFunctionsProgram.v
@@ -3,7 +3,7 @@
     This is the second article (initially published on #<span
     class="time">January 01, 2017</span>#) of a series of two on how to write
     strongly-specified functions in Coq. You can read the previous part #<a
-    href="/posts/StronglySpecifiedFunctions">here</a>#. # *)
+    href="./StronglySpecifiedFunctions.html">here</a>#. # *)
 
 (** #<div id="generate-toc"></div>#
 
diff --git a/site/posts/index.org b/site/posts/index.org
new file mode 100644
index 0000000..3c583a5
--- /dev/null
+++ b/site/posts/index.org
@@ -0,0 +1,88 @@
+#+OPTIONS: toc:nil num:nil
+
+#+BEGIN_EXPORT html
+<h1>Write-ups</h1>
+
+<article class="index">
+#+END_EXPORT
+
+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 email to [[mailto:~lthms/lthms.xyz@lists.sr.ht][the dedicated mailing list]] (see the [[https://lists.sr.ht/~lthms/lthms.xyz/%3C20190127111504.n27ttkvtl7l3lzwb%40ideepad.localdomain%3E][annoucement]] for a
+guide on how to subscribe).
+
+* 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.
+
+- [[./MiniHTTPServer.html][Implementing and Certifying a Web Server in Coq]] ::
+  An explanation on how to write an almost pure Coq, and working (albeit
+  minimal) HTTP server.
+
+- [[./Ltac101.html][Ltac 101]] ::
+  Ltac is the “tactic language” of Coq. It allows for writing proof scripts
+  which construct proof terms later checked by Coq.
+
+- [[./RewritingInCoq.html][Rewriting in Coq]] ::
+  The ~rewrite~ tactics are really useful, since they are not limited to the Coq
+  built-in equality relation.
+
+- A Series on Strongly-Specified Funcions in Coq ::
+  Coq ~Prop~ sort allows for defining properties function arguments have to
+  satisfy, such that using such a function requires providing a proof the
+  property is satisfied.
+
+  1. [[./StronglySpecifiedFunctions.html][Using the ~refine~ Tactics]]
+  2. [[./StronglySpecifiedFunctionsProgram.html][Using the ~Program~ Framework]]
+
+* About Haskell
+
+Haskell is a pure, lazy, functional programming language with a very expressive
+type system.
+
+- [[./ExtensibleTypeSafeErrorHandling.html][Extensible, Type-Safe Error Handling In Haskell]] ::
+  Ever heard of “extensible effects?” By applying the same principle, but for
+  error handling, the result is nice, type-safe API for Haskell, with a lot of
+  GHC magic under the hood.
+
+- [[/posts/MonadTransformers/][Monad Transformers are a Great Abstraction]] ::
+  Monads are hard to get right, monad transformers are harder. Yet, they remain
+  a very powerful abstraction.
+
+* About Common Lisp
+
+Common Lisp is a venerable programming languages like no other I know.
+
+- [[./DiscoveringCommonLisp.html][Discovering Common Lisp with ~trivial-gamekit~]] ::
+  From the creation of a Lisp package up to the creation of a standalone
+  executable.
+
+* About this website
+
+One of my goal with this website is for it to /feel/ simple, but the truth is
+under the hood it is generated from a bunch of files using a not-that-simple
+process.
+
+- [[./meta.html][A Series on Generating this Static Website]] ::
+  The toolchain behind the generation of this website ---called *~cleopatra~*---
+  is a literate programming document which build itself in addition to the HTML
+  files composing this corner of the Internet.
+
+  1. [[./meta/Bootstrap.html][Bootstrapping an Extensible Toolchain]]
+  2. [[./meta/Contents.html][Authoring Contents and HTML Generation ~(WIP)~]]
+  3. [[./meta/Soupault.html][Configuring ~soupault~ ~(WIP)~]]
+  4. [[./meta/Theme.html][Theming and Templating ~(WIP)~]]
+
+
+- [[./Thanks.html][Thanks!]] ::
+  If it were not for many awesome FOSS projects, this corner of the Internet
+  would not exists. This is my attempt to give well-deserved credit to them and
+  their creators.
+
+#+BEGIN_EXPORT html
+</article>
+#+END_Export
diff --git a/site/posts/meta/Bootstrap.org b/site/posts/meta/Bootstrap.org
index 0f3a07e..8e645c7 100644
--- a/site/posts/meta/Bootstrap.org
+++ b/site/posts/meta/Bootstrap.org
@@ -90,8 +90,8 @@ their output files (using ~+=~).
   List *~cleopatra~* Makefiles and scripts tangled throughout the generation
   process (with the notable exception of ~Makefile~ itself).
 - ~GENSASS~ ::
-  List auxiliary ~sass~ files which can be imported by the main ~sass~ files
-  (see [[/posts/meta/Theme/][“Theming and Templating”]]).
+  List auxiliary ~sass~ files which can later be imported by the main ~sass~
+  files (see [[./Theme.org][“Theming and Templating”]]).
 - ~CONTENTS~ ::
   List generated files which are part of the target website, and acts as inputs
   for ~soupault~.
@@ -207,7 +207,7 @@ can insert the result of the evaluation of =extends= inside another source block
 when the latter is tangled.
 
 The twist is, we derive the rule to tangle ~bootstrap.mk~ using
-~<<extends>>~. The syntax is the following:
+=extends=. The syntax is the following:
 
 #+BEGIN_SRC verbatim
 <<extends(IN="Bootstrap.org", MK="bootstrap.mk", GF="scripts/update-gitignore.sh")>>
@@ -220,7 +220,7 @@ previous source block.
 <<extends(IN="Bootstrap.org", MK="bootstrap.mk", GF="scripts/update-gitignore.sh")>>
 #+END_SRC
 
-Beware that, as a consequence, modifying code block of ~<<extends>>~ is as
+Beware that, as a consequence, modifying code block of =extends= is as
 “dangerous” as modifying ~Makefile~ itself. Keep that in mind if you start
 hacking *~cleopatra~*!
 
@@ -231,7 +231,7 @@ modify ~bootstrap.mk~ accordingly.
 
 * Generation Processes
 
-Thanks to ~<<extends>>~, *~cleopatra~* is easily extensible. In this section, we
+Thanks to =extends=, *~cleopatra~* is easily extensible. In this section, we
 enumerate the generation processes that are currently used to generate the
 website you are reading.
 
@@ -247,16 +247,16 @@ In the present website, contents can be written in the following format:
 - Regular Coq files ::
   Coq is a system which allows to write machine-checked proofs, and it comes
   with a source “prettifier” called ~coqdoc~.
-  [[/posts/meta/Contents/Coq/][Learn more about the generation process for Coq files]]
+  [[./Contents/Coq.org][Learn more about the generation process for Coq files]]
 - Org documents ::
   Emacs comes with a powerful editing mode called [[https://orgmode.org/][Org mode]], and Org documents
   are really pleasant to work with.
-  [[/posts/meta/Contents/Org/][Learn more about the generation process for Org documents]]
+  [[./Contents/Org.org][Learn more about the generation process for Org documents]]
 
 If you want *~cleopatra~* to support more input formats, you have to
 
 1. Create a org file which, once tangled, provide a dedicated makefile
-2. Edit this file (~Bootstrap.org~) here, and use ~<<extends>>~ to make sure it
+2. Edit this file (~Bootstrap.org~) here, and use =extends= to make sure it
    is actually tangled when necessary
 
 #+BEGIN_SRC makefile :tangle bootstrap.mk :noweb tangle :exports none
diff --git a/site/posts/meta/Soupault.org b/site/posts/meta/Soupault.org
index 913c8ae..aab5476 100644
--- a/site/posts/meta/Soupault.org
+++ b/site/posts/meta/Soupault.org
@@ -23,7 +23,7 @@
   default_template = "templates/main.html"
   content_selector = "main"
   doctype = "<!DOCTYPE html>"
-  clean_urls = true
+  clean_urls = false
 
 [widgets.page-title]
   widget = "title"
diff --git a/site/posts/meta.org b/site/posts/meta/index.org
index 22f200f..db5542e 100644
--- a/site/posts/meta.org
+++ b/site/posts/meta/index.org
@@ -17,19 +17,19 @@ my contents. Did you know that Cleopatra was a reputed polyglot (at least
 according to [[https://fr.wikipedia.org/wiki/Polyglotte][Wikipedia France]])?
 
 #+BEGIN_EXPORT html
-<div id="history">site/posts/meta.org</div>
+<div id="history">site/posts/meta/index.org</div>
 <article class="index">
 #+END_EXPORT
 
 *Beware* this series is far from being complete.
 
-- [[/posts/meta/Bootstrap][Bootstrapping an Extensible Toolchain ~(WIP)~]] ::
+- [[./Bootstrap.org][Bootstrapping an Extensible Toolchain]] ::
 
-- [[/posts/meta/Contents][Authoring Content and HTML Generation ~(WIP)~]] ::
+- [[./Contents.org][Authoring Content and HTML Generation ~(WIP)~]] ::
 
-- [[/posts/meta/Theme][Theming and Templating ~(WIP)~]] ::
+- [[./Soupault.org][Soupault Configuration ~(WIP)~]] ::
 
-- [[/posts/meta/Soupault/][Soupault Configuration ~(WIP)~]] ::
+- [[./Theme.org][Theming and Templating ~(WIP)~]] ::
 
 #+BEGIN_EXPORT html
 </article>