In short, benchpress is a tool I use for running provers, by which I mean, generally, command-line tools that take a logic problem as input, and output something about the file such as "it's a valid theorem" or "it typechecks" or some sort of failure or timeout. The idea is to make it easy to run a tool you're developing (e.g. E, Zipperposition, Batsat, Archsat, etc.) on a large set of benchmarks, and analyze the results.
But today, we're going to solve Sudoku grids. My goal is to showcase mSAT, a parametrized SAT solver written in OCaml by my good friend Guillaume Bury and myself. The solver's code can be found on github, but I'm going to detail the most salient parts here.
Last October, I moved in Nancy to start working as an engineer with
Jasmin Blanchette on an exciting
project called Nunchaku.
Since my domain is formal logic, I spend a lot of time manipulating,
transforming, and traversing ASTs (abstract syntax trees). My primary
method for debugging is pretty-printing structures; in nunchaku,
I even have a
--print-all flag to print the AST after each transformation,
since the tool is basically a bidirectional pipeline that composes
transformations. I will certainly blog on the design of Nunchaku
later, but today I want to present the
module from OCaml, that I use for pretty-printing all my data structures.
Greating, earthlings! Today I will present an exciting new OCaml library called maki. This post will be longer as usual, because it is actually two posts in one:
- first, I'll present the goals of Maki, sketch its design, and present the most salient parts of its API;
- then I will demonstrate how to use it to quickly build a (very naive) OCaml build system, featuring parallel build and cached computations thanks to Maki.
A quick note about my current OCaml setup, in my last project, Nunchaku.
I have been hacking on the OCaml compiler recently; in particular, I added some support for coloring warning/error messages. At some point during the discussion over this pull request, it became clear that colored output should only be enabled if
stderr was an interactive terminal (in opposition to a regular file handle or whatnot). The compiler does not link with the
Unix library, so I finally decided to add a primitive
caml_sys_is_interactive. My purpose here is to explain how it works (from what I gathered) and how to do it.
For more than one year, vulnerabilies in software (especially pervasive C software) have been disclosed at an alarmingly high rate. I love OCaml, which is definitely safer, but still has gaps left open. I believe formal verification, albeit a very powerful tool, is not mature enough for most programmers (too difficult to use, requires too much efforts), so I'm thinking about alternative solutions that would be more lightweight to define and use, but would still increase the confidence in source code.
So here is a draft of a relatively simple extension to OCaml, that allows to specify more invariants in types without requiring a full-fledged proof system. It's purely hypothetical and I did not implement it (nor don't I plan to do it, not before the end of my PhD). The purpose is to propose a conservative extension of OCaml with a type system that can represent more complex invariants, without putting too much of a burden on the user, in a way so adding annotations to existing programs incrementally is feasible and even easy.