[Termtools] runtime environments for provers (was: new mu-term)

[Johannes Waldmann]

Salvador Lucas wrote:
>
> We are pleased to announce the new web site for the termination tool
> MU-TERM:
>

Nice. And fast!


When I run the command-line executable, it seems that it calls
"./bc2sat" and "./sat"
This requires that I have them in the directory from where I call muterm.

This is certainly in accordance with the setting of previous competitions,
but I feel this should be changed in order to be more user-friendly.
That's why I'm asking prover authors for their opinions here.


As a user, I expect to call (e.g.) muterm  from anywhere,
after installing in some fixed place (e.g. /usr/local/bin),
and I don't necessarily have bc2sat in exactly the same place.
I'd expect muterm to use the $PATH to find the tools it wants.

(if you'd release the source, then I'd make this patch myself,
that is, change System.Cmd.system $ unwords [ "./bc2sat", ... ]
to System.Cmd.system $ unwords [ "bc2sat", ... ]  or something.)


Another question is where provers put temporary files.
(They'd need them e.g. for interfacing external solvers.)
Current competition guidelines require "." (and that's what muterm does)
Another obvious choice would be "/tmp" (that's what I'd expect, e.g.
from compilers)

Note that "the place where the prover is installed" is a non-choice
because this is impossible to find correctly (at runtime),
and even if you have it, you sure would not want to give a user write
access.

Another choice is of course to let the user choose.
Matchbox has options (with defaults) "--solver=minisat --tmpdir=/tmp"


Best regards, Johannes.