Provide several tools and one library,
frogutils. The tools are the
froglock: execute commands sequentially, no overlap.
frogmap: run a command on many inputs (files?), with parallelization.
frogiter: run a command on every result obtained with
frogtptp: run a TPTP prover (more specific!) and analyse its output.
frogplot: prints the cumulative times of TPTP provers
The basic usage is
froglock -- <cmd>. This has the same behavior
<cmd>, except for one point: at any given time, on a given
computer, at most one command launched from
froglock -- <cmd> runs.
Until it terminates, the other commands aren't started yet; once
it terminates one waiting command is started and takes ownership of the "lock".
This works by connecting to a daemon on a given port, starting it if required.
The daemon will stop if its queue is empty.
froglock status can be used to display the current queue of tasks (including
the one that owns the lock). It prints nothing if no task is launched.
There is one "lock" per TCP port on the machine (although only ports > 1024
should be used, otherwise only root will be able to use
port can be changed with
frogmap -- <cmd> <args...> applies a command
<cmd> (shell command) to a
list of elements, and stores the result of
<cmd> <arg> for every such
Parallelism (on a single computer) can be achieved with
-j <n> where
<n> is the number of parallel invocations of
frogmap is killed or stopped for any other reason before it could
process every argument, it is possible to resume the computation
from where it left:
frogmap resume <state_file.json>.
Results stored in a file
<file.json> can be analysed either using the module
FrogMapState (in the library
src/frogMapState.mli) or with
frogiter (see below).
frogiter goes hand in hand with
frogmap. It is a simple way to
apply a command to all the results stored in some
<file.json> produced by
frogmap -o foo.json -j 20 'sleep 3; echo ' `seq 1 1000` # later... frogiter -c foo.json 'grep 11'
will print all number from 1 to 1000 that contains the string 11 in their decimal representation. In a slightly inefficient way. The command is passed the following environment:
FROG_OUT: the command's stdout
FROG_ERR: the command's stderr
FROG_ARG: the argument given to the command
FROG_TIME: number of seconds the command took to complete
FROG_ERRCODE: exit code of the command
frogiter shell foo.json \ 'echo on $FROG_ARG, time $FROG_TIME, `wc -l <<< "$FROG_OUT"` lines'
Frogtptp provides several commands to deal with TPTP provers (although it would probably work almost as-is with SMT solvers too).
The commands are:
frogtptp run <prover_name> file.pruns a theorem prover on the TPTP file.
<prover_name>is the name of a prover as listed in the config file
$HOME/.frogtptp.toml(or with the
-configflag). Other options specify the memory limit and timeout for the prover.
frogtptp listlists the known provers (those detailed in the config file).
frogtptp analyse <prover>=<file.json>analyses a single output file as obtained from
frogmap 'frogtptp -run <prover>' file1 file2 ....
frogtptp analyse <prover1>=<file1.json>,<prover2>=<file2.json> ...will do the same but also compare the performance of the different provers. No other option might follow
analyse. This is still work in progress.
frogtptp plot -o out <prover>=<file.json>prints the cumulative time of the provers on the
# I have 10 cores, let's prove stuff with E frogmap -j 10 -o bench.json \ 'frogtptp run eprover -t 5' \ $TPTP/Problems/*/*.p # gosh, I have to reboot! sleep 500; reboot # resume where I left. But now I have 30 cores! frogmap resume -j 30 bench.json # then: basic statistics on the results frogtptp analyse eprover=bench.json # print the cumulative times frogtptp plot -o plot.png eprover=bench.json
runs the E prover (named
eprover) on all files in
a TPTP archive, resumes the computation
after a reboot, prints some basic statistics about the results,
and finally plots the cumulative times in a file
A sample config file for
frogtptp can be found in
format is toml, a simple textual
configuration format, close to
$ opam pin add frogutils https://github.com/c-cube/frog-utils.git