summaryrefslogtreecommitdiffstats
path: root/site
diff options
context:
space:
mode:
authorThomas Letan <lthms@soap.coffee>2020-07-14 11:26:58 +0200
committerThomas Letan <lthms@soap.coffee>2020-07-14 11:26:58 +0200
commitc62a61dba7285a034fc0405edbd47dcc48bf03f5 (patch)
tree994a21ae6741acb026e73a8d0e85933f04562732 /site
parent3deedaa389ab67148e1ca55febf919b30fbb4df2 (diff)
Prepare the introduction of a RSS feed
Diffstat (limited to 'site')
-rw-r--r--site/posts/CleopatraV1.org4
-rw-r--r--site/posts/ClightIntroduction.v7
-rw-r--r--site/posts/ExtensibleTypeSafeErrorHandling.org4
-rw-r--r--site/posts/Ltac101.v12
-rw-r--r--site/posts/MonadTransformers.org4
-rw-r--r--site/posts/RewritingInCoq.v24
-rw-r--r--site/posts/StronglySpecifiedFunctions.v12
-rw-r--r--site/posts/StronglySpecifiedFunctionsProgram.v6
8 files changed, 36 insertions, 37 deletions
diff --git a/site/posts/CleopatraV1.org b/site/posts/CleopatraV1.org
index 349e237..11d796b 100644
--- a/site/posts/CleopatraV1.org
+++ b/site/posts/CleopatraV1.org
@@ -28,6 +28,10 @@ purpose is to introduce two Makefiles: ~Makefile~ and ~bootstrap.mk~.
#+TOC: headlines 2
+#+BEGIN_EXPORT html
+<div id="history">site/posts/CleopatraV1.org</div>
+#+END_EXPORT
+
~Makefile~ serves two purposes: it initiates a few global variables, and it
provides a rule to generate ~bootstrap.mk~. At this point, some readers may
wonder /why/ we need ~Makefile~ in this context, and the motivation behind this
diff --git a/site/posts/ClightIntroduction.v b/site/posts/ClightIntroduction.v
index 0d53f33..13bf773 100644
--- a/site/posts/ClightIntroduction.v
+++ b/site/posts/ClightIntroduction.v
@@ -8,10 +8,9 @@ Import ListNotations.
you write is preserved by CompCert compilation passes up to the generated
machine code.
- I have been interested in CompCert for quite some times now. Today (#<span
- id="time">#March 18, 2020#</span>#), I have challenged myself to study
- Clight and its semantics. This write-up is the result of this challenge,
- written as I was progressing.
+ I had been interested in CompCert for quite some times, and ultimately
+ 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>#
diff --git a/site/posts/ExtensibleTypeSafeErrorHandling.org b/site/posts/ExtensibleTypeSafeErrorHandling.org
index 3af3d44..cc276f0 100644
--- a/site/posts/ExtensibleTypeSafeErrorHandling.org
+++ b/site/posts/ExtensibleTypeSafeErrorHandling.org
@@ -1,8 +1,8 @@
#+BEGIN_EXPORT html
<h1>Extensible Type-Safe Error Handling in Haskell</h1>
-<p>This article has originally been published on <span class="time">February 04,
-2018</span>.</p>
+<p>This article has originally been published on <span
+id="original-created-at">February 04, 2018</span>.</p>
#+END_EXPORT
#+TOC: headlines 2
diff --git a/site/posts/Ltac101.v b/site/posts/Ltac101.v
index 1bc9907..bd539e7 100644
--- a/site/posts/Ltac101.v
+++ b/site/posts/Ltac101.v
@@ -1,12 +1,12 @@
(** * Ltac 101
- This article has originally been published on #<span class="time">October
- 16, 2017</span>#. *)
+ This article has . *)
-(** 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. *)
+(** In this article (originally published on #<span
+ id="original-created-at">October 16, 2017</span>#), 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>#
diff --git a/site/posts/MonadTransformers.org b/site/posts/MonadTransformers.org
index 4c28fe5..b2bd2ca 100644
--- a/site/posts/MonadTransformers.org
+++ b/site/posts/MonadTransformers.org
@@ -1,8 +1,8 @@
#+BEGIN_EXPORT html
<h1>Monad Transformers are a Great Abstraction</h1>
-<p>This article has originally been published on <span class="time">July 15,
-2017</span>.</p>
+<p>This article has originally been published on <span
+id="original-created-at">July 15, 2017</span>.</p>
#+END_EXPORT
#+OPTIONS: toc:nil
diff --git a/site/posts/RewritingInCoq.v b/site/posts/RewritingInCoq.v
index 9c2efaf..0020a3e 100644
--- a/site/posts/RewritingInCoq.v
+++ b/site/posts/RewritingInCoq.v
@@ -1,17 +1,13 @@
-(** * Rewriting in Coq
-
- This article has originally been published on #<span class="time">May 13,
- 2017</span>.# *)
-
-(** I have to confess something. In the published codebase of SpecCert lies a
- shameful secret. It takes the form of a set of axioms which are not
- required. I thought they were when I wrote them, but it was before I heard
- about “generalized rewriting,” setoids and morphisms.
-
- Now, I know the truth. I will have to update SpecCert eventually. But,
- in the meantime, let me try to explain how it is possible to rewrite a
- term in a proof using a ad-hoc equivalence relation and, when
- necessary, a proper morphism. *)
+(** * Rewriting in Coq *)
+
+(** I have to confess something. In the codebase of SpecCert lies a shameful
+ secret. It takes the form of a set of unnecessary axioms. I thought I
+ couldn’t avoid them at first, but it was before I heard about “generalized
+ rewriting,” setoids and morphisms. Now, I know the truth, and I will have
+ to update SpecCert eventually. But, in the meantime, let me try to explain
+ in this article originally published on #<span id="original-created-at">May
+ 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>#
diff --git a/site/posts/StronglySpecifiedFunctions.v b/site/posts/StronglySpecifiedFunctions.v
index ac55b7e..5d0e69a 100644
--- a/site/posts/StronglySpecifiedFunctions.v
+++ b/site/posts/StronglySpecifiedFunctions.v
@@ -1,11 +1,11 @@
-(** * Strongly-Specified Functions in Coq, part 1: using the <<refine>> Tactic
+(** * Strongly-Specified Functions in Coq, part 1: using the <<refine>> Tactic *)
- 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="./StronglySpecifiedFunctionsProgram.html">here</a>#. *)
+(** This is the first article (initially published on #<span
+ class="original-created-at">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="./StronglySpecifiedFunctionsProgram.html">here</a>#.
-(** I started to play with Coq, the interactive theorem prover
+ I started to play with Coq, the interactive theorem prover
developed by Inria, a few weeks ago. It is a very powerful tool,
yet hard to master. Fortunately, there are some very good readings
if you want to learn (I recommend the Coq'Art). This article is
diff --git a/site/posts/StronglySpecifiedFunctionsProgram.v b/site/posts/StronglySpecifiedFunctionsProgram.v
index 2a998aa..f7f84df 100644
--- a/site/posts/StronglySpecifiedFunctionsProgram.v
+++ b/site/posts/StronglySpecifiedFunctionsProgram.v
@@ -1,9 +1,9 @@
(** * Strongly-Specified Functions in Coq, part 2: the <<Program>> Framework
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="./StronglySpecifiedFunctions.html">here</a>#. # *)
+ id="original-created-at">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="./StronglySpecifiedFunctions.html">here</a>#. # *)
(** #<div id="generate-toc"></div>#