summaryrefslogtreecommitdiffstats
path: root/site/posts
diff options
context:
space:
mode:
authorThomas Letan <lthms@soap.coffee>2020-02-23 13:50:58 +0100
committerThomas Letan <lthms@soap.coffee>2020-02-23 14:28:42 +0100
commitfbe5ef4028dc61ce28026e66e64ddfcdfcc6f6ec (patch)
treec8f70b15ddcdce87e5742ae099debb51e79980cc /site/posts
parentFirst complete draft for the Root of Generation section (diff)
Give up on clean URLs
Diffstat (limited to 'site/posts')
-rw-r--r--site/posts/StronglySpecifiedFunctions.v2
-rw-r--r--site/posts/StronglySpecifiedFunctionsProgram.v2
-rw-r--r--site/posts/index.org88
-rw-r--r--site/posts/meta/Bootstrap.org16
-rw-r--r--site/posts/meta/Soupault.org2
-rw-r--r--site/posts/meta/index.org (renamed from site/posts/meta.org)10
6 files changed, 104 insertions, 16 deletions
diff --git a/site/posts/StronglySpecifiedFunctions.v b/site/posts/StronglySpecifiedFunctions.v
index fa5df95..ac55b7e 100644
--- a/site/posts/StronglySpecifiedFunctions.v
+++ b/site/posts/StronglySpecifiedFunctions.v
@@ -3,7 +3,7 @@
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>#. *)
+ href="./StronglySpecifiedFunctionsProgram.html">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,
diff --git a/site/posts/StronglySpecifiedFunctionsProgram.v b/site/posts/StronglySpecifiedFunctionsProgram.v
index 33200c8..2a998aa 100644
--- a/site/posts/StronglySpecifiedFunctionsProgram.v
+++ b/site/posts/StronglySpecifiedFunctionsProgram.v
@@ -3,7 +3,7 @@
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>#. # *)
+ href="./StronglySpecifiedFunctions.html">here</a>#. # *)
(** #<div id="generate-toc"></div>#
diff --git a/site/posts/index.org b/site/posts/index.org
new file mode 100644
index 0000000..3c583a5
--- /dev/null
+++ b/site/posts/index.org
@@ -0,0 +1,88 @@
+#+OPTIONS: toc:nil num:nil
+
+#+BEGIN_EXPORT html
+<h1>Write-ups</h1>
+
+<article class="index">
+#+END_EXPORT
+
+Over the past years, I have tried to capitalize on my findings. What I have
+lacked in regularity I made up for in subject exoticism.
+
+If you like what you read, have a question or for any other reasons really, you
+can shoot an email to [[mailto:~lthms/lthms.xyz@lists.sr.ht][the dedicated mailing list]] (see the [[https://lists.sr.ht/~lthms/lthms.xyz/%3C20190127111504.n27ttkvtl7l3lzwb%40ideepad.localdomain%3E][annoucement]] for a
+guide on how to subscribe).
+
+* About Coq
+
+Coq is a formal proof management system which provides a pure functional
+language with nice dependent types together with an environment for writing
+machine-checked proofs.
+
+- [[./MiniHTTPServer.html][Implementing and Certifying a Web Server in Coq]] ::
+ An explanation on how to write an almost pure Coq, and working (albeit
+ minimal) HTTP server.
+
+- [[./Ltac101.html][Ltac 101]] ::
+ Ltac is the “tactic language” of Coq. It allows for writing proof scripts
+ which construct proof terms later checked by Coq.
+
+- [[./RewritingInCoq.html][Rewriting in Coq]] ::
+ The ~rewrite~ tactics are really useful, since they are not limited to the Coq
+ built-in equality relation.
+
+- A Series on Strongly-Specified Funcions in Coq ::
+ Coq ~Prop~ sort allows for defining properties function arguments have to
+ satisfy, such that using such a function requires providing a proof the
+ property is satisfied.
+
+ 1. [[./StronglySpecifiedFunctions.html][Using the ~refine~ Tactics]]
+ 2. [[./StronglySpecifiedFunctionsProgram.html][Using the ~Program~ Framework]]
+
+* About Haskell
+
+Haskell is a pure, lazy, functional programming language with a very expressive
+type system.
+
+- [[./ExtensibleTypeSafeErrorHandling.html][Extensible, Type-Safe Error Handling In Haskell]] ::
+ Ever heard of “extensible effects?” By applying the same principle, but for
+ error handling, the result is nice, type-safe API for Haskell, with a lot of
+ GHC magic under the hood.
+
+- [[/posts/MonadTransformers/][Monad Transformers are a Great Abstraction]] ::
+ Monads are hard to get right, monad transformers are harder. Yet, they remain
+ a very powerful abstraction.
+
+* About Common Lisp
+
+Common Lisp is a venerable programming languages like no other I know.
+
+- [[./DiscoveringCommonLisp.html][Discovering Common Lisp with ~trivial-gamekit~]] ::
+ From the creation of a Lisp package up to the creation of a standalone
+ executable.
+
+* About this website
+
+One of my goal with this website is for it to /feel/ simple, but the truth is
+under the hood it is generated from a bunch of files using a not-that-simple
+process.
+
+- [[./meta.html][A Series on Generating this Static Website]] ::
+ The toolchain behind the generation of this website ---called *~cleopatra~*---
+ is a literate programming document which build itself in addition to the HTML
+ files composing this corner of the Internet.
+
+ 1. [[./meta/Bootstrap.html][Bootstrapping an Extensible Toolchain]]
+ 2. [[./meta/Contents.html][Authoring Contents and HTML Generation ~(WIP)~]]
+ 3. [[./meta/Soupault.html][Configuring ~soupault~ ~(WIP)~]]
+ 4. [[./meta/Theme.html][Theming and Templating ~(WIP)~]]
+
+
+- [[./Thanks.html][Thanks!]] ::
+ If it were not for many awesome FOSS projects, this corner of the Internet
+ would not exists. This is my attempt to give well-deserved credit to them and
+ their creators.
+
+#+BEGIN_EXPORT html
+</article>
+#+END_Export
diff --git a/site/posts/meta/Bootstrap.org b/site/posts/meta/Bootstrap.org
index 0f3a07e..8e645c7 100644
--- a/site/posts/meta/Bootstrap.org
+++ b/site/posts/meta/Bootstrap.org
@@ -90,8 +90,8 @@ their output files (using ~+=~).
List *~cleopatra~* Makefiles and scripts tangled throughout the generation
process (with the notable exception of ~Makefile~ itself).
- ~GENSASS~ ::
- List auxiliary ~sass~ files which can be imported by the main ~sass~ files
- (see [[/posts/meta/Theme/][“Theming and Templating”]]).
+ List auxiliary ~sass~ files which can later be imported by the main ~sass~
+ files (see [[./Theme.org][“Theming and Templating”]]).
- ~CONTENTS~ ::
List generated files which are part of the target website, and acts as inputs
for ~soupault~.
@@ -207,7 +207,7 @@ can insert the result of the evaluation of =extends= inside another source block
when the latter is tangled.
The twist is, we derive the rule to tangle ~bootstrap.mk~ using
-~<<extends>>~. The syntax is the following:
+=extends=. The syntax is the following:
#+BEGIN_SRC verbatim
<<extends(IN="Bootstrap.org", MK="bootstrap.mk", GF="scripts/update-gitignore.sh")>>
@@ -220,7 +220,7 @@ previous source block.
<<extends(IN="Bootstrap.org", MK="bootstrap.mk", GF="scripts/update-gitignore.sh")>>
#+END_SRC
-Beware that, as a consequence, modifying code block of ~<<extends>>~ is as
+Beware that, as a consequence, modifying code block of =extends= is as
“dangerous” as modifying ~Makefile~ itself. Keep that in mind if you start
hacking *~cleopatra~*!
@@ -231,7 +231,7 @@ modify ~bootstrap.mk~ accordingly.
* Generation Processes
-Thanks to ~<<extends>>~, *~cleopatra~* is easily extensible. In this section, we
+Thanks to =extends=, *~cleopatra~* is easily extensible. In this section, we
enumerate the generation processes that are currently used to generate the
website you are reading.
@@ -247,16 +247,16 @@ In the present website, contents can be written in the following format:
- Regular Coq files ::
Coq is a system which allows to write machine-checked proofs, and it comes
with a source “prettifier” called ~coqdoc~.
- [[/posts/meta/Contents/Coq/][Learn more about the generation process for Coq files​]]
+ [[./Contents/Coq.org][Learn more about the generation process for Coq files​]]
- Org documents ::
Emacs comes with a powerful editing mode called [[https://orgmode.org/][Org mode]], and Org documents
are really pleasant to work with.
- [[/posts/meta/Contents/Org/][Learn more about the generation process for Org documents]]
+ [[./Contents/Org.org][Learn more about the generation process for Org documents]]
If you want *~cleopatra~* to support more input formats, you have to
1. Create a org file which, once tangled, provide a dedicated makefile
-2. Edit this file (~Bootstrap.org~) here, and use ~<<extends>>~ to make sure it
+2. Edit this file (~Bootstrap.org~) here, and use =extends= to make sure it
is actually tangled when necessary
#+BEGIN_SRC makefile :tangle bootstrap.mk :noweb tangle :exports none
diff --git a/site/posts/meta/Soupault.org b/site/posts/meta/Soupault.org
index 913c8ae..aab5476 100644
--- a/site/posts/meta/Soupault.org
+++ b/site/posts/meta/Soupault.org
@@ -23,7 +23,7 @@
default_template = "templates/main.html"
content_selector = "main"
doctype = "<!DOCTYPE html>"
- clean_urls = true
+ clean_urls = false
[widgets.page-title]
widget = "title"
diff --git a/site/posts/meta.org b/site/posts/meta/index.org
index 22f200f..db5542e 100644
--- a/site/posts/meta.org
+++ b/site/posts/meta/index.org
@@ -17,19 +17,19 @@ my contents. Did you know that Cleopatra was a reputed polyglot (at least
according to [[https://fr.wikipedia.org/wiki/Polyglotte][Wikipedia France]])?
#+BEGIN_EXPORT html
-<div id="history">site/posts/meta.org</div>
+<div id="history">site/posts/meta/index.org</div>
<article class="index">
#+END_EXPORT
*Beware* this series is far from being complete.
-- [[/posts/meta/Bootstrap][Bootstrapping an Extensible Toolchain ~(WIP)~]] ::
+- [[./Bootstrap.org][Bootstrapping an Extensible Toolchain]] ::
-- [[/posts/meta/Contents][Authoring Content and HTML Generation ~(WIP)~]] ::
+- [[./Contents.org][Authoring Content and HTML Generation ~(WIP)~]] ::
-- [[/posts/meta/Theme][Theming and Templating ~(WIP)~]] ::
+- [[./Soupault.org][Soupault Configuration ~(WIP)~]] ::
-- [[/posts/meta/Soupault/][Soupault Configuration ~(WIP)~]] ::
+- [[./Theme.org][Theming and Templating ~(WIP)~]] ::
#+BEGIN_EXPORT html
</article>