From b47ee36ceab517ba84234bf09e3bb01035450a9a Mon Sep 17 00:00:00 2001 From: Thomas Letan Date: Sun, 16 Feb 2020 22:35:11 +0100 Subject: Automatically generate a revision table from git history --- site/posts/DiscoveringCommonLisp.org | 8 ++++++-- site/posts/ExtensibleTypeSafeErrorHandling.org | 7 ++++++- site/posts/Ltac101.v | 11 ++++++----- site/posts/MiniHTTPServer.v | 5 ++++- site/posts/MonadTransformers.org | 7 ++++++- site/posts/StronglySpecifiedFunctions.v | 26 ++++++++++++-------------- site/posts/StronglySpecifiedFunctionsProgram.v | 19 +++++++------------ 7 files changed, 47 insertions(+), 36 deletions(-) (limited to 'site/posts') 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

Discovering Common Lisp with trivial-gamekit

-June 17, 2018 +

This article has originally been published on June 17, +2018.

#+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 +
site/posts/DiscoveringCommonLisp.org
+#+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

Extensible Type-Safe Error Handling in Haskell

-February 04, 2018 +

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

#+END_EXPORT #+OPTIONS: toc:nil #+TOC: headlines 2 +#+BEGIN_EXPORT html +
site/posts/ExtensibleTypeSafeErrorHandling.org
+#+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 @@ -(** # -

Ltac 101

+(** #

Ltac 101

# -October 16, 2017 - # *) + This article has originally been published on #October + 16, 2017#. *) (** 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. *) -(** #
# *) +(** #
# + + #
site/posts/Ltac101.v
# *) (** ** 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 @@ (** #

Implementing and Certifying a Web Server in Coq

# *) -(** #February 02, 2020# *) +(** This article has originally been published on #February +02, 2020#. *) (** 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 @@ #
# + #
site/posts/MiniHTTPServer.v
# + 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

Monad Transformers are a Great Abstraction

-July 15, 2017 +

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

#+END_EXPORT #+OPTIONS: toc:nil +#+BEGIN_EXPORT html +
site/posts/MonadTransformers.org
+#+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 @@ -(** # -

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 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 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 + #
# + + #
site/posts/StronglySpecifiedFunctions.v
# *) + +(** ** 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. -(** #
# *) - -(** ** 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 @@ -(** # -

Strongly-Specified Functions in Coq, part 2: the Program Framework

+(** #

Strongly-Specified Functions in Coq, part 2: the Program 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. -

-# *) + 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#. # *) -(** #
# *) +(** #
# -(** For the past few weeks, I have been playing around with the <> (or - Russel) framework of Coq. *) + #
site/posts/StronglySpecifiedFunctionsProgram.v
# *) (** ** The Theory *) -- cgit v1.2.3