Tiago Cogumbreiro

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

135 followers291 following82 posts

Tiago Cogumbreiro reposted

Leanpub
@leanpub.bsky.social

The OCaml Handbook: A Complete Guide from First Program to Production Systems by Steve T. Publications is a new release on Leanpub! Discover the power and elegance of OCaml, from your very first program to production-ready applications. The OCaml Handbook … leanpub.com/theocamlhand...

Tiago Cogumbreiro reposted

Sung Kim
@sungkim.bsky.social

People are using AI to break CUDA’s moat. Given any pytorch model, it profiles it, ranks bottlenecks by amdahl's law, writes triton or CUDA C++ replacements, and runs 300+ experiments overnight with no human in the loop. - 5.29x over pytorch eager on rmsnorm - 2.82x on softmax

Tiago Cogumbreiro
@forkjoin.bsky.social

I'm getting closer to having an e-graphs library that can be shared with others. I'm porting some of the tutorials from Egg to finetune the UX and to see if I can reproduce some of the functionality. I am really enjoying ODoc+Dune! Nice combo.

Tiago Cogumbreiro reposted

Arjun Guha
@arjunguha.bsky.social

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)

Tiago Cogumbreiro reposted

Stefan Marr
@stefan-marr.de

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

jobs.royalholloway.ac.ukJob Opportunity at Royal Holloway University of London: Postdoctoral Research AssociateFull-Time, Fixed-Term until 30 November 2028Applications are invited for the post of Post Doctoral Research Associate (PDRA) in the Department of Computer Science at Royal Holloway.This is a three-year full-time position funded by the EPSRC project...
Tiago Cogumbreiro
@forkjoin.bsky.social

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.

Tiago Cogumbreiro
@forkjoin.bsky.social

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 reposted

OCaml
@ocaml.org

#OCaml #OCamlPlanet

dlvr.itStatic linking in OCamlMost 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.

Tiago Cogumbreiro reposted

Joseph Garvin
@josephhgarvin.bsky.social

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

Tiago Cogumbreiro
@forkjoin.bsky.social

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.

Tiago Cogumbreiro reposted

Kiran
@kirancodes.me

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

Kiran@kirancodes.me

Calling for Presentations!!! The OCaml Workshop 2025 welcomes presentations on any topic related to OCaml (such as multicore, algebraic effects, testing, ppxs, etc.) Have fun!! Submissions due: July 3rd AoE Workshop: Oct 17th Here's the link to website: conf.researchr.org/home/icfp-sp... #OCaml

conf.researchr.orgOCaml 2025 - OCaml Users and Developers Workshop 2025 - ICFP/SPLASH 2025The OCaml Users and Developers Workshop brings together industrial users of OCaml with academics and hackers who are working on extending the language, type system, and tools. Previous editions have b...
Tiago Cogumbreiro
@forkjoin.bsky.social

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.

Tiago Cogumbreiro reposted

Kiran
@kirancodes.me

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

Kiran@kirancodes.me

Calling for Presentations!!! The OCaml Workshop 2025 welcomes presentations on any topic related to OCaml (such as multicore, algebraic effects, testing, ppxs, etc.) Have fun!! Submissions due: July 3rd AoE Workshop: Oct 17th Here's the link to website: conf.researchr.org/home/icfp-sp... #OCaml

conf.researchr.orgOCaml 2025 - OCaml Users and Developers Workshop 2025 - ICFP/SPLASH 2025The OCaml Users and Developers Workshop brings together industrial users of OCaml with academics and hackers who are working on extending the language, type system, and tools. Previous editions have b...

Tiago Cogumbreiro reposted

Kiran
@kirancodes.me

Replying to @forkjoin.bsky.social

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

github.comGitHub - 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.
Tiago Cogumbreiro
@forkjoin.bsky.social

I really enjoy reviewing papers. I am reviewing this paper for OOPSLA. I understood the intro. The overview section started by making me giggle and the problem statement was clear as day. I'm pumped to discover what comes next. Hopefully, a strong accept.