Description
Running different versions of KeY requires different JDKs.
JDKs are typically configured by setting envvar JAVA_HOME. This works for Gradle (and many other shell scripts starting Java).
testRunAllFunProofs and testRunAllInfProofs spawn Java subprocesses using java from $PATH. If the which java is older than $JAVA_HOME/bin/java, spawning results in "classes are compiled with a later version".
Here, we should rather use the generation of unit-tests for run-all-proofs, or respect the environment variable $JAVA_HOME.
Reproducible
Is the issue reproducible?
Select one of: always, sometimes, random, have not tried, n/a
always.
You need to JDKs, e.g., 8 and 21.
$ sdk d java java-8.x.x-tem # make JDK 8 default
$ export JAVA_HOME=$HOME/.sdks/candidates/java/... # set to JDK21
$ ./gradlew testRunAllFunProofs
What is your expected behavior and what was the actual behavior?
Additional information
Description
Running different versions of KeY requires different JDKs.
JDKs are typically configured by setting envvar
JAVA_HOME. This works for Gradle (and many other shell scripts starting Java).testRunAllFunProofsandtestRunAllInfProofsspawn Java subprocesses usingjavafrom$PATH. If thewhich javais older than$JAVA_HOME/bin/java, spawning results in "classes are compiled with a later version".Here, we should rather use the generation of unit-tests for run-all-proofs, or respect the environment variable
$JAVA_HOME.Reproducible
always.
You need to JDKs, e.g., 8 and 21.
Additional information
Commit: 2026-06-20
Should be present in all KeY versions since the Wallisch did the run-all-proofs test classes.