summaryrefslogtreecommitdiffstats
path: root/site
diff options
context:
space:
mode:
authorThomas Letan <lthms@soap.coffee>2020-02-14 08:06:52 +0100
committerThomas Letan <lthms@soap.coffee>2020-02-14 08:06:52 +0100
commit707ccc2e782b359725308ebd8cbcc3f904a1b0d9 (patch)
tree3766533c63b055ae1e45f9fbe0842125bc8169b6 /site
parent7c47d2b8f99be4a53f50e46015c15301ffa16ae1 (diff)
Provide an index page for write-ups with more value
Diffstat (limited to 'site')
-rw-r--r--site/index.html2
-rw-r--r--site/posts.org66
-rw-r--r--site/posts/index.html22
-rw-r--r--site/style/main.css17
4 files changed, 84 insertions, 23 deletions
diff --git a/site/index.html b/site/index.html
index 0fa4132..7d08c4a 100644
--- a/site/index.html
+++ b/site/index.html
@@ -24,7 +24,7 @@
<nav>
<dl>
- <dt><a href="/posts/">my blog</a></dt>
+ <dt><a href="/posts/">my write-ups</a></dt>
<dd>
You may find interesting my articles if you are into functional
programming languages.
diff --git a/site/posts.org b/site/posts.org
new file mode 100644
index 0000000..b2096e0
--- /dev/null
+++ b/site/posts.org
@@ -0,0 +1,66 @@
+#+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 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.
+
+- [[/posts/MiniHTTPServer/][Implementing and Certifying a Web Server in Coq]] ::
+ An explanation on how to write an almost pure Coq, and working (albeit
+ minimal) HTTP server.
+
+- [[/posts/Ltac101/][Ltac 101]] ::
+ Ltac is the “tactic language” of Coq. It allows for writing proof scripts
+ which construct proof terms later checked by Coq.
+
+- [[/posts/RewritingInCoq/][Rewriting in Coq]] ::
+ The ~rewrite~ tactics are really useful, since they are not limited to the Coq
+ built-in equality relation.
+
+- A Series on Specifying 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. [[/posts/StronglySpecifiedFunctions/][Using the ~refine~ Tactics]]
+ 2. [[/posts/StronglySpecifiedFunctionsProgram][Using the ~Program~ Framework]]
+
+* About Haskell
+
+Haskell is a pure, lazy, functional programming language with a very expressive
+type system.
+
+- [[/posts/ExtensibleTypeSafeErrorHandling/][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.
+
+- [[/posts/DiscoveringCommonLisp/][Discovering Common Lisp with ~trivial-gamekit~]] ::
+ From the creation of a Lisp package up to the creation of a standalone
+ executable.
+
+#+BEGIN_EXPORT html
+</article>
+#+END_Export
diff --git a/site/posts/index.html b/site/posts/index.html
deleted file mode 100644
index 7643b21..0000000
--- a/site/posts/index.html
+++ /dev/null
@@ -1,22 +0,0 @@
-<div>
- <h1>Blog</h1>
-
- <p>Hi.</p>
-
- <p>
- For several years now, I have been trying to publish interesting content. My
- articles are mostly about functional programming languages such as Coq or
- Haskell.
- </p>
-
- <ul id="index">
- </ul>
-
- <p>
- If you like what you read, have a question or for any other reasons really,
- you can shoot to <a href="mailto:~lthms/lthms.xyz@lists.sr.ht">this blog
- mailing list</a> (see
- the <a href="https://lists.sr.ht/~lthms/lthms.xyz/%3C20190127111504.n27ttkvtl7l3lzwb%40ideepad.localdomain%3E">annoucement</a>
- for a guide on how to subscribe).
- </p>
-</div>
diff --git a/site/style/main.css b/site/style/main.css
index e58b933..8a9c589 100644
--- a/site/style/main.css
+++ b/site/style/main.css
@@ -49,6 +49,7 @@ body#default nav li {
text-transform: uppercase;
font-family: sans-serif;
font-size: 130%;
+ font-weight: bold;
}
body#default nav li a {
@@ -158,3 +159,19 @@ body#vcard nav dd {
body#vcard nav dt a {
color: #68d3a7;
}
+
+/* indexes */
+
+.index dt {
+ font-weight: bold;
+ color: #68d3a7;
+}
+
+.index dd {
+ margin-left: 0;
+ margin-bottom: 1em;
+}
+
+.index dd ol {
+ margin-top: 0.3em;
+}