Dear all,
the testing for the competition categories is over. Some tools still
have problems regarding their performance (rejects in certified
categories or severe regressions compared to last year), but from a
technical point of view, all tools (*) are working.
If your tool has rejects or significant regressions, then you've been
notified. I'll continue to accept updates, but I won't run any more
tests. So if you update your tool, please make sure that the updated
version works on StarExec.
Moreover, the links to the proofs in the demo categories are working again.
Best
Florian
(*) AutoNon still has a few issues, but that's a 'historical' tool that
was just registered for reference. I'll take care of updating it.
Dear all,
the registration for termCOMP is over. Some teams worked really hard to
fix issues caused by the StarExec update, resulting in some last minute
registrations. Thanks for that!
If you missed the deadline, but intended to participate, please get in
touch.
Best
Florian
Dear all,
I was just informed that the benchmarking framework that we used in the
past (BenchExec) is no longer available on StarExec. Hence, we'll have
to work with "runsolver" instead. If I remember correctly, we used
runsolver at some point, but then we switched to BenchExec due to issues
with the measurement of the runtime. If you remember any details / your
tool was affected by these problems, please let me know.
Best
Florian
Dear all,
can I express in CPF (for Ceta-2)
that I want to apply "flat context closure" to a subset of rules only?
specifically, I want this for rules with empty lhs or rhs,
as it seems to increase the power of matrix interpretations.
(as shown by Aprove in TC 23).
I am looking at
http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR/file/825022…
but the example seems to close all rules.
I guess I can indeed context-close all rules uniformly,
and use the same interpretation, to remove the same rules.
But perhaps I want other methods that refer to the original rules.
Well it's a bit late anyway.
- J.
Dear all,
just to clarify, we expect the tools to output *CPF2 proofs* in the
certified categories (just like last year). If your tool already
supports the new CPF3 format and you planned to make use of that at
termCOMP, please let me know.
Best
Florian
Dear all,
for uncertified categories that use the new ARI format, you can start
testing with the following post-processor:
plain.ari.24.1 (784)
I tested it successfully on 1(!) example, so it might still have some
issues.
Best
Florian
Dear all,
here is the information that I have about the current StarExec
configuration:
root@starexec2:~# uname -r
5.15.0-112-generic
oot@starexec2:~# dpkg -l libc6-dev:amd64 python3
Desired=Unknown/Install/Remove/Purge/Hold
|
Status=Not/Inst/Conf-files/Unpacked/halF-conf/Half-inst/trig-aWait/Trig-pend
|/ Err?=(none)/Reinst-required (Status,Err: uppercase=bad)
||/ Name Version Architecture Description
+++-===============-===============-============-=========================================================================
ii libc6-dev:amd64 2.35-0ubuntu3.8 amd64 GNU C Library:
Development Libraries and Header Files
ii python3 3.10.6-1~22.04 amd64 interactive high-level
object-oriented language (default python3 version)
Note that the information here
https://www.starexec.org/starexec/public/machine-specs.txt
is outdated!
Best
Florian
