Posts tagged by Gabriel Scherer

Syntactic parametricity strikes again

:: by Gabriel Scherer, by Li-Yao Xia

In this blog post, reporting on a collaboration with Li-Yao Xia, I will show an example of how some results that we traditionally think of as arising from free theorems / parametricity can be established in a purely “syntactic” way, by looking at the structure of canonical derivations. More precisely, I prove that is isomorphic to where is the type of integers smaller than , corresponding to the set .

Bullets are good for your Coq proofs

:: coq, by Gabriel Scherer

I believe that bullets are one of the most impactful features of recent versions of Coq, among those that non-super-expert users can enjoy. They had a big impact on the maintainability of my proofs. Unfortunately, they are not very well-known, due to the fact that some introductory documents have not been updated to use them.

Bullets are a very general construction and there are several possible ways to use them; I have iterated through different styles. In this post I will give the general rules, and explain my current usage style.


:: by Gabriel Scherer

Max New, Daniel Patterson and Ben Greenman recently wrote three two-page abstracts on what they are working on right now. Come have a look — and any feedback is welcome!

Emacs daemon for fast editor startup

:: System Administration, Emacs, by Gabriel Scherer

In the early days of the famous Emacs/Vim debates, Emacs was often ridiculed for its bulkiness (Eight Megabytes-of-RAM And Constantly Swapping, etc.). The computational power of our computer has grown much faster than Emacs’ bloat: it takes exactly one second to load on my machine. However, our workflows have also changed, and my workflow implies frequently starting new text editors — on each git commit for example, or when I use a Firefox extension to edit a textarea content in a proper editor.

In this blog post, I describe how to use emacsclient to reuse an existing Emacs process when creating a new editor window, which reduces editor startup times from 1s to 0.150s on my machine.

Measuring GC latencies in Haskell, OCaml, Racket

:: garbage collection, latency, instrumentation, haskell, ghc, ocaml, racket, by Gabriel Scherer

James Fisher has a blog post on a case where GHC’s runtime system imposed unpleasant latencies on their Haskell program:

Low latency, large working set, and GHC’s garbage collector: pick two of three

The blog post proposes a very simple, synthetic benchmark that exhibits the issue — basically, latencies incurred by copy time — with latencies of 50ms that are considered excessive. I thought it would be amusing to reproduce the synthetic benchmark in OCaml and Racket, to see how other GCs handle this.

Without further ado, the main take-away are as follows: the OCaml GC has no issue with large objects in its old generation, as it uses a mark&sweep instead of copying collection, and exhibits less than 3ms worst-case pauses on this benchmark.

The Racket GC also does not copy the old generation, but its incremental GC is still in infancy (compared to the throughput-oriented settings which works well) so the results are less good. It currently suffer from a “ramp-up” effect that I will describe, that causes large pauses at the beginning of the benchmark (up to 120ms latency), but in its steady state the longest pause are around 22ms.

Please keep in mind that the original benchmark is designed to exercise a very specific workflow that exercises worst-case behavior for GHC’s garbage collector. This does not mean that GHC’s latencies are bad in general, or that the other tested languages have smaller latencies in general.

The implementations I use, with a Makefile encapsulating the logic for running and analyzing them, are available in a Gitlab repository: