path: root/site
diff options
authorThomas Letan <>2020-12-20 12:47:37 +0100
committerThomas Letan <>2020-12-20 12:47:37 +0100
commit9722f57891b99694a60d2fcb376375606741445e (patch)
tree8b69d0ac330580a89bc3e4d270d75cbb78554053 /site
parent240f069dad61a85dbfc281472a2af6cb91ef07d4 (diff)
Provide some insight on how literate programming projects are built
Diffstat (limited to 'site')
2 files changed, 54 insertions, 21 deletions
diff --git a/site/ b/site/
index 313007f..77e8ff1 100644
--- a/site/
+++ b/site/
@@ -40,7 +40,13 @@ written as literate programs.
- [[file:cleopatra/][Authoring Contents As Coq Documents ~(TODO)~]] ::
-- [[./cleopatra/][Authoring Literate Programs ~(TODO)~]] ::
+- [[./cleopatra/][Authoring Literate Programs]] ::
+ Literate programming is an interesting exercice, and it is
+ particularly well-suited for blog posts, since at the very least it
+ provides the tool to enforce the code presented to readers is
+ correct. We use Emacs and ~org-mode~ to tangle the literate
+ programming projects present in the ~posts/~ directory of this
+ website.
- [[./cleopatra/][Authoring Contents As Org Documents ~(TODO)~]] ::
diff --git a/site/cleopatra/ b/site/cleopatra/
index 3b56924..be25097 100644
--- a/site/cleopatra/
+++ b/site/cleopatra/
@@ -2,12 +2,56 @@
<h1>Literate Programming Projects</h1>
+Literate programming is an interesting exercice. It forces programmers
+to think about how to present their code for other people to
+understand it. It poses several significant challenges, in particular
+in terms of code refactoring. If a given piece of code is too much
+entangled with proses explaining it, rewriting it becomes cumbersome.
+That being said, literate programming is particularly well-suited for
+blog posts, since at the very least it provides the tool to enforce
+the code presented to readers is correct.
+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
+ 'org-babel-load-languages
+ '((shell . t))) ; allow the execution of shell block code
+ ;; scan the posts/ directory and tangled it into lp/
+(setq org-publish-project-alist
+ '(("lp"
+ :base-directory "site/posts"
+ :publishing-directory "lp"
+ :recursive t
+ :publishing-function cleopatra:tangle-publish)))
+Tangling literate programming is done in the =prebuild= phase of
#+BEGIN_SRC makefile :tangle
literate-programming-prebuild :
@cleopatra echo "Tangling" "literate programming project"
@cleopatra exec -- cleopatra-run-elisp export-lp.el \
>> build.log 2>&1
+ARTIFACTS += lp/ site/posts/deps.svg
+In the =build= phase, we actually try to compile the tangled projects.
+As of now, there is only one literate program: [[../posts/][the Echo server
+implemented in Coq]] which demonstrates how ~coqffi~ can be used to
+implement realistic software projects.
+#+BEGIN_SRC makefile :tangle
COQFFI_ARCHIVE := site/files/coqffi-tutorial.tar.gz
coqffi-tutorial-build : literate-programming-prebuild
@@ -15,28 +59,11 @@ coqffi-tutorial-build : literate-programming-prebuild
@cd lp/coqffi-tutorial; dune build --display quiet
@cleopatra echo "Archiving" "coqffi tutorial"
- @tar --exclude="_build" -C lp/ -czvf ${COQFFI_ARCHIVE} coqffi-tutorial >> build.log
+ @tar --exclude="_build" -C lp/ -czvf ${COQFFI_ARCHIVE} coqffi-tutorial \
+ 2>&1 >> build.log
site/posts/CoqffiEcho.html : coqffi-tutorial-build
literate-programming-build : coqffi-tutorial-build
-ARTIFACTS += lp/ ${COQFFI_ARCHIVE} site/posts/deps.svg
-#+BEGIN_SRC emacs-lisp :tangle export-lp.el
- 'org-babel-load-languages
- '((shell . t)))
-(setq org-publish-project-alist
- '(("lp"
- :base-directory "site/posts"
- :publishing-directory "lp"
- :recursive t
- :publishing-function cleopatra:tangle-publish)))