Benchpress hacking: log 1
I've decided I want to resume blogging. So without further ado, here's a short piece about one of my side projects: benchpress (with a live hosting of the web ui).
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.
Currently Benchpress is composed of two distinct tools that share a common library:
benchpressis a CLI tool with subcommands such as
benchpress run, which I tend to put in makefiles as
make benchpress-foobarto run the solver I'm developping on some set of files labelled
foobarwhich a bunch of preset parameters.
a sample run of benchpress
benchpress-serveris a daemon embedding a tiny httpd server to visualize results produced by
Anyhow. Currently my friend Guillaume Bury and myself are working on different things: Guillaume is stress testing benchpress by running hundreds of thousands of job pairs at once, for his tool dolmen, and I work a bit on the web UI and a dynamic notification system. Together we worked on a previous tool to the same effect.
Storage of results with sqlite
An interesting (imho) design decision that was made at the beginning of the current iteration of benchpress, is to store the result of each run into a separate sqlite file. These files can be safely copied from a big workstation onto someone's machine, they can be deleted, backuped, etc. quite nicely.
Yet, it's useful to compare the results from distinct runs, to find regressions or improvements between successive versions of a tool. The killer sqlite feature that enables that is its ability to query several files at the same time, by attaching them onto an existing database. The code to compare two files does exactly that, onto an in-memory database. Sqlite also provides excellent indexing into the tables of results (which can now reach hundreds of thousands of results in one run); this makes the web interface quick to produce results.
Web UI architecture
The web UI is pretty basic. It's almost entirely static, produced via tiny tiny httpd (which serves the content over http/1.1) and tyxml (which provides well-typed combinators for producing the html). Bootstrap helped make the UI not too ugly, as I don't know anything about modern CSS. I found class-based CSS to be quite convenient.
Sqlite is used for answering most queries. The notable exception is the main
page, which lists results by exploring the
directory (xdg compliant); but even then, each result has a summary
associated that is lazily loaded and incurs a query to gather metadata
such as the set of solvers used in this run, the number of problems,
and the total clock time it took.