Guillaume Bury
Guillaume Bury
## Desired Behavior Have builtin rules for `.messages` files produced by menhir (cf [menhir's manual](http://cambium.inria.fr/~fpottier/menhir/manual.html#sec67) ). This would include: - generating a fresh `.messages` file for a new grammar /...
In short, it would be interesting to be able to do the following: - from inside an ocaml program, set the maximum stack size for fibers (or set it to...
Sometimes shrinking can take a long time, so a way to stop shrinking after some time and/or a number of failed tests would be nice to have. The new events...
Currently coq proof can be quite slow (and even fail to check within reasonable time/memory). One solution would be to change the structure of coq output from a srie of...
The graphical interface of alt-ergo (i.e. altgr-ergo), is relatively heavy to maintain and imposes many restrictions on development, so we are currently considering removing it entirely from the project. Before...
Following the recent addition of [Gbury/dolmen](https://github.com/Gbury/dolmen) (that will allow alt-ergo to more input languages such as smtlib, tptp, etc...), we are considering potentially removing the support for dynlinked parsers, as...
On a view such as https://benchpress.cedeela.fr/show_table/res-20200515T222015-2eed2c42-3d64-4611-956f-341d3b2d54ab.sqlite/?offset=0 , it would be useful to be able to list only the results that differ between provers (and this list would be linked to...
It is very convenient that currently benchpress records the time for each prover run, but it would be even more useful to also have an estimation of the memory used...
Similarly to how provers are identified by a name (rather than their command line), it would be useful to be able to name directories. This would allow a few things...
It seems that inserting conditions via a preformatted string in a statement does not work. More precisely, consider the follwing piece of code: ``` ocaml module Sqlexpr = Sqlexpr_sqlite.Make(Sqlexpr_concurrency.Id) let...