Fix version parsing script (#4095)

This PR applies some minor cleanup to the `checkJava` script's parsing
of `java --version` output. The new code will produce a correct error
message for Java >= 11, and better handles slightly different formats of
version data produced by different JVM implementations.

Fixes #4059
Fixes #4061

---------

Co-authored-by: rv-jenkins <admin@runtimeverification.com>

k-distribution/src/main/scripts/lib/checkJava

@@ -3,10 +3,8 @@ MIN_VERSION="17"
 echoerr() { echo "$@" 1>&2; }
 
 if type -p java >/dev/null; then
-#    echo found java executable in PATH
     _java=java
 elif [[ -n "$JAVA_HOME" ]] && [[ -x "$JAVA_HOME/bin/java" ]];  then
-#    echo found java executable in JAVA_HOME
     _java="$JAVA_HOME/bin/java"
 else
     echoerr -e "\033[1;31mError:\033[0m K requires Java $MIN_VERSION to run but Java was not detected."
@@ -36,7 +34,7 @@ else
     setarch
     JAVA=$NG
   else
-    version=$("$_java" -version 2>&1)
+    version=$("$_java" --version)
     setarch
     if [ $ARCH -eq 64 ]; then
       TIERED=-XX:+TieredCompilation
@@ -46,20 +44,23 @@ else
   fi
 fi
 
+# The Java version information we're parsing here looks something like this:
+#
+#   openjdk 21.0.2 2024-01-16
+#   OpenJDK Runtime Environment Homebrew (build 21.0.2)
+#   OpenJDK 64-Bit Server VM Homebrew (build 21.0.2, mixed mode, sharing)
+#
+# To get the major version, we need to look at the first line's second field,
+# then use a regex to extract the major version component. If the JVM changes
+# the format of the version that gets printed, this script needs to be updated
+# as well.
 
-if [[ "$_java" ]]; then
-    version=$(echo $version | awk -F '"' '/version/ {print $2}')
-#    echo version "$version"
-    if [[ $version = "1."* ]]; then
-      version=$(echo $version | sed -e 's/1\.\([0-9]*\)\(.*\)/\1/; 1q')
-    else
-      version=$(echo $version | sed -e 's/\([0-9]*\)\(.*\)/\1/; 1q')
-    fi
-    if [[ "$version" -lt "$MIN_VERSION" ]]; then
-        echoerr -e "\033[1;31mError:\033[0m K requires Java $MIN_VERSION to run but the detected version is $version."
-        echoerr "Please either add Java $MIN_VERSION bin directory to the PATH or set the JAVA_HOME
+version=$(echo "$version" | head -1 | cut -d ' ' -f2)
+version=$(echo "$version" | sed -e 's/\([0-9]*\)\(.*\)/\1/; 1q')
+
+if [[ "$version" -lt "$MIN_VERSION" ]]; then
+    echoerr -e "\033[1;31mError:\033[0m K requires Java $MIN_VERSION to run but the detected version is $version."
+    echoerr "Please either add Java $MIN_VERSION bin directory to the PATH or set the JAVA_HOME
 environment variable accordingly."
-	exit 2
-    fi
+    exit 2
 fi
-

kernel/src/main/java/org/kframework/main/JavaVersion.java

@@ -4,8 +4,14 @@
 /** Created by dwightguth on 9/23/15. */
 public class JavaVersion {
 
+  /**
+   * Prints a version string that can be parsed by checkJava.
+   *
+   * <p>For more context on what format is expected here, see the checkJava script. If the output of
+   * `java --version` ever changes, this class should do so as well.
+   */
   public static void main(String[] args) {
-    System.err.println("java version \"" + System.getProperty("java.version") + "\"");
+    System.err.println("java " + System.getProperty("java.version"));
     System.err.println(System.getProperty("sun.arch.data.model") + "-Bit");
   }
 }