benchpress

benchpress copied to clipboard

stop/resume jobs

1

- when starting a job, put its full serialized description into a dotfile, and append each individual result as we go (use cbor+decoders?) - command to list interrupted jobs -...

c-cube

- triggered by CLI option, task option, or general option - make a subdirectory in xdg state dir for the particular benchmark - in db, just save `external:file_path` for both...

c-cube

command for regression testing

1

iterate on existing results and use olinq to find problems where the result is different (and time is not too close to timeout); summarize in csv/printbox

c-cube

more dynamic task system

1

- `par_map` should take a pool as argument, not create one - dynamic scheduling of tasks such as: * run proof checker upon unsat * run program for finding expected...

c-cube

add per-prover parameters

1

allow, say: ```toml [prover] cmd = "prover $a $b $file $timeout a = [a1, a2, a3] b = [b1, b2] ``` and test on the whole matrix.

c-cube

- have a separate binary for `logitest-irc`, with its own config perhaps, and launch it iff it's present and asked for (a "service") on stdio - communicate via jsonrpc2 -...

c-cube

- use ezcurl to interact with their web API - make that a sublibrary - have a series of subcommands for querying starexec (or maybe a separate binary? `logitest-starexec`?)

c-cube

see https://wwwlehre.dhbw-stuttgart.de/~sschulz/THESES/e_bench2.html for the goals

c-cube

instead of `expect = unknown` (as a fallback for problems where an expect string isn't found), a useful feature for benchmarks is to *force* the expect field to be unknown...

c-cube

Copy input and output of provers to RAM

1

This is the RAM disk part of #69, split off from #69 It includes the changes from #69 because there are multiple changes in `Misc.ml` and that would cause conflicts...

bclement-ocp