July 2025 - Termtools - lists.rwth-aachen.de

stdout, stderr
by Johannes Waldmann 21 Jul '25

21 Jul '25

Hi Florian, are we allowed to print diagnostics/trace to stderr? will you store/show it? I found out that `docker run -t` merges these streams but without `-t` they are separate. - Johannes.

1 0

--cert
by Johannes Waldmann 21 Jul '25

21 Jul '25

Hi Florian, when the executor does `solver --cert` then my solver knows what to do. but how do you know what solvers have this option? This needs some extra step in registration? as in previous years, matchbox wants to do both (cert and uncert), to show the difference. - Johannes

1 0

bind-moun-point in the container?
by Johannes Waldmann 21 Jul '25

21 Jul '25

Hi Florian, the container needs a mount point? in order to make this work: docker run -v ./data:/mnt:Z,ro --rm -it jwaldmann/termcomp2025-mbox:21-07-2025 solver /mnt/Zantema/z001.srs You can do the mount when running (apptainer does it?) but the name "/mnt" must exist in the container? so it has to be known when building the container? (a super minimal container ("FROM scratch") might not have it) - Johannes. NB: I managed to build a nice small container (20 MB compressed - about the same size as the zip file for starexec) with the two-stage approach described here https://jpetazzo.github.io/2020/02/01/quest-minimal-docker-images-part-1/ (busybox:glibc)

1 0

termcomp: solver names, category names, cores, RAM, ...
by Johannes Waldmann 18 Jul '25

18 Jul '25

Hi Florian - on https://termination-portal.org/wiki/Termination_Competition_2025_technical_… you write "following two commands will be executed in your container: solver --name solver --timeout=$timeout --category=$category $benchmark" * what do you recommend for --name? (how many lines, words, characters) (e.g., can/should it contain precise version information?) * I can just ignore timeout? (and expect it to be 60 seconds?) * how many cores can I expect to use? RAM? * what are the possible values for $category? (they are names of top-level directories in TPDB? e.g., SRS_Standard, SRS_Relative ? Could you provide empty files in https://github.com/TermCOMP/registration ?) * How do I know whether it's certified or not? * $benchmark : will it have a specific extension (.ari)? - Johannes.

2 5

Workshop on Termination 2025 - register now
by Johannes Waldmann 11 Jul '25

11 Jul '25

20 Intl. Workshop on Termination, Leipzig, Germany, September 3-4, 2025. Co-located with 14th Intl. Workshop on Confluence, September 2-3. https://www.imn.htwk-leipzig.de/WST2025/ News: - Registration opened (deadline: July 23) - Joint IWC and WST Invited Talk announced Aart Middeldorp, University of Innsbruck: Termination and Confluence: Remembering Hans Zantema In this presentation I give an incomplete overview of the many contributions of Hans Zantema to termination and confluence. Several of these were presented at earlier workshops on termination and confluence, and I include a biased overview of the development of these workshops and associated competitions. - WST accepted papers announced Best regards, Dieter Hofbauer and Johannes Waldmann, WST co-chairs.

1 0

FSCD 2025: Free online participation, 15 - 18 July 2025
by Carsten Fuhs 09 Jul '25

09 Jul '25

The organisers of FSCD 2025 are delighted to announce free best-effort virtual participation in the 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025) in Birmingham, 15 - 18 July 2025. Please register your email in advance to receive login information for the live stream. For details, please see the information on the conference website: https://fscd-conference.org/2025

1 0