Skip to content

RunAllProofs disrepects JAVA_HOME #3630

@wadoon

Description

@wadoon

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

  • Commit: 2026-06-20

    Should be present in all KeY versions since the Wallisch did the run-all-proofs test classes.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    Projects

    No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions