[Termtools] current competition test run

Johannes Waldmann waldmann at imn.htwk-leipzig.de
Thu Jul 10 12:44:40 CEST 2008


-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Dear colleagues,

currently "last year's competition" is executing
on the new hardware and software platform.
So, results are expected to match those of 2007.

One difference is that now all problems from TPDB are used,
in contrast to last year's random selection in oversized subdirectories.
I think this is fine - the idea is to have a complete data set,
while interpretation of the data is another, separate step.

There has been one technical problem:  Torpa didn't find the SAT solver.
This has been repaired but the change can only be made effective
after the current run of the SRS categories will be completed.
So, the Torpa column in the SRS tables is meaningless for the moment.

The underlying problem (for not finding the SAT solver) is this:

>> (what should tool authors expect/require about PWD and PATH), 
>> I tried to raise this issue before,
>> http://lists.lri.fr/pipermail/termtools/2007-November/000475.html
>>
>> the problem is that currenty provers rarely have a
>> "./configure ; make install", where you could declare
>> the installation location.

Simon says:

> my suggestion would be that tools add their working directory to their
> path themselves and call external programs from the path.

Opinions?

Best regards, Johannes.
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.9 (GNU/Linux)
Comment: Using GnuPG with SUSE - http://enigmail.mozdev.org

iEYEARECAAYFAkh16BgACgkQDqiTJ5Q4dm8gOwCgsM/LZf1YbXEYfHgaIgQYLTec
EYcAniYs6UMHdykwgOnZvopXn4xkzBhQ
=4GnA
-----END PGP SIGNATURE-----


More information about the Termtools mailing list