Tiago Cogumbreiro
@forkjoin.bsky.social
Associate professor @ UMass Boston | https://cogumbreiro.github.io/ | Faial is a verifier for #CUDA and #WebGPU written in #OCaml https://gitlab.com/umb-svl/faial #ocaml #rocq
Oh, thanks for letting me know. It should be fixed now.
November 28, 2025 at 9:05 PM
Oh, thanks for letting me know. It should be fixed now.
Dream, ppx_blob, mustache were a pleasure to use. Of course, always a major fan of cmdliner (using the new, lovely API).
The old server was powered by nodejs. Dream boots much faster. I am also more familiar with the OCaml ecosystem, so no more wondering how to install/update my slides server.
The old server was powered by nodejs. Dream boots much faster. I am also more familiar with the OCaml ecosystem, so no more wondering how to install/update my slides server.
November 28, 2025 at 7:42 PM
Dream, ppx_blob, mustache were a pleasure to use. Of course, always a major fan of cmdliner (using the new, lovely API).
The old server was powered by nodejs. Dream boots much faster. I am also more familiar with the OCaml ecosystem, so no more wondering how to install/update my slides server.
The old server was powered by nodejs. Dream boots much faster. I am also more familiar with the OCaml ecosystem, so no more wondering how to install/update my slides server.
For instance, I noticed that the results I ask my students to prove are much simpler at the end of the course than at the beginning, so teaching in reverse would simplify what needs to be taught in terms of proof theory.
November 25, 2025 at 8:17 PM
For instance, I noticed that the results I ask my students to prove are much simpler at the end of the course than at the beginning, so teaching in reverse would simplify what needs to be taught in terms of proof theory.
I love that. It's something I've been meaning to do in a while, but b/c I followed Sipser I started from the usual way, and I haven't had the energy to do rethink the presentation. But good to know all of these great resources. Thanks for sharing these links!
November 25, 2025 at 8:13 PM
I love that. It's something I've been meaning to do in a while, but b/c I followed Sipser I started from the usual way, and I haven't had the energy to do rethink the presentation. But good to know all of these great resources. Thanks for sharing these links!
Haha I need to try that out. I've seen so many cool examples of DSLs in Lean
November 18, 2025 at 7:48 PM
Haha I need to try that out. I've seen so many cool examples of DSLs in Lean
The tool is all implemented in OCaml. The monadic-design pattern of parsing JSON comes from what I learned in Faial <https://gitlab.com/umb-svl/faial/> and I think it looks neat.
October 25, 2025 at 6:28 PM
The tool is all implemented in OCaml. The monadic-design pattern of parsing JSON comes from what I learned in Faial <https://gitlab.com/umb-svl/faial/> and I think it looks neat.
The output is Markdown-formatted and the tool can figure out your Rocq project. I've been using this to help Claude Code help me, with some success. I have some scratch files in the project, including playing around with Fleche, but I haven't figured that code base yet.
October 25, 2025 at 6:24 PM
The output is Markdown-formatted and the tool can figure out your Rocq project. I've been using this to help Claude Code help me, with some success. I have some scratch files in the project, including playing around with Fleche, but I haven't figured that code base yet.
Reposted by Tiago Cogumbreiro
decoders library is quite elegant, esp if your format is absolutely disgusting
(source used it to parse the activitypub spec, the most underspecified and broken format known to humankind)
github.com/kiranandcode...
(source used it to parse the activitypub spec, the most underspecified and broken format known to humankind)
github.com/kiranandcode...
ocamlot/lib/activitypub/decode.ml at d677ae6b208074660811dc9120e6b90353e7f338 · kiranandcode/ocamlot
An Activitypub server in OCaml! Contribute to kiranandcode/ocamlot development by creating an account on GitHub.
github.com
July 17, 2025 at 6:31 PM
decoders library is quite elegant, esp if your format is absolutely disgusting
(source used it to parse the activitypub spec, the most underspecified and broken format known to humankind)
github.com/kiranandcode...
(source used it to parse the activitypub spec, the most underspecified and broken format known to humankind)
github.com/kiranandcode...
Progress here: github.com/ocaml/dune/i...
Dune Developer Preview (Sept-28-2024) fails to build z3 · Issue #10970 · ocaml/dune
Expected Behavior I would like to migrate my project to Dune developer preview. Actual Behavior dune build is unable to compile the package z3. See point 4 below for output. Reproduction 1. Create ...
github.com
July 14, 2025 at 8:28 PM
Progress here: github.com/ocaml/dune/i...
Turns out, I forgot to run `dune pkg lock` and z3 doesn't work with Dune Preview 😭
I managed to advance a bit further by changing Z3's lock file, but since I have no idea of what I'm doing, z3 then failed in the linking stage.
I managed to advance a bit further by changing Z3's lock file, but since I have no idea of what I'm doing, z3 then failed in the linking stage.
July 14, 2025 at 8:28 PM
Turns out, I forgot to run `dune pkg lock` and z3 doesn't work with Dune Preview 😭
I managed to advance a bit further by changing Z3's lock file, but since I have no idea of what I'm doing, z3 then failed in the linking stage.
I managed to advance a bit further by changing Z3's lock file, but since I have no idea of what I'm doing, z3 then failed in the linking stage.
Having Claude keep tabs of what was done and then generate the migration notes was invaluable. I would've forgotten all the steps otherwise. Humans and tools can use the guide and I already used it to have Claude migrate another project without further input.
June 29, 2025 at 3:19 PM
Having Claude keep tabs of what was done and then generate the migration notes was invaluable. I would've forgotten all the steps otherwise. Humans and tools can use the guide and I already used it to have Claude migrate another project without further input.