diff options
34 files changed, 1411 insertions, 1020 deletions
@@ -5,32 +5,44 @@ _opam .cleopatra .emacs .lia.cache +_opam build.log -build/ +commands.mk coq.mk +dependencies.mk export-lp.el -katex.mk literate-programming.mk lp/ -node_modules/ +node_modules org.mk +out package-lock.json package.json +plugins/clean-up.lua +plugins/css.lua plugins/external-urls.lua -plugins/fix-org-urls.lua +plugins/series.lua plugins/urls-rewriting.lua +rss.json +scripts/css.sh scripts/export-org.el scripts/history.sh -scripts/katex.js scripts/packages.el +scripts/render-equations.js site/cleopatra.html +site/cleopatra/commands.html site/cleopatra/coq.html +site/cleopatra/dependencies.html site/cleopatra/literate-programming.html site/cleopatra/org.html site/cleopatra/soupault.html site/cleopatra/theme.html +site/coq.html site/files/coqffi-tutorial.tar.gz +site/haskell.html site/index.html +site/meta.html +site/miscellaneous.html site/news/ColorlessThemes-0.2.html site/opinions/MonadTransformers.html site/opinions/index.html @@ -93,13 +105,10 @@ site/posts/StronglySpecifiedFunctionsRefine.vos site/posts/Thanks.html site/posts/deps.svg site/projects/index.html -site/style/coq.sass -site/style/main.css -site/style/main.sass -site/style/org.sass -site/style/plugins.sass soupault.conf soupault.mk +style.css +style.min.css templates/history.html templates/main.html theme.mk 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 Binary files differdeleted file mode 100644 index c0e6354..0000000 --- a/site/img/merida.webp +++ /dev/null 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 |
