[Termtools] runtime environments for provers

[Salvador Lucas]

Dear Johannes,

You are right. This should be improved...
We'll think on that.

Best regards,

Salvador.

Johannes Waldmann wrote:

>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.
>
>
>_______________________________________________
>Termtools mailing list
>Termtools at lists.lri.fr
>http://lists.lri.fr/mailman/listinfo/termtools
>  
>