summaryrefslogtreecommitdiffstats
path: root/site/posts
diff options
context:
space:
mode:
authorThomas Letan <lthms@soap.coffee>2021-03-28 00:03:41 +0100
committerThomas Letan <lthms@soap.coffee>2021-03-28 14:19:29 +0200
commit495f9db0606b0ed09e6fac59dc32de4cdc8c0087 (patch)
tree82ea5c5e247c664de247a0f3818f393ffdb00067 /site/posts
parent1a197fb354a82a31deca4f9b118f057bbd0038b6 (diff)
2021 Spring redesign
Diffstat (limited to 'site/posts')
-rw-r--r--site/posts/AlgebraicDatatypes.v6
-rw-r--r--site/posts/ClightIntroduction.v6
-rw-r--r--site/posts/Coqffi.org7
-rw-r--r--site/posts/CoqffiEcho.org10
-rw-r--r--site/posts/CoqffiIntro.org10
-rw-r--r--site/posts/ExtensibleTypeSafeErrorHandling.org9
-rw-r--r--site/posts/Ltac.org18
-rw-r--r--site/posts/LtacMetaprogramming.v3
-rw-r--r--site/posts/LtacPatternMatching.v10
-rw-r--r--site/posts/MixingLtacAndGallina.v5
-rw-r--r--site/posts/RewritingInCoq.v6
-rw-r--r--site/posts/StronglySpecifiedFunctions.org7
-rw-r--r--site/posts/StronglySpecifiedFunctionsProgram.v11
-rw-r--r--site/posts/StronglySpecifiedFunctionsRefine.v20
-rw-r--r--site/posts/Thanks.org40
15 files changed, 91 insertions, 77 deletions
diff --git a/site/posts/AlgebraicDatatypes.v b/site/posts/AlgebraicDatatypes.v
index 1b24520..f32551c 100644
--- a/site/posts/AlgebraicDatatypes.v
+++ b/site/posts/AlgebraicDatatypes.v
@@ -1,3 +1,7 @@
+(** #<nav><p class="series">../coq.html</p>
+ <p class="series-prev">./ClightIntroduction.html</p>
+ <p class="series-next">./Coqffi.html</p></nav># *)
+
(** * Proving Algebraic Datatypes are “Algebraic” *)
(** Several programming languages allow programmers to define (potentially
@@ -93,7 +97,7 @@ Inductive prod (A B : Type) : Type :=
| pair : A -> B -> prod A B
>>
- #<div id="generate-toc"></div>#
+ #<nav id="generate-toc"></nav>#
#<div id="history">site/posts/AlgebraicDatatypes.v</div># *)
diff --git a/site/posts/ClightIntroduction.v b/site/posts/ClightIntroduction.v
index 4bd9a52..85d084b 100644
--- a/site/posts/ClightIntroduction.v
+++ b/site/posts/ClightIntroduction.v
@@ -1,3 +1,7 @@
+(** #<nav><p class="series">../coq.html</p>
+ <p class="series-prev">./RewritingInCoq.html</p>
+ <p class="series-next">./AlgebraicDatatypes.html</p></nav># *)
+
(** * A Study of Clight and its Semantics *)
(* begin hide *)
From Coq Require Import List.
@@ -12,7 +16,7 @@ Import ListNotations.
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>#
+ #<nav id="generate-toc"></nav>#
#<div id="history">site/posts/ClightIntroduction.v</div># *)
diff --git a/site/posts/Coqffi.org b/site/posts/Coqffi.org
index 3d8b867..f8d9695 100644
--- a/site/posts/Coqffi.org
+++ b/site/posts/Coqffi.org
@@ -1,6 +1,7 @@
-#+BEGIN_EXPORT html
-<h1>A Series on <code>coqffi</code></h1>
-#+END_EXPORT
+#+TITLE: A series on ~coqffi~
+
+#+SERIES: ../coq.html
+#+SERIES_PREV: AlgebraicDatatypes.html
~coqffi~ generates Coq FFI modules from compiled OCaml interface
modules (~.cmi~). In practice, it greatly reduces the hassle to mix
diff --git a/site/posts/CoqffiEcho.org b/site/posts/CoqffiEcho.org
index 04fa253..81ae0e9 100644
--- a/site/posts/CoqffiEcho.org
+++ b/site/posts/CoqffiEcho.org
@@ -1,6 +1,7 @@
-#+BEGIN_EXPORT html
-<h1>Implementing an Echo Server in Coq with <code>coqffi</code></h1>
-#+END_EXPORT
+#+TITLE: Implementing an Echo Server in Coq with ~coqffi~
+
+#+SERIES: ./Coqffi.html
+#+SERIES_PREV: ./CoqffiIntro.html
#+NAME: coqffi_output
#+BEGIN_SRC sh :results output :exports none :var mod=""
@@ -21,9 +22,8 @@ Besides, this article is a literate program, and you can download
[[/files/coqffi-tutorial.tar.gz][the resulting source tree]] if you
want to try to read the source directly, or modify it to your taste.
-#+TOC: headlines 2
-
#+BEGIN_EXPORT html
+<nav id="generate-toc"></nav>
<div id="history">site/posts/CoqffiEcho.org</div>
#+END_EXPORT
diff --git a/site/posts/CoqffiIntro.org b/site/posts/CoqffiIntro.org
index 053826b..411f3cf 100644
--- a/site/posts/CoqffiIntro.org
+++ b/site/posts/CoqffiIntro.org
@@ -1,6 +1,7 @@
-#+BEGIN_EXPORT html
-<h1><code>coqffi</code> in a Nutshell</h1>
-#+END_EXPORT
+#+TITLE: ~coqffi~ in a Nutshell
+
+#+SERIES: ./Coqffi.html
+#+SERIES_NEXT: ./CoqffiEcho.html
For each entry of a ~cmi~ file (a /compiled/ ~mli~ file), ~coqffi~
tries to generate an equivalent (from the extraction mechanism
@@ -10,9 +11,8 @@ perspective) Coq definition. In this article, we walk through how
Note that we do not dive into the vernacular commands ~coqffi~
generates. They are of no concern for users of ~coqffi~.
-#+TOC: headlines 2
-
#+BEGIN_EXPORT html
+<nav id="generate-toc"></nav>
<div id="history">site/posts/CoqffiIntro.org</div>
#+END_EXPORT
diff --git a/site/posts/ExtensibleTypeSafeErrorHandling.org b/site/posts/ExtensibleTypeSafeErrorHandling.org
index cc276f0..e817e31 100644
--- a/site/posts/ExtensibleTypeSafeErrorHandling.org
+++ b/site/posts/ExtensibleTypeSafeErrorHandling.org
@@ -1,13 +1,14 @@
-#+BEGIN_EXPORT html
-<h1>Extensible Type-Safe Error Handling in Haskell</h1>
+#+TITLE: Extensible Type-Safe Error Handling in Haskell
+
+#+SERIES: ../haskell.html
+#+BEGIN_EXPORT html
<p>This article has originally been published on <span
id="original-created-at">February 04, 2018</span>.</p>
#+END_EXPORT
-#+TOC: headlines 2
-
#+BEGIN_EXPORT html
+<nav id="generate-toc"></nav>
<div id="history">site/posts/ExtensibleTypeSafeErrorHandling.org</div>
#+END_EXPORT
diff --git a/site/posts/Ltac.org b/site/posts/Ltac.org
index caba76c..37580cd 100644
--- a/site/posts/Ltac.org
+++ b/site/posts/Ltac.org
@@ -1,12 +1,16 @@
-#+BEGIN_EXPORT html
-<h1>A Series on Ltac</h1>
-#+END_EXPORT
+#+TITLE: A Series on Ltac
+
+#+SERIES: ../coq.html
+#+SERIES_PREV: ./StronglySpecifiedFunctions.html
+#+SERIES_NEXT: ./RewritingInCoq.html
Ltac is the “tactic language” of Coq. It is commonly advertised as the common
-approach to write proofs, which tends to bias how it is introduced to new Coq
-users (/e.g./, in Master courses). In this series, we present Ltac as the
-metaprogramming tool it is, since fundamentally it is an imperative language
-which allows for constructing Coq terms interactively and incrementally.
+approach to write proofs, which tends to bias how it is introduced to
+new Coq users[fn::I know /I/ was introduced to Coq in a similar way in
+my Master courses.]. In this series, we present Ltac as the
+metaprogramming tool it is, since fundamentally it is an imperative
+language which allows for constructing Coq terms interactively and
+incrementally.
- [[./LtacMetaprogramming.html][Ltac is an Imperative Metaprogramming Language]] ::
Ltac generates terms, therefore it is a metaprogramming language. It does it
diff --git a/site/posts/LtacMetaprogramming.v b/site/posts/LtacMetaprogramming.v
index 2a4fe50..6b086e3 100644
--- a/site/posts/LtacMetaprogramming.v
+++ b/site/posts/LtacMetaprogramming.v
@@ -1,3 +1,6 @@
+(** #<nav><p class="series">Ltac.html</p>
+ <p class="series-next">LtacPatternMatching.html</p></nav># *)
+
(** * Ltac is an Imperative Metaprogramming Language *)
(** #<div id="history">site/posts/LtacMetaprogramming.v</div># *)
diff --git a/site/posts/LtacPatternMatching.v b/site/posts/LtacPatternMatching.v
index d52d0bf..a0b8a4d 100644
--- a/site/posts/LtacPatternMatching.v
+++ b/site/posts/LtacPatternMatching.v
@@ -1,3 +1,7 @@
+(** #<nav><p class="series">Ltac.html</p>
+ <p class="series-prev">./LtacMetaprogramming.html</p>
+ <p class="series-next">./MixingLtacAndGallina.html</p></nav># *)
+
(** * Pattern Matching on Types and Contexts *)
(** In the #<a href="LtacMetaprogramming.html">#previous article#</a># of our
@@ -11,7 +15,7 @@
contexts. In this article, we give a short introduction on this feature of
key importance. *)
-(** #<div id="generate-toc"></div>#
+(** #<nav id="generate-toc"></nav>#
#<div id="history">site/posts/LtacPatternMatching.v</div># *)
@@ -137,8 +141,8 @@ Ltac not_param_type x :=
| _ => idtac
end.
-(** Both <<not_param_type (@nil nat)>> of type [list nat] and <<(@eq_refl nat
- 0)>> of type [0 = 0] fail, but <<not_param_type 0>> of type [nat]
+(** Both <<not_param_type (@nil nat)>> of type [list nat] and
+ <<(@eq_refl nat 0)>> of type [0 = 0] fail, but <<not_param_type 0>> of type [nat]
succeeds. *)
(** ** Pattern Matching on the Context with [goal] *)
diff --git a/site/posts/MixingLtacAndGallina.v b/site/posts/MixingLtacAndGallina.v
index 4e6b28d..d77cd8a 100644
--- a/site/posts/MixingLtacAndGallina.v
+++ b/site/posts/MixingLtacAndGallina.v
@@ -1,3 +1,6 @@
+(** #<nav><p class="series">Ltac.html</p>
+ <p class="series-prev">./LtacPatternMatching.html</p></nav># *)
+
(** * Mixing Ltac and Gallina for Fun and Profit *)
(** One of the most misleading introduction to Coq is to say that “Gallina is
@@ -20,7 +23,7 @@
It turns out these features are more than handy when it comes to
metaprogramming (that is, the generation of programs by programs). *)
-(** #<div id="generate-toc"></div>#
+(** #<nav id="generate-toc"></nav>#
#<div id="history">site/posts/MixingLtacAndGallina.v</div># *)
diff --git a/site/posts/RewritingInCoq.v b/site/posts/RewritingInCoq.v
index 0020a3e..a285e09 100644
--- a/site/posts/RewritingInCoq.v
+++ b/site/posts/RewritingInCoq.v
@@ -1,3 +1,7 @@
+(** #<nav><p class="series">../coq.html</p>
+ <p class="series-prev">./Ltac.html</p>
+ <p class="series-next">./ClightIntroduction.html</p></nav># *)
+
(** * Rewriting in Coq *)
(** I have to confess something. In the codebase of SpecCert lies a shameful
@@ -9,7 +13,7 @@
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>#
+(** #<nav id="generate-toc"></nav>#
#<div id="history">site/posts/RewritingInCoq.v</div># *)
diff --git a/site/posts/StronglySpecifiedFunctions.org b/site/posts/StronglySpecifiedFunctions.org
index 805b944..83148c6 100644
--- a/site/posts/StronglySpecifiedFunctions.org
+++ b/site/posts/StronglySpecifiedFunctions.org
@@ -1,8 +1,7 @@
-#+OPTIONS: toc:nil num:nil
+#+TITLE: A Series on Strongly-Specified Functions in Coq
-#+BEGIN_EXPORT html
-<h1>A Series on Strongly-Specified Functions in Coq</h1>
-#+END_EXPORT
+#+SERIES: ../coq.html
+#+SERIES_NEXT: ./Ltac.html
Using dependent types and the ~Prop~ sort, it becomes possible to specify
functions whose arguments and results are constrained by properties. Using such
diff --git a/site/posts/StronglySpecifiedFunctionsProgram.v b/site/posts/StronglySpecifiedFunctionsProgram.v
index 1b4ab5f..c5763ea 100644
--- a/site/posts/StronglySpecifiedFunctionsProgram.v
+++ b/site/posts/StronglySpecifiedFunctionsProgram.v
@@ -5,7 +5,7 @@
to write strongly-specified functions in Coq. You can read the previous part
#<a href="./StronglySpecifiedFunctionsRefine.html">here</a>#. # *)
-(** #<div id="generate-toc"></div>#
+(** #<nav id="generate-toc"></nav>#
#<div id="history">site/posts/StronglySpecifiedFunctionsProgram.v</div># *)
@@ -341,7 +341,8 @@ Defined.
(** val extract : 'a1 vector -> nat -> nat -> 'a1 vector **)
let extract v e b =
take (drop v b) (sub e b)
->> *)
+>>
+ *)
(** I was pretty happy, so I tried some more. Each time, using [nth], I managed
to write a precise post condition and to prove it holds true. For instance,
@@ -467,7 +468,8 @@ cannot be applied to the terms
"b" : "Type"
The 3rd term has type "Type" which should be coercible
to "nat".
->> *)
+>>
+ *)
#[program]
Fixpoint map2 {a b c n}
@@ -520,4 +522,5 @@ cannot be applied to the terms
"wildcard'" : "vector A n'"
The 3rd term has type "vector A n'" which should be
coercible to "nat".
->> *)
+>>
+ *)
diff --git a/site/posts/StronglySpecifiedFunctionsRefine.v b/site/posts/StronglySpecifiedFunctionsRefine.v
index 1d4ec2e..4ffb385 100644
--- a/site/posts/StronglySpecifiedFunctionsRefine.v
+++ b/site/posts/StronglySpecifiedFunctionsRefine.v
@@ -19,7 +19,7 @@
return value is the list passed in argument in which the first
element has been removed for example.
- #<div id="generate-toc"></div>#
+ #<nav id="generate-toc"></nav>#
#<div id="history">site/posts/StronglySpecifiedFunctionsRefine.v</div># *)
@@ -54,7 +54,8 @@ Import ListNotations.
<<
Definition predicate_b (args) :=
if predicate_dec args then true else false.
->> *)
+>>
+ *)
(** *** Defining the <<empty>> predicate *)
@@ -174,7 +175,8 @@ Definition pop {a} (l : list a) (h : ~ empty l)
h : ~ empty l
============================
list a
->> *)
+>>
+ *)
(** Using the [refine] tactic naively, for instance this way: *)
@@ -280,7 +282,8 @@ Definition pop {a} (l : list a | ~ empty l)
equ : proj1_sig l = []
============================
{l' : list a | exists a0 : a, proj1_sig l = a0 :: l'}
->> *)
+>>
+ *)
+ destruct l as [l nempty]; cbn in *.
rewrite equ in nempty.
@@ -299,7 +302,8 @@ Definition pop {a} (l : list a | ~ empty l)
equ : proj1_sig l = a0 :: rst
============================
exists a1 : a, proj1_sig l = a1 :: rst
->> *)
+>>
+ *)
+ destruct l as [l nempty]; cbn in *.
rewrite equ.
@@ -339,7 +343,8 @@ Definition push {a} (l : list a) (x : a)
<<
let push l a =
Cons (a, l)
->> *)
+>>
+ *)
(** ** Defining [head] *)
@@ -376,7 +381,8 @@ Defined.
let head = function
| Nil -> assert false (* absurd case *)
| Cons (a, l0) -> a
->> *)
+>>
+ *)
(** ** Conclusion & Moving Forward *)
diff --git a/site/posts/Thanks.org b/site/posts/Thanks.org
index ba76a88..c20f1e5 100644
--- a/site/posts/Thanks.org
+++ b/site/posts/Thanks.org
@@ -1,18 +1,15 @@
-#+BEGIN_EXPORT html
-<h1>Thanks!</h1>
-
-<article class="index">
-#+END_EXPORT
+#+TITLE: Thanks!
-This website could not exist without (many) awesome free software
-projects. Although I could not list them all even if I wanted, my desire is at
-least to try keeping up-to-date a curated description of the “main” ones.
+#+SERIES: ../meta.html
+#+SERIES_NEXT: ../cleopatra.html
-#+OPTIONS: toc:nil num:nil
+This website could not exist without many awesome free software
+projects. Although I could not list them all even if I wanted, my
+desire is at least to try keeping up-to-date a curated description of
+the most significant ones.
#+BEGIN_EXPORT html
-<div id="generate-toc"></div>
-
+<nav id="generate-toc"></nav>
<div id="history">site/posts/Thanks.org</div>
#+END_EXPORT
@@ -35,9 +32,6 @@ least to try keeping up-to-date a curated description of the “main” ones.
- [[https://soupault.neocities.org][soupault]] ::
Soupault is a static website generator and HTML processor written by [[https://www.baturin.org/][Daniil
Baturin]].
-- [[https://github.com/sass/sassc][~sassc~]] ::
- ~sassc~ is a compiler for SASS files (actually, a wrapper around [[https://github.com/sass/libsass][~libsass~]]),
- authored by [[https://github.com/akhleung][Aaron Leung]], [[https://github.com/hcatlin][Hampton Catlin]], [[https://github.com/mgreter][Marcel Greter]], and [[https://github.com/xzyfer][Michael Mifsud]].
- [[https://cleopatra.soap.coffee][~cleopatra~]] ::
~cleopatra~ is a generic, extensible toolchain with facilities for
literate programming projects using Org mode and more. I have
@@ -45,25 +39,9 @@ least to try keeping up-to-date a curated description of the “main” ones.
* Frontend
-- [[https://forkaweso.me/Fork-Awesome/][Fork Awesome]] ::
- Fork Awesome is a collection of icons for the web. It is a community fork of
- [[https://fontawesome.com/][Font Awesome]].
- [[https://katex.org][\im \KaTeX \mi]] ::
\im \KaTeX \mi is the “fastest” math typesetting library for the web, and is
- uses to render inline mathematics in my posts at build time. It has been
+ used to render inline mathematics in my posts at build time. It has been
created by [[https://github.com/xymostech][Emily Eisenberg]] and
[[https://sophiebits.com/][Sophie Alpert]], with the help of
[[https://github.com/KaTeX/KaTeX/graphs/contributors][many contributors]].
-- [[https://github.com/tonsky/FiraCode][Fira Code]] ::
- Fira Code is a monospaced font by [[https://github.com/tonsky][Nikita Prokopov]] inspired with Fira Mono by
- the [[https://www.mozilla.org/en-US/][Mozilla Foundation]], with “programming ligatures” (/e.g./, =>>==, ====,
- =!==, etc.), and it is used here for verbatim content (principally source
- code).
-- [[https://github.com/productiontype/spectral][Spectral]] ::
- Spectral is an original typeface designed by Production Type,
- primarily intended for use inside Google’s Docs and Slides. It is
- used as the main font of this website.
-
-#+BEGIN_EXPORT html
-</article>
-#+END_EXPORT