Provide a generic and reliable way to extends cleopatra

5 files changed, 441 insertions, 169 deletions

diff --git a/.gitignore b/.gitignore
index 00c3b4c..3e485c5 100644
--- a/.gitignore
+++ b/.gitignore
@@ -11,33 +11,36 @@ node_modules/
 package-lock.json
 
 # begin generated files
+site/posts/StronglySpecifiedFunctionsProgram.html
+site/posts/MiniHTTPServer.html
+site/posts/StronglySpecifiedFunctions.html
+site/posts/RewritingInCoq.html
+site/posts/Ltac101.html
 site/posts.html
 site/news/ColorlessThemes-0.2.html
 site/posts/meta/Contents.html
 site/posts/meta/Bootstrap.html
 site/posts/meta/Theme.html
 site/posts/meta/Soupault.html
+site/posts/meta/Contents/Org.html
+site/posts/meta/Contents/Coq.html
 site/posts/Thanks.html
 site/posts/meta.html
 site/posts/DiscoveringCommonLisp.html
 site/posts/ExtensibleTypeSafeErrorHandling.html
 site/posts/MonadTransformers.html
-site/posts/StronglySpecifiedFunctionsProgram.html
-site/posts/MiniHTTPServer.html
-site/posts/StronglySpecifiedFunctions.html
-site/posts/RewritingInCoq.html
-site/posts/Ltac101.html
 site/style/main.css
 scripts/tangle-org.el
 bootstrap.mk
+coq.mk
 org.mk
 scripts/export-org.el
-coq.mk
-sass.mk
-templates/main.html
-soupault.conf
-emacs.d/
+emacs.d
 site/style/main.sass
-site/style/org.sass
+theme.mk
+soupault.conf
+site/style/coq.sass
 site/style/coq.sass
+site/style/org.sass
+site/style/main.sass
 # begin generated files
diff --git a/Makefile b/Makefile
index 565cd8a..297f87e 100644
--- a/Makefile
+++ b/Makefile
@@ -1,8 +1,9 @@
 ROOT := $(shell pwd)
 CLEODIR := site/posts/meta
-GENFILES := scripts/tangle-org.el bootstrap.mk
 EMACS := ROOT="${ROOT}" emacs
 
+GENFILES := scripts/tangle-org.el bootstrap.mk
+
 default: build
 
 include bootstrap.mk
@@ -12,5 +13,8 @@ Makefile bootstrap.mk scripts/tangle-org.el \
 	@echo "  tangle  $<"
 	@${EMACS} $< --batch \
 	   --eval "(require 'org)" \
+	   --eval "(cd (getenv \"ROOT\"))" \
 	   --eval "(setq org-src-preserve-indentation t)" \
-	   --eval "(org-babel-tangle)" 2>/dev/null
+           --eval "(org-babel-do-load-languages 'org-babel-load-languages'((shell . t)))" \
+           --eval "(setq org-confirm-babel-evaluate nil)" \
+	   --eval "(org-babel-tangle)"
diff --git a/site/posts/meta/Bootstrap.org b/site/posts/meta/Bootstrap.org
index 1683df5..379ad0b 100644
--- a/site/posts/meta/Bootstrap.org
+++ b/site/posts/meta/Bootstrap.org
@@ -2,10 +2,10 @@
 <h1>Bootstrapping an Extensible Toolchain</h1>
 #+END_EXPORT
 
-A literate program is a particular type of software program where the sentence
-/“the code is the documentation”/ is actually the expected result, rather than
-an admission of failure. That is, the same source files are used to generate the
-program *and* the documentation.
+A literate program is a particular type of software program where code is not
+directly written in source files, but rather in text document as code
+snippets. In some sense, literate programming allows for writing in the same
+place both the software program and its technical documentation.
 
 That being said, *~cleopatra~* is a toolchain to build a website before being a
 literate program, and one of its objective is to be /part of this very website
@@ -17,6 +17,8 @@ files.
 The page you are currently reading is *~cleopatra~* entry point. Its primilarly
 purpose is to introduce two Makefiles: ~Makefile~ and ~bootstrap.mk~.
 
+#+TOC: headlines 2
+
 * The Root of Generation
 
 ~Makefile~ serves two purposes: it initiates a few global variables, and it
@@ -33,27 +35,101 @@ clean~.
 This is similar to your computer: it requires a firmware to boot, whose purpose
 —in a nutshell— is to find and load an operating system.
 
+Here, the generation process proceeds as follows:
+
 Modifying the content of ~Makefile~ in this document /will/ modify
 ~Makefile~. This means one can easily put *~cleopatra~* into an inconsistent
 state, which would prevent further generation. This is why the generated
-~Makefile~ should be versioned, so that you can use
+~Makefile~ should be versioned, so that you can restore it using ~git~ if you
+made a mistake when you modified it.
 
-#+BEGIN_SRC shell
-git restore Makefile
-#+END_SRC
+We now detail the rules introduce by ~Makefile~, and why they effectively
+bootstrap a generation process. For readers interested in using *~cleopatra~*
+for their own websites, we highlight the potential modifications they would have
+to make.
+
+** Global Constants and Variables
+
+First, ~Makefile~ defines several global “constants” (although as far as I know
+~make~ does not support true constant values, it is expected further generation
+“components” will not modify them).
+
+In a nutshell,
+
+- ~ROOT~ ::
+  Tell Emacs where the root of your website sources is, so that tangled output
+  filenames can be given relative to it rather than the org files.  So for
+  instance, the ~BLOCK_SRC~ headers for ~Makefile~ looks like
+
+  #+BEGIN_SRC org
+  #+BEGIN_SRC makefile :tangle Makefile :noweb tangle
+  #+END_SRC
+
+  instead of, /e.g./,
 
-before fixing your error.
+  #+BEGIN_SRC org
+  #+BEGIN_SRC makefile :tangle ../../../Makefile :noweb tangle
+  #+END_SRC
 
-#+BEGIN_SRC makefile :tangle (concat (getenv "ROOT") "/Makefile") :noweb tangle
+- ~CLEODIR~ ::
+  Tell *~cleopatra~* where its sources live. If you place it inside the ~site/~
+  directory (as it is intended), and you enable the use of ~org~ files to author
+  your contents, then *~cleopatra~* documents will be part of your website. If
+  you don’t want that, just move the directory outside the ~site/~ directory,
+  and update the ~CLEODIR~ variable accordingly.
+
+- ~EMACS~ ::
+  Tell *~cleopatra~* the command to use to call Emacs. You can modify it to use
+  a custom Emacs you build yourself if you so desire. Note that the command *has
+  to be prefixed by ~ROOT=${ROOT}~, otherwise the source defined in
+  *~cleopatra~* documents will not be tangled in the right places.
+
+For this website, these constants are defined as follows.
+
+#+BEGIN_SRC makefile :tangle Makefile :noweb tangle
 ROOT := $(shell pwd)
 CLEODIR := site/posts/meta
-GENFILES := scripts/tangle-org.el bootstrap.mk
 EMACS := ROOT="${ROOT}" emacs
 #+END_SRC
 
-#+BEGIN_SRC makefile :tangle (concat (getenv "ROOT") "/Makefile") :noweb tangle
+We then introduce a variable that “generation” components will populate with
+their output files (using ~+=~).
+
+- ~GENFILES~ ::
+  List *~cleopatra~* Makefiles and scripts tangled throughout the generation
+  process (with the notable exception of ~Makefile~ itself).
+
+~GENFILES~ is initiated with files obtained after tangling this very document.
+
+#+BEGIN_SRC makefile :tangle Makefile :noweb tangle
+GENFILES := scripts/tangle-org.el bootstrap.mk
+#+END_SRC
+
+#+BEGIN_TODO
+One desired feature for *~cleopatra~* would be to let it populate ~GENFILES~
+automatically, by looking for relevant ~:tangle~ directives. The challenge lies
+in the “relevant” part: the risk exists that we have false posivite. Whether or
+not it is an issue remains an open question.
+#+END_TODO
+
+** Bootstrapping
+
+The core purpose of ~Makefile~ remains *(1)* to bootstrap the generation process
+by generating ~bootstrap.mk~, and *(2)* to enforce the ~build~ rules hopefully
+defined by the latter is called.
+
+For *(2)*, we introduce a ~default~ rule with ~build~ as a
+dependency.
+
+#+BEGIN_SRC makefile :tangle Makefile :noweb tangle
 default: build
+#+END_SRC
+
+For *(1)*, we rely on a particular behavior of ~make~ regarding the ~include~
+directive. If an operand of ~include~ does not yet exists, ~make~ will search
+for a rule to generate it.
 
+#+BEGIN_SRC makefile :tangle Makefile :noweb tangle
 include bootstrap.mk
 
 Makefile bootstrap.mk scripts/tangle-org.el \
@@ -61,60 +137,124 @@ Makefile bootstrap.mk scripts/tangle-org.el \
 	@echo "  tangle  $<"
 	@${EMACS} $< --batch \
 	   --eval "(require 'org)" \
+	   --eval "(cd (getenv \"ROOT\"))" \
 	   --eval "(setq org-src-preserve-indentation t)" \
-	   --eval "(org-babel-tangle)" 2>/dev/null
+           --eval "(org-babel-do-load-languages 'org-babel-load-languages'((shell . t)))" \
+           --eval "(setq org-confirm-babel-evaluate nil)" \
+	   --eval "(org-babel-tangle)"
 #+END_SRC
 
-* Bootstrapping
+~&:~ is used in place of ~:~ to separate the target from its dependencies in
+this rule to tell to ~make~ that the commands run will generate all these files.
+
+From now on, the bootstrap process is completed: further generation processes
+will fully be defined using literate programming, with no special treatment for
+its output. For instance, you may not want to use ~soupault~? You can! Just
+modify ~bootstrap.mk~ accordingly.
+
+* Generation Processes
+
+*~cleopatra~* has been designed with extensibility in mind. In particular, it
+should be fairly easy to extend it to support additional input format. In this
+section, we explain how this is achieved.
+
+** Initialization
+
+First, additional global variables are introduced, since ~GENFILES~ is specific
+to *~cleopatra~*. These variables are
+
+- ~GENSASS~ ::
+  List auxiliary ~sass~ files which can be imported by the main ~sass~ files
+  (see [[/posts/meta/Theme/][“Theming and Templating”]]).
+- ~CONTENTS~ ::
+  List generated files which are part of the target website, and acts as inputs
+  for ~soupault~.
+
+and they are initially empty
+
+#+BEGIN_SRC makefile :tangle bootstrap.mk
+GENSASS :=
+CONTENTS :=
+#+END_SRC
 
-#+NAME: tangle-org
-#+BEGIN_SRC emacs-lisp :tangle (concat (getenv "ROOT") "/scripts/tangle-org.el")
+#+BEGIN_SRC emacs-lisp :tangle scripts/tangle-org.el
 (require 'org)
+(cd (getenv "ROOT"))
+(setq org-confirm-babel-evaluate nil)
 (setq org-src-preserve-indentation t)
+(org-babel-do-load-languages
+ 'org-babel-load-languages
+ '((shell . t)))
 (org-babel-tangle)
 #+END_SRC
 
-#+BEGIN_SRC makefile :tangle (concat (getenv "ROOT") "/bootstrap.mk")
-GENSASS :=
-CONTENTS :=
-GENFILES += org.mk scripts/export-org.el coq.mk \
-            sass.mk ${SASS} templates/main.html \
-            soupault.conf
+#+BEGIN_SRC makefile :tangle bootstrap.mk
+TANGLEARGS := --batch \
+              --load="${ROOT}/scripts/tangle-org.el"
+#+END_SRC
 
-include org.mk coq.mk sass.mk
+#+NAME: extends
+#+BEGIN_SRC bash :var MK="" :var IN="" :var GF="" :var GS="" :results output :exports none
+cat <<EOF
+include ${MK}
 
-TANGLEARGS := --batch \
-              --load="${ROOT}/scripts/tangle-org.el" \
-              2>/dev/null
+${MK} ${GF} ${GS} \\
+  &: \${CLEODIR}/${IN}
+	@echo "  tangle  \$<"
+	@\${EMACS} $< \${TANGLEARGS}
 
+GENFILES += ${MK} ${GF}
+GENSASS += ${GS}
+EOF
+#+END_SRC
+
+#+BEGIN_SRC makefile :noweb yes
+<<extends(MK="${MK}", MF="${MF}", IN="${IN}", GF="${GF}", GS="${GS}")>>
+#+END_SRC
+
+** Authoring Contents
+
+- Using Coq :: [[/posts/meta/Contents/Coq/][Learn more]]
+- Using Org :: [[/posts/meta/Contents/Org/][Learn more]]
+
+#+BEGIN_SRC makefile :tangle bootstrap.mk :noweb tangle :exports none
+<<extends(MK="coq.mk", IN="Contents/Coq.org", GS="site/style/coq.sass")>>
+#+END_SRC
+
+#+BEGIN_SRC makefile :tangle bootstrap.mk :noweb tangle :exports none
+<<extends(MK="org.mk", IN="Contents/Org.org", GF="scripts/export-org.el emacs.d", GS="site/style/org.sass")>>
+#+END_SRC
+
+** Theming and Templating
+
+#+BEGIN_SRC makefile :tangle bootstrap.mk :noweb tangle :exports none
+<<extends(MK="theme.mk", IN="Theme.org", GS="site/style/main.sass")>>
+#+END_SRC
+
+** Postprocessing HTML using ~soupault~
+
+#+BEGIN_SRC makefile :tangle bootstrap.mk :noweb tangle :exports none
+<<extends(IN="Soupault.org", GF="soupault.conf")>>
+#+END_SRC
+
+** Wrapping-up
+
+#+BEGIN_SRC makefile :tangle bootstrap.mk
 build : ${CONTENTS} ${GENFILES}
 	@echo "     run  soupault"
 	@soupault
 	@echo "  update  .gitignore"
 	@scripts/update-gitignore.sh ${CONTENTS} ${GENFILES} ${GENSASS}
 
+serve :
+	@echo "   start  a python server"
+	@cd build; python -m http.server 2>/dev/null
+
 clean :
 	@echo "  remove  generated files"
 	@rm -rf ${CONTENTS} ${GENFILES} build/
 
 force : clean build
-
-soupault.conf : ${CLEODIR}/Soupault.org
-	@echo "  tangle  $<"
-	@${EMACS} $< ${TANGLEARGS}
-
-org.mk scripts/export-org.el site/style/org.sass \
-coq.mk site/style/coq.sass \
-  &: ${CLEODIR}/Contents.org
-	@echo "  tangle  $<"
-	@${EMACS} $< ${TANGLEARGS}
-
-sass.mk ${SASS} templates/main.html \
-  &: ${CLEODIR}/Theme.org
-	@echo "  tangle  $<"
-	@${EMACS} $< ${TANGLEARGS}
-
-.PHONY: clean build force default
 #+END_SRC
 
 # Local Variables:
diff --git a/site/posts/meta/Contents.org b/site/posts/meta/Contents.org
index d287585..0863709 100644
--- a/site/posts/meta/Contents.org
+++ b/site/posts/meta/Contents.org
@@ -1,116 +1,3 @@
 #+BEGIN_EXPORT html
 <h1>Authoring Contents and HTML Generation</h1>
 #+END_EXPORT
-
-* Using Org files
-
-** Author Guidelines
-
-** Under the Hood
-
-#+BEGIN_SRC emacs-lisp :tangle (concat (getenv "ROOT") "/scripts/export-org.el")
-(require 'package)
-
-(setq user-emacs-directory (concat (getenv "ROOT") "/emacs.d"))
-(setq package-user-dir (concat (getenv "ROOT") "/emacs.d"))
-(setq package-archives '(("gnu"   . "https://elpa.gnu.org/packages/")
-                         ("melpa" . "https://melpa.org/packages/")))
-
-(package-initialize)
-
-(or (file-exists-p package-user-dir)
-    (package-refresh-contents))
-
-(defun require-packages-force (&rest packages)
-  "Ensure every PACKAGES is available"
-  (mapcar
-   (lambda (package)
-     (let ((package (if (listp package)
-                        package
-                      (cons package package))))
-       (if (not (package-installed-p (car package)))
-           (package-install (car package)))
-       (if (cdr package)
-           (require (cdr package)))
-       package))
-   packages))
-
-(require-packages-force
- 'org 'htmlize 'nordless-theme
- 'sass-mode 'haskell-mode)
-#+END_SRC
-
-#+BEGIN_SRC emacs-lisp :tangle (concat (getenv "ROOT") "/scripts/export-org.el")
-(setq htmlize-output-type 'inline-css)
-(setq org-export-with-toc nil)
-(org-html-export-to-html nil nil nil t)
-#+END_SRC
-
-#+BEGIN_SRC makefile :tangle (concat (getenv "ROOT") "/org.mk")
-ORG_POSTS := $(shell find site/ -name "*.org")
-
-CONTENTS += $(ORG_POSTS:.org=.html)
-GENSASS += site/style/org.sass
-GENFILES += emacs.d/
-
-EXPORTARGS := --batch \
-              --load="${ROOT}/scripts/export-org.el"
-
-%.html : %.org scripts/export-org.el
-	@echo "  export  $*.org"
-	@${EMACS} $< ${EXPORTARGS}
-#+END_SRC
-
-#+BEGIN_SRC sass :tangle (concat (getenv "ROOT") "/site/style/org.sass")
-.footpara
-    display: inline
-    margin-left: .2em
-
-.section-number-2:after, .section-number-3:after, .section-number-4:after
-    content: ". "
-#+END_SRC
-
-* Using Coq files
-
-** Author Guidelines
-
-** Under the Hood
-
-#+BEGIN_SRC makefile :tangle (concat (getenv "ROOT") "/coq.mk")
-COQ_POSTS := $(shell find site/ -name "*.v")
-CONTENTS += $(COQ_POSTS:.v=.html)
-GENSASS += site/style/coq.sass
-
-COQLIB := "https://coq.inria.fr/distrib/current/stdlib/"
-COQCARG := -async-proofs-cache force \
-           -w -custom-entry-overriden
-COQDOCARG := --no-index --charset utf8 --short \
-             --body-only --coqlib "${COQLIB}"
-
-%.html : %.v
-	@echo "  export  $*.v"
-	@coqc ${COQCARG} $<
-	@coqdoc ${COQDOCARG} -d $(shell dirname $<) $<
-	@sed -i -e 's/href="$(shell basename $@)\#/href="\#/g' $@
-	@rm -f $(shell dirname $<)/coqdoc.css
-#+END_SRC
-
-#+BEGIN_SRC sass :tangle (concat (getenv "ROOT") "/site/style/coq.sass")
-div.code
-    white-space: nowrap
-    overflow-x: visible
-
-.code a[href]
-    text-decoration: none
-
-    .fa-external-link
-      display: none
-
-.paragraph
-    margin-top: 1em
-    margin-bottom: 1em
-#+END_SRC
-
-# Local Variables:
-# org-src-preserve-indentation: t
-# End:
diff --git a/site/posts/meta/Theme.org b/site/posts/meta/Theme.org
new file mode 100644
index 0000000..51981d2
--- /dev/null
+++ b/site/posts/meta/Theme.org
@@ -0,0 +1,238 @@
+#+BEGIN_EXPORT html
+<h1>Theming and Templating</h1>
+#+END_EXPORT
+
+* Main HTML Template
+
+#+NAME: js_lazyloading
+#+BEGIN_SRC js
+let noscript = document.getElementById('lazyloading');
+let resources = noscript.innerText.split('\n');
+
+for (var ix in resources) {
+    noscript.insertAdjacentHTML('beforebegin', resources[ix]);
+}
+#+END_SRC
+
+#+NAME: html_lazyloading
+#+BEGIN_SRC html
+<noscript id="lazyloading">
+  <link rel="stylesheet" href="/vendors/katex.0.11.1/katex.css">
+  <link rel="stylesheet"
+        href="/vendors/fork-awesome.1.1.7/css/fork-awesome.min.css">
+  <link rel="stylesheet" href="/vendors/fira-code.2/font.css">
+  <link rel="stylesheet" href="/vendors/et-book/font.css">
+</nolink>
+#+END_SRC
+
+#+BEGIN_SRC html  :tangle templates/main.html :noweb tangle
+<html lang="en">
+  <head>
+    <meta charset="utf-8">
+    <title> <!-- set automatically, see soupault.conf --> </title>
+    <meta name="viewport"
+          content="width=device-width, initial-scale=1.0">
+    <link rel="stylesheet" href="/style/main.css">
+    <link rel="icon" type="image/ico"  href="/img/merida.webp">
+    <<html_lazyloading>>
+  </head>
+  <body id="default">
+    <nav>
+      <ul>
+        <li> <a href="/news">News</a></li>
+        <li> <a href="/posts">Write-ups</a></li>
+        <li> <a href="/">About</a></li>
+      </ul>
+    </nav>
+    <header>
+      <img src="/img/merida.webp"
+           alt="This picture is Merida in Ralph 2.0, and is my main avatar" />
+    </header>
+    <main>
+    <!-- your page content will be inserted here,
+         see the content_selector option in soupault.conf -->
+    </main>
+    <script>
+      <<js_lazyloading>>
+    </script>
+  </body>
+</html>
+#+END_SRC
+
+* Main SASS File
+
+#+BEGIN_SRC sass :tangle site/style/main.sass
+$bg-color: #fcfcfc
+$fg-color: #333
+$primary-color: black
+
+*
+  box-sizing: border-box
+
+body, html
+    width: 100%
+    height: 100%
+    padding: 0
+    margin: 0
+    font-size: 100%
+    background: $bg-color
+    color: $fg-color
+    font-family: 'et-book', serif
+
+h1, h2, h3, h4, h5, a[href]
+    color: $primary-color
+
+h1, h2, h3, h4, h5
+    font-family: sans-serif
+
+h1
+    text-align: center
+
+a[href] .url-mark
+    font-size: smaller;
+    padding-left: 0.2em
+
+/* default */
+
+body#default
+    overflow-x: hidden
+
+    nav
+        padding-top: 1em
+        padding-bottom: 1em
+        width: 100%
+
+        ul
+            padding: 0
+            margin: 0
+            width: 100%
+            display: flex
+            flex-direction: row
+            justify-content: center
+            list-style-type: none
+
+        li
+            padding-left: .5em
+            padding-right: .5em
+            text-transform: uppercase
+            font-family: sans-serif
+            font-size: 130%
+            font-weight: bold
+
+            a
+                text-decoration: none
+
+    header
+        text-align: center
+
+        img
+            text-align: center
+            border-radius: 50%
+            width: 125px
+
+    main
+        max-width: 550px
+        margin: auto
+        padding: 0em 1em 1em 1em
+        font-size: 130%
+
+body#default main .code, code, pre, .inlinecode, tt
+    font-family: 'Fira Code', monospace
+    font-size: 75%
+
+
+body#default
+    main
+        @import coq, org
+
+        .TODO
+            background: #fae7c5
+            padding: 1em 1em 1em 1em
+
+            p
+                margin: 0
+            p:not(:list-child)
+                margin-bottom: 1em
+
+/* VCARD (index.html) */
+body#vcard
+    display: flex
+    align-items: center
+    flex-direction: column
+    font-size: 125%
+
+    article
+        max-width: 400px
+        width: 80%
+        margin: auto
+
+        img
+            display: block
+            border-radius: 50%
+            width: 175px
+            margin: auto
+            margin-bottom: 3em
+
+    h1
+        color: $primary-color
+        font-size: 300%
+        text-align: center
+
+    nav dt
+        font-weight: bold
+
+        a
+            color: $primary-color
+
+/* indexes */
+
+.index
+    dt
+        font-weight: bold
+        color: $primary-color
+
+    dd
+        margin-left: 0
+        margin-bottom: 1em
+
+        ol
+            margin-top: 0.3em
+
+#history
+  summary
+    color: $primary-color
+    font-weight: bold
+
+  table
+    border-top: 2px solid $primary-color
+    border-bottom: 2px solid $primary-color
+    border-collapse: collapse;
+
+  td
+    border-bottom: 1px solid $primary-color
+    padding: .5em
+    vertical-align: top
+
+  td.commit
+    font-size: smaller
+
+  td.commit
+    font-family: 'Fira Code', monospace
+    font-size: 80%
+    white-space: nowrap;
+
+.imath
+  font-size: smaller
+#+END_SRC
+
+#+BEGIN_SRC makefile :tangle theme.mk
+SASS := site/style/main.sass
+CSS := $(SASS:.sass=.css)
+
+GENFILES += ${CLEO_THEME_TANGLE} ${SASS}
+CONTENTS += ${CSS}
+
+${CSS} : ${SASS} ${GENSASS}
+	@echo " compile  $<"
+	@sassc --style=compressed --sass $< $@
+#+END_SRC