- The Free and Open Source Software Projects This Website is Built Upon in June 2023 (
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.
Extensible Records in OCaml Using
We show how it is possible to use
dmapto implement extensible records (that is, records which can be extended with new fields after they have been defined) in OCaml.
- ★ The Chaotic Debut of My Software Projects (
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.”
- What happened since December 2022? (
“Regularity is key.” But sometimes, it is a bit hard to get right. Anyway, let’s catch up.
- Neovim, OCaml Interfaces, Tree-Sitter and LSP (
Can we all agree that witnessing syntax highlighting being absolutely off is probably the most annoying thing that can happen to anybody?
- Spatial Shell: Call For Testers (
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.
- Patch Dependencies for Stacked Git (
Could patch dependencies could help reduce the friction my branchless workflow suffers from when it comes to stacked MRs?
How I Keep Using Stacked Git at
One year has passed, and I keep using Stacked Git almost daily. How I am using it has slightly changed, though.
- What happened in October and November 2022? (
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
- What happened in September 2022? (
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.
- What happened in August 2022? (
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.
- Writing a Function Whose Argument is a Polymorphic Function in OCaml (
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.
How I Use Stacked Git at
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.
Implementing an Echo Server in Coq with
In this article, we will demonstrate how
coqffican be used to implement an echo server, i.e., a TCP server which sends back any input it receives from its clients.
coqffi.1.0.0In A Nutshell (
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.
- Pattern Matching on Types and Contexts (
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 xwill refine the current goal using an inductive principle dedicated to the type of
- Ltac is an Imperative Metaprogramming Language (
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.
- Mixing Ltac and Gallina for Fun and Profit (
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.
- Proving Algebraic Datatypes are “Algebraic” (
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
prodCoq types satisfy these properties.
- 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.
Introducing a new macro, more friendly with themes gallery like Peach Melpa.
- A Literate Toolchain To Build This Website (
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.
- ★ I am no longer a PhD. student (
It has been a long journey —4 years, 10 days— but I have completed my PhD on October 25, 2018.
Discovering Common Lisp with
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.
- 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.
- Monad Transformers are a Great Abstraction (
Monads are hard to get right, monad transformers are harder. Yet, they remain a very powerful abstraction.
- Rewriting in Coq (
rewritetactics are really useful, since they are not limited to the Coq built-in equality relation.
Implementing Strongly-Specified Functions with the
Programis the heir of the
refinetactic. It gives you a convenient way to embed proofs within functional programs that are supposed to fade away during code extraction.
Implementing Strongly-Specified Functions with the
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.