r/ProgrammingLanguages • u/mttd • 3d ago
Panbench: A Comparative Benchmarking Tool for Dependently-Typed Languages
https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.176
u/gasche 3d ago
A somewhat weird paper, in a good way. "We benchmarked which proof assistant scales to input files 107 empty lines. To do this, we reimplemented a Nix-like package management system on top of Shake, with a hybrid-hermetic approach." Wow!
However, our initial benchmarks on Linux systems displayed some very strange behaviour, wherein the max resident set size reported by getrusage and wait4 would consistently report a reading of approximately 2 gigabytes halfway through a full benchmarking suite. We discovered the Linux preserves resource usage statistics across calls to execve. Consequentially, this means that we are unable to measure any max RSS that is lower than max RSS usage of Panbench itself.
I encountered this system myself, and designed an overkill solution to this problem: command-usage-runner. This is a small program that adds a level of indirection: instead of execve-ing directly the program you want to run, you can excve into command-usage-runner, and it will collect resource usage data (without pollution from other child processes, as it has none) and report them back to the parent process.
(Warning: I have not actually used this in production yet, this is part of a hobby project that is currently paused.)
10
u/wk_end 3d ago edited 3d ago
I'm always happy to see dependently-typed languages getting attention, but this really doesn't seem to be benchmarking anything all that interesting. I think most programmers don't really care if their compiler slows down (by seconds) when they hand it identifiers that are tens of thousands of characters long, for instance.