Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Migrate Ultimate to Java 21 and update framework components #672

Draft
wants to merge 61 commits into
base: dev
Choose a base branch
from

Conversation

bahnwaerter
Copy link
Member

This series of patches migrates Ultimate to Java 21 and updates the framework components to the following versions:

  • Eclipse 4.32
  • Eclipse CDT 11.6
  • Jetty 12

The patches also improve the build process by unifying build automation for Ant tasks in Eclipse and Maven builds. Specific Ant settings and the installation of the Tycho plugin in the Eclipse IDE are no longer required for building Ultimate. In addition, dependencies from the P2 repositories are resolved automatically. Therefore, only one PDE target platform file is now required for all supported target architectures.

@bahnwaerter
Copy link
Member Author

bahnwaerter commented Aug 10, 2024

The following tasks must be completed before the migration is completed:

  • Implementation and optimization:

    • Fix broken Jetty logging in the WebBackend by getting Jetty logging working via SLF4J facade provided by Pax Logging
    • Extend Jenkins build environment for Java 21 builds (install OpenJDK 21)
    • Create Eclipse IDE workspace settings file for Eclise IDE 2024-06 to simplify development setup
      • Include code formatter styles and complete styles with settings for new Java 21 language features
      • Add save actions to the workspace settings
  • Testing and quality assurance:

    • Check that an Eclipse and Maven build succeeds on Linux
    • Check that an Eclipse and Maven build succeeds on MacOS
    • Check that an Eclipse and Maven build succeeds on Windows
    • Check that a built Ultimate products run on Linux
    • Check that a built Ultimate products run on MacOS
    • Check that a built Ultimate products run on Windows
    • Check that a nightly build via Maven succeeds on Jenkins
    • Check that a nightly Sonar run via Maven succeeds on Jenkins
    • Ensure that the performance of Ultimate is not degraded by the migration (comparison through benchmark runs)
  • Documentation and explanation:

    • Add brief Ultimate build and run description to the project's README
    • Add brief development setup description to the project's README
    • Remove deprecated development setup instructions from the GitHub Wiki

@danieldietsch
Copy link
Member

I tried makeFresh.sh with Maven 3.9.8 and Java 21.04 on my Windows 10 machine and it built successfully.

@bahnwaerter
Copy link
Member Author

I can confirm that I'm able to build Ultimate on MacOS Ventura via Maven 3.9.8 and Eclipse 2024-06 and that the built products run as expected.

@maul-esel
Copy link
Contributor

👍 great work 🎉

From a quick test: I was able to set up an eclipse workspace, build and run Ultimate, and verify a simple program successfully (on Ubuntu).

Observations:

  • When first building, I had the usual ~4300 build errors, mostly in projects with parser generators (ASTBuilder, Library-BoogieAST, ...). Refreshing and rebuilding 2 or 3 times fixed them.
  • I ran into the usual problem that upon first launch, Z3 is not on the PATH. Do you know if it's possible to change the default environment for run configurations, such that we can initialize that correctly? (Of course, this would be a very specific bonus feature).

@maul-esel
Copy link
Contributor

One additional observation: The startup time of Debug-EA.product is currently extremely high for me. I tried it twice just now, once it took 37s, the second time 30s!

@schuessf
Copy link
Contributor

One additional observation: The startup time of Debug-EA.product is currently extremely high for me. I tried it twice just now, once it took 37s, the second time 30s!

I experienced the same issue.

@bahnwaerter
Copy link
Member Author

bahnwaerter commented Aug 13, 2024

I ran into the usual problem that upon first launch, Z3 is not on the PATH. Do you know if it's possible to change the default environment for run configurations, such that we can initialize that correctly? (Of course, this would be a very specific bonus feature).

Great to hear that you are able to build Ultimate successfully using the Eclipse IDE. That's a good point and I think it should be possible by either adjust the launch configuration or (if available) adjust a global setting automatically (through our upcoming idea of a importing a preconfigured workspace settings file).

@bahnwaerter
Copy link
Member Author

bahnwaerter commented Aug 13, 2024

One additional observation: The startup time of Debug-EA.product is currently extremely high for me. I tried it twice just now, once it took 37s, the second time 30s!

I experienced the same issue.

I can report the same observation. Currently, I don't know the reason for that performance issue but it seems like Eclipse executes the built product without any delay directly. But then framework startup slows down the execution ...

@bahnwaerter bahnwaerter force-pushed the wip/mb/framework-migration-java-21 branch from eedd9c5 to 4b570c8 Compare August 20, 2024 08:52
@bahnwaerter bahnwaerter force-pushed the wip/mb/framework-migration-java-21 branch 3 times, most recently from 040386b to d2ac62f Compare October 21, 2024 00:38
@bahnwaerter
Copy link
Member Author

After further investigation, the following error seems to be present when reading or writing *.graphml witnesses using the JUNG library:

[de.uni_freiburg.informatik.ultimate.core: NoClassDefFoundError: edu/uci/ics/jung/graph/DirectedGraph: de.uni_freiburg.informatik.ultimate.witnessparser.WitnessAutomatonConstructor.getGraphTransformer(WitnessAutomatonConstructor.java:250)]

For example, if a DirectedSparseGraph is created in the WitnessAutomatonConstructor on line 256, the DirectedGraph interface in the package edu.uci.ics.jung.graph must be loaded for the internal data structures. The Equinox framework tries to load this interface from the JUNG graph implementation module (jung-graph-impl). However, the interface is not stored there, as a package with the same name is also provided in the JUNG API module (jung-api). All data structures are located there, but they cannot be resolved from the jung-graph-impl module due to the package name clash.

The problem that the edu.uci.ics.jung.graph package appears in both separate modules and causes problems while resolving dependencies has already been reported in the JUNG project. Unfortunately, this issue will no longer be fixed in JUNG version 2.

bahnwaerter and others added 29 commits November 4, 2024 16:01
This change reverts the following commits:

  - dc22a55: "disable sonar until further notice"
  - 6ba0640: "use JDK 17 for sonar run"
  - 7843020: "fix indentation"
  - 76e8aa7: "add tool section"
This should drastically simplify the initial setup.
These settings include:
* the target platform
* the workspace dir (is this still necessary?)
* the configuration of the warnings/errors/etc.
* the configuration of the Java formatter (from coding-conventions/eclipse-java-formatter.xml; has slightly changed; might be removed)
* the save actions (slightly more than before; also updated for new Java features)

The last two points modify our coding conventions (but also "force" everyone to use them), so existing source files might have to be modified.
@bahnwaerter bahnwaerter force-pushed the wip/mb/framework-migration-java-21 branch from 7eef340 to f6ca609 Compare November 4, 2024 15:08
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
build system / releases dependencies Pull requests that update a dependency file enhancement
Projects
None yet
Development

Successfully merging this pull request may close these issues.

8 participants