summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorThomas Letan <lthms@soap.coffee>2020-03-20 21:31:21 +0100
committerThomas Letan <lthms@soap.coffee>2020-03-20 21:31:21 +0100
commitb4a2c6e9cdda16c8bf4a154d0c90508538c33830 (patch)
tree602290871c2f5eb29bd4713bb745e564d8396c31
parent70731164b51f44b57044f01d111b1a7bd30298f9 (diff)
Remove the “About” page and use the “Write-up” page as default index
-rw-r--r--.gitignore2
-rw-r--r--site/cleopatra/Theme.org3
-rw-r--r--site/index.html72
-rw-r--r--site/index.org (renamed from site/posts/index.org)20
4 files changed, 12 insertions, 85 deletions
diff --git a/.gitignore b/.gitignore
index 985d6e8..72e0f9f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -16,6 +16,7 @@ site/posts/ClightIntroduction.html
site/posts/StronglySpecifiedFunctions.html
site/posts/RewritingInCoq.html
site/posts/Ltac101.html
+site/index.html
site/news/ColorlessThemes-0.2.html
site/cleopatra/Contents.html
site/cleopatra/index.html
@@ -25,7 +26,6 @@ site/cleopatra/Soupault.html
site/cleopatra/Contents/Org.html
site/cleopatra/Contents/Coq.html
site/posts/Thanks.html
-site/posts/index.html
site/posts/DiscoveringCommonLisp.html
site/posts/ExtensibleTypeSafeErrorHandling.html
site/posts/MonadTransformers.html
diff --git a/site/cleopatra/Theme.org b/site/cleopatra/Theme.org
index 47bef25..41faa8b 100644
--- a/site/cleopatra/Theme.org
+++ b/site/cleopatra/Theme.org
@@ -89,8 +89,7 @@ noscript.parentNode.removeChild(noscript);
<nav>
<ul>
<li> <a href="/news">News</a></li>
- <li> <a href="/posts">Write-ups</a></li>
- <li> <a href="/">About</a></li>
+ <li> <a href="/">Write-ups</a></li>
</ul>
</nav>
<header>
diff --git a/site/index.html b/site/index.html
deleted file mode 100644
index deddc99..0000000
--- a/site/index.html
+++ /dev/null
@@ -1,72 +0,0 @@
-<!doctype html>
-<html lang="en">
- <head>
- <meta charset="utf-8">
- <meta name="viewport" content="width=device-width, initial-scale=1.0">
- <link rel="icon" type="image/ico" href="/img/merida.webp">
- <link rel="stylesheet" href="/style/main.css">
- <noscript id="lazyloading">
- <link rel="stylesheet" href="https://soap.coffee/+vendors/fira-code.2+swap/font.css">
- <link rel="stylesheet" href="https://soap.coffee/+vendors/et-book+swap/font.css">
- <link rel="stylesheet" href="https://soap.coffee/+vendors/fork-awesome.1.1.7+swap/css/fork-awesome.min.css">
- </noscript>
- <title></title>
- </head>
- <body id="vcard">
- <article>
- <img src="/img/merida.webp"
- alt="Merida in the movie Ralph 2.0" />
- <p>
- Hi, awesome stranger.
- </p>
-
- <p>
- I am <strong>lthms</strong>, and I welcome you in my little corner of
- the Internet.
- </p>
-
- <nav>
- <dl>
- <dt><a href="/posts/">my write-ups</a></dt>
- <dd>
- You may find interesting my articles if you are into functional
- programming languages.
- </dd>
- </dl>
- <dl>
- <dt><a href="https://code.soap.coffee"><i class="fa fa-code" aria-hidden="true"></i> code.soap.coffee</a></dt>
- <dd>
- A collection of personal git repositories, including a set of
- dotfiles (emacs, sway…), a set of tools for story writers.
- </dd>
- </dl>
- <dl>
- <dt><a rel="me" href="https://mastodon.social/@lthms"><i class="fa fa-mastodon" aria-hidden="true"></i> @lthms@mastodon.social</a></dt>
- <dd>
- My personal account on the fediverse. I mostly toot about functional
- programming languages, formal methods, and my Emacs configuration.
- </dd>
- </dl>
- <dl>
- <dt><a href="https://dblp.org/pers/hd/l/Letan:Thomas">my academic publications</a></dt>
- <dd>
- I have a PhD in computer science, and I focus my research on
- applying formal methods approaches to prove security properties.
- </dd>
- </dl>
- </nav>
-
- <p>
- I wish you a wonderful day.
- </p>
- </article>
- <script>
- let noscript = document.getElementById('lazyloading');
- let resources = noscript.innerText.split('\n');
-
- for (var ix in resources) {
- noscript.insertAdjacentHTML('beforebegin', resources[ix]);
- }
- </script>
- </body>
-</html>
diff --git a/site/posts/index.org b/site/index.org
index 6b2e304..2a5e085 100644
--- a/site/posts/index.org
+++ b/site/index.org
@@ -19,20 +19,20 @@ 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.
-- [[./ClightIntroduction.html][A Study of Clight and its Semantics]] ::
+- [[./posts/ClightIntroduction.html][A Study of Clight and its Semantics]] ::
Clight is a “simplified” C AST used by CompCert, the certified C compiler. In
this write-up, we prove a straighforward functional property of a small C
function, as an exercise to discover the Clight semantics.
-- [[./MiniHTTPServer.html][Implementing and Certifying a Web Server in Coq]] ::
+- [[./posts/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.
-- [[./Ltac101.html][Ltac 101]] ::
+- [[./posts/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.
-- [[./RewritingInCoq.html][Rewriting in Coq]] ::
+- [[./posts/RewritingInCoq.html][Rewriting in Coq]] ::
The ~rewrite~ tactics are really useful, since they are not limited to the Coq
built-in equality relation.
@@ -41,20 +41,20 @@ machine-checked proofs.
satisfy, such that using such a function requires providing a proof the
property is satisfied.
- 1. [[./StronglySpecifiedFunctions.html][Using the ~refine~ Tactics]]
- 2. [[./StronglySpecifiedFunctionsProgram.html][Using the ~Program~ Framework]]
+ 1. [[./posts/StronglySpecifiedFunctions.html][Using the ~refine~ Tactics]]
+ 2. [[./posts/StronglySpecifiedFunctionsProgram.html][Using the ~Program~ Framework]]
* About Haskell
Haskell is a pure, lazy, functional programming language with a very expressive
type system.
-- [[./ExtensibleTypeSafeErrorHandling.html][Extensible, Type-Safe Error Handling In Haskell]] ::
+- [[./posts/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.
-- [[./MonadTransformers.org][Monad Transformers are a Great Abstraction]] ::
+- [[./posts/MonadTransformers.org][Monad Transformers are a Great Abstraction]] ::
Monads are hard to get right, monad transformers are harder. Yet, they remain
a very powerful abstraction.
@@ -62,7 +62,7 @@ type system.
Common Lisp is a venerable programming languages like no other I know.
-- [[./DiscoveringCommonLisp.html][Discovering Common Lisp with ~trivial-gamekit~]] ::
+- [[./posts/DiscoveringCommonLisp.html][Discovering Common Lisp with ~trivial-gamekit~]] ::
From the creation of a Lisp package up to the creation of a standalone
executable.
@@ -83,7 +83,7 @@ process.
4. [[/cleopatra/Contents/Coq.org][Generating Contents from Coq Documents ~(TODO)~]]
5. [[/cleopatra/Theme.html][Theming and Templating ~(TODO)~]]
-- [[./Thanks.html][Thanks!]] ::
+- [[./posts/Thanks.html][Thanks!]] ::
If it were not for many awesome FOSS projects, this corner of the Internet
would not exist. This is my attempt to give well-deserved credit to them and
their creators.