diff options
-rw-r--r-- | site/news/index.html | 2 | ||||
-rw-r--r-- | site/posts/StronglySpecifiedFunctions.v | 2 | ||||
-rw-r--r-- | site/posts/StronglySpecifiedFunctionsProgram.v | 2 | ||||
-rw-r--r-- | site/posts/index.org (renamed from site/posts.org) | 26 | ||||
-rw-r--r-- | site/posts/meta/Bootstrap.org | 16 | ||||
-rw-r--r-- | site/posts/meta/Soupault.org | 2 | ||||
-rw-r--r-- | site/posts/meta/index.org (renamed from site/posts/meta.org) | 10 |
7 files changed, 30 insertions, 30 deletions
diff --git a/site/news/index.html b/site/news/index.html index 8249a08..0dfe7e3 100644 --- a/site/news/index.html +++ b/site/news/index.html @@ -8,7 +8,7 @@ released <code>colorless-themes-0.2</code>, <code>nordless-theme-0.2</code>, and <code>lavenderless-theme-0.2</code>. <br /> - <a href="/news/ColorlessThemes-0.2">Learn more.</a> + <a href="./ColorlessThemes-0.2.html">Learn more.</a> </li> </ul> diff --git a/site/posts/StronglySpecifiedFunctions.v b/site/posts/StronglySpecifiedFunctions.v index fa5df95..ac55b7e 100644 --- a/site/posts/StronglySpecifiedFunctions.v +++ b/site/posts/StronglySpecifiedFunctions.v @@ -3,7 +3,7 @@ This is the first article (initially published on #<span class="time">January 11, 2015</span>#) of a series of two on how to write strongly-specified functions in Coq. You can read the next part #<a - href="/posts/StronglySpecifiedFunctionsProgram">here</a>#. *) + href="./StronglySpecifiedFunctionsProgram.html">here</a>#. *) (** I started to play with Coq, the interactive theorem prover developed by Inria, a few weeks ago. It is a very powerful tool, diff --git a/site/posts/StronglySpecifiedFunctionsProgram.v b/site/posts/StronglySpecifiedFunctionsProgram.v index 33200c8..2a998aa 100644 --- a/site/posts/StronglySpecifiedFunctionsProgram.v +++ b/site/posts/StronglySpecifiedFunctionsProgram.v @@ -3,7 +3,7 @@ This is the second article (initially published on #<span class="time">January 01, 2017</span>#) of a series of two on how to write strongly-specified functions in Coq. You can read the previous part #<a - href="/posts/StronglySpecifiedFunctions">here</a>#. # *) + href="./StronglySpecifiedFunctions.html">here</a>#. # *) (** #<div id="generate-toc"></div># diff --git a/site/posts.org b/site/posts/index.org index a3a3e37..3c583a5 100644 --- a/site/posts.org +++ b/site/posts/index.org @@ -19,15 +19,15 @@ 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/MiniHTTPServer/][Implementing and Certifying a Web Server in Coq]] :: +- [[./MiniHTTPServer.html][Implementing and Certifying a Web Server in Coq]] :: An explanation on how to write an almost pure Coq, and working (albeit minimal) HTTP server. -- [[/posts/Ltac101/][Ltac 101]] :: +- [[./Ltac101.html][Ltac 101]] :: Ltac is the “tactic language” of Coq. It allows for writing proof scripts which construct proof terms later checked by Coq. -- [[/posts/RewritingInCoq/][Rewriting in Coq]] :: +- [[./RewritingInCoq.html][Rewriting in Coq]] :: The ~rewrite~ tactics are really useful, since they are not limited to the Coq built-in equality relation. @@ -36,15 +36,15 @@ machine-checked proofs. satisfy, such that using such a function requires providing a proof the property is satisfied. - 1. [[/posts/StronglySpecifiedFunctions/][Using the ~refine~ Tactics]] - 2. [[/posts/StronglySpecifiedFunctionsProgram][Using the ~Program~ Framework]] + 1. [[./StronglySpecifiedFunctions.html][Using the ~refine~ Tactics]] + 2. [[./StronglySpecifiedFunctionsProgram.html][Using the ~Program~ Framework]] * About Haskell Haskell is a pure, lazy, functional programming language with a very expressive type system. -- [[/posts/ExtensibleTypeSafeErrorHandling/][Extensible, Type-Safe Error Handling In Haskell]] :: +- [[./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. @@ -57,7 +57,7 @@ type system. Common Lisp is a venerable programming languages like no other I know. -- [[/posts/DiscoveringCommonLisp/][Discovering Common Lisp with ~trivial-gamekit~]] :: +- [[./DiscoveringCommonLisp.html][Discovering Common Lisp with ~trivial-gamekit~]] :: From the creation of a Lisp package up to the creation of a standalone executable. @@ -67,18 +67,18 @@ One of my goal with this website is for it to /feel/ simple, but the truth is under the hood it is generated from a bunch of files using a not-that-simple process. -- [[/posts/meta/][A Series on Generating this Static Website]] :: +- [[./meta.html][A Series on Generating this Static Website]] :: The toolchain behind the generation of this website ---called *~cleopatra~*--- is a literate programming document which build itself in addition to the HTML files composing this corner of the Internet. - 1. [[/posts/meta/Bootstrap/][Bootstrapping an Extensible Toolchain ~(TODO)~]] - 2. [[/posts/meta/Contents][Authoring Contents and HTML Generation ~(WIP)~]] - 3. [[/posts/meta/Soupault/][Configuring ~soupault~ ~(WIP)~]] - 4. [[/posts/meta/Theme/][Theming and Templating ~(WIP)~]] + 1. [[./meta/Bootstrap.html][Bootstrapping an Extensible Toolchain]] + 2. [[./meta/Contents.html][Authoring Contents and HTML Generation ~(WIP)~]] + 3. [[./meta/Soupault.html][Configuring ~soupault~ ~(WIP)~]] + 4. [[./meta/Theme.html][Theming and Templating ~(WIP)~]] -- [[/posts/Thanks/][Thanks!]] :: +- [[./Thanks.html][Thanks!]] :: If it were not for many awesome FOSS projects, this corner of the Internet would not exists. This is my attempt to give well-deserved credit to them and their creators. diff --git a/site/posts/meta/Bootstrap.org b/site/posts/meta/Bootstrap.org index 0f3a07e..8e645c7 100644 --- a/site/posts/meta/Bootstrap.org +++ b/site/posts/meta/Bootstrap.org @@ -90,8 +90,8 @@ their output files (using ~+=~). 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”]]). + List auxiliary ~sass~ files which can later be imported by the main ~sass~ + files (see [[./Theme.org][“Theming and Templating”]]). - ~CONTENTS~ :: List generated files which are part of the target website, and acts as inputs for ~soupault~. @@ -207,7 +207,7 @@ can insert the result of the evaluation of =extends= inside another source block when the latter is tangled. The twist is, we derive the rule to tangle ~bootstrap.mk~ using -~<<extends>>~. The syntax is the following: +=extends=. The syntax is the following: #+BEGIN_SRC verbatim <<extends(IN="Bootstrap.org", MK="bootstrap.mk", GF="scripts/update-gitignore.sh")>> @@ -220,7 +220,7 @@ previous source block. <<extends(IN="Bootstrap.org", MK="bootstrap.mk", GF="scripts/update-gitignore.sh")>> #+END_SRC -Beware that, as a consequence, modifying code block of ~<<extends>>~ is as +Beware that, as a consequence, modifying code block of =extends= is as “dangerous” as modifying ~Makefile~ itself. Keep that in mind if you start hacking *~cleopatra~*! @@ -231,7 +231,7 @@ modify ~bootstrap.mk~ accordingly. * Generation Processes -Thanks to ~<<extends>>~, *~cleopatra~* is easily extensible. In this section, we +Thanks to =extends=, *~cleopatra~* is easily extensible. In this section, we enumerate the generation processes that are currently used to generate the website you are reading. @@ -247,16 +247,16 @@ In the present website, contents can be written in the following format: - Regular Coq files :: Coq is a system which allows to write machine-checked proofs, and it comes with a source “prettifier” called ~coqdoc~. - [[/posts/meta/Contents/Coq/][Learn more about the generation process for Coq files]] + [[./Contents/Coq.org][Learn more about the generation process for Coq files]] - Org documents :: Emacs comes with a powerful editing mode called [[https://orgmode.org/][Org mode]], and Org documents are really pleasant to work with. - [[/posts/meta/Contents/Org/][Learn more about the generation process for Org documents]] + [[./Contents/Org.org][Learn more about the generation process for Org documents]] If you want *~cleopatra~* to support more input formats, you have to 1. Create a org file which, once tangled, provide a dedicated makefile -2. Edit this file (~Bootstrap.org~) here, and use ~<<extends>>~ to make sure it +2. Edit this file (~Bootstrap.org~) here, and use =extends= to make sure it is actually tangled when necessary #+BEGIN_SRC makefile :tangle bootstrap.mk :noweb tangle :exports none diff --git a/site/posts/meta/Soupault.org b/site/posts/meta/Soupault.org index 913c8ae..aab5476 100644 --- a/site/posts/meta/Soupault.org +++ b/site/posts/meta/Soupault.org @@ -23,7 +23,7 @@ default_template = "templates/main.html" content_selector = "main" doctype = "<!DOCTYPE html>" - clean_urls = true + clean_urls = false [widgets.page-title] widget = "title" diff --git a/site/posts/meta.org b/site/posts/meta/index.org index 22f200f..db5542e 100644 --- a/site/posts/meta.org +++ b/site/posts/meta/index.org @@ -17,19 +17,19 @@ my contents. Did you know that Cleopatra was a reputed polyglot (at least according to [[https://fr.wikipedia.org/wiki/Polyglotte][Wikipedia France]])? #+BEGIN_EXPORT html -<div id="history">site/posts/meta.org</div> +<div id="history">site/posts/meta/index.org</div> <article class="index"> #+END_EXPORT *Beware* this series is far from being complete. -- [[/posts/meta/Bootstrap][Bootstrapping an Extensible Toolchain ~(WIP)~]] :: +- [[./Bootstrap.org][Bootstrapping an Extensible Toolchain]] :: -- [[/posts/meta/Contents][Authoring Content and HTML Generation ~(WIP)~]] :: +- [[./Contents.org][Authoring Content and HTML Generation ~(WIP)~]] :: -- [[/posts/meta/Theme][Theming and Templating ~(WIP)~]] :: +- [[./Soupault.org][Soupault Configuration ~(WIP)~]] :: -- [[/posts/meta/Soupault/][Soupault Configuration ~(WIP)~]] :: +- [[./Theme.org][Theming and Templating ~(WIP)~]] :: #+BEGIN_EXPORT html </article> |