diff options
-rw-r--r-- | .gitignore | 25 | ||||
-rw-r--r-- | Makefile | 8 | ||||
-rw-r--r-- | site/posts/meta/Bootstrap.org | 226 | ||||
-rw-r--r-- | site/posts/meta/Contents.org | 113 | ||||
-rw-r--r-- | site/posts/meta/Theme.org | 238 |
5 files changed, 441 insertions, 169 deletions
@@ -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 @@ -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 |