What happened since December 2022?

Initially, I started this “What happened” series as an exercise to publish more regularly on this website. Suffice to say, I haven’t done a particularly impressive job in that regard, which only means I have a lot of room for improvement.

Anyway, if the first few months of 2023 has been mostly $WORK focus, the same cannot be said for April and May. For one, I have started running again. But this is only the tip of the iceberg.

Spatial Shell got its first releases

Spatial Shell  is probably my hobby project I am most excited about. The “call for testers” article I have published recently managed to catch the attention of a few folksYou want to hear a lesson I learned the hard way just after publishing it? Before calling for testers, it is better to be sure your project can actually be compiled easily by the potential volunteers . . The perspective to publish such a write-up was a very strong source of motivation for me to clean up a project I was using daily for several months now, and I am very satisfied with the result.

Mass adoption is still a distant horizon, but still, the project is now mainstream enough that it has already been mentioned in a random topic on the OCaml discourse by someone who isn’t me . 🎉

This led me to formally release a first version of Spatial Shell in the end of April, and a second today. For the first time, I have also published an Archlinux package , to make the life of potential early adopters even easier. Do not hesitate to upvote it so that it can find its way to the extra repository some day.

Goodbye Emacs! Remember me, Neovim?

In 2015, I started using Coq for my PhD thesis and at the time, there was no real support for (Neo)vimThe situation later improved. Nowadays, you can implement your theories using Coqtail , and Coq LSP  will probably become a viable and interesting setup in a near future. . Everyone was using Proof General  and Emacs, so I was left with little choice but to follow through. With only my courage and the good advice of a fellow “vimer” who had also made a similar journey , I started using Emacs.

Fast forward 8 years later, and my Emacs configuration  has become a project of its own. Overall, I was pretty happy with my setup, but in the same time, I always remained a bit nostalgic of my Neovim days. This is probably why I decided to give this old friend a try when my company bought me a new laptop. I also used this as an opportunity to try out this LSP-thing everyone was talking about.

It has been a month now, and I do not plan to come back to my previous habits. There are still some few edges here and there, I still need to get my head around lua, but LSP is nice, and plugins like telescope  are simply too beautiful.

That being said, there was one aspect of moving from Emacs to Neovim I had not anticipated: Org mode. Which constitutes a perfect transition to the next session.

Website redesign, again

Did you notice this website has been revamping recently? The changes are actually deeper than “just” a redesign, to a point where I had to port all my write-ups to a different markup languageAre you starting to understand why “Org mode” was the perfect transition to move on to this section? .

Why, you ask? Well, it’s actually pretty simple: as time goes, I’ve grown lazier.

Let me give you some context. Until very recently, my website was built around the idea to have literate programming as a first-class citizen of my author tools. For instance, you can have a look at what used to be the literate program which was responsible for generating the website. Similarly, most of my write-ups about Coq were actually Coq documents. Literate programming is actually a very nice paradigm for authoring technical contents, because it gives you the tools to keep said contents accurate and up-to-date. In a nutshell, you cannot have a typo in one of your code snippets which would prevent it from compiling, because you actually compile the snippet and catch the typo when you try to generate your website. Or at least, it is what I used to do.

I decided to stop because, for all its benefits, this approach has one major drawback: it is hard to maintain. I had invested quite some time and efforts to keep my website sources under control, but it really was an everyday fight. There are some strange things which start happening when you fully commit to this, as I think I did. For instance, software dependencies tie your article together. Suddenly, you cannot talk about this new fancy feature of the latest Coq release without upgrading all your write-ups implemented as Coq documentsWell, in theory you can. Just have each Coq document specifies the Coq version it requires, and support this level of customization in your build toolchain. But then, your blog takes forever to build from a cold repository. .

That being said, most of the work had already been done. This website was a collection of literate programs, and I was pretty proud of the state of things. I could deal with the annoyancesLike using Coqdoc syntax to write my articles, for instance. I could write about how the Coqdoc syntax irks me for ages. . But then, as I explained in the previous section, I decided to move away from Emacs. The first time I tried to start a new write-up, it hit me.

I used to write most of my contents using Org mode. Org mode, also known as the Emacs markup language.

I know of at least one “Org plugin” for Neovim , but instead of giving it a try, I decided to use this opportunity to tackle my “maintenance problem” once and for all. I gave up on literate programming for this website. As a result, this website is now generated from Markdown files only (using markdown-it  with many plugins). As a consequence, the generated HTML is way more “predictable.” This was enough to motivate me at giving a try at Soupault’s indexes , which are way more powerful than I anticipated. Now, this website has

• Tags. Each write-up can be labeled with as many tags as I want, there is a page which lists all the tags used in the website, and each tag has its own page (for instance, the coq tag.
• A RSS feed. It was actually one of the main features I really wanted to get with this revamp.
• Automatically generated list of articles in the home page, for each series (see the Ltac series for instance). Before, I was publishing “curated indexes,” or put in other words: I was writing these indexes myself, by hand. And again, I’ve grown lazier.

It took me a week to go through this rework. Translating manually every write-up was tedious, to say the least, as was implementing the Lua plugins for Soupault since I have neither proficiency nor tooling to help me write Lua code. But I am very glad for the final result.

Also, I have invested in an Antidote license, so hopefully, this website will have fewer typos and English butchering as of now. A clean text, delivered with a nice and simple design, from a sane and maintainable Git repository .