Tiago Cogumbreiro

no-more-cover-pages interface, showing thumbnails of annoying cover pages that no-more-cover-pages will helpfully remove for you

I don't like cover pages on my PDFs so I made a li'l program to strip them from PDFs in my Zotero library

uvx no-more-cover-pages

github.com/joshuahhh/no-more-cover-pages/

Introducing SlopOS: a new vibe-coded, operating system for safety-critical applications. SlopOS leapfrogs existing OS designs with first-class support for a new memory managed, object-capability based programming language for the userland and core kernel routines. (1/3)

At Harmonic we've just announced $1,000,000 of sponsorship for Principal Investigators and Rising Mathematicians. Significant O($100K) funding for high-impact projects. Early access to next-generation Aristotle models. Please apply! aristotle.harmonic.fun/sponsorships

Haiku also works pretty well with OCaml

Screenshot of git history showing 14 commits.

I think my macos build of faial seems to be working again.

I would be very appreciated if you have an Apple laptop (m1 or newer) and you can the give binary dist of faial a go, you'll be able to find the link on top of the readme:

gitlab.com/umb-svl/faial

Yeah I am trying to revive my macos runner. I was struggling to get the cache working and it was kind of flaky (from what I remember). But I'll definitely have a peek at your CI script.

I'm doing my bi-annual tradition of trying to build Faial for windows/macos with a CI script and failing miserably. It's been +5 years 🥳

.@julien-lange.bsky.social and I are looking for a PostDoc to work on our EPSRC Project "INDIMO: Invariant Discovery and Monitoring for Message-Passing Programs".

If you know someone, or are interested, please reach out!

A few details here: jobs.royalholloway.ac.uk/Vacancy.aspx...

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.

Sign in · GitLab GitLab.com

I've been using gnab/remark's slides for almost 10 years now. I was using sinedied/backslide as a launcher for a while, but finally decided to write my own in OCaml with Dream as I had heard about it.
Presenting Shearwater, a remark server that should work out of the box:
gitlab.com/cogumbreiro/...

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!

susam.net/fizz-buzz-wi...

This was a lot of fun, via lobste.rs

A comment also mentioned this fascinating video youtu.be/j5s0h42GfvM?...

Haha I need to try that out. I've seen so many cool examples of DSLs in Lean

I think I get Ltac2. It's refreshing to write tactics that have typing information. It really cleans up detailed proof manipulation.

I have big dreams for Claude Code automating Rocq proofs, but it keeps responding in Lean tactics 😞 Is Lean the TypeScript of LLMs?

A new book on the history of control structures by the creator of #OCaml himself @camlist.bsky.social xavierleroy.org/control-stru...

A screenshot of OCaml code showing some JSON deserialization code.

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.

A screenshot of `proof-ls` in action, showing a proof state.

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.

Tiago Cogumbreiro / Proof Archivist · GitLab GitLab.com

I am publishing an itch I've add in the last few days
gitlab.com/cogumbreiro/...

This is a simple CLI tool for Rocq that shows the proof state/typing info of a source code location, via rocq-lsp. I'm trying to learn the code base of rocq-lsp, but it's a large project.

Interactive Theorem Provers for Proof Education | Proceedings of the 2025 ACM SIGPLAN International Symposium on SPLASH-E

Interactive theorem provers for proof education. ~ Romina Mahinpei, Manoel Horta Ribeiro, Mae Milano. dl.acm.org/doi/abs/10.1... #ITP #CoqProver #Teaching

Static linking in OCaml Most of the time, you don’t think about how your file is linked. We’ve come to love dynamically linked files with their small file sizes and reduced memory requirements, but there are times when the convenience of a single binary download from a GitHub release page is really what you need. To do this in OCaml, we need to add -ccopt -static to the ocamlopt. I’m building with dune, so I can configure that in my dune file using a flags directive. (flags (:standard -ccopt -static)) This can be extended for maximum compatibility by additionally adding -ccopt -march=x86-64, which ensures the generated code will run on any x86_64 processor and will not use newer instruction set extensions like SSE3, AVX, etc. So what about Windows? The Mingw tool chain accepts -static. Including (flags (:standard -ccopt "-link -Wl,-static -v")) got my options applied to my dune build: x86_64-w64-mingw32-gcc -mconsole -L. -I"C:/Users/Administrator/my-app/_opam/lib/ocaml" -I"C:\Users\Administrator\my-app\_opam\lib\mccs" -I"C:\Users\Administrator\my-app\_opam\lib\mccs\glpk/internal" -I"C:\Users\Administrator\my-app\_opam\lib\opam-core" -I"C:\Users\Administrator\my-app\_opam\lib\sha" -I"C:/Users/Administrator/my-app/_opam/lib/ocaml\flexdll" -L"C:/Users/Administrator/my-app/_opam/lib/ocaml" -L"C:\Users\Administrator\my-app\_opam\lib\mccs" -L"C:\Users\Administrator\my-app\_opam\lib\mccs\glpk/internal" -L"C:\Users\Administrator\my-app\_opam\lib\opam-core" -L"C:\Users\Administrator\my-app\_opam\lib\sha" -L"C:/Users/Administrator/my-app/_opam/lib/ocaml\flexdll" -o "bin/main.exe" "C:\Users\ADMINI~1\AppData\Local\Temp\2\build_d62d04_dune\dyndllb7e0e8.o" "@C:\Users\ADMINI~1\AppData\Local\Temp\2\build_d62d04_dune\camlrespec7816" "-municode" "-Wl,-static" However, ldd showed that this wasn’t working: $ ldd main.exe | grep mingw libstdc++-6.dll => /mingw64/bin/libstdc++-6.dll (0x7ffabf3e0000) libgcc_s_seh-1.dll => /mingw64/bin/libgcc_s_seh-1.dll (0x7ffac3130000) libwinpthread-1.dll => /mingw64/bin/libwinpthread-1.dll (0x7ffac4b40000) I tried a lot of different variations. I asked Claude… then I asked @dra27 who recalled @kit-ty-kate working on this for opam. PR#5680 The issue is the auto-response file, which precedes my static option. We can remove that by adding -noautolink, but now we must do all the work by hand and build a massive command line. (executable (public_name main) (name main) (flags (:standard -noautolink -cclib -lunixnat -cclib -lmccs_stubs -cclib -lmccs_glpk_stubs -cclib -lsha_stubs -cclib -lopam_core_stubs -cclib -l:libstdc++.a -cclib -l:libpthread.a -cclib -Wl,-static -cclib -ladvapi32 -cclib -lgdi32 -cclib -luser32 -cclib -lshell32 -cclib -lole32 -cclib -luuid -cclib -luserenv -cclib -lwindowsapp)) (libraries opam-client)) It works, but it’s not for the faint-hearted. I additionally added (enabled_if (= %{os_type} Win32)) to my rule so it only runs on Windows.

#OCaml #OCamlPlanet

Interesting retrospective 👇 on why V8 team abandoned Sea of Nodes. Have to say SoN seems obviously correct, is Javascript just not designed to leverage it. AFAICT they treated memory as one giant register re: dependencies; langs like Rust w/ better aliasing info should do better

Pleased to announce that the third edition of my PL book, PLAI, is finally available on paper! Same price as it's been for 20 years (-:. Also made it available on Kindle EPUB, and a few other options. (Always free options, of course.) Enjoy!
www.plai.org

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...

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 ...

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.

PSA! Please share around! Due to a limited number of submissions, we're extending the OCaml Workshop deadline by a week to July 10th AoE!

Functional programmers! Heed my call! We need your submissions!!

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.