diff options
Diffstat (limited to 'site/posts')
-rw-r--r-- | site/posts/AlgebraicDatatypes.v | 2 | ||||
-rw-r--r-- | site/posts/ClightIntroduction.v | 2 | ||||
-rw-r--r-- | site/posts/Coqffi.org | 2 | ||||
-rw-r--r-- | site/posts/DiscoveringCommonLisp.org | 2 | ||||
-rw-r--r-- | site/posts/ExtensibleTypeSafeErrorHandling.org | 2 | ||||
-rw-r--r-- | site/posts/Ltac.org | 2 | ||||
-rw-r--r-- | site/posts/RankNTypesInOCaml.org | 2 | ||||
-rw-r--r-- | site/posts/RewritingInCoq.v | 2 | ||||
-rw-r--r-- | site/posts/StronglySpecifiedFunctions.org | 2 | ||||
-rw-r--r-- | site/posts/Thanks.org | 8 | ||||
-rw-r--r-- | site/posts/cleopatra.org | 66 | ||||
-rw-r--r-- | site/posts/cleopatra/commands.org | 36 | ||||
-rw-r--r-- | site/posts/cleopatra/coq.org | 47 | ||||
-rw-r--r-- | site/posts/cleopatra/dependencies.org | 95 | ||||
-rw-r--r-- | site/posts/cleopatra/literate-programming.org | 82 | ||||
-rw-r--r-- | site/posts/cleopatra/org.org | 144 | ||||
-rw-r--r-- | site/posts/cleopatra/soupault.org | 702 | ||||
-rw-r--r-- | site/posts/cleopatra/theme.org | 573 | ||||
-rw-r--r-- | site/posts/coq.org | 44 | ||||
-rw-r--r-- | site/posts/haskell.org | 13 | ||||
-rw-r--r-- | site/posts/index.org | 28 | ||||
-rw-r--r-- | site/posts/meta.org | 16 | ||||
-rw-r--r-- | site/posts/miscellaneous.org | 20 |
23 files changed, 1877 insertions, 15 deletions
diff --git a/site/posts/AlgebraicDatatypes.v b/site/posts/AlgebraicDatatypes.v index f32551c..77ecc3c 100644 --- a/site/posts/AlgebraicDatatypes.v +++ b/site/posts/AlgebraicDatatypes.v @@ -1,4 +1,4 @@ -(** #<nav><p class="series">../coq.html</p> +(** #<nav><p class="series">./coq.html</p> <p class="series-prev">./ClightIntroduction.html</p> <p class="series-next">./Coqffi.html</p></nav># *) diff --git a/site/posts/ClightIntroduction.v b/site/posts/ClightIntroduction.v index 85d084b..755d505 100644 --- a/site/posts/ClightIntroduction.v +++ b/site/posts/ClightIntroduction.v @@ -1,4 +1,4 @@ -(** #<nav><p class="series">../coq.html</p>
+(** #<nav><p class="series">./coq.html</p>
<p class="series-prev">./RewritingInCoq.html</p>
<p class="series-next">./AlgebraicDatatypes.html</p></nav># *)
diff --git a/site/posts/Coqffi.org b/site/posts/Coqffi.org index f8d9695..6116612 100644 --- a/site/posts/Coqffi.org +++ b/site/posts/Coqffi.org @@ -1,6 +1,6 @@ #+TITLE: A series on ~coqffi~ -#+SERIES: ../coq.html +#+SERIES: ./coq.html #+SERIES_PREV: AlgebraicDatatypes.html ~coqffi~ generates Coq FFI modules from compiled OCaml interface diff --git a/site/posts/DiscoveringCommonLisp.org b/site/posts/DiscoveringCommonLisp.org index 307a315..f31f280 100644 --- a/site/posts/DiscoveringCommonLisp.org +++ b/site/posts/DiscoveringCommonLisp.org @@ -1,6 +1,6 @@ #+TITLE: Discovering Common Lisp with ~trivial-gamekit~ -#+SERIES: ../miscellaneous.html +#+SERIES: ./miscellaneous.html #+SERIES_NEXT: ./RankNTypesInOCaml.html #+BEGIN_EXPORT html diff --git a/site/posts/ExtensibleTypeSafeErrorHandling.org b/site/posts/ExtensibleTypeSafeErrorHandling.org index e817e31..67ad3b1 100644 --- a/site/posts/ExtensibleTypeSafeErrorHandling.org +++ b/site/posts/ExtensibleTypeSafeErrorHandling.org @@ -1,6 +1,6 @@ #+TITLE: Extensible Type-Safe Error Handling in Haskell -#+SERIES: ../haskell.html +#+SERIES: ./haskell.html #+BEGIN_EXPORT html <p>This article has originally been published on <span diff --git a/site/posts/Ltac.org b/site/posts/Ltac.org index 37580cd..3dffb66 100644 --- a/site/posts/Ltac.org +++ b/site/posts/Ltac.org @@ -1,6 +1,6 @@ #+TITLE: A Series on Ltac -#+SERIES: ../coq.html +#+SERIES: ./coq.html #+SERIES_PREV: ./StronglySpecifiedFunctions.html #+SERIES_NEXT: ./RewritingInCoq.html diff --git a/site/posts/RankNTypesInOCaml.org b/site/posts/RankNTypesInOCaml.org index fb21e4b..a8ffb3b 100644 --- a/site/posts/RankNTypesInOCaml.org +++ b/site/posts/RankNTypesInOCaml.org @@ -1,6 +1,6 @@ #+TITLE: Writing a Function Whose Argument is a Polymorphic Function in OCaml -#+SERIES: ../miscellaneous.html +#+SERIES: ./miscellaneous.html #+SERIES_PREV: ./DiscoveringCommonLisp.html #+BEGIN_EXPORT html diff --git a/site/posts/RewritingInCoq.v b/site/posts/RewritingInCoq.v index a285e09..f58e9e0 100644 --- a/site/posts/RewritingInCoq.v +++ b/site/posts/RewritingInCoq.v @@ -1,4 +1,4 @@ -(** #<nav><p class="series">../coq.html</p> +(** #<nav><p class="series">./coq.html</p> <p class="series-prev">./Ltac.html</p> <p class="series-next">./ClightIntroduction.html</p></nav># *) diff --git a/site/posts/StronglySpecifiedFunctions.org b/site/posts/StronglySpecifiedFunctions.org index 83148c6..4a608c7 100644 --- a/site/posts/StronglySpecifiedFunctions.org +++ b/site/posts/StronglySpecifiedFunctions.org @@ -1,6 +1,6 @@ #+TITLE: A Series on Strongly-Specified Functions in Coq -#+SERIES: ../coq.html +#+SERIES: ./coq.html #+SERIES_NEXT: ./Ltac.html Using dependent types and the ~Prop~ sort, it becomes possible to specify diff --git a/site/posts/Thanks.org b/site/posts/Thanks.org index 22e2d57..ae23b7b 100644 --- a/site/posts/Thanks.org +++ b/site/posts/Thanks.org @@ -1,7 +1,7 @@ #+TITLE: Thanks! -#+SERIES: ../meta.html -#+SERIES_NEXT: ../cleopatra.html +#+SERIES: ./meta.html +#+SERIES_NEXT: ./cleopatra.html This website could not exist without many awesome free software projects. Although I could not list them all even if I wanted, my @@ -32,10 +32,6 @@ the most significant ones. - [[https://soupault.app][soupault]] :: Soupault is a static website generator and HTML processor written by [[https://www.baturin.org/][Daniil Baturin]]. -- [[https://cleopatra.soap.coffee][~cleopatra~]] :: - ~cleopatra~ is a generic, extensible toolchain with facilities for - literate programming projects using Org mode and more. I have - written it for this very website. * Frontend diff --git a/site/posts/cleopatra.org b/site/posts/cleopatra.org new file mode 100644 index 0000000..6081708 --- /dev/null +++ b/site/posts/cleopatra.org @@ -0,0 +1,66 @@ +#+TITLE: An Unfinished Series on How This Static Website Used to be Generated + +#+SERIES: ./meta.html +#+SERIES_PREV: ./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]]. + +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::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. + +Now, I don’t use *~cleopatra~* anymore. Literate programming is a fun +paradigm, but I never took the time to actually document in depth most +of the bits on how this website is built. So I took the various +scripts extracted by *~cleopatra~*, and recreated a straightforward +~makefile~ file on top of it. The nice thing is, it now takes way less +time to build! + +Anyway, coming back to this series, it is just the very reason why I +started using *~cleopatra~* in the first place: the generation +processes I was using to generate this website, written as literate +programs. If you are curious, you can have a look. + +- [[./cleopatra/dependencies.org][Installing Dependencies]] :: + +- [[file:cleopatra/coq.org][Authoring Contents with Coq ~(TODO)~]] :: + +- [[./cleopatra/org.org][Authoring Contents with ~org-mode~ ~(TODO)~]] :: + +- [[./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 + correct. We use Emacs and ~org-mode~ to tangle the literate + programming projects present in the ~posts/~ directory of this + website. + +- [[./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 + generator. We leverage *~soupault~* to provide a unified look and feel to a + website generated with diverse tools. + +*Appendix:* In case you are curious, you can have a look at +[[./posts/CleopatraV1.html][the first implementaiton of *~cleopatra~*]]. diff --git a/site/posts/cleopatra/commands.org b/site/posts/cleopatra/commands.org new file mode 100644 index 0000000..fbf0430 --- /dev/null +++ b/site/posts/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/posts/cleopatra/coq.org b/site/posts/cleopatra/coq.org new file mode 100644 index 0000000..81f3d27 --- /dev/null +++ b/site/posts/cleopatra/coq.org @@ -0,0 +1,47 @@ +#+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 + +#+BEGIN_SRC makefile :tangle coq.mk +COQ_POSTS := $(shell find site/ -name "*.v") +COQ_HTML := $(COQ_POSTS:.v=.html) +COQ_ARTIFACTS := $(COQ_POSTS:.v=.vo) \ + $(COQ_POSTS:.v=.vok) \ + $(COQ_POSTS:.v=.vos) \ + $(COQ_POSTS:.v=.glob) \ + $(join $(dir ${COQ_POSTS}),$(addprefix ".",$(notdir $(COQ_POSTS:.v=.aux)))) + +coq-build : ${COQ_HTML} + +soupault-build : coq-build + +ARTIFACTS += ${COQ_ARTIFACTS} .lia.cache +ARTIFACTS += ${COQ_HTML} + +COQLIB := "https://coq.inria.fr/distrib/current/stdlib/" +COQCARG := -async-proofs-cache force \ + -w -custom-entry-overriden +COQDOCARG := --no-index --charset utf8 --short \ + --body-only --coqlib "${COQLIB}" \ + --external "https://coq-community.org/coq-ext-lib/v0.11.2/" ExtLib \ + --external "https://compcert.org/doc/html" compcert \ + --external "https://lysxia.github.io/coq-simple-io" SimpleIO + +%.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 diff --git a/site/posts/cleopatra/dependencies.org b/site/posts/cleopatra/dependencies.org new file mode 100644 index 0000000..7858df4 --- /dev/null +++ b/site/posts/cleopatra/dependencies.org @@ -0,0 +1,95 @@ +#+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.2 | + | coq-compcert | 3.8 | + + #+caption: Dependencies for the ~coqffi~ series + #+name: lp-deps + | Package | Version | + |---------------+-------------| + | dune | 2.9.0 | + | coq-coqffi | 1.0.0~beta7 | + | coq-simple-io | 1.5.0 | + + #+caption: Soupault + #+name: soupault-deps + | Package | Version | + |----------+---------| + | soupault | 4.0.1 | + + #+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.12.0 +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.13 | + | minify | 7.0.2 | + | 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 + +CONFIGURE += package-lock.json + #+end_src + + #+begin_src makefile :tangle dependencies.mk :noweb yes +dependencies-prebuild : _opam/init package-lock.json + #+end_src diff --git a/site/posts/cleopatra/literate-programming.org b/site/posts/cleopatra/literate-programming.org new file mode 100644 index 0000000..63e0b02 --- /dev/null +++ b/site/posts/cleopatra/literate-programming.org @@ -0,0 +1,82 @@ +#+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 +understand it. It poses several significant challenges, in particular +in terms of code refactoring. If a given piece of code is too much +entangled with proses explaining it, rewriting it becomes cumbersome. + +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 +;; 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))) + +;; scan the posts/ directory and tangled it into lp/ +(setq org-publish-project-alist + '(("lp" + :base-directory "site/posts" + :publishing-directory "lp" + :recursive t + :publishing-function cleopatra:tangle-publish))) + +(org-publish-all) +#+END_SRC + +Tangling literate programming is done in the =prebuild= phase of +*~cleopatra~*. + +#+BEGIN_SRC makefile :tangle literate-programming.mk +literate-programming-prebuild : + @cleopatra echo "Tangling" "literate programming project" + @cleopatra exec -- cleopatra-run-elisp export-lp.el \ + >> build.log 2>&1 + +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 +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 _opam/init + @cleopatra echo "Building" "coqffi tutorial" + @cd lp/coqffi-tutorial; dune build --display quiet + @cleopatra echo "Archiving" "coqffi tutorial" + @rm -f ${COQFFI_ARCHIVE} + @tar --exclude="_build" -C lp/ -czvf ${COQFFI_ARCHIVE} coqffi-tutorial \ + 2>&1 >> build.log + +site/posts/CoqffiEcho.html : coqffi-tutorial-build +literate-programming-build : coqffi-tutorial-build + +ARTIFACTS += ${COQFFI_ARCHIVE} +#+END_SRC diff --git a/site/posts/cleopatra/org.org b/site/posts/cleopatra/org.org new file mode 100644 index 0000000..9f5a77c --- /dev/null +++ b/site/posts/cleopatra/org.org @@ -0,0 +1,144 @@ +#+TITLE: Authoring Content with ~org-mode~ + +#+SERIES: ../cleopatra.html +#+SERIES_PREV: ./coq.html +#+SERIES_NEXT: ./literate-programming.html + +#+BEGIN_EXPORT html +<nav id="generate-toc"></nav> +<div id="history">site/cleopatra/org.org</div> +#+END_EXPORT + +* Author Guidelines + +* Implementation + +#+begin_src makefile :tangle org.mk +EMACS := cleopatra-emacs + +ORG_IN := $(shell find site/ -name "*.org") +ORG_OUT := $(ORG_IN:.org=.html) + +org-prebuild : .emacs +org-build : ${ORG_OUT} + +soupault-build : org-build + +ARTIFACTS += ${ORG_OUT} +CONFIGURE += .emacs + +EXPORT := --batch \ + --load="${ROOT}/scripts/packages.el" \ + --load="${ROOT}/scripts/export-org.el" \ + 2>> build.log + +INIT := --batch --load="${ROOT}/scripts/packages.el" \ + 2>> build.log + +.emacs : scripts/packages.el + @cleopatra echo Initiating "Emacs configuration" + @${EMACS} ${INIT} + @touch .emacs + +%.html : %.org scripts/packages.el scripts/export-org.el \ + .emacs org.mk + @cleopatra echo Exporting "$*.org" + @${EMACS} $< ${EXPORT} +#+end_src + +#+begin_src emacs-lisp :tangle scripts/packages.el +(use-package ox-tufte :ensure t) +#+end_src + +We also use the OCaml backend for ~org-babel~ to ensure our OCaml +snippets are well-typed, among other things. + +#+begin_src emacs-lisp :tangle scripts/packages.el +(use-package tuareg :ensure t + :config + (require 'ob-ocaml)) +#+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) + (ocaml . 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/posts/cleopatra/soupault.org b/site/posts/cleopatra/soupault.org new file mode 100644 index 0000000..3fdb8d6 --- /dev/null +++ b/site/posts/cleopatra/soupault.org @@ -0,0 +1,702 @@ +#+TITLE: ~soupault~ + +#+SERIES: ../cleopatra.html +#+SERIES_PREV: ./theme.html +#+SERIES_NEXT: ./commands.html + +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 + +* Installation + + 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~*. + + #+begin_src makefile :tangle soupault.mk +CONFIGURE += _opam rss.json +ARTIFACTS += out + +soupault-prebuild : _opam/init + #+end_src + + Using ~soupault~ is as simple as calling it, without any particular + command-line arguments. + + #+begin_src makefile :tangle soupault.mk +soupault-build : dependencies-prebuild style.min.css + @cleopatra echo "Executing" "soupault" + @soupault + #+end_src + + We now describe our configuration file for ~soupault~. + +* Configuration + + #+name: base-dir + #+begin_src verbatim :noweb yes :exports none +~lthms + #+end_src + +** 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 +site_dir = "site" +build_dir = "out/<<base-dir>>" +doctype = "<!DOCTYPE html>" +clean_urls = false +generator_mode = true +complete_page_selector = "html" +default_content_selector = "main" +default_content_action = "append_child" +page_file_extensions = ["html"] +ignore_extensions = [ + "v", "vo", "vok", "vos", "glob", + "html~", "org" +] +default_template_file = "templates/main.html" +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. + + #+begin_src toml :tangle soupault.conf +[widgets.page-title] +widget = "title" +selector = "h1" +default = "~lthms" +prepend = "~lthms: " + #+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. + + #+NAME: soupault-version + #+begin_src bash :results verbatim output +soupault --version | head -n 1 | tr -d '\n' + #+end_src + + 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 +[widgets.generator-meta] +widget = "insert_html" +html = """<meta name="generator" content="<<soupault-version()>>">""" +selector = "head" + #+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[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. + + From a high-level perspective, the plugin structure is the following. + + First, we validate the widget configuration. + + #+BEGIN_SRC lua :tangle plugins/urls-rewriting.lua +prefix_url = config["prefix_url"] + +if not prefix_url then + Plugin.fail("Missing mandatory field: `prefix_url'") +end + +if not Regex.match(prefix_url, "^/(.*)") then + prefix_url = "/" .. prefix_url +end + +if not Regex.match(prefix_url, "(.*)/$") then + prefix_url = prefix_url .. "/" +end + #+END_SRC + + Then, we propose a generic function to enumerate and rewrite tags + which can have. + + #+BEGIN_SRC lua :tangle plugins/urls-rewriting.lua +function prefix_urls (links, attr, prefix_url) + index, link = next(links) + + while index do + href = HTML.get_attribute(link, attr) + + if href then + if Regex.match(href, "^/") then + href = Regex.replace(href, "^/*", "") + href = prefix_url .. href + end + + HTML.set_attribute(link, attr, href) + end + index, link = next(links, index) + end +end + #+END_SRC + + 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) +prefix_urls(HTML.select(page, "use"), "href", prefix_url) + #+END_SRC + + Again, configuring soupault to use this plugin is relatively + straightforward. + + #+BEGIN_SRC toml :tangle soupault.conf :noweb yes +[widgets.urls-rewriting] +widget = "urls-rewriting" +prefix_url = "<<base-dir>>" +after = "mark-external-urls" + #+END_SRC + +** Marking External Links + + #+BEGIN_SRC lua :tangle plugins/external-urls.lua +function mark(name) + return '<span class="icon"><svg><use href="/img/icons.svg#' + .. name .. + '"></use></svg></span>' +end + +links = HTML.select(page, "a") + +index, link = next(links) + +while index do + href = HTML.get_attribute(link, "href") + + if href then + if Regex.match(href, "^https?://github.com") then + icon = HTML.parse(mark("github")) + HTML.append_child(link, icon) + elseif Regex.match(href, "^https?://") then + icon = HTML.parse(mark("external-link")) + HTML.append_child(link, icon) + end + end + + index, link = next(links, index) +end + #+END_SRC + + #+BEGIN_SRC toml :tangle soupault.conf +[widgets.mark-external-urls] +after = "generate-history" +widget = "external-urls" + #+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 = "insert_html" +selector = "#generate-toc" +action = "prepend_child" +html = '<h2>Table of Contents</h2>' +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. + + For instance, considering the following HTML snippet + + #+begin_src html +<div id="history"> + site/posts/FooBar.org +</div> + #+end_src + + 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 is src_verbatim[:noweb yes :exports code]{<<repo>>}. + + #+name: repo + #+begin_src verbatim :exports none +https://src.soap.coffee/soap.coffee/lthms.git + #+end_src + + 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. + </p> + + <p> + You can consult the source of this file in its current version + <a href="<<repo>>/tree/{{file}}">here</a>. + </p> + + <table class="fullwidth"> + {{#history}} + <tr> + <td class="date" +{{#created}} + id="created-at" +{{/created}} +{{#modified}} + id="modified-at" +{{/modified}} + >{{date}}</td> + <td class="subject">{{subject}}</td> + <td class="commit"> + <a href="<<repo>>/commit/{{filename}}/?id={{hash}}">{{abbr_hash}}</a> + </td> + </tr> + {{/history}} + </table> +</details> + #+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. + + #+begin_src toml :tangle soupault.conf +[widgets.generate-history] +widget = "preprocess_element" +selector = "#history" +command = 'scripts/history.sh templates/history.html' +action = "replace_element" + #+end_src + + 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~ + + This translates in Bash like this. + + #+begin_src bash :tangle scripts/history.sh :shebang "#!/usr/bin/bash" +function main () { + local file="${1}" + local template="${2}" + + tmp_file=$(mktemp) + generate_json ${file} > ${tmp_file} + 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 +function gitlog () { + local file="${1}" + git --no-pager log \ + --follow \ + --stat=10000 \ + --pretty=format:'%s%n%h%n%H%n%cs%n' \ + "${file}" +} + #+end_src + + 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 + + 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 +<<gitlog>> +gitlog "soupault.org" | head -n8 + #+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}~. + + #+begin_src bash :tangle scripts/history.sh :noweb yes +function parse_filename () { + local line="${1}" + local shrink='s/ *\(.*\) \+|.*/\1/' + local unfold='s/\(.*\){\(.*\) => \(.*\)}/\1\3/' + + 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 +function generate_json () { + local input="${1}" + local logs="$(gitlog ${input})" + + if [ ! $? -eq 0 ]; then + exit 1 + fi + + let "idx=0" + let "last_entry=$(echo "${logs}" | wc -l) / 8" + + local subject="" + local abbr_hash="" + local hash="" + local date="" + local file="" + local created="true" + local modified="false" + + echo -n "{" + echo -n "\"file\": \"${input}\"" + echo -n ",\"history\": [" + + while read -r subject; do + read -r abbr_hash + read -r hash + read -r date + read -r # empty line + read -r file + read -r # short log + read -r # empty line + + if [ ${idx} -ne 0 ]; then + echo -n "," + fi + + if [ ${idx} -eq ${last_entry} ]; then + created="true" + modified="false" + else + created="false" + modified="true" + fi + + output_json_entry "${subject}" \ + "${abbr_hash}" \ + "${hash}" \ + "${date}" \ + "$(parse_filename "${file}")" \ + "${created}" \ + "${modified}" + + let idx++ + done < <(echo "${logs}") + + echo -n "]}" +} + #+end_src + + Generating the JSON object for a given commit is as simple as + + #+begin_src bash :tangle scripts/history.sh :noweb yes +function output_json_entry () { + local subject="${1}" + local abbr_hash="${2}" + local hash="${3}" + local date="${4}" + local file="${5}" + local created="${6}" + local last_entry="${7}" + + echo -n "{\"subject\": \"${subject}\"" + echo -n ",\"created\":${created}" + echo -n ",\"modified\":${modified}" + echo -n ",\"abbr_hash\":\"${abbr_hash}\"" + echo -n ",\"hash\":\"${hash}\"" + echo -n ",\"date\":\"${date}\"" + echo -n ",\"filename\":\"${file}\"" + echo -n "}" +} + #+end_src + + And we are done! We can safely call the =main= function to generate + our revisions table. + + #+begin_src bash :tangle scripts/history.sh +main "$(cat)" "${1}" + #+end_src + +** Rendering Equations Offline + :PROPERTIES: + :CUSTOM_ID: katex + :END: + +*** 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. + + Using this widgets requires being able to inject raw HTML in + input files. + +*** Implementation + + #+begin_src js :tangle scripts/render-equations.js +var katex = require("katex"); +var fs = require("fs"); +var input = fs.readFileSync(0); +var displayMode = process.env.DISPLAY != undefined; + +var html = katex.renderToString(String.raw`${input}`, { + throwOnError : false, + displayModed : displayMode +}); + +console.log(html) + #+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. + + #+begin_src toml :tangle soupault.conf +[widgets.inline-math] +widget = "preprocess_element" +selector = ".imath" +command = "node scripts/render-equations.js" +action = "replace_content" + +[widgets.display-math] +widget = "preprocess_element" +selector = ".dmath" +command = "DISPLAY=1 node scripts/render-equations.js" +action = "replace_content" + #+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"] } +modified-at = { selector = ["#modified-at"] } +created-at = { selector = ["#created-at"] } + #+end_src + +** Series Navigation + + #+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") + + 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 lua :tangle plugins/series.lua +function generate_nav_items (cwd, cls, template) + local elements = HTML.select(page, cls) + + 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) + + HTML.replace_content( + element, + generate_nav_item_from_title(title_str, url, template) + ) + + i = i + 1 + end +end + #+end_src + + #+begin_src lua :tangle plugins/series.lua +cwd = Sys.dirname(page_file) + +home_template = 'This article is part of the series “<a href="{{ url }}">{{ title }}</a>.”' +nav_template = '<a href="{{ url }}">{{ title }}</a>' + +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 + +#+begin_src toml :tangle soupault.conf +[widgets.series] +widget = "series" +#+end_src + +** Injecting Minified CSS + + #+begin_src lua :tangle plugins/css.lua +style = HTML.select_one(page, "style") + +if style then + css = HTML.create_text(Sys.read_file("style.min.css")) + HTML.replace_content(style, css) +end + #+end_src + + #+begin_src toml :tangle soupault.conf +[widgets.css] +widget = "css" + #+end_src + +** Cleaning-up + + #+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 + + #+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 + +#+begin_src toml :tangle soupault.conf +[widgets.clean-up] +widget = "clean-up" +#+end_src diff --git a/site/posts/cleopatra/theme.org b/site/posts/cleopatra/theme.org new file mode 100644 index 0000000..9b1a129 --- /dev/null +++ b/site/posts/cleopatra/theme.org @@ -0,0 +1,573 @@ +#+TITLE: Layout and Style + +#+SERIES: ../cleopatra.html +#+SERIES_PREV: ./literate-programming.html +#+SERIES_NEXT: ./soupault.html + +#+BEGIN_EXPORT html +<nav id="generate-toc"></nav> +<div id="history">site/cleopatra/theme.org</div> +#+END_EXPORT + +* 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. + + #+caption: Widths of page components (in ~rem~) + #+name: widths + | Content | 35 | + | Gutter | 3 | + | Margin | 13 | + + #+name: main-width + #+begin_src emacs-lisp :exports none :noweb yes :var widths=widths[,1] +(nth 0 widths) + #+end_src + + #+name: gutter-width + #+begin_src emacs-lisp :exports none :noweb yes :var widths=widths[,1] +(nth 1 widths) + #+end_src + + #+name: margin-width + #+begin_src emacs-lisp :exports none :noweb yes :var widths=widths[,1] +(nth 2 widths) + #+end_src + + #+begin_src css :tangle style.css :noweb yes +:root { + --main-width: <<main-width()>>rem; + --gutter-width: <<gutter-width()>>rem; + --margin-width: <<margin-width()>>rem; + --code-width: calc(var(--main-width) + var(--gutter-width) + var(--margin-width)); + --body-width: calc(var(--main-width) + 2 * (var(--gutter-width) + var(--margin-width))); +} + #+end_src + + According to CSS’ own [[https://www.w3.org/TR/css-variables-1/#using-variables][specification]], you cannot use ~var()~ inside + media queries. As a consequnece, for our theme to be responsive, + the full width of the page content (\im 2 \times (that is, + \mathrm{margin\_width} + \mathrm{gutter\_width}) + + \mathrm{content\_width} \mi or call_body-width[:results raw]()rem) + has to be hard-coded[fn::Fortunately, this is a literate + program. This value is actually programmatically computed, so that + we do not have to worry about forgetting to update it]. + + #+name: body-width + #+begin_src bash :exports none :noweb yes +echo $((2 * (<<margin-width()>> + <<gutter-width()>>) + <<main-width()>>)) + #+end_src + + #+begin_src css :tangle style.css :noweb yes +@media (max-width: <<body-width()>>rem) { + :root { + --body-width: var(--main-width); + --code-width: var(--main-width); + } +} + #+end_src + + And now, we are free to actually implement the layout. + + #+begin_src css :tangle style.css :noweb yes +,* { + box-sizing: border-box; +} + +.fullwidth { + width: var(--body-width); +} + +@media (min-width: <<body-width()>>rem) { + .fullwidth { + margin-left: calc(-1 * (var(--margin-width) + var(--gutter-width))); + } +} + +html { + font-size: 1rem; +} + +body { + line-height: 1.4; + 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); + margin: auto; +} + +main nav { + font-style: italic; + 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%; +} + +#whoami.marginnote { + color: var(--fg); + margin-bottom: 2em; +} + +img.avatar { + border-radius: 20px; + display: block; + max-width: 90%; + margin: auto; +} + +dd { + margin-left: 0; + margin-bottom: 0.5rem; +} + +.sidenote, +.marginnote { + font-size: smaller; + position: relative; + width: var(--margin-width); +} + +.sidenote { + margin-right: calc(-1 * (var(--margin-width) + var(--gutter-width))); + float: right; + clear: right; +} + +.marginnote { + float: left; + clear: left; + margin-left: calc(-1 * (var(--margin-width) + var(--gutter-width))); +} + +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(--code-width); + overflow-x: auto; + overflow-y: hidden; + padding: 1rem 2rem; +} + +main { + padding-top: 4.2rem; + padding-bottom: 4.2rem; +} + +h1 { + text-align: center; +} + +h2, h3, h4 { + font-style: italic; +} + +h1, h2, h3, h4 { + color: var(--doc); + font-family: serif; + font-weight: normal; +} + +dt { + font-weight: bold; +} + +div.code, +span.inlinecode, +pre, +tt, +.dmath, +.imath { + font-family: monospace; + font-size: 85%; +} + +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: <<body-width()>>rem) { + 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, div.code { + width: 100%; + } +} + #+end_src + +** Colors + + #+begin_src css :tangle style.css +:root { + --bg: white; + --bg-plus: #f7f7f7; + --current-line: #fbfbfb; + --fade: #cfcecb; + --fg: #3c3c3c; + --fg-plus: #575757; + --doc: black; + --warning: #bd745e; + --red: #b3534b; + --green: #6d9319; + --yellow: #d4b100; +} + #+end_src + + #+begin_src css :tangle style.css +body { + font-family: sans-serif; + color: var(--fg); + background: var(--bg); +} + +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); +} + +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 + +** Icons + + #+begin_src css :tangle style.css +.icon svg { + display: inline; + width: 1em; + height: .9em; + vertical-align: text-top; +} + +a[href], .margin-toggle { + color: #0000ee; +} + +a[href] .icon svg { + fill: #0000ee; +} + +a[href]:visited { + color: #25008b; +} + +a[href]:visited .icon svg { + fill: #25008b; +} + +.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 dependencies-prebuild + @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 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> + <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> + <span id="whoami" class="marginnote"> + <img class="avatar" src="/img/vampy.jpg" /> + + <p> + Hi, I’m <strong>lthms</strong>. + </p> + + <p> + I don’t like syntax highlighting, but I like + types and functional programming languages. + He/him. + </p> + + <p> + Interested in starting a discussion? Don’t hesitate to <a + href="mailto:~lthms/public-inbox@lists.sr.ht">shoot me an + email</a>. + </p> + </span> + </main> + </body> +</html> + #+end_src diff --git a/site/posts/coq.org b/site/posts/coq.org new file mode 100644 index 0000000..b8b6818 --- /dev/null +++ b/site/posts/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. + +- [[./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. + +- [[./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. + +- [[./RewritingInCoq.html][Rewriting in Coq]] :: + The ~rewrite~ tactics are really useful, since they are not limited to the Coq + built-in equality relation. + +- [[./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. + +- [[./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. + +- [[./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/posts/haskell.org b/site/posts/haskell.org new file mode 100644 index 0000000..cf06b89 --- /dev/null +++ b/site/posts/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. + +- [[./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/posts/index.org b/site/posts/index.org new file mode 100644 index 0000000..bc53280 --- /dev/null +++ b/site/posts/index.org @@ -0,0 +1,28 @@ +#+TITLE: Technical Articles + +Over the past years, I have tried to capitalize on my findings. More +often than not, I have lacked in regularity, but I hope I have made up +for it in exoticism. + +#+begin_export html +<nav id="generate-toc"></nav> +#+end_export + +* About Coq + :PROPERTIES: + :CUSTOM_ID: coq + :END: + + #+include: ./coq.org + +* About Haskell + + #+include: ./haskell.org + +* Miscellaneous + + #+include: ./miscellaneous.org + +* About this Website + + #+include: ./meta.org diff --git a/site/posts/meta.org b/site/posts/meta.org new file mode 100644 index 0000000..f6c1de5 --- /dev/null +++ b/site/posts/meta.org @@ -0,0 +1,16 @@ +#+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. + +- [[./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. diff --git a/site/posts/miscellaneous.org b/site/posts/miscellaneous.org new file mode 100644 index 0000000..7458cb3 --- /dev/null +++ b/site/posts/miscellaneous.org @@ -0,0 +1,20 @@ +#+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. + +- [[./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. + +- [[./RankNTypesInOCaml.html][Writing a Function Whose Argument is a Polymorphic Function in OCaml]] :: + In OCaml, it is not possible to write a function whose argument is a + polymorphic function. Trying to write such a function results in the + type-checker complaining back at you. The trick to be able to write + such a function is to use records. |