Java 17 (still) not supported in kore submodule

[Scott-Guest]

The kore submodule seems unable to compile any Java 17 features. Compare the two commits in #4039 , where a record class compiles just fine in the kernel submodule, but the same exact file fails to parse when moved to kore.

I thought I solved this with #4032, however, after doing a fresh clone I'm still encountering the same errors. This will be a blocker for #4038, #4030, and #4022.

[Scott-Guest]

I'm working to produce a minimal maven project example, but am pretty at a loss why this is happening. I'd appreciate some assistance from anyone more familiar with Maven.

[Baltoli]

That's really odd; will take a look and see if I can figure out what's going on!

[Scott-Guest]

Finally narrowed this down! While it's not mentioned in any changelog I can find, this appears to be a bug in scala-maven-plugin that was fixed in version 4.0.0 (we were using 3.3.1).

Ugh looks like this is still not sufficient - bumping the version fixes a minimized reproduction I have, but doesn't fix #4039.

[Scott-Guest]

After digging through Scala's source code a bit, my understanding is that

• scala-maven-plugin is backed by zinc, which is a wrapper around the Scala compiler for incremental compilation.
• If only Java source files are provided, zinc just delegates to javac. Otherwise, it delegates to scalac.
• To support Java-Scala interop, scalac needs the type signatures and symbol information for the Java code:
  • In JavaThenScala mode, where Scala code may depend on Java code but not vice-versa, scalac just delegates to javac and unpickles the symbol information from the compiled .class files.
  • In the default Mixed mode, where Scala code and Java code may both depend on each other, scalac instead has to parse the Java source code using its own internal Java parser.

This explains why the minimal example I was investigating was fixed by just bumping the scala-maven-plugin version - I had only included Java source files, so it was just delegating to javac which of course properly supported Java 17.

However, for K itself, we have inter-dependent Scala and Java code, so the errors were actually arising due to lack of support for Java 17 in scalac's internal Java parser.

While our Scala version (2.12.18) purportedly supports JDK 17, this is a bit misleading, and apparently only refers to bytecode compatibility and being able to run the Scala compiler using that JDK. Support for parsing newer Java source code tends to lag behind.

Looking through scala's issue tracker, the lack of support for some Java 17 features has already already been reported:

• scala.tools.nsc.javac.JavaParsers can't parse JDK14 records scala/bug#11908,
• scala.tools.nsc.javac.JavaParsers can't parse JDK17 "Sealed Classes" scala/bug#12159
• scalac cannot parse records that implement interfaces scala/bug#12474.

However, all of these issues were only patched in 2.13.x and closed without ever patching 2.12.x. For example, records are handled in the 2.13.x parser, but there is no such logic in the 2.12.x parser.

We could try submitting an issue requesting similar patches be made to 2.12.x. However, based on the comments here, 2.12.x is in "light maintenance" mode, so it's unclear whether they would be willing to make this change. Even if it were patched, we would have to wait for the next release or switch to using nightly builds.

Frustratingly, I think our best option then is to upgrade / port our codebase to 2.13.x (a bit ironic that we need to bump our Scala version in order to eventually remove all the Scala 😄). There are a number breaking changes (some are outlined here), but from a quick look trying this with our codebase, it seems doable within a day's work.

[Baltoli]

Wow - excellent debugging Scott! Let's discuss properly later but it seems like the trajectory we want is:

• Upgrade all our Scala code to 2.13
• Combine the kore and kernel modules to make a larger "frontend" module once the compiler settings allow us to do so
• Begin to remove / reimplement the Scala code in this new module piece by piece

[Baltoli]

Closed by #4168, I think!

[Scott-Guest]

Not quite, still need to wait for runtimeverification/llvm-backend#1024 to automerge then update the frontend Scala version.

#4168 is unrelated

[Baltoli]

Ah, I thought the update from SK -> LLVM -> K had gone through with #4168 but clearly didn't check well enough!

[Scott-Guest]

Closed by #4171