diff options
Diffstat (limited to 'site/posts')
-rw-r--r-- | site/posts/DiscoveringCommonLisp.org | 8 | ||||
-rw-r--r-- | site/posts/ExtensibleTypeSafeErrorHandling.org | 7 | ||||
-rw-r--r-- | site/posts/Ltac101.v | 11 | ||||
-rw-r--r-- | site/posts/MiniHTTPServer.v | 5 | ||||
-rw-r--r-- | site/posts/MonadTransformers.org | 7 | ||||
-rw-r--r-- | site/posts/StronglySpecifiedFunctions.v | 26 | ||||
-rw-r--r-- | site/posts/StronglySpecifiedFunctionsProgram.v | 19 |
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 *) |