Remove the “About” page and use the “Write-up” page as default index

1 files changed, 0 insertions, 93 deletions

diff --git a/site/posts/index.org b/site/posts/index.org
deleted file mode 100644
index 6b2e304..0000000
--- a/site/posts/index.org
+++ /dev/null
@@ -1,93 +0,0 @@
-#+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][announcement]] 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.
-
-- [[./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.
-
-- [[./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.
-
-- [[./MonadTransformers.org][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.
-
-- [[/cleopatra/][A Series on Generating this Static Website]] ::
-  The toolchain behind the generation of this website ---called *~cleopatra~*---
-  is a literate program which build itself in addition to the HTML files
-  composing this corner of the Internet. This series /is/ *~cleopatra~*.
-
-  1. [[/cleopatra/Bootstrap.html][Bootstrapping an Extensible Toolchain]]
-  2. [[/cleopatra/Soupault.html][~soupault~ Configuration]]
-  3. [[/cleopatra/Contents/Org.org][Generating Contents from Org Documents ~(TODO)~]]
-  4. [[/cleopatra/Contents/Coq.org][Generating Contents from Coq Documents ~(TODO)~]]
-  5. [[/cleopatra/Theme.html][Theming and Templating ~(TODO)~]]
-
-- [[./Thanks.html][Thanks!]] ::
-  If it were not for many awesome FOSS projects, this corner of the Internet
-  would not exist. This is my attempt to give well-deserved credit to them and
-  their creators.
-
-#+BEGIN_EXPORT html
-</article>
-#+END_Export