From fbe5ef4028dc61ce28026e66e64ddfcdfcc6f6ec Mon Sep 17 00:00:00 2001 From: Thomas Letan Date: Sun, 23 Feb 2020 13:50:58 +0100 Subject: Give up on clean URLs --- site/posts/StronglySpecifiedFunctions.v | 2 +- site/posts/StronglySpecifiedFunctionsProgram.v | 2 +- site/posts/index.org | 88 ++++++++++++++++++++++++++ site/posts/meta.org | 36 ----------- site/posts/meta/Bootstrap.org | 16 ++--- site/posts/meta/Soupault.org | 2 +- site/posts/meta/index.org | 36 +++++++++++ 7 files changed, 135 insertions(+), 47 deletions(-) create mode 100644 site/posts/index.org delete mode 100644 site/posts/meta.org create mode 100644 site/posts/meta/index.org (limited to 'site/posts') 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 #January 11, 2015#) of a series of two on how to write strongly-specified functions in Coq. You can read the next part #here#. *) + href="./StronglySpecifiedFunctionsProgram.html">here#. *) (** 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 #January 01, 2017#) of a series of two on how to write strongly-specified functions in Coq. You can read the previous part #here#. # *) + href="./StronglySpecifiedFunctions.html">here#. # *) (** #
# 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 +

Write-ups

+ +
+#+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 +
+#+END_Export diff --git a/site/posts/meta.org b/site/posts/meta.org deleted file mode 100644 index 22f200f..0000000 --- a/site/posts/meta.org +++ /dev/null @@ -1,36 +0,0 @@ -#+BEGIN_EXPORT html -

A Series on Generating this Static Website

-#+END_EXPORT - -The generation of this humble static website is far from being trivial, and -require a combination of —too— many tools. It turned out that some choices I -have made early on gave to the build toolchain I ended up writing a pretty nice -property: I could easily integrate its code to the very website it was conceived -to build, by means of [[http://www.literateprogramming.com/][literate programming]]! - -This series is just that: the literate programming document of my home-grown -build toolchain, called *~cleopatra~*. The motivations behind this name are -twofold. First, I wanted to follow the example of [[https://soupault.neocities.org/][~soupault~]], named after [[https://fr.wikipedia.org/wiki/Philippe_Soupault][a -famous personality]]. Secondly, one of my main objective when I started working on -this “project” was to be able to easily use whatever format I wanted to author -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 -
site/posts/meta.org
-
-#+END_EXPORT - -*Beware* this series is far from being complete. - -- [[/posts/meta/Bootstrap][Bootstrapping an Extensible Toolchain ~(WIP)~]] :: - -- [[/posts/meta/Contents][Authoring Content and HTML Generation ~(WIP)~]] :: - -- [[/posts/meta/Theme][Theming and Templating ~(WIP)~]] :: - -- [[/posts/meta/Soupault/][Soupault Configuration ~(WIP)~]] :: - -#+BEGIN_EXPORT html -
-#+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 -~<>~. The syntax is the following: +=extends=. The syntax is the following: #+BEGIN_SRC verbatim <> @@ -220,7 +220,7 @@ previous source block. <> #+END_SRC -Beware that, as a consequence, modifying code block of ~<>~ 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 ~<>~, *~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 ~<>~ 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 = "" - clean_urls = true + clean_urls = false [widgets.page-title] widget = "title" diff --git a/site/posts/meta/index.org b/site/posts/meta/index.org new file mode 100644 index 0000000..db5542e --- /dev/null +++ b/site/posts/meta/index.org @@ -0,0 +1,36 @@ +#+BEGIN_EXPORT html +

A Series on Generating this Static Website

+#+END_EXPORT + +The generation of this humble static website is far from being trivial, and +require a combination of —too— many tools. It turned out that some choices I +have made early on gave to the build toolchain I ended up writing a pretty nice +property: I could easily integrate its code to the very website it was conceived +to build, by means of [[http://www.literateprogramming.com/][literate programming]]! + +This series is just that: the literate programming document of my home-grown +build toolchain, called *~cleopatra~*. The motivations behind this name are +twofold. First, I wanted to follow the example of [[https://soupault.neocities.org/][~soupault~]], named after [[https://fr.wikipedia.org/wiki/Philippe_Soupault][a +famous personality]]. Secondly, one of my main objective when I started working on +this “project” was to be able to easily use whatever format I wanted to author +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 +
site/posts/meta/index.org
+
+#+END_EXPORT + +*Beware* this series is far from being complete. + +- [[./Bootstrap.org][Bootstrapping an Extensible Toolchain]] :: + +- [[./Contents.org][Authoring Content and HTML Generation ~(WIP)~]] :: + +- [[./Soupault.org][Soupault Configuration ~(WIP)~]] :: + +- [[./Theme.org][Theming and Templating ~(WIP)~]] :: + +#+BEGIN_EXPORT html +
+#+END_EXPORT -- cgit v1.2.3