HeVeA : a new Rope

I recently started an internship in Gallium, working on the HeVeA LaTeX to HTML compiler from and with Luc Maranget. I’ll stay here for two months, which is sufficient for having to “blog about it”. In my civil life, I’m interested in about approximately everything concerning language(-related) theory.

My first job for HeVeA was changing the structure used by the Out module. It was yielding the ouput by concatenating together bare strings, thus blowing up the maximal size of strings on 32 bits machines. A data structure fit for concatenations was therefore needed, and a good choice for it is Ropes.

next

Half-hearted hash table

Hash tables have slightly changed between OCaml 3.12.1 and OCaml 4.00.0. While some care has been taken for forward compatibility, you might encounter strange behaviors if you accidentally try to backport a hash table.

next

The story of a stack overflow during Coq extraction

I routinely extract my Coq development into an executable I can test and benchmark. However, on one fateful afternoon, the extraction process failed with a stack overflow. I had to dive deep into the code. This is the fable of how things went right and wrong, moral of the story included.

next