Tiago Cogumbreiro

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.

I migrated from a Coq 8.19 + coq_makefile to dune + Rocq 9.0, assisted with Claude Code. It was a great experience, as there are so many little (tedious) details, from opam, Git, dune, etc.

gitlab.com/cogumbreiro/...

If you are a functional programmer in Asia, then it is your obligation, nay your existential imperative to submit to the OCaml workshop this year

SPLASH/ICFP is in Asia this year and we have fewer submissions from the western folks because of the distance

Submit!!! Plsplsplsplsplz

**CRITICAL RULE**: If ANY proof attempt fails to compile, STOP IMMEDIATELY.

I'm learning to use Claude code for my Rocq proof development. First rule of fight club: If ANY proof attempt fails to compile, STOP IMMEDIATELY.

Otherwise, Claude just exhausts my tokens.

If I may ask, what tolling are you using?

Original post: types.pl/@liamoc/1145...

GitHub - kiranandcode/LeanTeX: Write LaTeX presentations directly from Lean4~ Write LaTeX presentations directly from Lean4~. Contribute to kiranandcode/LeanTeX development by creating an account on GitHub.

Oh, defo you should! I am sad that I don't currently have any research actively working on lean at the moment because programming in it is honestly like working in the language of my dreams; I can truly extend it as much and as often as I want to fix any pain points

github.com/kiranandcode...

So cool! You're making me want to play with Lean 👀

Yes, we use ocaml's binding of z3 directly. We have used the stdin+smtlib in the past, but for our use case using the API works quite well and it is simpler to package.

For libclang we have use the stdin approach, which is not ideal. I haven't tried the llvm opam package, but it appears outdated.