A research blog about programming languages, formal logics, software development and their interactions, by Matthias Puech.

Tag: dev

An OCaml hack: recover the abstraction of abstract types

Here is a scoop: in OCaml, your abstract types aren’t really abstract (unfortunately). This is because some magical functions in the standard library don’t respect the abstraction of data types:, Hashtbl.hash, Pervasive.(=) — yes, the very equality you use everyday — etc. The problem is that if you contribute to a large project written in OCaml and you want to take advantage of abstract types, these functions become your worst enemies because they are breaking the abstraction you were carefully designing. You’ll probably end up as I did finding and removing by hand every occurrence of these magical functions in your code. The following is for you then. Read the rest of this entry »


Set the root directory of a project in Emacs with dir-locals.el

Hi, and welcome to my blog. I’ll try to write here about the stuff I do, use or discover during my work as a Ph.D in Computer Science. There will hopefully be a bit of science (proof theory), some code (functional programming), some tips and tricks for developers.

For a gentle start, I’d like to share a nice little trick I put together for Emacs. I am developing in a big project (Coq) with multiple subdirectories, which compilation is managed by GNU make. When I open a file in a subdirectory and then hit M-x compile, make complains because I am now in the subdirectory and not at the root of the project anymore. So I took the habit for hitting very fast M-x cd .. every time I open a new file in a subdirectory. Annoying… Read the rest of this entry »