summaryrefslogtreecommitdiffstats
path: root/site
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
parent1a197fb354a82a31deca4f9b118f057bbd0038b6 (diff)
2021 Spring redesign
Diffstat (limited to 'site')
-rw-r--r--site/cleopatra.org62
-rw-r--r--site/cleopatra/commands.org36
-rw-r--r--site/cleopatra/coq.org60
-rw-r--r--site/cleopatra/dependencies.org89
-rw-r--r--site/cleopatra/literate-programming.org27
-rw-r--r--site/cleopatra/org.org183
-rw-r--r--site/cleopatra/soupault.org811
-rw-r--r--site/cleopatra/theme.org722
-rw-r--r--site/coq.org44
-rw-r--r--site/haskell.org13
-rw-r--r--site/img/icons.svg39
-rw-r--r--site/img/merida.webpbin36922 -> 0 bytes
-rw-r--r--site/index.org77
-rw-r--r--site/meta.org23
-rw-r--r--site/miscellaneous.org14
-rw-r--r--site/news/index.html15
-rw-r--r--site/opinions/MonadTransformers.org13
-rw-r--r--site/opinions/index.org6
-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
33 files changed, 1392 insertions, 1010 deletions
diff --git a/site/cleopatra.org b/site/cleopatra.org
index 77e8ff1..0831621 100644
--- a/site/cleopatra.org
+++ b/site/cleopatra.org
@@ -1,46 +1,44 @@
-#+BEGIN_EXPORT html
-<h1>A Series on Generating this Static Website</h1>
-#+END_EXPORT
+#+TITLE: A Series on Generating this Static Website
-The generation of this website is far from being trivial, and requires the
-combination of —probably too— many tools. For instance, my write-ups about Coq
-are actually Coq files, and I use ~coqdoc~ to generate the HTML pages you read.
-The theme is not written in CSS, but in SASS that needs to be compiled. Even
-more, the whole website is postprocessed using ~soupault~.
+#+SERIES: ./meta.html
+#+SERIES_PREV: ./posts/Thanks.html
+
+At some point, I felt like the whole process of generating this
+website was interesting enough so that it would deserve a write-up of
+its own, but the risk was that such a piece of text would quickly
+become out-dated. This is reminescent of documenting any software
+project, and I was aware at that time of a dedicated paradigm to
+prevent these kind of issues: [[http://www.literateprogramming.com/][literate programming]].
-At some point, I felt like the whole process was interesting enough so that it
-would deserve a write-up of its own, but the risk was that such a piece of text
-would quickly become out-dated. This is reminescent of documenting any software
-project, and I was aware at that time of a dedicated paradigm to prevent these
-kind of issues: [[http://www.literateprogramming.com/][literate programming]].
I spent quite some time turning my custom toolchain into a literate program, so
that its actual code source would actually be the write-ups I wanted to add to
my website. This was an interesting challenge, since it meant *~cleopatra~*
would have to generate itself before it could build my website. In other words,
*~cleopatra~* achieves the bootstsrapping challenge!
-I really enjoyed this first experiment with literate programming, and I started
-using *~cleopatra~* for other projects of mine where literate programming felt
-like an interesting choice. In doing so, it quickly became clear *~cleopatra~*
-was cumbersome to set-up for a new project. At the end,
-[[https://cleopatra.soap.coffee][I ended up rewriting it]] to overcome the
-specific issues posed by its initial design[fn:bootstrap]. But the so-called
-generation processes I had written for *~cleopatra~* the first basically “just
-worked” with *~cleopatra~* the second.
+I really enjoyed this first experiment with literate programming, and
+I started using *~cleopatra~* for other projects of mine where
+literate programming felt like an interesting choice. In doing so, it
+quickly became clear *~cleopatra~* was cumbersome to set-up for a new
+project. At the end, [[https://cleopatra.soap.coffee][I ended up rewriting it]] to overcome the specific
+issues posed by its initial design[fn::For the record, this second
+version is also implemented using literate programming, and if I was
+first using the first version to build it, I quickly “made the
+bootstrap jump.”]. But the so-called generation processes I had
+written for *~cleopatra~* the first basically “just worked” with
+*~cleopatra~* the second.
So, coming back to this series, it is just the very reason why I started using
*~cleopatra~* in the first place: the generation processes used by this website,
written as literate programs.
-#+BEGIN_EXPORT html
-<article class="index">
-#+END_EXPORT
+- [[./cleopatra/dependencies.org][Installing Dependencies]] ::
-- [[./cleopatra/theme.org][Theming and Templating]] ::
+- [[file:cleopatra/coq.org][Authoring Contents with Coq ~(TODO)~]] ::
-- [[file:cleopatra/coq.org][Authoring Contents As Coq Documents ~(TODO)~]] ::
+- [[./cleopatra/org.org][Authoring Contents with ~org-mode~ ~(TODO)~]] ::
-- [[./cleopatra/literate-programming.org][Authoring Literate Programs]] ::
+- [[./cleopatra/literate-programming.org][Literate Programming Projects]] ::
Literate programming is an interesting exercice, and it is
particularly well-suited for blog posts, since at the very least it
provides the tool to enforce the code presented to readers is
@@ -48,7 +46,7 @@ written as literate programs.
programming projects present in the ~posts/~ directory of this
website.
-- [[./cleopatra/org.org][Authoring Contents As Org Documents ~(TODO)~]] ::
+- [[./cleopatra/theme.org][Layout and Style]] ::
- [[./cleopatra/soupault.org][Processing HTML with ~soupault~]] ::
~soupault~ is a HTML processor, and it can be used as a static website
@@ -57,11 +55,3 @@ written as literate programs.
*Appendix:* In case you are curious, you can have a look at
[[./posts/CleopatraV1.html][the first implementaiton of *~cleopatra~*]].
-
-#+BEGIN_EXPORT html
-</article>
-#+END_EXPORT
-
-[fn:bootstrap] For the record, this second version is also implemented using
-literate programming, and if I was first using the first version to build it, I
-quickly “made the bootstrap jump.”
diff --git a/site/cleopatra/commands.org b/site/cleopatra/commands.org
new file mode 100644
index 0000000..fbf0430
--- /dev/null
+++ b/site/cleopatra/commands.org
@@ -0,0 +1,36 @@
+#+TITLE: Adhoc *~cleopatra~* commands
+
+#+SERIES: ../cleopatra.html
+#+SERIES_PREV: ./soupault.html
+
+In this generation process, we provide adhoc commands to ease the
+authoring experience. A given command ~<cmd>~ is implemented as a
+~makefile~ rule, and can be called with ~cleopatra <cmd>~.
+
+#+BEGIN_EXPORT html
+<nav id="generate-toc"></nav>
+<div id="history">site/cleopatra/commands.org</div>
+#+END_EXPORT
+
+* ~serve~
+
+ This command spawns a simple HTTP server which allows us to navigate
+ the website more easily.
+
+ #+begin_src makefile :tangle commands.mk
+serve :
+ @cleopatra echo Spwaning "HTTP server"
+ @cd out && python -m http.server
+ #+end_src
+
+* ~update~
+
+ This commands updates the various dependencies locally installed to
+ build this website, such as ~soupault~ for instance.
+
+ #+begin_src makefile :tangle commands.mk
+update :
+ @cleopatra echo "Updating" "OCaml dependencies"
+ @opam update
+ @opam upgrade -y
+ #+end_src
diff --git a/site/cleopatra/coq.org b/site/cleopatra/coq.org
index 64d1e9d..81f3d27 100644
--- a/site/cleopatra/coq.org
+++ b/site/cleopatra/coq.org
@@ -1,3 +1,15 @@
+#+TITLE: Authoring Content with Coq
+
+#+SERIES: ../cleopatra.html
+#+SERIES_PREV: ./dependencies.html
+#+SERIES_NEXT: ./org.html
+
+#+BEGIN_EXPORT html
+<nav id="generate-toc"></nav>
+<div id="history">site/cleopatra/coq.org</div>
+#+END_EXPORT
+
+
* Author Guidelines
* Under the Hood
@@ -13,7 +25,6 @@ COQ_ARTIFACTS := $(COQ_POSTS:.v=.vo) \
coq-build : ${COQ_HTML}
-theme-build : site/style/coq.sass
soupault-build : coq-build
ARTIFACTS += ${COQ_ARTIFACTS} .lia.cache
@@ -28,52 +39,9 @@ COQDOCARG := --no-index --charset utf8 --short \
--external "https://compcert.org/doc/html" compcert \
--external "https://lysxia.github.io/coq-simple-io" SimpleIO
-%.html : %.v coq.mk
- @cleopatra echo Exporting "$*.v"
+%.html : %.v coq.mk _opam/init
+ @cleopatra echo Exporting "$*.v"
@coqc ${COQCARG} $<
@coqdoc ${COQDOCARG} -d $(shell dirname $<) $<
@rm -f $(shell dirname $<)/coqdoc.css
#+END_SRC
-
-#+BEGIN_SRC sass :tangle site/style/coq.sass
-div.code
- padding-left : 1.5rem
- padding-left : 1.5rem
- white-space: nowrap
- line-height : 140%
-
-div.code,
-span.inlinecode
- font-family : 'Fira Code', monospace
- color : $monospace-color
- font-size : 80%
- overflow-x : auto
-
-div.doc
- max-width : $content-width
- line-height : 140%
-
- /* dirty patch to get the code in full page width */
- pre
- width : calc(100vw - 2*var(--side-margin))
-
-.paragraph
- margin-bottom : .8em
-#+END_SRC
-
-#+BEGIN_SRC sass :tangle site/style/coq.sass
-.code
- a[href]
- color : inherit
- text-decoration : none
- background : #f7f7f7
- padding : .1rem .15rem .1rem .15rem
- border-radius : 15%
-
- .url-mark
- display: none
-#+END_SRC
-
-# Local Variables:
-# org-src-preserve-indentation: t
-# End:
diff --git a/site/cleopatra/dependencies.org b/site/cleopatra/dependencies.org
new file mode 100644
index 0000000..5a79741
--- /dev/null
+++ b/site/cleopatra/dependencies.org
@@ -0,0 +1,89 @@
+#+TITLE: Installing Dependencies
+
+#+SERIES: ../cleopatra.html
+#+SERIES_NEXT: ./coq.html
+
+* OCaml and Coq
+
+ #+caption: Dependencies for Coq articles
+ #+name: coq-deps
+ | Package | Version |
+ |--------------+---------|
+ | coq | 8.13.1 |
+ | coq-compcert | 3.8 |
+
+ #+caption: Dependencies for the ~coqffi~ series
+ #+name: lp-deps
+ | Package | Version |
+ |---------------+-------------|
+ | dune | 2.8.4 |
+ | coq-coqffi | 1.0.0~beta5 |
+ | coq-simple-io | 1.5.0 |
+
+ #+caption: Soupault
+ #+name: soupault-deps
+ | Package | Version |
+ |----------+---------|
+ | soupault | 2.5.0 |
+
+ #+name: deps-listing
+ #+begin_src emacs-lisp :noweb yes :var coq-deps=coq-deps :var lp-deps=lp-deps :var soupault-deps=soupault-deps :results value raw :exports none
+;; We use this Emacs Lisp snippet to generate the list of dependencies
+;; we have to install with Opam
+(defun fmt-deps (d)
+ (mapconcat (lambda (d) (format "%s" d)) d "."))
+
+(string-join
+ (append (mapcar 'fmt-deps lp-deps)
+ (mapcar 'fmt-deps soupault-deps)
+ (mapcar 'fmt-deps coq-deps))
+ " ")
+ #+end_src
+
+ #+begin_src makefile :tangle dependencies.mk :noweb yes
+OCAML_VERSION := 4.11.2
+OCAML := ocaml-base-compiler.${OCAML_VERSION}
+
+_opam/init :
+ @cleopatra echo "Creating" "a local Opam switch"
+ @opam switch create . ${OCAML} --repos default,coq-released || true
+ @cleopatra echo "Installing" "OCaml dependencies"
+ @opam install <<deps-listing()>> -y
+ @touch $@
+
+CONFIGURE += _opam
+ #+end_src
+
+* Frontend
+
+ #+caption: Frontend dependencies
+ #+name: frontend-deps
+ | Package | Version |
+ |---------------+---------|
+ | katex | 0.13.0 |
+ | minify | 7.0.1 |
+ | normalize.css | 8.0.1 |
+
+ #+name: frontend-listing
+ #+begin_src emacs-lisp :var frontend-deps=frontend-deps :exports none
+;; We use this Emacs Lisp snippet to generate the list of dependencies
+;; we have to install with npm
+(defun fmt-deps (d)
+ (format " \"%s\": \"^%s\"" (nth 0 d) (nth 1 d)))
+
+(string-join (mapcar 'fmt-deps frontend-deps) ",\n")
+ #+end_src
+
+ #+begin_src json :tangle package.json :noweb yes
+{
+ "dependencies": {
+ <<frontend-listing()>>
+ }
+}
+ #+end_src
+
+ #+begin_src makefile :tangle dependencies.mk :noweb yes
+package-lock.json : package.json
+ @cleopatra echo "Installing" "frontend dependencies"
+ @npm install
+ #+end_src
diff --git a/site/cleopatra/literate-programming.org b/site/cleopatra/literate-programming.org
index be25097..63e0b02 100644
--- a/site/cleopatra/literate-programming.org
+++ b/site/cleopatra/literate-programming.org
@@ -1,6 +1,8 @@
-#+BEGIN_EXPORT html
-<h1>Literate Programming Projects</h1>
-#+END_EXPORT
+#+TITLE: Literate Programming Projects
+
+#+SERIES: ../cleopatra.html
+#+SERIES_PREV: ./org.html
+#+SERIES_NEXT: ./theme.html
Literate programming is an interesting exercice. It forces programmers
to think about how to present their code for other people to
@@ -12,18 +14,27 @@ That being said, literate programming is particularly well-suited for
blog posts, since at the very least it provides the tool to enforce
the code presented to readers is correct.
+#+BEGIN_EXPORT html
+<nav id="generate-toc"></nav>
+<div id="history">site/cleopatra/literate-programming.org</div>
+#+END_EXPORT
+
+* Tangling
+
We use Emacs and ~org-mode~ to tangle the literate programming
projects present in the ~posts/~ directory of this website. This is
done with the following emacs lisp script.
#+BEGIN_SRC emacs-lisp :tangle export-lp.el
-(cleopatra:configure) ; opinionated configuration provided by cleopatra
+;; opinionated configuration provided by cleopatra
+(cleopatra:configure)
+;; allow the execution of shell block code
(org-babel-do-load-languages
'org-babel-load-languages
- '((shell . t))) ; allow the execution of shell block code
+ '((shell . t)))
- ;; scan the posts/ directory and tangled it into lp/
+;; scan the posts/ directory and tangled it into lp/
(setq org-publish-project-alist
'(("lp"
:base-directory "site/posts"
@@ -46,6 +57,8 @@ literate-programming-prebuild :
ARTIFACTS += lp/ site/posts/deps.svg
#+END_SRC
+* Building
+
In the =build= phase, we actually try to compile the tangled projects.
As of now, there is only one literate program: [[../posts/CoqffiEcho.org][the Echo server
implemented in Coq]] which demonstrates how ~coqffi~ can be used to
@@ -54,7 +67,7 @@ implement realistic software projects.
#+BEGIN_SRC makefile :tangle literate-programming.mk
COQFFI_ARCHIVE := site/files/coqffi-tutorial.tar.gz
-coqffi-tutorial-build : literate-programming-prebuild
+coqffi-tutorial-build : literate-programming-prebuild _opam/init
@cleopatra echo "Building" "coqffi tutorial"
@cd lp/coqffi-tutorial; dune build --display quiet
@cleopatra echo "Archiving" "coqffi tutorial"
diff --git a/site/cleopatra/org.org b/site/cleopatra/org.org
index acfd432..829272b 100644
--- a/site/cleopatra/org.org
+++ b/site/cleopatra/org.org
@@ -1,54 +1,30 @@
-* Author Guidelines
-
-* Under the Hood
+#+TITLE: Authoring Content with ~org-mode~
-#+BEGIN_SRC emacs-lisp :tangle scripts/packages.el
-(use-package lua-mode :ensure t :defer t)
-(use-package rust-mode :ensure t :defer t)
-(use-package sass-mode :ensure t :defer t)
-(use-package haskell-mode :ensure t :defer t)
-(use-package toml-mode :ensure t :defer t)
-(use-package json-mode :ensure t :defer t)
-(use-package proof-general :ensure t :defer t)
-(use-package tuareg :ensure t :defer t)
-#+END_SRC
-
-#+BEGIN_SRC emacs-lisp :tangle scripts/export-org.el
-(cleopatra:configure)
+#+SERIES: ../cleopatra.html
+#+SERIES_PREV: ./coq.html
+#+SERIES_NEXT: ./literate-programming.html
-(setq org-html-doctype "html5")
-(setq org-html-html5-fancy t)
-
-(org-babel-do-load-languages
- 'org-babel-load-languages
- '((shell . t)
- (dot . t)))
+#+BEGIN_EXPORT html
+<nav id="generate-toc"></nav>
+<div id="history">site/cleopatra/org.org</div>
+#+END_EXPORT
-(setq org-html-htmlize-output-type nil)
-(setq org-export-with-toc nil)
-
-(add-to-list 'org-entities-user
- '("im" "\\(" nil "<span class=\"imath\">" "" "" ""))
-(add-to-list 'org-entities-user
- '("mi" "\\)" nil "</span>" "" "" ""))
+* Author Guidelines
-(org-html-export-to-html nil nil nil t)
-#+END_SRC
+* Implementation
-#+BEGIN_SRC makefile :tangle org.mk
+#+begin_src makefile :tangle org.mk
EMACS := cleopatra-emacs
-ORG_POSTS := $(shell find site/ -name "*.org")
-ORG_HTML := $(ORG_POSTS:.org=.html)
+ORG_IN := $(shell find site/ -name "*.org")
+ORG_OUT := $(ORG_IN:.org=.html)
org-prebuild : .emacs
-org-build : ${ORG_HTML}
+org-build : ${ORG_OUT}
-theme-build : site/style/org.sass
soupault-build : org-build
-org-build : literate-programming-build
-ARTIFACTS += ${ORG_HTML}
+ARTIFACTS += ${ORG_OUT}
CONFIGURE += .emacs
EXPORT := --batch \
@@ -68,44 +44,91 @@ INIT := --batch --load="${ROOT}/scripts/packages.el" \
.emacs org.mk
@cleopatra echo Exporting "$*.org"
@${EMACS} $< ${EXPORT}
-#+END_SRC
-
-#+BEGIN_SRC sass :tangle site/style/org.sass
-#text-footnotes
- max-width : 35rem
-
-.footpara
- display: inline
- margin-left: .2em
-
-.section-number-2:after,
-.section-number-3:after
- content: ". "
-
-.section-number-4,
-.section-number-5,
-.section-number-6
- display: none
-
-dl
- dd p
- margin-top: 0
-
-.footnotes
- font-size : 1rem
-
-.org-literate-programming
- .org-src-tangled-to:before
- content: "\f054"
- font : normal normal normal 11px/1 ForkAwesome
-
- .org-src-tangled-to,
- padding-left : 2rem
-
- .org-src-tangled-to,
- .org-src-name
- font-family : 'Fira Code', monospace
- font-size : 70%
- font-weight: bold
- color : #444
-#+END_SRC
+#+end_src
+
+#+begin_src emacs-lisp :tangle scripts/packages.el
+(use-package ox-tufte :ensure t)
+#+end_src
+
+#+begin_src emacs-lisp :tangle scripts/export-org.el
+(cleopatra:configure)
+
+(org-babel-do-load-languages
+ 'org-babel-load-languages
+ '((dot . t)
+ (shell . t)))
+
+(setq org-export-with-toc nil
+ org-html-htmlize-output-type nil
+ org-export-with-section-numbers nil)
+
+(add-to-list 'org-entities-user
+ '("im" "\\(" nil "<span class=\"imath\">" "" "" ""))
+(add-to-list 'org-entities-user
+ '("mi" "\\)" nil "</span>" "" "" ""))
+
+(defun with-keyword (keyword k)
+ "Look-up for keyword KEYWORD, and call continuation K with its value."
+ (pcase (org-collect-keywords `(,keyword))
+ (`((,keyword . ,kw))
+ (when kw (funcall k (string-join kw " "))))))
+
+(defun get-keyword (keyword)
+ "Look-up for keyword KEYWORD, and returns its value"
+ (with-keyword keyword (lambda (x) x)))
+
+(defun get-org-title (path)
+ "Fetch the title of an Org file whose path is PATH."
+ (with-temp-buffer
+ (find-file-read-only path)
+ (get-keyword "TITLE")))
+
+(defun insert-title ()
+ "Insert the title of the article."
+ (with-keyword
+ "TITLE"
+ (lambda (title)
+ (insert
+ (format "\n\n@@html:<h1>@@ %s @@html:</h1>@@\n\n" title)))))
+
+(defun insert-series ()
+ "Insert the series root link."
+ (with-keyword
+ "SERIES"
+ (lambda (series)
+ (insert "\n\n#+attr_html: :class series\n")
+ (insert series))))
+
+(defun insert-series-prev ()
+ "Insert the series previous article link."
+ (with-keyword
+ "SERIES_PREV"
+ (lambda (series-prev)
+ (insert "\n\n#+attr_html: :class series-prev\n")
+ (insert series-prev))))
+
+(defun insert-series-next ()
+ "Insert the series next article link."
+ (with-keyword
+ "SERIES_NEXT"
+ (lambda (series-next)
+ (insert "\n\n#+attr_html: :class series-next\n")
+ (insert series-next))))
+
+(defun insert-nav ()
+ "Insert the navigation links."
+ (when (get-keyword "SERIES")
+ (insert "\n\n#+begin_nav\n")
+ (insert-series)
+ (insert-series-prev)
+ (insert-series-next)
+ (insert "\n\n#+end_nav\n")))
+
+(beginning-of-buffer)
+(insert-nav)
+(insert-title)
+
+(let ((outfile (org-export-output-file-name ".html"))
+ (org-html-footnotes-section "<!-- %s --><!-- %s -->"))
+ (org-export-to-file 'tufte-html outfile nil nil nil t))
+#+end_src
diff --git a/site/cleopatra/soupault.org b/site/cleopatra/soupault.org
index 452f442..92042c2 100644
--- a/site/cleopatra/soupault.org
+++ b/site/cleopatra/soupault.org
@@ -1,209 +1,136 @@
-#+BEGIN_EXPORT html
-<h1><code>soupault</code> Configuration</h1>
-#+END_EXPORT
+#+TITLE: ~soupault~
-#+NAME: build-dir
-#+BEGIN_SRC text :exports none
-build
-#+END_SRC
+#+SERIES: ../cleopatra.html
+#+SERIES_PREV: ./theme.html
+#+SERIES_NEXT: ./commands.html
-#+NAME: prefix
-#+BEGIN_SRC text :exports none
-~lthms
-#+END_SRC
+We use ~soupault~ to build this website[fn::~soupault~ is an awesome
+free software project, with a unique approach to static website
+generation. You should definitely [[https://soupault.app][check out their website]]!].
+
+#+begin_export html
+<nav id="generate-toc"></nav>
+#+end_export
-In a nutshell, the purpose of ~soupault~ is to post-process HTML files
-generated by the generation processes of *~cleopatra~*
+* Installation
-The rest of this document proceeds as follows. We first describe the general
-settings of ~soupault~. Then, we enumerate the widgets enabled for this website.
-Finally, we provide a proper definition for ~soupault~ the *~cleopatra~*
-generation process.
+ We install ~soupault~ in a local switch. We use a witness file
+ ~_opam/.init~ to determine whether or not our switch has always been
+ created during a previous invocation of *~cleopatra~*.
-#+TOC: headlines 2
+ #+begin_src makefile :tangle soupault.mk
+OCAML_VERSION := 4.11.2
+OCAML := ocaml-base-compiler.${OCAML_VERSION}
-* ~soupault~ General Settings
+CONFIGURE += _opam rss.json
+ARTIFACTS += out
-The general ~settings~ section of ~soupault.conf~ is fairly basic, and there is
-little to say that the
-[[https://soupault.neocities.org/reference-manual/#getting-started][“Getting
-Started”]] already discuss in length.
+soupault-prebuild : _opam/init
+ #+end_src
-We emphasize three things:
+ Using ~soupault~ is as simple as calling it, without any particular
+ command-line arguments.
+
+ #+begin_src makefile :tangle soupault.mk
+soupault-build : package-lock.json style.min.css
+ @cleopatra echo "Executing" "soupault"
+ @soupault
+ #+end_src
-- The ~build_dir~ is set to src_text[:exports code :noweb yes]{<<build-dir>>/<<prefix>>}
- in place of simply src_text[:exports code :noweb yes]{<<build-dir>>}.
-- The ~ignore_extensions~ shall be updated to take into account artifacts
- produces by other *~cleopatra~* generation processes.
-- We disable the “clean URLs” feature of ~soupault. This option renames
- a HTML files ~foo/bar.html~ into ~foo/bar/index.html~, which means when served
- by a HTTP server, the ~foo/bar~ URL will work. The issue we have with this
- feature is that the internal links within your websiste needs to take their
- /final/ URL into account, rather than their actual name. If one day ~soupault~
- starts rewriting internal URLs when ~clean_url~ is enabled, we might
- reconsider using it.
+ We now describe our configuration file for ~soupault~.
+
+* Configuration
+
+ #+name: base-dir
+ #+begin_src verbatim :noweb yes :exports none
+~lthms
+ #+end_src
-#+BEGIN_SRC toml :tangle soupault.conf :noweb yes
+** Global Settings
+
+ The options of the ~[settings]~ section of a ~soupault~
+ configuration are often self-explanatory, and we do not spend too
+ much time to detaul them.
+
+ #+begin_src toml :tangle soupault.conf :noweb yes
[settings]
strict = true
-verbose = false
-debug = false
site_dir = "site"
-build_dir = "<<build-dir>>/<<prefix>>"
-
+build_dir = "out/<<base-dir>>"
+doctype = "<!DOCTYPE html>"
+clean_urls = false
+generator_mode = true
+complete_page_selector = "html"
+default_content_selector = "main"
page_file_extensions = ["html"]
ignore_extensions = [
- "draft", "vo", "vok", "vos", "glob",
- "html~", "org", "aux", "sass",
+ "v", "vo", "vok", "vos", "glob",
+ "html~", "org"
]
-
-generator_mode = true
-complete_page_selector = "html"
default_template_file = "templates/main.html"
-default_content_selector = "main"
-doctype = "<!DOCTYPE html>"
-clean_urls = false
-#+END_SRC
-
-#+BEGIN_TODO
-The list of ignored extensions should be programmatically generated with the
-help of *~cleopatra~*.
-#+END_TODO
-
-* Widgets
+pretty_print_html = false
+ #+end_src
** Setting Page Title
-We use the “page title” widget to set the title of the webpage based on the
-first (and hopefully the only) ~<h1>~ tag of the page.
+ We use the “page title” widget to set the title of the webpage
+ based on the first (and hopefully the only) ~<h1>~ tag of the
+ page.
-#+BEGIN_SRC toml :tangle soupault.conf
+ #+begin_src toml :tangle soupault.conf
[widgets.page-title]
widget = "title"
selector = "h1"
default = "~lthms"
prepend = "~lthms: "
-#+END_SRC
+ #+end_src
** Acknowledging ~soupault~
-When creating a new ~soupault~ project (using ~soupault --init~), the default
-configuration file suggests advertising the use of ~soupault~. Rather than
-hard-coding the used version of ~soupault~ (which is error-prone), we rather
-determine the version of ~soupault~ with the following script.
+ When creating a new ~soupault~ project (using ~soupault --init~),
+ the default configuration file suggests advertising the use of
+ ~soupault~. Rather than hard-coding the used version of ~soupault~
+ (which is error-prone), we rather determine the version of
+ ~soupault~ with the following script.
-#+NAME: soupault-version
-#+BEGIN_SRC bash :results verbatim output
+ #+NAME: soupault-version
+ #+begin_src bash :results verbatim output
soupault --version | head -n 1 | tr -d '\n'
-#+END_SRC
+ #+end_src
-The configuration of the widget ---initially provided by ~soupault~--- becomes
-less subject to the obsolescence.
+ The configuration of the widget ---initially provided by
+ ~soupault~--- becomes less subject to the obsolescence[fn::That
+ is, as long as ~soupault~ does not change the output of its
+ ~--version~ option.].
-#+BEGIN_SRC toml :tangle soupault.conf :noweb yes
+ #+begin_src toml :tangle soupault.conf :noweb yes
[widgets.generator-meta]
widget = "insert_html"
html = """<meta name="generator" content="<<soupault-version()>>">"""
selector = "head"
-#+END_SRC
-
-** Generating Table of Contents
-
-The ~toc~ widget allows for generating a table of contents for HTML files which
-contains a node matching a given ~selector~ (in the case of this document,
-~#generate-toc~).
-
-#+BEGIN_SRC toml :tangle soupault.conf
-[widgets.table-of-contents]
-widget = "toc"
-selector = "#generate-toc"
-action = "replace_element"
-valid_html = true
-min_level = 2
-numbered_list = true
-#+END_SRC
-
-#+BEGIN_TODO
-We could propose a patch to ~soupault~'s upstream to add numbering in titles.
-#+END_TODO
-
-** Fixing Org Internal Links
-
-For some reason, Org prefix internal links to other Org documents with
-~file://~. To avoid that, we provide a simple plugin which removes ~file://~
-from the begining of a URL.
-
-#+BEGIN_TODO
-This plugin definition should be part of [[./Contents/Org.org][the ~org~
-generation process]], but that would require to aggregate “subconfig” into a
-larger one.
-#+END_TODO
-
-This plugin key component is the =fix_org_urls= function.
-
-- =fix_org_urls(LIST, ATTR)= ::
- Enumerate the DOM elements of =LIST=, and check their =ATTR= attribute.
-
-#+BEGIN_SRC lua :tangle plugins/fix-org-urls.lua
-function fix_org_urls(list, attr)
- index, link = next(list)
-
- while index do
- href = HTML.get_attribute(link, attr)
-
- if href then
- href = Regex.replace(href, "^file://", "")
- HTML.set_attribute(link, attr, href)
- end
-
- index, link = next(list, index)
- end
-end
-#+END_SRC
-
-We use this function to fix the URLs of tags known to be subject to Org strange
-behavior. For now, only ~<a>~ has been affected.
-
-#+BEGIN_SRC lua :tangle plugins/fix-org-urls.lua
-fix_org_urls(HTML.select(page, "a"), "href")
-fix_org_urls(HTML.select(page, "img"), "src")
-#+END_SRC
-
-The configuration of this plugin, and the associated widget, is straightforward.
-
-#+BEGIN_SRC toml :tangle soupault.conf :noweb tangle
-[widgets.fix-org-urls]
-widget = "fix-org-urls"
-#+END_SRC
+ #+end_src
** Prefixing Internal URLs
-On the one hand, internal links can be absolute, meaning they start with a
-leading ~/~, and therefore are relative to the website root. On the other hand,
-website (especially static website) can be placed in larger context. For
-instance, my personal website lives inside the ~~lthms~ directory of the
-~soap.coffee~ domain.
+ On the one hand, internal links can be absolute, meaning they
+ start with a leading ~/~, and therefore are relative to the
+ website root. On the other hand, website (especially static
+ website) can be placed in larger context. For instance, my
+ personal website lives inside the ~~lthms~ directory of the
+ ~soap.coffee~ domain[fn::To my experience in hosting webapps and
+ websites, this set-up is way harder to get right than I initially
+ expect.].
-The purpose of this plugin is to rewrite internal URLs which are relative to the
-root, in order to properly prefix them.
+ The purpose of this plugin is to rewrite internal URLs which are relative to the
+ root, in order to properly prefix them.
-From a high-level perspective, the plugin structure is the following.
+ From a high-level perspective, the plugin structure is the following.
-#+BEGIN_SRC lua :tangle plugins/urls-rewriting.lua :noweb no-export
-prefix_url = config["prefix_url"]
-<<validate_prefix>>
+ First, we validate the widget configuration.
-<<prefix_func>>
-<<prefix_calls>>
-#+END_SRC
-
-1. We validate the widget configuration.
-2. We propose a generic function to enumerate and rewrite tags which can have
- internal URLs as attribute argument.
-3. We use this generic function for relevant tags.
+ #+BEGIN_SRC lua :tangle plugins/urls-rewriting.lua
+prefix_url = config["prefix_url"]
-#+NAME: validate_prefix
-#+BEGIN_SRC lua
if not prefix_url then
Plugin.fail("Missing mandatory field: `prefix_url'")
end
@@ -215,10 +142,12 @@ end
if not Regex.match(prefix_url, "(.*)/$") then
prefix_url = prefix_url .. "/"
end
-#+END_SRC
+ #+END_SRC
+
+ Then, we propose a generic function to enumerate and rewrite tags
+ which can have.
-#+NAME: prefix_func
-#+BEGIN_SRC lua
+ #+BEGIN_SRC lua :tangle plugins/urls-rewriting.lua
function prefix_urls (links, attr, prefix_url)
index, link = next(links)
@@ -236,33 +165,35 @@ function prefix_urls (links, attr, prefix_url)
index, link = next(links, index)
end
end
-#+END_SRC
+ #+END_SRC
-#+NAME: prefix_calls
-#+BEGIN_SRC lua
+ Finally, we use this generic function for relevant tags.
+
+ #+BEGIN_SRC lua :tangle plugins/urls-rewriting.lua
prefix_urls(HTML.select(page, "a"), "href", prefix_url)
prefix_urls(HTML.select(page, "link"), "href", prefix_url)
prefix_urls(HTML.select(page, "img"), "src", prefix_url)
prefix_urls(HTML.select(page, "script"), "src", prefix_url)
-#+END_SRC
+prefix_urls(HTML.select(page, "use"), "href", prefix_url)
+ #+END_SRC
-Again, configuring soupault to use this plugin is relatively straightforward.
-The only important thing to notice is the use of the ~after~ field, to ensure
-this plugin is run /after/ the plugin responsible for fixing Org documents URLs.
+ Again, configuring soupault to use this plugin is relatively
+ straightforward.
-#+BEGIN_SRC toml :tangle soupault.conf :noweb tangle
+ #+BEGIN_SRC toml :tangle soupault.conf :noweb yes
[widgets.urls-rewriting]
widget = "urls-rewriting"
-prefix_url = "<<prefix>>"
-after = "fix-org-urls"
-#+END_SRC
+prefix_url = "<<base-dir>>"
+after = "mark-external-urls"
+ #+END_SRC
** Marking External Links
-#+BEGIN_SRC lua :tangle plugins/external-urls.lua
+ #+BEGIN_SRC lua :tangle plugins/external-urls.lua
function mark(name)
- return '<i class="url-mark fa fa-' .. name ..
- '" aria-hidden="true"></i>'
+ return '<span class="icon"><svg><use href="/img/icons.svg#'
+ .. name ..
+ '"></use></svg></span>'
end
links = HTML.select(page, "a")
@@ -274,85 +205,101 @@ while index do
if href then
if Regex.match(href, "^https?://github.com") then
- icon = HTML.parse(mark('github'))
+ icon = HTML.parse(mark("github"))
HTML.append_child(link, icon)
elseif Regex.match(href, "^https?://") then
- icon = HTML.parse(mark('external-link'))
+ icon = HTML.parse(mark("external-link"))
HTML.append_child(link, icon)
end
end
index, link = next(links, index)
end
-#+END_SRC
-
-#+BEGIN_SRC sass :tangle site/style/plugins.sass
-.url-mark.fa
- display: inline
- font-size: 90%
- width: 1em
-
-.url-mark.fa-github::before
- content: "\00a0\f09b"
+ #+END_SRC
-.url-mark.fa-external-link::before
- content: "\00a0\f08e"
-#+END_SRC
-
-#+BEGIN_SRC toml :tangle soupault.conf
+ #+BEGIN_SRC toml :tangle soupault.conf
[widgets.mark-external-urls]
after = "generate-history"
widget = "external-urls"
-#+END_SRC
+ #+END_SRC
+
+** Generating a Table of Contents
+
+ The ~toc~ widget allows for generating a table of contents for
+ HTML files which contains a node matching a given ~selector~ (in
+ the case of this document, ~#generate-toc~).
+
+ #+begin_src toml :tangle soupault.conf
+[widgets.table-of-contents]
+widget = "toc"
+selector = "#generate-toc"
+action = "replace_content"
+valid_html = true
+min_level = 2
+max_level = 3
+numbered_list = false
+heading_links = true
+heading_link_text = " §"
+heading_links_append = true
+heading_link_class = "anchor-link"
+
+[widgets.append-toc-title]
+widget = "preprocess_element"
+selector = "#generate-toc"
+command = 'echo "<h2>Table of Contents</h2> $(cat)"'
+after = "table-of-contents"
+ #+end_src
** Generating Per-File Revisions Tables
*** Users Instructions
-This widgets allows to generate a so-called “revisions table” of the filename
-contained in a DOM element of id ~history~, based on its history. Paths should
-be relative to the directory from which you start the build process (typically,
-the root of your repository). The revisions table notably provides hyperlinks to
-a ~git~ webview for each commit.
+ This widgets allows to generate a so-called “revisions table” of
+ the filename contained in a DOM element of id ~history~, based on
+ its history. Paths should be relative to the directory from which
+ you start the build process (typically, the root of your
+ repository). The revisions table notably provides hyperlinks to a
+ ~git~ webview for each commit.
-For instance, considering the following HTML snippet
+ For instance, considering the following HTML snippet
-#+BEGIN_SRC html
+ #+begin_src html
<div id="history">
site/posts/FooBar.org
</div>
-#+END_SRC
+ #+end_src
-This plugin will replace the content of this ~<div>~ with the revisions table of
-~site/posts/FooBar.org~.
+ This plugin will replace the content of this ~<div>~ with the
+ revisions table of ~site/posts/FooBar.org~.
*** Customization
-The base of the URL webview for the document you are currently reading
-—afterwards abstracted with the ~<<repo>>~ noweb reference— is
+ The base of the URL webview for the document you are currently
+ reading is src_verbatim[:noweb yes :exports code]{<<repo>>}.
-#+NAME: repo
-#+BEGIN_SRC text
+ #+name: repo
+ #+begin_src verbatim :exports none
https://code.soap.coffee/writing/lthms.git
-#+END_SRC
+ #+end_src
-#+BEGIN_SRC html :tangle templates/history.html :noweb tangle
-<details class="history">
+ The template used to generate the revision table is the following.
+
+ #+begin_src html :tangle templates/history.html :noweb yes
+<details id="history">
<summary>Revisions</summary>
<p>
This revisions table has been automatically generated
- from <a href="<<repo>>">the <code>git</code> history
- of this website repository</a>, and the change
- descriptions may not always be as useful as they
- should.
+ from <a href="<<repo>>">the
+ <code>git</code> history of this website repository</a>, and the
+ change descriptions may not always be as useful as they should.
</p>
<p>
- You can consult the source of this file in its current
- version <a href="<<repo>>/tree/{{file}}">here</a>.
+ You can consult the source of this file in its current version
+ <a href="<<repo>>/tree/{{file}}">here</a>.
</p>
- <table>
+ <table class="fullwidth">
{{#history}}
<tr>
<td class="date"
@@ -362,66 +309,44 @@ https://code.soap.coffee/writing/lthms.git
{{#modified}}
id="modified-at"
{{/modified}}
- >
- {{date}}
- </td>
+ >{{date}}</td>
<td class="subject">{{subject}}</td>
<td class="commit">
- <a href="<<repo>>/commit/{{filename}}/?id={{hash}}">
- {{abbr_hash}}
- </a>
+ <a href="<<repo>>/commit/{{filename}}/?id={{hash}}">{{abbr_hash}}</a>
</td>
</tr>
{{/history}}
</table>
</details>
-#+END_SRC
-
-#+BEGIN_SRC sass :tangle site/style/plugins.sass
-table
- border-top : 2px solid black
- border-bottom : 2px solid black
- border-collapse : collapse
- width : 35rem
-
-td
- border-bottom : 1px solid black
- padding : .5em
-
-#history .commit
- font-size : smaller
- font-family : 'Fira Code', monospace
- width : 7em
- text-align : center
-#+END_SRC
+ #+end_src
*** Implementation
-We use the built-in [[https://soupault.neocities.org/reference-manual/#widgets-preprocess-element][=preprocess_element=]] to implement, which means we need a
-script which gets its input from the standard input, and echoes its output to
-the standard input.
+ We use the built-in [[https://soupault.neocities.org/reference-manual/#widgets-preprocess-element][=preprocess_element=]] to implement, which
+ means we need a script which gets its input from the standard
+ input, and echoes its output to the standard input.
-#+BEGIN_SRC toml :tangle soupault.conf
+ #+begin_src toml :tangle soupault.conf
[widgets.generate-history]
widget = "preprocess_element"
selector = "#history"
command = 'scripts/history.sh templates/history.html'
-action = "replace_content"
-#+END_SRC
+action = "replace_element"
+ #+end_src
-This plugin proceeds as follows:
+ This plugin proceeds as follows:
-1. Using an ad-hoc script, it generates a JSON containing for each revision
- - The subject, date, hash, and abbreviated hash of the related commit
- - The name of the file at the time of this commit
-2. This JSON is passed to a mustache engine (~haskell-mustache~) with a
- proper template
-3. The content of the selected DOM element is replaced with the output of
- ~haskell-mustache~
+ 1. Using an ad-hoc script, it generates a JSON containing for each revision
+ - The subject, date, hash, and abbreviated hash of the related commit
+ - The name of the file at the time of this commit
+ 2. This JSON is passed to a mustache engine (~haskell-mustache~) with a
+ proper template
+ 3. The content of the selected DOM element is replaced with the output of
+ ~haskell-mustache~
-This translates in Bash like this.
+ This translates in Bash like this.
-#+BEGIN_SRC bash :tangle scripts/history.sh :shebang "#!/usr/bin/bash"
+ #+begin_src bash :tangle scripts/history.sh :shebang "#!/usr/bin/bash"
function main () {
local file="${1}"
local template="${2}"
@@ -431,26 +356,27 @@ function main () {
haskell-mustache ${template} ${tmp_file}
rm ${tmp_file}
}
-#+END_SRC
-
-Generating the expected JSON is therefore as simple as:
-
-- Fetching the logs
-- Reading 8 line from the logs, parse the filename from the 6th
- line
-- Outputing the JSON
-
-We will use ~git~ to get the information we need. By default, ~git~
-subcommands use a pager when its output is likely to be long. This
-typically includes ~git-log~. To disable this behavior, ~git~ exposes
-the ~--no-pager~ command. Besides, we also need ~--follow~ and
-~--stat~ to deal with file renaming. Without this option, ~git-log~
-stops when the file first appears in the repository, even if this
-“creation” is actually a renaming. Therefore, the ~git~ command line
-we use to collect our history is
-
-#+NAME: gitlog
-#+BEGIN_SRC bash :tangle scripts/history.sh :noweb yes
+ #+end_src
+
+ Generating the expected JSON is therefore as simple as:
+
+ - Fetching the logs
+ - Reading 8 line from the logs, parse the filename from the 6th
+ line
+ - Outputing the JSON
+
+ We will use ~git~ to get the information we need. By default,
+ ~git~ subcommands use a pager when its output is likely to be
+ long. This typically includes ~git-log~. To disable this
+ behavior, ~git~ exposes the ~--no-pager~ command. Besides, we
+ also need ~--follow~ and ~--stat~ to deal with file
+ renaming. Without this option, ~git-log~ stops when the file
+ first appears in the repository, even if this “creation” is
+ actually a renaming. Therefore, the ~git~ command line we use to
+ collect our history is
+
+ #+name: gitlog
+ #+begin_src bash :tangle scripts/history.sh :noweb yes
function gitlog () {
local file="${1}"
git --no-pager log \
@@ -459,33 +385,35 @@ function gitlog () {
--pretty=format:'%s%n%h%n%H%n%cs%n' \
"${file}"
}
-#+END_SRC
+ #+end_src
-This function will generate a sequence of 8 lines containing all the
-relevant information we are looking for, for each commit, namely:
+ This function will generate a sequence of 8 lines containing all
+ the relevant information we are looking for, for each commit,
+ namely:
-- Subject
-- Abbreviated hash
-- Full hash
-- Date
-- Empty line
-- Change summary
-- Shortlog
-- Empty line
+ - Subject
+ - Abbreviated hash
+ - Full hash
+ - Date
+ - Empty line
+ - Change summary
+ - Shortlog
+ - Empty line
-For instance, the =gitlog= function will output the following lines
-for the last commit of this very file:
+ For instance, the =gitlog= function will output the following
+ lines for the last commit of this very file:
-#+BEGIN_SRC bash :results verbatim :exports results :noweb yes
+ #+begin_src bash :results verbatim :exports results :noweb yes
<<gitlog>>
gitlog "soupault.org" | head -n8
-#+END_SRC
+ #+end_src
-Among other things, the 6th line contains the filename. We need to
-extract it, and we do that with ~sed~. In case of file renaming, we
-need to parse something of the form ~both/to/{old => new}~.
+ Among other things, the 6th line contains the filename. We need
+ to extract it, and we do that with ~sed~. In case of file
+ renaming, we need to parse something of the form ~both/to/{old =>
+ new}~.
-#+BEGIN_SRC bash :tangle scripts/history.sh :noweb yes
+ #+begin_src bash :tangle scripts/history.sh :noweb yes
function parse_filename () {
local line="${1}"
local shrink='s/ *\(.*\) \+|.*/\1/'
@@ -493,18 +421,18 @@ function parse_filename () {
echo ${line} | sed -e "${shrink}" | sed -e "${unfold}"
}
-#+END_SRC
-
-The next step is to process the logs to generate the expected JSON. We
-have to deal with the fact that JSON does not allow the last item of
-an array to be concluded by ",". Besides, we also want to indicate
-which commit is responsible for the creation of the file. To do that,
-we use two variables: =idx= and =last_entry=. When =idx= is equal to
-0, we know it is the latest commit. When =idx= is equal to
-=last_entry=, we know we are looking at the oldest commit for that
-file.
-
-#+BEGIN_SRC bash :tangle scripts/history.sh :noweb yes
+ #+end_src
+
+ The next step is to process the logs to generate the expected
+ JSON. We have to deal with the fact that JSON does not allow the
+ last item of an array to be concluded by ",". Besides, we also
+ want to indicate which commit is responsible for the creation of
+ the file. To do that, we use two variables: =idx= and
+ =last_entry=. When =idx= is equal to 0, we know it is the latest
+ commit. When =idx= is equal to =last_entry=, we know we are
+ looking at the oldest commit for that file.
+
+ #+begin_src bash :tangle scripts/history.sh :noweb yes
function generate_json () {
local input="${1}"
local logs="$(gitlog ${input})"
@@ -562,11 +490,11 @@ function generate_json () {
echo -n "]}"
}
-#+END_SRC
+ #+end_src
-Generating the JSON object for a given commit is as simple as
+ Generating the JSON object for a given commit is as simple as
-#+BEGIN_SRC bash :tangle scripts/history.sh :noweb yes
+ #+begin_src bash :tangle scripts/history.sh :noweb yes
function output_json_entry () {
local subject="${1}"
local abbr_hash="${2}"
@@ -585,66 +513,31 @@ function output_json_entry () {
echo -n ",\"filename\":\"${file}\""
echo -n "}"
}
-#+END_SRC
+ #+end_src
-And we are done! We can safely call the =main= function to generate
-our revisions table.
+ And we are done! We can safely call the =main= function to generate
+ our revisions table.
-#+BEGIN_SRC bash :tangle scripts/history.sh
+ #+begin_src bash :tangle scripts/history.sh
main "$(cat)" "${1}"
-#+END_SRC
+ #+end_src
** Rendering Equations Offline
*** Users instructions
-Inline equations written in the DOM under the class src_css{.imath} and using
-the \im \LaTeX \mi syntax can be rendered once and
-for all by ~soupault~. User For instance, ~<span class="imath">\LaTeX</span>~ is
-rendered \im \LaTeX \mi as expected.
+ Inline equations written in the DOM under the class
+ src_css{.imath} and using the \im \LaTeX \mi syntax can be
+ rendered once and for all by ~soupault~. User For instance,
+ ~<span class="imath">\LaTeX</span>~ is rendered \im \LaTeX \mi as
+ expected.
-Using this widgets requires being able to inject raw HTML in input files.
+ Using this widgets requires being able to inject raw HTML in
+ input files.
*** Implementation
-We will use [[https://katex.org][\im \KaTeX \mi]] to render equations offline. \im \KaTeX \mi
-availability on most systems is unlikely, but it is part of [[https://www.npmjs.com/package/katex][npm]], so we can
-define a minimal ~package.json~ file to fetch it automatically.
-
-#+BEGIN_SRC json :tangle package.json
-{
- "private": true,
- "devDependencies": {
- "katex": "^0.11.1"
- }
-}
-#+END_SRC
-
-We introduce a Makefile recipe to call ~npm install~. This command produces a
-file called ~package-lock.json~ that we add to ~GENFILES~ to ensure \im \KaTeX
-\mi will be available when ~soupault~ is called.
-
-If ~Soupault.org~ has been modified since the last generation, Babel will
-generate ~package.json~ again. However, if the modifications of ~Soupault.org~
-do not concern ~package.json~, then ~npm install~ will not modify
-~package-lock.json~ and its “last modified” time will not be updated. This means
-that the next time ~make~ will be used, it will replay this recipe again. As a
-consequence, we systematically ~touch~ ~packase-lock.json~ to satisfy ~make~.
-
-#+BEGIN_SRC makefile :tangle katex.mk
-package-lock.json : package.json
- @cleopatra echo "Fetching" "npm packages"
- @npm install &>> build.log
- @touch $@
-
-CONFIGURE += package-lock.json node_modules/
-#+END_SRC
-
-Once installed and available, \im \KaTeX \mi is really simple to use. The
-following script reads (synchronously!) the standard input, renders it using \im
-\KaTeX \mi and outputs the resut to the standard output.
-
-#+BEGIN_SRC js :tangle scripts/katex.js
+ #+begin_src js :tangle scripts/render-equations.js
var katex = require("katex");
var fs = require("fs");
var input = fs.readFileSync(0);
@@ -656,102 +549,160 @@ var html = katex.renderToString(String.raw`${input}`, {
});
console.log(html)
-#+END_SRC
+ #+end_src
-We reuse once again the =preprocess_element= widget. The selector is ~.imath~
-(~i~ stands for inline in this context), and we replace the previous content
-with the result of our script.
+ We reuse once again the =preprocess_element= widget. The selector
+ is ~.imath~ (~i~ stands for inline in this context), and we
+ replace the previous content with the result of our script.
-#+BEGIN_SRC toml :tangle soupault.conf
+ #+begin_src toml :tangle soupault.conf
[widgets.inline-math]
widget = "preprocess_element"
selector = ".imath"
-command = "node scripts/katex.js"
+command = "node scripts/render-equations.js"
action = "replace_content"
[widgets.display-math]
widget = "preprocess_element"
selector = ".dmath"
-command = "DISPLAY=1 node scripts/katex.js"
+command = "DISPLAY=1 node scripts/render-equations.js"
action = "replace_content"
-#+END_SRC
+ #+end_src
+
+** RSS Feed
+
+ #+begin_src toml :tangle soupault.conf
+[index]
+index = true
+dump_json = "rss.json"
+extract_after_widgets = ["urls-rewriting"]
+
+[index.fields]
+title = {
+ selector = ["h1"]
+}
-The \im\KaTeX\mi font is bigger than the serif font used for this
-website, so we reduce it a bit with a dedicated SASS rule.
+modified-at = {
+ selector = ["#modified-at"]
+}
-#+BEGIN_SRC sass :tangle site/style/plugins.sass
-.imath, .dmath
- font-size : smaller
+created-at = {
+ selector = ["#created-at"]
+}
+ #+end_src
-.dmath
- text-align : center
-#+END_SRC
+** Series Navigation
-* *~cleopatra~* Generation Process Definition
+ #+begin_src lua :tangle plugins/series.lua
+function get_title_from_path (path)
+ if Sys.is_file(path) then
+ local content_raw = Sys.read_file(path)
+ local content_dom = HTML.parse(content_raw)
+ local title = HTML.select_one(content_dom, "h1")
-We introduce the ~soupault~ generation process, obviously based on the
-[[https://soupault.neocities.org/][~soupault~ HTML processor]]. The structure of
-a *~cleopatra~* generation process is always the same.
+ if title then
+ return String.trim(HTML.inner_html(title))
+ else
+ Plugin.fail(path .. ' has no <h1> tag')
+ end
+ else
+ Plugin.fail(path .. ' is not a file')
+ end
+end
+ #+end_src
+
+ #+begin_src lua :tangle plugins/series.lua
+function generate_nav_item_from_title (title, url, template)
+ local env = {}
+ env["url"] = url
+ env["title"] = title
+ local new_content = String.render_template(template, env)
+ return HTML.parse(new_content)
+end
+ #+end_src
-#+BEGIN_SRC makefile :tangle soupault.mk :noweb no-export
-<<stages>>
-<<dependencies>>
-<<ad-hoc-cmds>>
-#+END_SRC
+ #+begin_src lua :tangle plugins/series.lua
+function generate_nav_items (cwd, cls, template)
+ local elements = HTML.select(page, cls)
-In the rest of this section, we define these three components.
+ local i = 1
+ while elements[i] do
+ local element = elements[i]
+ local url = HTML.strip_tags(element)
+ local path = Sys.join_path(cwd, url)
+ local title_str = get_title_from_path(path)
-** Build Stages
+ HTML.replace_content(
+ element,
+ generate_nav_item_from_title(title_str, url, template)
+ )
-From the perspective of *~cleopatra~*, it is a rather simple component, since
-the ~build~ stage is simply a call to ~soupault~, whose outputs are located in a
-single (configurable) directory.
+ i = i + 1
+ end
+end
+ #+end_src
-#+NAME: stages
-#+BEGIN_SRC makefile :noweb yes
-soupault-build :
- @cleopatra echo Running soupault
- @soupault
+ #+begin_src lua :tangle plugins/series.lua
+cwd = Sys.dirname(page_file)
-ARTIFACTS += <<build-dir>>/
-#+END_SRC
+home_template = 'This article is part of the series “<a href="{{ url }}">{{ title }}</a>.”'
+nav_template = '<a href="{{ url }}">{{ title }}</a>'
-** Dependencies
+generate_nav_items(cwd, ".series", home_template)
+generate_nav_items(cwd, ".series-prev", nav_template)
+generate_nav_items(cwd, ".series-next", nav_template)
+ #+end_src
-Most of the generation processes (if not all of them) need to declare themselves
-as a prerequisite for ~soupault-build~. If they do not, they will likely be
-executed after ~soupault~ is called.
+#+begin_src toml :tangle soupault.conf
+[widgets.series]
+widget = "series"
+#+end_src
-This file defines an auxiliary SASS sheet that needs to be declared as a
-dependency of the build stage of the [[./Theme.org][~theme~ generation
-process]].
+** Injecting Minified CSS
-Finally, the offline rendering of equations requires \im \KaTeX \mi to be
-available, so we include the ~katex.mk~ file, and make ~package-lock.json~ (the
-proof that ~npm install~ has been executed) a prerequisite of ~soupault-build~.
+ #+begin_src lua :tangle plugins/css.lua
+style = HTML.select_one(page, "style")
-#+NAME: dependencies
-#+BEGIN_SRC makefile
-theme-build : site/style/plugins.sass
-include katex.mk
-soupault-build : package-lock.json
-#+END_SRC
+if style then
+ css = HTML.create_text(Sys.read_file("style.min.css"))
+ HTML.replace_content(style, css)
+end
+ #+end_src
-** Ad-hoc Commands
+ #+begin_src toml :tangle soupault.conf
+[widgets.css]
+widget = "css"
+ #+end_src
-Finally, this generation process introduces a dedicated (~PHONY~) command to
-start a HTTP server in order to navigate the generated website from a browser.
+** Cleaning-up
-#+NAME: ad-hoc-cmds
-#+BEGIN_SRC makefile :noweb yes
-serve :
- @echo " start a python server"
- @cd <<build-dir>>; python -m http.server 2>/dev/null
+ #+begin_src lua :tangle plugins/clean-up.lua
+function remove_if_empty(html)
+ if String.trim(HTML.inner_html(html)) == "" then
+ HTML.delete(html)
+ end
+end
+ #+end_src
+
+ #+begin_src lua :tangle plugins/clean-up.lua
+function remove_all_if_empty(cls)
+ local elements = HTML.select(page, cls)
+
+ local i = 1
+ while elements[i] do
+ local element = elements[i]
+ remove_if_empty(element)
+ i = i + 1
+ end
+end
+ #+end_src
-.PHONY : serve
-#+END_SRC
+ #+begin_src lua :tangle plugins/clean-up.lua
+remove_all_if_empty("p") -- introduced by org-mode
+remove_all_if_empty("div.code") -- introduced by coqdoc
+ #+end_src
-This command does not assume anything about the current state of generation of
-the project. In particular, it does not check whether or not the ~<<build-dir>>~
-directory exists. The responsibility to use ~make serve~ in a good setting lies
-with final users.
+#+begin_src toml :tangle soupault.conf
+[widgets.clean-up]
+widget = "clean-up"
+#+end_src
diff --git a/site/cleopatra/theme.org b/site/cleopatra/theme.org
index dce9520..9041be8 100644
--- a/site/cleopatra/theme.org
+++ b/site/cleopatra/theme.org
@@ -1,267 +1,471 @@
-#+BEGIN_EXPORT html
-<h1>Theming and Templating</h1>
-#+END_EXPORT
+#+TITLE: Layout and Style
-The purpose of this build process is to implement the default layout of this
-website. To that end, it provides a template file (~main.html~), and a
-collection of SASS files that *~cleopatra~* then compiles into a single CSS file
-using ~sassc~.
+#+SERIES: ../cleopatra.html
+#+SERIES_PREV: ./literate-programming.html
+#+SERIES_NEXT: ./soupault.html
-We first discuss the structure of the website, by defining the default HTML
-template =soupault= will use to generate the website. Then, we specify its
-minimal design, implemented in SASS. Finally, we discuss the necessary build
-instructions for *~cleopatra~*.
+#+BEGIN_EXPORT html
+<nav id="generate-toc"></nav>
+<div id="history">site/cleopatra/theme.org</div>
+#+END_EXPORT
-* Main HTML Template
+* Setup
+
+ As often when it comes to frontend development, we will use several
+ tools hosted in the ~npm~ packages repository. ~npm~ is infamous
+ for downloading lots of files and to store it in the ~node_modules/~
+ directory. We configure *~cleopatra~* accordingly.
+
+ #+begin_src makefile :tangle theme.mk
+CONFIGURE += package.json package-lock.json node_modules
+ #+end_src
+
+* Base CSS
+
+ We know construct piece by piece the “base” CSS layout which we will
+ inject inside a ~<style>~ tag in each web page.
+
+** Layout
+
+ Our goal is to have a three columns layout: one aside menu, with
+ the top-level navigation links (technical articles, news, etc.) and
+ the table of contents of the current pages if relevant, one main
+ area for the webpage content, and a margin column with side notes
+ and margin notes.
+
+ #+begin_src css :tangle style.css
+:root {
+ --main-width: 30rem;
+ --gutter-width: 5rem;
+ --margin-width: 15rem;
+ --body-width: calc(var(--main-width) + var(--gutter-width) + var(--margin-width));
+}
+
+@media (max-width: 55rem) {
+ :root {
+ --body-width: var(--main-width);
+ }
+}
+ #+end_src
+
+ #+begin_src css :tangle style.css
+,* {
+ box-sizing: border-box;
+}
+
+.fullwidth {
+ width: var(--body-width);
+}
+
+html {
+ font-size: 1.1rem;
+}
+
+body {
+ line-height: 1.3;
+ max-width: var(--body-width);
+ margin-left: auto;
+ margin-right: auto;
+}
+
+aside {
+ background: var(--bg);
+ z-index: 9999;
+ width: var(--body-width);
+ align-self: flex-start;
+ position: sticky;
+ top: 0;
+}
+
+aside nav {
+ text-align: center;
+ border-bottom: 1px solid var(--fade);
+}
+
+aside nav ul {
+ list-style: none;
+ padding: 1rem 0;
+ margin: 0;
+}
+
+aside nav li {
+ display: inline;
+}
+
+aside nav li:not(:first-of-type)::before {
+ content: " · ";
+}
+
+main {
+ counter-reset: sidenote-counter;
+ max-width: var(--main-width);
+}
+
+main nav {
+ font-style: italic;
+ font-size: smaller;
+ color: var(--fg-plus);
+ background: var(--current-line);
+ padding: .5rem 1rem;
+}
+
+main nav .series-next {
+ text-align: right;
+}
+
+main nav p.series-next::after {
+ content: " →";
+}
+
+main nav p.series-prev::before {
+ content: "← ";
+}
+
+img {
+ max-width: 100%;
+}
+
+.sidenote,
+.marginnote {
+ font-size: smaller;
+ float: right;
+ clear: right;
+ margin-right: calc(-1 * (var(--margin-width) + var(--gutter-width)));
+ width: var(--margin-width);
+ position: relative;
+}
+
+input.margin-toggle {
+ display: none;
+}
+
+label.sidenote-number {
+ display: inline;
+}
+
+label.margin-toggle:not(.sidenote-number) {
+ display: none;
+}
+
+.sidenote-number:after,
+.sidenote:before {
+ position: relative;
+ vertical-align: baseline;
+}
+
+.sidenote-number {
+ counter-increment: sidenote-counter;
+}
+
+.sidenote-number::after {
+ content: "(" counter(sidenote-counter, lower-greek) ")";
+ font-size: 60%;
+ top: -0.4rem;
+ left: 0.1rem;
+}
+
+.sidenote::before {
+ content: "(" counter(sidenote-counter, lower-greek) ")";
+ font-size: 70%;
+ top: -0.5rem;
+ right: 0.1rem;
+}
+
+div.code,
+pre {
+ width: var(--body-width);
+ overflow-x: auto;
+ overflow-y: hidden;
+ padding: 1rem 2rem;
+}
+
+main {
+ padding-top: 4.2rem;
+}
+
+h1 {
+ text-align: center;
+}
+
+h2, h3, h4 {
+ font-style: italic;
+}
+
+h1, h2, h3, h4 {
+ font-weight: normal;
+}
+
+dt {
+ font-weight: bold;
+}
+
+div.code,
+span.inlinecode,
+code,
+.doc pre,
+tt,
+.dmath,
+.imath {
+ font-family: monospace;
+ font-size: 80%;
+}
+
+details {
+ margin: 1.5rem 0;
+}
+
+table {
+ border-top: 2px solid var(--fg);
+ border-bottom: 2px solid var(--fg);
+ border-collapse: collapse;
+ width: 100%;
+ margin: 1.5rem 0;
+}
+
+th {
+ font-weight: normal;
+ text-transform: uppercase;
+}
+
+td,
+th {
+ border-top: 1px solid var(--fade);
+ height: 2em;
+ padding: 0 1em;
+}
+
+td.date,
+td.commit {
+ text-align: center;
+ font-size: 0.75em;
+ font-family: monospace;
+}
+
+/* max-width has to be equal to --body-width */
+@media (max-width: 55rem) {
+ body {
+ padding: 2rem;
+ margin: auto;
+ display: block;
+ }
+
+ aside {
+ width: var(--main-width);
+ margin: auto;
+ }
+
+ label.margin-toggle:not(.sidenote-number) {
+ display: inline;
+ }
+
+ .sidenote,
+ .marginnote {
+ display: none;
+ }
+
+ .margin-toggle:checked + .sidenote,
+ .margin-toggle:checked + .marginnote {
+ display: block;
+ float: left;
+ left: 1rem;
+ clear: both;
+ width: 95%;
+ margin: 1rem 2.5%;
+ vertical-align: baseline;
+ position: relative;
+ }
+
+ label {
+ cursor: pointer;
+ }
+
+ pre, aside {
+ width: 100%;
+ }
+}
+ #+end_src
+
+** Colors
+
+ #+begin_src css :tangle style.css
+:root {
+ --bg: white;
+ --bg-plus: #f9f8f4;
+ --current-line: #fbfbfb;
+ --fade: #cfcecb;
+ --fg: #3c3c3c;
+ --fg-plus: #575757;
+ --doc: #ff4c99;
+ --warning: #bd745e;
+ --red: #b3534b;
+ --green: #6d9319;
+ --yellow: #d4b100;
+}
+ #+end_src
+
+ #+begin_src css :tangle style.css
+body {
+ font-family: serif;
+ color: var(--fg);
+ background: var(--bg);
+}
+
+a[href] {
+ color: inherit;
+ text-decoration-color: var(--doc);
+}
+
+h2 a.anchor-link,
+h3 a.anchor-link,
+h4 a.anchor-link {
+ display: none;
+ font-style: normal;
+ text-decoration: none;
+ font-family: monospace;
+ font-size: smaller;
+ color: var(--doc);
+}
+
+[id] {
+ scroll-margin-top: 4rem;
+}
+
+h2:hover a.anchor-link,
+h3:hover a.anchor-link,
+h4:hover a.anchor-link {
+ display: inline;
+}
+
+.sidenote,
+.marginnote {
+ color: var(--fg-plus);
+}
+
+.sidenote-number:after,
+.sidenote:before,
+pre,
+code,
+div.code,
+span.inlinecode,
+tt {
+ color: var(--doc);
+}
+ #+end_src
+
+** Coq
+
+ #+begin_src css :tangle style.css
+div.code {
+ white-space: nowrap;
+}
+
+div.code,
+span.inlinecode {
+ font-family : monospace;
+}
+
+.paragraph {
+ margin-bottom : .8em;
+}
+
+.code a[href] {
+ color : inherit;
+ text-decoration : none;
+ background : var(--bg-plus);
+ padding : .1rem .15rem .1rem .15rem;
+ border-radius : 15%;
+}
+
+.code .icon {
+ display: none;
+}
+#+END_SRC
-#+BEGIN_SRC html :tangle templates/main.html :noweb yes
+** Icons
+
+ #+begin_src css :tangle style.css
+.icon svg {
+ fill: var(--doc);
+ display: inline;
+ width: 1em;
+ height: .9em;
+ vertical-align: text-top;
+}
+
+.url-mark.fa {
+ display: inline;
+ font-size: 90%;
+ width: 1em;
+}
+
+.url-mark.fa-github::before {
+ content: "\00a0\f09b";
+}
+
+.url-mark.fa-external-link::before {
+ content: "\00a0\f08e";
+}
+ #+end_src
+
+** Minify CSS
+
+ #+begin_src shell :shebang #!/bin/bash :tangle scripts/css.sh
+minify="$(npm bin)/minify"
+normalize="$(npm root)/normalize.css/normalize.css"
+style="style.css"
+
+# minify add a newline character at the end of its input
+# we remove it using `head'
+echo "
+@charset \"UTF-8\";
+$(cat ${normalize})
+$(cat ${style})
+" | ${minify} --css | head -c -1 > style.min.css
+ #+end_src
+
+ #+begin_src makefile :tangle theme.mk
+style.min.css : style.css
+ @cleopatra echo "Minifying" "CSS"
+ @scripts/css.sh
+
+ARTIFACTS += style.min.css
+
+theme-build : style.min.css
+ #+end_src
+
+* HTML Templates
+
+ It would be best if we had a preprocessing step to inject the
+ minified style, rather than using ~soupault~ to do the work once per
+ page.
+
+ #+begin_src html :tangle templates/main.html :noweb yes
<html lang="en">
<head>
- <<meta-tags>>
- <title><!-- page title will be inserted here --></title>
- <<syncloading_html>>
- <<asyncloading_html>>
+ <meta charset="utf-8">
+ <meta name="viewport" content="width=device-width, initial-scale=1.0">
+ <style></style>
+ <link href="https://soap.coffee/+vendors/katex.0.11.1+swap/katex.css" rel="stylesheet" media="none" onload="if(media!='all')media='all'">
+ <title></title>
</head>
- <<body>>
+ <body>
+ <aside>
+ <nav>
+ <ul>
+ <li>
+ <a href="/">Technical Posts</a>
+ </li>
+ <li>
+ <a href="/opinions">Opinions</a>
+ </li>
+ <li>
+ <a href="/news">News</a>
+ </li>
+ </ul>
+ </nav>
+ </aside>
+ <main>
+ </main>
+ </body>
</html>
-#+END_SRC
-
-** ~<head>~
-
-#+NAME: meta-tags
-#+BEGIN_SRC html :noweb no-export
-<meta charset="utf-8">
-<meta name="viewport"
- content="width=device-width, initial-scale=1.0">
-#+END_SRC
-
-*** Assets Loading
-
-#+NAME: syncloading_html
-#+BEGIN_SRC html
-<link href="https://soap.coffee/+vendors/normalize.css.8.0.1/normalize.css"
- rel="stylesheet">
-<link rel="stylesheet" href="/style/main.css">
-<link rel="icon" type="image/ico" href="/img/merida.webp">
-#+END_SRC
-
-#+NAME: asyncloading_js
-#+BEGIN_SRC js
-let noscript = document.getElementById('asyncloading');
-noscript.insertAdjacentHTML('beforebegin', noscript.innerText);
-noscript.parentNode.removeChild(noscript);
-#+END_SRC
-
-#+NAME: asyncloading_html
-#+BEGIN_SRC html
-<noscript id="asyncloading">
- <link href="https://soap.coffee/+vendors/fira-code.2+swap/font.css"
- rel="stylesheet">
- <link href="https://soap.coffee/+vendors/katex.0.11.1+swap/katex.css"
- rel="stylesheet">
- <link href="https://soap.coffee/+vendors/fork-awesome.1.1.7+swap/css/fork-awesome.min.css"
- rel="stylesheet">
-</noscript>
-#+END_SRC
-
-** ~body~
-
-#+NAME: body
-#+BEGIN_SRC html :noweb no-export
-<body>
- <header>
- <a href="/">Technical Articles</a> /
- <a href="/opinions">Opinions</a> /
- <a href="/news">News</a> /
- <a href="/projects">Projects</a>
- </header>
- <main>
- <!-- page content will be inserted here -->
- </main>
- <footer>
- <img src="https://soap.coffee/~lthms/img/merida.webp"
- alt="Merida from the movie Ralph 2.0 from Disney is the
- avatar I use most of the time on the Internet"
- title="lthms’ avatar" />
-
- <p>
- Hi, I’m <strong>lthms</strong>, and this is my humble corner of the
- Internet. You are very welcome here! If you are interested in
- <em>functional programming</em>, <em>formal verification</em>, or <em>free
- software projects in the making</em>, you may even enjoy your stay!
- </p>
-
- <p>
- This website has been generated using a collection of <a
- href="/posts/Thanks.html">awesome free software projects</a>. You can have
- a look at <a href="https://code.soap.coffee/writing/lthms.git/">the source
- of this website</a> or <a href="/cleopatra.html">how it is being
- generated</a>, and if you run into an error, feel free to <a
- href="mailto:lthms@soap.coffee">shoot me a friendly email</a>.
- </p>
- </footer>
- <script>
- <<asyncloading_js>>
- </script>
-</body>
-#+END_SRC
-
-* Main SASS File
-
-First, we introduce a set of variables.
-
-#+BEGIN_SRC sass :tangle site/style/main.sass
-$content-width : 30rem
-$large-side-margin : 7rem
-$small-side-margin : 2rem
-$monospace-color : #FF006D
-#+END_SRC
-
-Then, we introduce a key CSS variable whose definition will change according to
-the current width of the page (something we cannot achieve with SASS variables,
-whose behavior is purely static).
-
-#+BEGIN_SRC sass :tangle site/style/main.sass
-\:root
- @media screen and (min-width: calc(#{$content-width} + 2 * #{$large-side-margin}))
- --side-margin : #{$large-side-margin}
- @media screen and (max-width: calc(#{$content-width} + 2 * #{$large-side-margin}))
- --side-margin : #{$small-side-margin}
-#+END_SRC
-
-Then, we style!
-
-#+BEGIN_SRC sass :tangle site/style/main.sass
-*
- box-sizing : border-box
-
-html
- width : 100%
- height : 100%
- font-size : 100%
- font-weight : normal
- color : #222
-
-a
- color : black
-
-a:visited
- color : #222
-
-body
- font-family : serif
- margin : 0 var(--side-margin) 0 calc(var(--side-margin) - 2rem) !important
- padding : 2rem
- @media screen and (min-width: calc(#{$content-width} + 2 * #{$large-side-margin}))
- border-left : 1px solid #ccc
-
-main p,
-main h1,
-main h2,
-main h3,
-main h4,
-main h5,
-main h6,
-main ul,
-main dl,
-main ol,
-header,
-footer
- max-width : $content-width
- line-height : 140%
-
-main h1,
-main h2,
-main h3,
-main h4,
-main h5,
-main h6
- font-weight : bold
- color : #0c0016
-
-header a,
-footer p
- font-size : 90%
-
-main
- padding-top : 4rem
- padding-bottom : 4rem
-
- dl dd
- margin-left : 0
-
- dl dt
- font-weight : bold
-
- dl dt:not(:first-child)
- padding-top : .5rem
-
- details
- font-size : 90%
- filter : opacity(0.8)
-
-footer img
- border-radius : 100%
- max-width : 7rem
- float : right
- margin-left : 1rem
- margin-bottom : 1rem
-
-pre
- padding-left : 1.5rem
- padding-right : 1.5rem
- overflow-x : auto
-
-code,
-tt,
-pre
- font-family : 'Fira Code', monospace
- font-size : 80%
- line-height : 140%
- color : $monospace-color
-
-#gallery
- display : flex
- flex-wrap : wrap
- align-content : flex-start
-
- img
- max-width : 20rem
-
-@import plugins
-@import org
-@import coq
-#+END_SRC
-
-* Build Instructions
-
-The build instruction are pretty straightforward. We start by how to compile the
-main CSS file.
-
-#+BEGIN_SRC makefile :tangle theme.mk
-SASS := $(wildcard site/style/*.sass)
-MAIN_SASS := site/style/main.sass
-CSS := $(MAIN_SASS:.sass=.css)
-
-${CSS} : ${SASS}
- @cleopatra echo Compiling "${CSS}"
- @sassc --style=compressed --sass ${MAIN_SASS} ${CSS}
-#+END_SRC
-
-Since the HTML template does not need any particular processing, the
-=theme-build= phase is only responsible for generating the main CSS file. The
-[[./soupault.org][=soupault= build phase]] needs to start after the CSS file is
-compiled (since it copies all relevant files to the ~build/~ directory), so we
-explicit this dependency.
-
-#+BEGIN_SRC makefile :tangle theme.mk
-theme-build : ${CSS}
-soupault-build : theme-build
-#+END_SRC
-
-Therefore, at the end of this generation process only one file has been
-generated.
-
-#+BEGIN_SRC makefile :tangle theme.mk
-ARTIFACTS += ${CSS}
-#+END_SRC
+ #+end_src
diff --git a/site/coq.org b/site/coq.org
new file mode 100644
index 0000000..d13d387
--- /dev/null
+++ b/site/coq.org
@@ -0,0 +1,44 @@
+#+SERIES: ./index.html
+#+SERIES_NEXT: haskell.html
+
+#+TITLE: 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.
+
+- [[./posts/StronglySpecifiedFunctions.org][A Series on Strongly-Specified Funcions in Coq]] ::
+ Using dependent types and the ~Prop~ sort, it becomes possible to specify
+ functions whose arguments and results are constrained by properties.
+ Using such a “strongly-specified” function requires to provide a proof that
+ the supplied arguments satisfy the expected properties, and allows for soundly
+ assuming the results are correct too. However, implementing dependently-typed
+ functions can be challenging.
+
+- [[./posts/Ltac.org][A Series on Ltac]] ::
+ 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.
+
+- [[./posts/RewritingInCoq.html][Rewriting in Coq]] ::
+ The ~rewrite~ tactics are really useful, since they are not limited to the Coq
+ built-in equality relation.
+
+- [[./posts/ClightIntroduction.html][A Study of Clight and its Semantics]] ::
+ Clight is a “simplified” C AST used by CompCert, the certified C compiler. In
+ this write-up, we prove a straighforward functional property of a small C
+ function, as an exercise to discover the Clight semantics.
+
+- [[./posts/AlgebraicDatatypes.html][Proving Algebraic Datatypes are “Algebraic”]] ::
+ The set of types which can be defined in a language together with ~+~ and ~*~
+ form an “algebraic structure” in the mathematical sense, hence the name. It
+ means the definitions of ~+~ and ~*~ have to satisfy properties such as
+ commutativity or the existence of neutral elements.
+
+- [[./posts/Coqffi.org][A Series on ~coqffi~]] ::
+ ~coqffi~ generates Coq FFI modules from compiled OCaml interface
+ modules (~.cmi~). In practice, it greatly reduces the hassle to
+ together OCaml and Coq modules within the same codebase, especially
+ when used together with the ~dune~ build system.
diff --git a/site/haskell.org b/site/haskell.org
new file mode 100644
index 0000000..c18fbb7
--- /dev/null
+++ b/site/haskell.org
@@ -0,0 +1,13 @@
+#+SERIES: index.html
+#+SERIES_PREV: coq.html
+#+SERIES_NEXT: miscellaneous.html
+
+#+TITLE: About Haskell
+
+Haskell is a pure, lazy, functional programming language with a very
+expressive type system.
+
+- [[./posts/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.
diff --git a/site/img/icons.svg b/site/img/icons.svg
new file mode 100644
index 0000000..917a417
--- /dev/null
+++ b/site/img/icons.svg
@@ -0,0 +1,39 @@
+<svg version="1.1" xmlns="http://www.w3.org/2000/svg">
+ <symbol id="external-link" viewBox="0 0 511.626 511.627">
+ <path d="M392.857,292.354h-18.274c-2.669,0-4.859,0.855-6.563,2.573c-1.718,1.708-2.573,3.897-2.573,6.563v91.361
+ c0,12.563-4.47,23.315-13.415,32.262c-8.945,8.945-19.701,13.414-32.264,13.414H82.224c-12.562,0-23.317-4.469-32.264-13.414
+ c-8.945-8.946-13.417-19.698-13.417-32.262V155.31c0-12.562,4.471-23.313,13.417-32.259c8.947-8.947,19.702-13.418,32.264-13.418
+ h200.994c2.669,0,4.859-0.859,6.57-2.57c1.711-1.713,2.566-3.9,2.566-6.567V82.221c0-2.662-0.855-4.853-2.566-6.563
+ c-1.711-1.713-3.901-2.568-6.57-2.568H82.224c-22.648,0-42.016,8.042-58.102,24.125C8.042,113.297,0,132.665,0,155.313v237.542
+ c0,22.647,8.042,42.018,24.123,58.095c16.086,16.084,35.454,24.13,58.102,24.13h237.543c22.647,0,42.017-8.046,58.101-24.13
+ c16.085-16.077,24.127-35.447,24.127-58.095v-91.358c0-2.669-0.856-4.859-2.574-6.57
+ C397.709,293.209,395.519,292.354,392.857,292.354z"/>
+ <path d="M506.199,41.971c-3.617-3.617-7.905-5.424-12.85-5.424H347.171c-4.948,0-9.233,1.807-12.847,5.424
+ c-3.617,3.615-5.428,7.898-5.428,12.847s1.811,9.233,5.428,12.85l50.247,50.248L198.424,304.067
+ c-1.906,1.903-2.856,4.093-2.856,6.563c0,2.479,0.953,4.668,2.856,6.571l32.548,32.544c1.903,1.903,4.093,2.852,6.567,2.852
+ s4.665-0.948,6.567-2.852l186.148-186.148l50.251,50.248c3.614,3.617,7.898,5.426,12.847,5.426s9.233-1.809,12.851-5.426
+ c3.617-3.616,5.424-7.898,5.424-12.847V54.818C511.626,49.866,509.813,45.586,506.199,41.971z"/>
+ </symbol>
+ <symbol id="github" viewBox="0 0 438.549 438.549">
+ <path d="M409.132,114.573c-19.608-33.596-46.205-60.194-79.798-79.8C295.736,15.166,259.057,5.365,219.271,5.365
+ c-39.781,0-76.472,9.804-110.063,29.408c-33.596,19.605-60.192,46.204-79.8,79.8C9.803,148.168,0,184.854,0,224.63
+ c0,47.78,13.94,90.745,41.827,128.906c27.884,38.164,63.906,64.572,108.063,79.227c5.14,0.954,8.945,0.283,11.419-1.996
+ c2.475-2.282,3.711-5.14,3.711-8.562c0-0.571-0.049-5.708-0.144-15.417c-0.098-9.709-0.144-18.179-0.144-25.406l-6.567,1.136
+ c-4.187,0.767-9.469,1.092-15.846,1c-6.374-0.089-12.991-0.757-19.842-1.999c-6.854-1.231-13.229-4.086-19.13-8.559
+ c-5.898-4.473-10.085-10.328-12.56-17.556l-2.855-6.57c-1.903-4.374-4.899-9.233-8.992-14.559
+ c-4.093-5.331-8.232-8.945-12.419-10.848l-1.999-1.431c-1.332-0.951-2.568-2.098-3.711-3.429c-1.142-1.331-1.997-2.663-2.568-3.997
+ c-0.572-1.335-0.098-2.43,1.427-3.289c1.525-0.859,4.281-1.276,8.28-1.276l5.708,0.853c3.807,0.763,8.516,3.042,14.133,6.851
+ c5.614,3.806,10.229,8.754,13.846,14.842c4.38,7.806,9.657,13.754,15.846,17.847c6.184,4.093,12.419,6.136,18.699,6.136
+ c6.28,0,11.704-0.476,16.274-1.423c4.565-0.952,8.848-2.383,12.847-4.285c1.713-12.758,6.377-22.559,13.988-29.41
+ c-10.848-1.14-20.601-2.857-29.264-5.14c-8.658-2.286-17.605-5.996-26.835-11.14c-9.235-5.137-16.896-11.516-22.985-19.126
+ c-6.09-7.614-11.088-17.61-14.987-29.979c-3.901-12.374-5.852-26.648-5.852-42.826c0-23.035,7.52-42.637,22.557-58.817
+ c-7.044-17.318-6.379-36.732,1.997-58.24c5.52-1.715,13.706-0.428,24.554,3.853c10.85,4.283,18.794,7.952,23.84,10.994
+ c5.046,3.041,9.089,5.618,12.135,7.708c17.705-4.947,35.976-7.421,54.818-7.421s37.117,2.474,54.823,7.421l10.849-6.849
+ c7.419-4.57,16.18-8.758,26.262-12.565c10.088-3.805,17.802-4.853,23.134-3.138c8.562,21.509,9.325,40.922,2.279,58.24
+ c15.036,16.18,22.559,35.787,22.559,58.817c0,16.178-1.958,30.497-5.853,42.966c-3.9,12.471-8.941,22.457-15.125,29.979
+ c-6.191,7.521-13.901,13.85-23.131,18.986c-9.232,5.14-18.182,8.85-26.84,11.136c-8.662,2.286-18.415,4.004-29.263,5.146
+ c9.894,8.562,14.842,22.077,14.842,40.539v60.237c0,3.422,1.19,6.279,3.572,8.562c2.379,2.279,6.136,2.95,11.276,1.995
+ c44.163-14.653,80.185-41.062,108.068-79.226c27.88-38.161,41.825-81.126,41.825-128.906
+ C438.536,184.851,428.728,148.168,409.132,114.573z"/>
+ </symbol>
+</svg>
diff --git a/site/img/merida.webp b/site/img/merida.webp
deleted file mode 100644
index c0e6354..0000000
--- a/site/img/merida.webp
+++ /dev/null
Binary files differ
diff --git a/site/index.org b/site/index.org
index e1b61bc..e4a7e18 100644
--- a/site/index.org
+++ b/site/index.org
@@ -1,76 +1,27 @@
-#+OPTIONS: toc:nil num:nil
-
-#+BEGIN_EXPORT html
-<h1>Technical Articles</h1>
-#+END_EXPORT
+#+TITLE: Technical Articles
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 [[mailto:lthms@soap.coffee][email]], or start a discussion on
-whichever site you like (I personnaly enjoy
-[[https://lobste.rs/search?q=domain%3Asoap.coffee&what=stories&order=relevance][Lobste.rs]]
-very much).
+If you like what you read, have a question or for any other reasons
+really, you can shoot an [[mailto:lthms@soap.coffee][email]], or start a discussion on whichever
+site you like[fn::I personnaly enjoy [[https://lobste.rs/search?q=domain%3Asoap.coffee&what=stories&order=relevance][Lobste.rs]] very much].
* About Coq
-:PROPERTIES:
-:CUSTOM_ID: coq
-:END:
-
-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.
-
-- [[./posts/StronglySpecifiedFunctions.org][A Series on Strongly-Specified Funcions in Coq]] ::
- Using dependent types and the ~Prop~ sort, it becomes possible to specify
- functions whose arguments and results are constrained by properties.
- Using such a “strongly-specified” function requires to provide a proof that
- the supplied arguments satisfy the expected properties, and allows for soundly
- assuming the results are correct too. However, implementing dependently-typed
- functions can be challenging.
-
-- [[./posts/Ltac.org][A Series on Ltac]] ::
- 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.
-
-- [[./posts/RewritingInCoq.html][Rewriting in Coq]] ::
- The ~rewrite~ tactics are really useful, since they are not limited to the Coq
- built-in equality relation.
+ :PROPERTIES:
+ :CUSTOM_ID: coq
+ :END:
-- [[./posts/ClightIntroduction.html][A Study of Clight and its Semantics]] ::
- Clight is a “simplified” C AST used by CompCert, the certified C compiler. In
- this write-up, we prove a straighforward functional property of a small C
- function, as an exercise to discover the Clight semantics.
-
-- [[./posts/AlgebraicDatatypes.html][Proving Algebraic Datatypes are “Algebraic”]] ::
- The set of types which can be defined in a language together with ~+~ and ~*~
- form an “algebraic structure” in the mathematical sense, hence the name. It
- means the definitions of ~+~ and ~*~ have to satisfy properties such as
- commutativity or the existence of neutral elements.
-
-- [[./posts/Coqffi.org][A Series on ~coqffi~]] ::
- ~coqffi~ generates Coq FFI modules from compiled OCaml interface
- modules (~.cmi~). In practice, it greatly reduces the hassle to
- together OCaml and Coq modules within the same codebase, especially
- when used together with the ~dune~ build system.
+ #+include: ./coq.org
* About Haskell
-Haskell is a pure, lazy, functional programming language with a very expressive
-type system.
-
-- [[./posts/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.
+ #+include: ./haskell.org
* Miscellaneous
-- [[./posts/DiscoveringCommonLisp.html][Discovering Common Lisp with ~trivial-gamekit~]] ::
- Common Lisp is a venerable programming languages like no other I know. From
- the creation of a Lisp package up to the creation of a standalone executable,
- we explore the shore of this strange beast.
+ #+include: ./miscellaneous.org
+
+* About this Website
+
+ #+include: ./meta.org
diff --git a/site/meta.org b/site/meta.org
new file mode 100644
index 0000000..d5ce4b4
--- /dev/null
+++ b/site/meta.org
@@ -0,0 +1,23 @@
+#+TITLE: About this Website
+
+#+SERIES: ./index.html
+#+SERIES_PREV: miscellaneous.html
+
+The generation of this website is far from being trivial, and requires
+the combination of —probably too— many tools. For instance, even if I
+mostly use Org mode for authoring content, most of my write-ups about
+Coq are actually Coq files, and I use ~coqdoc~ to generate the HTML
+pages you read.
+
+- [[./posts/Thanks.org][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 most significant ones.
+
+- [[./cleopatra.org][A Series on Generating this Website]] ::
+ At some point, I felt like the whole process of generating this
+ website was interesting enough so that it would deserve a write-up
+ of its own. As a result, I spent quite some time turning my custom
+ toolchain into a literate program, so that its actual code source
+ would actually be the write-ups I wanted to add to my website.
diff --git a/site/miscellaneous.org b/site/miscellaneous.org
new file mode 100644
index 0000000..c348c28
--- /dev/null
+++ b/site/miscellaneous.org
@@ -0,0 +1,14 @@
+#+SERIES: index.html
+#+SERIES_PREV: haskell.html
+#+SERIES_NEXT: meta.html
+
+#+TITLE: Miscellaneous
+
+Over the years, I have made a habit of learning new programming
+languages, out of curiosity, and I intend to continue this way for the
+time being.
+
+- [[./posts/DiscoveringCommonLisp.html][Discovering Common Lisp with ~trivial-gamekit~]] ::
+ Common Lisp is a venerable programming languages like no other I
+ know. From the creation of a Lisp package up to the creation of a
+ standalone executable, we explore the shore of this strange beast.
diff --git a/site/news/index.html b/site/news/index.html
index 5a0331e..43315c0 100644
--- a/site/news/index.html
+++ b/site/news/index.html
@@ -4,6 +4,21 @@
<ul>
<li>
+ On <strong>March 4, 2021</strong>,
+ FreeSpec packages
+ (<code>coq-freespec-core.0.3</code>, <code>coq-freespec-ffi.0.3</code>
+ and
+ <code>coq-freespec-exec.0.3</code>) have finally been released.
+ </li>
+ <li>
+ On <strong>March 1st, 2021</strong>, <code>coq-coqffi.1.0.0~beta5</code>
+ has been released.
+ </li>
+ <li>
+ On <strong>February 24, 2021</strong>, <code>coq-coqffi.1.0.0~beta4</code>
+ has been released.
+ </li>
+ <li>
On <strong>January 27, 2021</strong>,
<a href="https://github.com/lthms/FreeSpec">FreeSpec</a> has been
relicensed under the terms of the
diff --git a/site/opinions/MonadTransformers.org b/site/opinions/MonadTransformers.org
index 7296f08..0424c7b 100644
--- a/site/opinions/MonadTransformers.org
+++ b/site/opinions/MonadTransformers.org
@@ -1,12 +1,12 @@
-#+BEGIN_EXPORT html
-<h1>Monad Transformers are a Great Abstraction</h1>
+#+TITLE: Monad Transformers are a Great Abstraction
+
+#+SERIES: ../opinions/index.html
+#+BEGIN_EXPORT html
<p>This article has originally been published on <span
id="original-created-at">July 15, 2017</span>.</p>
#+END_EXPORT
-#+OPTIONS: toc:nil
-
#+BEGIN_EXPORT html
<div id="history">site/opinions/MonadTransformers.org</div>
#+END_EXPORT
@@ -14,8 +14,8 @@ id="original-created-at">July 15, 2017</span>.</p>
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
-define Monads in only a few words, [[https://techn.ical.ist/@lthms/590439][I say Monad is a convenient formalism to
-chain specific computations]]. Once I’ve got that, I started noticing “monadic
+define Monads in only a few words, I say monads are a convenient formalism to
+chain specific computations. Once I’ve got that, I started noticing “monadic
construction” everywhere, from the Rust ~?~ operator to the [[https://blog.drewolson.org/elixirs-secret-weapon/][Elixir ~with~
keyword]].
@@ -46,7 +46,6 @@ issue with the Monad Transformers.
#+BEGIN_SRC diff
-type Builder = StateT Text IO
+type Builder = StateT Text (ReaderT Language IO)
-
#+END_SRC
As you may have already understood, I wasn't using the “raw” ~State~ Monad, but
diff --git a/site/opinions/index.org b/site/opinions/index.org
index 0be267e..58b0407 100644
--- a/site/opinions/index.org
+++ b/site/opinions/index.org
@@ -1,8 +1,4 @@
-#+options: num:nil
-
-#+BEGIN_EXPORT html
-<h1>Opinions</h1>
-#+END_EXPORT
+#+TITLE: Opinions
I may have some opinions on some topics, and sometimes I may want to share
them. However, I strongly believe facts and opinions are two differents things,
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