Parts a tla2tools.jar should still work with Java 1.8.

If an execution does not use the TLAFlightRecorder class then yes it will work with Java 8. However I don't think it's a good idea to ship a library that says it's Java 8 compatible while parts of it are not Java 8 compatible and will fail at runtime for that reason.

Users can put their own version of TLAFlightRecorder on the classpath and continue with 1.8. IIRC there are still users with 1.8 out there.

All right well an issue is we won't be able to add -Werror to the javac args to treat warnings as errors (thus keeping more from being added) because javac detects that the code it's compiling isn't v8-compatible and issues the bootstrap path warning. Also it won't compile on Windows which is more strict about this kind of thing I guess.

Can you explain why Java is more strict on Windows? This sounds strange given that Java's main feature is platform independence.

Well it's a compile-once-run-anywhere thing so any artifacts we compile will run on windows just fine, but the actual act of compilation is I guess different enough that actually trying to run the ant build on windows will fail with "unable to find jdk.jfr package" errors. Maybe there's a workaround but I wasn't able to find it other than specifying release="11" in the customBuild.xml file.

This must be a local issue because compilation on Windows used to work when the CI (including UI tests) still ran on Azure Pipelines. At any rate, let's make a conscious/explicit decision to break (partial) 1.8 compatibly, instead of as a side-effect of turning warnings into errors. A message to the TLA+ Google group could, perhaps, answer if some users are still on 1.8.

I posted here: https://groups.google.com/g/tlaplus/c/BReLjG8ako4

If we go through with this change I suggest bumping the minor version so nightly releases are uploaded to a separate release from where they're uploaded now.

I don't think it's a good idea to ship a library that says it's Java 8 compatible while parts of it are not Java 8 compatible and will fail at runtime for that reason.

Welcome to the Java Ecosystem! 😅 What you've described is not a best practice, but it is a practice, and a remarkably common one. It works well for features that can be enabled/disabled at run-time.

Since AFAIK there's no flag or environment variable to disable TLAFlightRecorder, here's what I think we should do ---

IIRC there are still users with 1.8 out there.

The right (?) way to support those users is to ship a multi-release jar:

• Most of the tools' source code (including a no-op implementation of TLAFlightRecorder) should be compiled with -release 8 as @ahelwer suggested.
• The real implementation of TLAFlightRecorder should be compiled with -release 9 and the class file should be placed in the META-INF/versions/9 subdirectory of the final jar.
• The final jar manifest should include Multi-Release: true.

It should be confirmed that OSGi (the Toolbox) correctly handles such a multi-release.jar. That said, https://metabase.tlapl.us/dashboard/1 does not indicate Java 8 users.

Recent versions of OSGi do support multi-release jars c. 2018, but the toolbox might be using an older version that doesn't. (I don't know enough about OSGi to tell.)

If dropping Java 8 support is an option, it seems like the best one. I won't miss it. :)

No replies to the google group posting after a week. I don't know how long we ought to wait. Should we make the switch now? If it breaks for somebody then we can look at doing a multi-release jar.

Mention it one more time at next week's community meeting?