[Termtools] runtime environments for provers

[Johannes Waldmann]

Carsten Otto wrote:
> A common choice is the use of environment variables. If the variable TMP
> (or TEMP?) is set use the specified directory for temporary files. If
> not just use "/tmp" as a safe default.
>   
is this what Aprove does? (for reference, gcc uses $TMPDIR)

I'd favour command line options over variables
(because global variables are a BAD thing :-)

One reason for having TMPDIR="." in the competition is
that provers running in parallel  should not interfere.
Of course this property should be kept
(so it would be unwise to change "." to "/tmp" without any way of
overriding it).

Another point is that temporary files should be deleted immediately.
If a prover is aborted, it is perhaps unable to delete its own temp files.
If we have TMPDIR != "."  then it is easy to do  "rm $TMPDIR/*"
(for the competition master program).
Again, this would need one TMPDIR per prover, to be safe.

Best regards. Johannes.