diff options
| -rw-r--r-- | .gitignore | 7 | ||||
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | plugins/site-prefix.lua | 4 | ||||
| -rw-r--r-- | site/index.html | 2 | ||||
| -rw-r--r-- | site/posts.org | 66 | ||||
| -rw-r--r-- | site/posts/index.html | 22 | ||||
| -rw-r--r-- | site/style/main.css | 17 |
7 files changed, 94 insertions, 28 deletions
@@ -8,12 +8,13 @@ build/ *.html~ # begin generated files +site/posts.html +site/posts/DiscoveringCommonLisp.html site/posts/ExtensibleTypeSafeErrorHandling.html site/posts/MonadTransformers.html -site/posts/DiscoveringCommonLisp.html -site/posts/Ltac101.html -site/posts/RewritingInCoq.html site/posts/StronglySpecifiedFunctionsProgram.html site/posts/MiniHTTPServer.html site/posts/StronglySpecifiedFunctions.html +site/posts/RewritingInCoq.html +site/posts/Ltac101.html # begin generated files @@ -1,5 +1,5 @@ -ORG_POSTS := $(wildcard site/posts/*.org) -COQ_POSTS := $(wildcard site/posts/*.v) +ORG_POSTS := $(shell find site/ -name "*.org") +COQ_POSTS := $(shell find site/ -name "*.v") POSTS := $(ORG_POSTS:.org=.html) $(COQ_POSTS:.v=.html) COQCARGS := -async-proofs-cache force diff --git a/plugins/site-prefix.lua b/plugins/site-prefix.lua index e64f839..6c7f12a 100644 --- a/plugins/site-prefix.lua +++ b/plugins/site-prefix.lua @@ -15,7 +15,11 @@ index, link = next(links) while index do href = HTML.get_attribute(link, "href") + if href then + -- remove prefix sometimes introduced by org + href = Regex.replace(href, "^file://", "") + -- Check if URL starts with a leading "/" if Regex.match(href, "^/") then -- Remove leading slashes diff --git a/site/index.html b/site/index.html index 0fa4132..7d08c4a 100644 --- a/site/index.html +++ b/site/index.html @@ -24,7 +24,7 @@ <nav> <dl> - <dt><a href="/posts/">my blog</a></dt> + <dt><a href="/posts/">my write-ups</a></dt> <dd> You may find interesting my articles if you are into functional programming languages. diff --git a/site/posts.org b/site/posts.org new file mode 100644 index 0000000..b2096e0 --- /dev/null +++ b/site/posts.org @@ -0,0 +1,66 @@ +#+OPTIONS: toc:nil num:nil + +#+BEGIN_EXPORT html +<h1>Write-ups</h1> + +<article class="index"> +#+END_EXPORT + +Over the past years, I have tried to capitalize on my findings. What I have +lacked in regularity I made up for in subject exoticism. + +If you like what you read, have a question or for any other reasons really, you +can shoot to [[mailto:~lthms/lthms.xyz@lists.sr.ht][the dedicated mailing list]] (see the [[https://lists.sr.ht/~lthms/lthms.xyz/%3C20190127111504.n27ttkvtl7l3lzwb%40ideepad.localdomain%3E][annoucement]] for a guide on how +to subscribe). + +* About Coq + +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]] :: + An explanation on how to write an almost pure Coq, and working (albeit + minimal) HTTP server. + +- [[/posts/Ltac101/][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]] :: + The ~rewrite~ tactics are really useful, since they are not limited to the Coq + built-in equality relation. + +- A Series on Specifying Strongly-Specified Funcions in Coq :: + Coq ~Prop~ sort allows for defining properties function arguments have to + 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]] + +* 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]] :: + 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. + +- [[/posts/MonadTransformers/][Monad Transformers are a Great Abstraction]] :: + Monads are hard to get right, monad transformers are harder. Yet, they remain + a very powerful abstraction. + +* About Common Lisp + +Common Lisp is a venerable programming languages like no other I know. + +- [[/posts/DiscoveringCommonLisp/][Discovering Common Lisp with ~trivial-gamekit~]] :: + From the creation of a Lisp package up to the creation of a standalone + executable. + +#+BEGIN_EXPORT html +</article> +#+END_Export diff --git a/site/posts/index.html b/site/posts/index.html deleted file mode 100644 index 7643b21..0000000 --- a/site/posts/index.html +++ /dev/null @@ -1,22 +0,0 @@ -<div> - <h1>Blog</h1> - - <p>Hi.</p> - - <p> - For several years now, I have been trying to publish interesting content. My - articles are mostly about functional programming languages such as Coq or - Haskell. - </p> - - <ul id="index"> - </ul> - - <p> - If you like what you read, have a question or for any other reasons really, - you can shoot to <a href="mailto:~lthms/lthms.xyz@lists.sr.ht">this blog - mailing list</a> (see - the <a href="https://lists.sr.ht/~lthms/lthms.xyz/%3C20190127111504.n27ttkvtl7l3lzwb%40ideepad.localdomain%3E">annoucement</a> - for a guide on how to subscribe). - </p> -</div> diff --git a/site/style/main.css b/site/style/main.css index e58b933..8a9c589 100644 --- a/site/style/main.css +++ b/site/style/main.css @@ -49,6 +49,7 @@ body#default nav li { text-transform: uppercase; font-family: sans-serif; font-size: 130%; + font-weight: bold; } body#default nav li a { @@ -158,3 +159,19 @@ body#vcard nav dd { body#vcard nav dt a { color: #68d3a7; } + +/* indexes */ + +.index dt { + font-weight: bold; + color: #68d3a7; +} + +.index dd { + margin-left: 0; + margin-bottom: 1em; +} + +.index dd ol { + margin-top: 0.3em; +} |