From c62a61dba7285a034fc0405edbd47dcc48bf03f5 Mon Sep 17 00:00:00 2001 From: Thomas Letan Date: Tue, 14 Jul 2020 11:26:58 +0200 Subject: Prepare the introduction of a RSS feed --- site/posts/CleopatraV1.org | 4 ++++ site/posts/ClightIntroduction.v | 7 +++---- site/posts/ExtensibleTypeSafeErrorHandling.org | 4 ++-- site/posts/Ltac101.v | 12 ++++++------ site/posts/MonadTransformers.org | 4 ++-- site/posts/RewritingInCoq.v | 24 ++++++++++-------------- site/posts/StronglySpecifiedFunctions.v | 12 ++++++------ site/posts/StronglySpecifiedFunctionsProgram.v | 6 +++--- 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 +
site/posts/CleopatraV1.org
+#+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 (##March 18, 2020##), 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. #
# 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

Extensible Type-Safe Error Handling in Haskell

-

This article has originally been published on February 04, -2018.

+

This article has originally been published on February 04, 2018.

#+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 #October - 16, 2017#. *) + 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 #October 16, 2017#), 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. *) (** #
# 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

Monad Transformers are a Great Abstraction

-

This article has originally been published on July 15, -2017.

+

This article has originally been published on July 15, 2017.

#+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 #May 13, - 2017.# *) - -(** 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 #May + 13, 2017 how it is possible to rewrite a term in a proof using a + ad-hoc equivalence relation and, when necessary, a proper morphism. *) (** #
# 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 <> Tactic +(** * Strongly-Specified Functions in Coq, part 1: using the <> Tactic *) - This is the first article (initially published on #January 11, 2015#) of a series of two on how to write - strongly-specified functions in Coq. You can read the next part #here#. *) +(** This is the first article (initially published on #January 11, 2015#) of a series of two on + how to write strongly-specified functions in Coq. You can read the next part + #here#. -(** 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 <> Framework This is the second article (initially published on #January 01, 2017#) of a series of two on how to write - strongly-specified functions in Coq. You can read the previous part #here#. # *) + id="original-created-at">January 01, 2017#) of a series of two on how + to write strongly-specified functions in Coq. You can read the previous part + #here#. # *) (** #
# -- cgit v1.2.3