A recollection of challenging myself to implement a simple tool to generate a summary from YouTube videos using Vosk for speech recognition and Ollama for generating summaries using LLMs running locally.| Thomas Letan’s website
<h1>Peer-Programming in Modern OCaml with ChatGPT and Gemini</h1><div><span class="icon"><svg><use href="/~lthms/img/icons.svg#tag"></use></svg></span> <a href="https://soap.coffee/~lthms/tags/ocaml.html" marked="" class="tag">ocaml</a> <span class="icon"><svg><use href="/~lthms/img/icons.svg#tag"></use></svg></span> <a href="https://soap.coffee/~lthms/tags/vibecoding.html" marked="" class="tag">vibecoding</a> </div>| The OCaml Planet
What Happened in 2024? meta opinions We are done with 2024, and now is a good time to reflect on what has happened over the past 12 months. I was not planning to, but my feed convinced me to give it a try . Plus, it is a good opportunity to revive my “Retrospective” series. Free and Open Source Software I’ve been a “prolific contributor” at $WORK, but less so with my personal projects. Spatial Shell remains my most “popular” projectWe should reach 100 stars on GitHub in 20...| Thomas Letan’s Blog
Serving This Article from RAM for Fun and No Real Benefit ocaml meta In 2022, Xe Iaso published a transcript of their talk on how their website was working at the time . In a nutshell, their approach consisted of a server preprocessing the website from its source at startup, then serving its contents from memory. If you have not already, I can only encourage you to read the article or watch the talk, as the story they tell is very interesting. For me personally, it sparked a question: wha...| Thomas Letan’s Blog
bepo-tsrn.nvim is a zero-configuration, global plugin for Neovim which remaps default Neovim bindings for the Bépo keyboard layout in an opinionated way.| Thomas Letan’s website
I describe how I have set up the host (an Arch Linux system on a LUKS-encrypted partition) of jasmine, my new VPS.| Thomas Letan’s website
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.| Thomas Letan’s website
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.| Thomas Letan’s website
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.| Thomas Letan’s website
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.| Thomas Letan’s website
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.”| Thomas Letan’s website
“Regularity is key.” But sometimes, it is a bit hard to get right. Anyway, let’s catch up.| Thomas Letan’s website
Can we all agree that witnessing syntax highlighting being absolutely off is probably the most annoying thing that can happen to anybody?| Thomas Letan’s website
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.| Thomas Letan’s website
Could patch dependencies could help reduce the friction my branchless workflow suffers from when it comes to stacked MRs?| Thomas Letan’s website
One year has passed, and I keep using Stacked Git almost daily. How I am using it has slightly changed, though.| Thomas Letan’s website
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.| Thomas Letan’s website
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.| Thomas Letan’s 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.| Thomas Letan’s website
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.| Thomas Letan’s website
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.| Thomas Letan’s website
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.| Thomas Letan’s website
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.| Thomas Letan’s website
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.| Thomas Letan’s website
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.| Thomas Letan’s website
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.| Thomas Letan’s website
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.| Thomas Letan’s website
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.| Thomas Letan’s website
Introducing a new macro, more friendly with themes gallery like Peach Melpa.| Thomas Letan’s 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.| Thomas Letan’s website
It has been a long journey —4 years, 10 days— but I have completed my PhD on October 25, 2018.| Thomas Letan’s website
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.| Thomas Letan’s website
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.| Thomas Letan’s website
Monads are hard to get right, monad transformers are harder. Yet, they remain a very powerful abstraction.| Thomas Letan’s website
The rewrite tactics are really useful, since they are not limited to the Coq built-in equality relation.| Thomas Letan’s website
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.| Thomas Letan’s website
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.| Thomas Letan’s website
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.| Thomas Letan’s website