Use `tangle-org.el' during bootstrap

4 files changed, 195 insertions, 77 deletions

diff --git a/site/posts/meta/Bootstrap.org b/site/posts/meta/Bootstrap.org
index 9196c6c..7e78e37 100644
--- a/site/posts/meta/Bootstrap.org
+++ b/site/posts/meta/Bootstrap.org
@@ -90,6 +90,18 @@ For this website, these constants are defined as follows.
 ROOT := $(shell pwd)
 CLEODIR := site/posts/meta
 EMACS := ROOT="${ROOT}" emacs
+TANGLE := --batch --load="${ROOT}/scripts/tangle-org.el" 2>> build.log
+#+END_SRC
+
+#+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
 
 We then introduce a variable that “generation” components will populate with
@@ -98,121 +110,105 @@ their output files (using ~+=~).
 - ~GENFILES~ ::
   List *~cleopatra~* Makefiles and scripts tangled throughout the generation
   process (with the notable exception of ~Makefile~ itself).
+- ~GENSASS~ ::
+  List auxiliary ~sass~ files which can be imported by the main ~sass~ files
+  (see [[/posts/meta/Theme/][“Theming and Templating”]]).
+- ~CONTENTS~ ::
+  List generated files which are part of the target website, and acts as inputs
+  for ~soupault~.
 
 ~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
+#+BEGIN_SRC makefile :tangle Makefile
+GENFILES :=
+CONTENTS :=
+GENSASS :=
 #+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
+#+BEGIN_REMARK
+One desired feature for *~cleopatra~* would be to let it populate ~GENFILES~ and
+~GENSASS~ 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_REMARK
 
 ** 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.
+by generating and loading ~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:
-	@make build
+default: init-log build
+
+init-log:
+	@echo "==========[CLEOPATRA BUILD LOG]==========" > build.log
+
+.PHONY: init-log 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 \
-  &: ${CLEODIR}/Bootstrap.org
-	@echo "  tangle  $<"
-	@${EMACS} $< --batch \
-	   --eval "(require 'org)" \
-	   --eval "(cd (getenv \"ROOT\"))" \
-	   --eval "(setq org-src-preserve-indentation t)" \
-           --eval "(org-babel-do-load-languages 'org-babel-load-languages'((shell . t)))" \
-           --eval "(setq org-confirm-babel-evaluate nil)" \
-	   --eval "(org-babel-tangle)"
+#+BEGIN_SRC makefile :noweb yes
+<<extends(MK="${MK}", MF="${MF}", IN="${IN}", GF="${GF}", GS="${GS}")>>
 #+END_SRC
 
 ~&:~ 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
-
-#+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 bootstrap.mk
-TANGLEARGS := --batch \
-              --load="${ROOT}/scripts/tangle-org.el"
-#+END_SRC
+#+BEGIN_TODO
+Introduce ~noweb~ and ~extends~.
+#+END_TODO
 
 #+NAME: extends
-#+BEGIN_SRC bash :var MK="" :var IN="" :var GF="" :var GS="" :results output :exports none
+#+BEGIN_SRC bash :var MK="" :var IN="" :var GF="" :var GS="" :results output
 cat <<EOF
+GENFILES += ${MK} ${GF}
+GENSASS += ${GS}
+
 include ${MK}
 
 ${MK} ${GF} ${GS} \\
   &: \${CLEODIR}/${IN}
 	@echo "  tangle  \$<"
-	@\${EMACS} $< \${TANGLEARGS}
-
-GENFILES += ${MK} ${GF}
-GENSASS += ${GS}
+	@\${EMACS} $< \${TANGLE}
 EOF
 #+END_SRC
 
-#+BEGIN_SRC makefile :noweb yes
-<<extends(MK="${MK}", MF="${MF}", IN="${IN}", GF="${GF}", GS="${GS}")>>
+The twist is, we derive the rule to tangle ~bootstrap.mk~ using
+~<<extends>>~.
+
+#+BEGIN_SRC verbatim
+<<extends(IN="Bootstrap.org", MK="bootstrap.mk")>>
+#+END_SRC
+
+This means that modifying code block of ~<<extends>>~ is as “dangerous” as
+modifying ~Makefile~ itself. Keep that in mind if you start hacking
+*~cleopatra~*!
+
+For purpose of illustrations, here is the snippet generated by Babel from the
+previous source block.
+
+#+BEGIN_SRC makefile :tangle Makefile :noweb yes
+<<extends(IN="Bootstrap.org", MK="bootstrap.mk")>>
 #+END_SRC
 
+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.
+
 ** Authoring Contents
 
 - Using Coq :: [[/posts/meta/Contents/Coq/][Learn more]]
@@ -256,6 +252,8 @@ clean :
 	@rm -rf ${CONTENTS} ${GENFILES} build/
 
 force : clean build
+
+.PHONY : serve clean force build
 #+END_SRC
 
 # Local Variables:
diff --git a/site/posts/meta/Contents/Coq.org b/site/posts/meta/Contents/Coq.org
new file mode 100644
index 0000000..50aca02
--- /dev/null
+++ b/site/posts/meta/Contents/Coq.org
@@ -0,0 +1,42 @@
+* Author Guidelines
+
+* Under the Hood
+
+#+BEGIN_SRC makefile :tangle 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 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/Contents/Org.org b/site/posts/meta/Contents/Org.org
new file mode 100644
index 0000000..6bf9207
--- /dev/null
+++ b/site/posts/meta/Contents/Org.org
@@ -0,0 +1,74 @@
+* Author Guidelines
+
+* Under the Hood
+
+#+BEGIN_SRC emacs-lisp :tangle 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 ensure-package-installed (&rest packages)
+  "Ensure every PACKAGES is installed.
+
+Ask for installation if it’s
+not.  Return a list of installed packages or nil for every skipped
+package."
+  (mapcar
+   (lambda (package)
+     (if (package-installed-p package)
+         nil
+       (package-install package))
+     package)
+   packages))
+
+(ensure-package-installed 'use-package)
+(eval-when-compile (require 'use-package))
+
+(use-package org :ensure t)
+(use-package htmlize :ensure t)
+(use-package sass-mode :ensure t :defer t)
+(use-package haskell-mode :ensure t :defer t)
+(use-package github-modern-theme :ensure t :defer t
+  :init
+  (load-theme 'github-modern t))
+#+END_SRC
+
+#+BEGIN_SRC emacs-lisp :tangle scripts/export-org.el
+(org-babel-do-load-languages 'org-babel-load-languages'((shell . t)))
+(setq org-src-preserve-indentation t)
+(setq org-confirm-babel-evaluate nil)
+(setq org-export-with-toc nil)
+(org-html-export-to-html nil nil nil t)
+#+END_SRC
+
+#+BEGIN_SRC makefile :tangle org.mk
+ORG_POSTS := $(shell find site/ -name "*.org")
+
+CONTENTS += $(ORG_POSTS:.org=.html)
+
+EXPORT := --batch  --load="${ROOT}/scripts/export-org.el" 2>> build.log
+
+%.html : %.org scripts/export-org.el
+	@echo "  export  $*.org"
+	@${EMACS} $< ${EXPORT}
+#+END_SRC
+
+#+BEGIN_SRC sass :tangle site/style/org.sass
+.footpara
+    display: inline
+    margin-left: .2em
+
+.section-number-2:after, .section-number-3:after, .section-number-4:after
+    content: ". "
+
+dl dd p
+    margin-top: 0
+#+END_SRC
diff --git a/site/posts/meta/Theme.org b/site/posts/meta/Theme.org
index 51981d2..0dd9d44 100644
--- a/site/posts/meta/Theme.org
+++ b/site/posts/meta/Theme.org
@@ -147,6 +147,10 @@ body#default
 
         .TODO
             background: #fae7c5
+        .REMARK
+            background: #d4f2fc
+
+        .TODO, .REMARK
             padding: 1em 1em 1em 1em
 
             p