Archives

I describe how I have set up the host (an Arch Linux system on a LUKS-encrypted partition) of jasmine, my new VPS.

git maintenance allows to run on the background a set of tasks which optimize commands like git add and git fetch for a responsive user experience. Out of the box, the scripts run by git mainentance have no way to use encrypted SSH keys, but it is possible to fix this.

Building static binaries can come in handy. Most notably, when the time comes to distribute executables. Fortunately, building static binaries from OCaml projects can be achieved pretty easily, when you know what you are doing.

After a first call for testers that could have been more effective if only the building instructions listed in the README were correct, I am quite happy to announce the 6th release for Spatial Shell that, I believe, is pretty usable for someone who isn’t me.

In the past, I had a page called “Thanks!” dedicated to listing the free and open source software projects I was relying on to create this website. I do want to approach this exercise differently this time: instead of keeping one page up to date with the latest software stack I am using, I will publish a new article every now and then. This article is the first of this series.

We show how it is possible to use dmap to implement extensible records (that is, records which can be extended with new fields after they have been defined) in OCaml.

I am no stranger to the exciting feeling of starting new projects. By dint of repeating this “exercise” over the years, I have come to build an intuitive process which “works for me.”

“Regularity is key.” But sometimes, it is a bit hard to get right. Anyway, let’s catch up.

Can we all agree that witnessing syntax highlighting being absolutely off is probably the most annoying thing that can happen to anybody?

In August, 2022, I have discovered Material Shell, and decided to implement a dynamic tiling management “a la Material Shell” for sway I called Spatial Shell. Spatial Shell works on my machine, which means it will definitely break on yours, and I would love to know how.

Could patch dependencies could help reduce the friction my branchless workflow suffers from when it comes to stacked MRs?

One year has passed, and I keep using Stacked Git almost daily. How I am using it has slightly changed, though.

Spatial Sway has basically reached the MVP stage, I failed to fully commit to this year’s NaNoWriMo, and someone has worked on adding some support for coqffi to dune.

In a nutshell, my latest hobby project (Spatial Sway) works well enough so that I can use it daily, and I have done some unsuccessful experiments for this website.

In an attempt to start a regular blogging habbits, I am giving a try to the monthly “status updates” format. This month: some Emacs config hacking, and some changes on how this website is generated.

In OCaml, it is not possible to write a function whose argument is a polymorphic function. Trying to write such a function results in the type-checker complaining back at you. The trick to be able to write such a function is to use records.

I’ve been using Stacked Git at work since early 2021, and as of January 2022, it has become a cornerstone of my daily workflow.

In this article, we will demonstrate how coqffi can be used to implement an echo server, i.e., a TCP server which sends back any input it receives from its clients.

For each entry of a cmi file, coqffi tries to generate an equivalent (from the extraction mechanism perspective) Coq definition. In this article, we walk through how coqffi works.

Ltac allows for pattern matching on types and contexts. In this article, we give a short introduction on this feature of key importance. Ltac programs (“proof scripts”) generate terms, and the shape of said terms can be very different regarding the initial context. For instance, induction x will refine the current goal using an inductive principle dedicated to the type of x.

Ltac generates terms, therefore it is a metaprogramming language. It does it incrementally, by using primitives to modifying an implicit state, therefore it is an imperative language. Henceforth, it is an imperative metaprogramming language.

One of the most misleading introduction to Coq is to say that “Gallina is for programs, while tactics are for proofs.” Gallina is the preferred way to construct programs, and tactics are the preferred way to construct proofs. The key word here is “preferred.” Coq actually allows for mixing Ltac and Gallina together.

The set of types which can be defined in a language together with $+$ and $*$ form an “algebraic structure” in the mathematical sense, hence the name. It means the definitions of $+$ and $*$ have to satisfy properties such as commutativity or the existence of neutral elements. In this article, we prove the sum and prod Coq types satisfy these properties.

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.

Introducing a new macro, more friendly with themes gallery like Peach Melpa.

Our literate programming toolchain cannot live solely inside Org files, waiting to be turned into actual code by Babel. Otherwise there we would not have any code to execute the first time we try to generate the website.

It has been a long journey —4 years, 10 days— but I have completed my PhD on October 25, 2018.

Common Lisp is a venerable programming languages like no other I know. From the creation of a Lisp package up to the creation of a standalone executable, we explore the shore of this strange beast.

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.

Monads are hard to get right, monad transformers are harder. Yet, they remain a very powerful abstraction.

The rewrite tactics are really useful, since they are not limited to the Coq built-in equality relation.

Program is the heir of the refine tactic. It gives you a convenient way to embed proofs within functional programs that are supposed to fade away during code extraction.

We see how to implement strongly-specified list manipulation functions in Coq. Strong specifications are used to ensure some properties on functions' arguments and return value. It makes Coq type system very expressive.