summaryrefslogtreecommitdiffstats
path: root/site/posts
diff options
context:
space:
mode:
authorThomas Letan <lthms@soap.coffee>2020-02-16 22:35:11 +0100
committerThomas Letan <lthms@soap.coffee>2020-02-16 22:35:11 +0100
commitb47ee36ceab517ba84234bf09e3bb01035450a9a (patch)
tree9d5cad60ba02a7a724f3c660f3b91e781bf0676d /site/posts
parent25e6a8c049dbc19ac752dda5995929695a1e10f1 (diff)
Automatically generate a revision table from git history
Diffstat (limited to 'site/posts')
-rw-r--r--site/posts/DiscoveringCommonLisp.org8
-rw-r--r--site/posts/ExtensibleTypeSafeErrorHandling.org7
-rw-r--r--site/posts/Ltac101.v11
-rw-r--r--site/posts/MiniHTTPServer.v5
-rw-r--r--site/posts/MonadTransformers.org7
-rw-r--r--site/posts/StronglySpecifiedFunctions.v26
-rw-r--r--site/posts/StronglySpecifiedFunctionsProgram.v19
7 files changed, 47 insertions, 36 deletions
diff --git a/site/posts/DiscoveringCommonLisp.org b/site/posts/DiscoveringCommonLisp.org
index a198c3d..cf31874 100644
--- a/site/posts/DiscoveringCommonLisp.org
+++ b/site/posts/DiscoveringCommonLisp.org
@@ -1,10 +1,10 @@
#+BEGIN_EXPORT html
<h1>Discovering Common Lisp with <code>trivial-gamekit</code></h1>
-<span class="time">June 17, 2018</span>
+<p>This article has originally been published on <span class="time">June 17,
+2018</span>.</p>
#+END_EXPORT
-
I always wanted to learn some Lisp dialect.
In the meantime, [[https://github.com/lkn-org/lykan][lykan]] —my Slayers Online clone— begins to take shape.
So, of course, my brain got an idea: /why not writing a client for lykan in some
@@ -30,6 +30,10 @@ gist]].
#+OPTIONS: toc:nil
#+TOC: headlines 2
+#+BEGIN_EXPORT html
+<div id="history">site/posts/DiscoveringCommonLisp.org</div>
+#+END_EXPORT
+
* Common Lisp, Quicklisp and trivial-gamekit
The trivial-gamekit [[https://borodust.github.io/projects/trivial-gamekit/][website]] lists several requirements.
diff --git a/site/posts/ExtensibleTypeSafeErrorHandling.org b/site/posts/ExtensibleTypeSafeErrorHandling.org
index 9164bc2..0d40ed7 100644
--- a/site/posts/ExtensibleTypeSafeErrorHandling.org
+++ b/site/posts/ExtensibleTypeSafeErrorHandling.org
@@ -1,12 +1,17 @@
#+BEGIN_EXPORT html
<h1>Extensible Type-Safe Error Handling in Haskell</h1>
-<span class="time">February 04, 2018</span>
+<p>This article has originally been published on <span class="time">February 04,
+2018</span>.</p>
#+END_EXPORT
#+OPTIONS: toc:nil
#+TOC: headlines 2
+#+BEGIN_EXPORT html
+<div id="history">site/posts/ExtensibleTypeSafeErrorHandling.org</div>
+#+END_EXPORT
+
A colleague of mine introduced me to the benefits of [[https://crates.io/crates/error-chain][~error-chain~]], a crate which
aims to implement /“consistent error handling”/ for Rust. I found the overall
design pretty convincing, and in his use case, the crate really makes its error
diff --git a/site/posts/Ltac101.v b/site/posts/Ltac101.v
index ebf3566..61d3bc9 100644
--- a/site/posts/Ltac101.v
+++ b/site/posts/Ltac101.v
@@ -1,15 +1,16 @@
-(** #
-<h1>Ltac 101</h1>
+(** #<h1>Ltac 101</h1>#
-<span class="time">October 16, 2017</span>
- # *)
+ This article has originally been published on #<span class="time">October
+ 16, 2017</span>#. *)
(** In this article, I give an overview of my findings about the Ltac language,
more precisely how it can be used to automate the construction of proof
terms. If you never wrote a tactic in Coq and are curious about the subject,
it might be a good starting point. *)
-(** #<div id="generate-toc"></div># *)
+(** #<div id="generate-toc"></div>#
+
+ #<div id="history">site/posts/Ltac101.v</div># *)
(** ** Tactics Aliases *)
diff --git a/site/posts/MiniHTTPServer.v b/site/posts/MiniHTTPServer.v
index ee6b572..e944075 100644
--- a/site/posts/MiniHTTPServer.v
+++ b/site/posts/MiniHTTPServer.v
@@ -1,6 +1,7 @@
(** #<h1>Implementing and Certifying a Web Server in Coq</h1># *)
-(** #<span class="time">February 02, 2020</span># *)
+(** This article has originally been published on #<span class="time">February
+02, 2020</span>#. *)
(** FreeSpec is a general-purpose framework for implementing (with a Free monad)
and certifying (with contracts) impure computations. In this tutorial, we
@@ -11,6 +12,8 @@
#<div id="generate-toc"></div>#
+ #<div id="history">site/posts/MiniHTTPServer.v</div>#
+
The [FreeSpec.Core] module reexports the key component provided by
FreeSpec. *)
diff --git a/site/posts/MonadTransformers.org b/site/posts/MonadTransformers.org
index e94f07d..7947ef4 100644
--- a/site/posts/MonadTransformers.org
+++ b/site/posts/MonadTransformers.org
@@ -1,11 +1,16 @@
#+BEGIN_EXPORT html
<h1>Monad Transformers are a Great Abstraction</h1>
-<span class="time">July 15, 2017</span>
+<p>This article has originally been published on <span class="time">July 15,
+2017</span>.</p>
#+END_EXPORT
#+OPTIONS: toc:nil
+#+BEGIN_EXPORT html
+<div id="history">site/posts/MonadTransformers.org</div>
+#+END_EXPORT
+
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
diff --git a/site/posts/StronglySpecifiedFunctions.v b/site/posts/StronglySpecifiedFunctions.v
index 6564413..3adfe50 100644
--- a/site/posts/StronglySpecifiedFunctions.v
+++ b/site/posts/StronglySpecifiedFunctions.v
@@ -1,13 +1,9 @@
-(** #
-<h1>Strongly-Specified Functions in Coq, part 1: using the <code>refine</code> Tactic</h1>
+(** # <h1>Strongly-Specified Functions in Coq, part 1: using the <code>refine</code> Tactic</h1>#
-<p>
- 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>.
-</p>
-# *)
+ 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>#. *)
(** I started to play with Coq, the interactive theorem prover
developed by Inria, a few weeks ago. It is a very powerful tool,
@@ -23,16 +19,18 @@
return value is the list passed in argument in which the first
element has been removed for example.
- But since we will manipulate lists in this article, we first
+ #<div id="generate-toc"></div>#
+
+ #<div id="history">site/posts/StronglySpecifiedFunctions.v</div># *)
+
+(** ** Is this list empty? *)
+
+(** Since we will manipulate lists in this article, we first
enable several notations of the standard library. *)
From Coq Require Import List.
Import ListNotations.
-(** #<div id="generate-toc"></div># *)
-
-(** ** Is this list empty? *)
-
(** It's the first question to deal with when manipulating
lists. There are some functions that require their arguments not
to be empty. It's the case for the [pop] function, for instance:
diff --git a/site/posts/StronglySpecifiedFunctionsProgram.v b/site/posts/StronglySpecifiedFunctionsProgram.v
index 24faf27..037b0dd 100644
--- a/site/posts/StronglySpecifiedFunctionsProgram.v
+++ b/site/posts/StronglySpecifiedFunctionsProgram.v
@@ -1,18 +1,13 @@
-(** #
-<h1>Strongly-Specified Functions in Coq, part 2: the <code>Program</code> Framework</h1>
+(** #<h1>Strongly-Specified Functions in Coq, part 2: the <code>Program</code> Framework</h1>#
-<p>
- 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>.
-</p>
-# *)
+ 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>#. # *)
-(** #<div id="generate-toc"></div># *)
+(** #<div id="generate-toc"></div>#
-(** For the past few weeks, I have been playing around with the <<Program>> (or
- Russel) framework of Coq. *)
+ #<div id="history">site/posts/StronglySpecifiedFunctionsProgram.v</div># *)
(** ** The Theory *)