Rodin Platform 3.10 Release Notes

What's New in Rodin 3.10?

Rodin 3.10 brings several bug fixes. It also upgrades the underlying Eclipse to 4.38 (2025-12), which can be run by Java 21 Runtimes.

Please note that we only provide 64-bit binary versions of the Rodin platform.

Changes for plugin developers

Rodin 3.10 is built on top of Eclipse 4.38 (2025-12), which requires Java 21.

Installing

Downloading

Download Rodin 3.10 now !

Upgrading from a previous version of Rodin 3.x

If you are running Rodin 3.1, 3.2, 3.3, 3.4, 3.5, 3.6, 3.7, 3.8, or 3.9, you can upgrade your Rodin Platform by clicking Help > Check for Updates, selecting Rodin 3.10 in the pop-up window, and accepting the license terms. Note that the upgrading process can take quite a long time.

Take care that Rodin 3.10 brings a new version of Eclipse. This means that once you have opened a workspace in Rodin 3.10, you will no longer be able to open it in a prior version of Rodin. Please consider copying your workspace for Rodin 3.10 to avoid any disaster.

If you are running Rodin 3.0 or earlier, you cannot upgrade to 3.10. You need to download the platform from SourceForge and reinstall your external plugins

Requirements - Compatibility

Supported operating systems

Rodin will work on the following operating systems

• macOS 64-bit
• Linux 64-bit
• Windows 64-bit

Java Runtime requirement

You need to have a 64-bit Java JRE (version 21 or later) installed on your computer. The Rodin application will not work with a previous version or with a 32-bit JRE.

macOS-specific requirements

For macOS, Rodin is available for both Intel (x86_64) and Apple Silicon (aarch64) architectures.

Please note that the SMT Provers plug-in is not yet available for Apple Silicon. If you need this plug-in, you must install the Intel version of Rodin for macOS together with an Intel-compatible JVM. Support for Apple Silicon is planned before the end of Rosetta support in macOS 28.

The Rodin application is not currently notarised. As a result, when downloaded from SourceForge, macOS may quarantine the application and report it as damaged or unable to be opened.

To remove the quarantine attribute, open a Terminal and run the following command:

xattr -rc Rodin.app

Linux specific requirements

Package libc6-amd64:i386 must be installed, in particular in order to run external prover binaries depending on the distribution, you could instead need these packages: lib32z1, lib32ncurses5, lib32bz2-1.0.

Windows specific requirements

Atelier B provers may work more slowly; it can cause ML to not automatically discharge some sequents that it discharges on windows 32-bit, due to its timeout. A workaround is to download a custom profile: DefaultAuto_ML800, then Window > Preferences > Event-B > Sequent Prover > Auto/Post Tactic > Profiles (tab) > Import..., point to the downloaded file, 'Select All' profiles (there are 2), OK. Then in 'Auto/Post Tactic' tab, select 'Default Auto Tactic Profile (ML 800)' profile for auto-tactics. It is the same as the 'Default Auto Tactic Profile', except ML has a longer timeout (800 ms). You can of course change this timeout by editing the 'ML (800)' profile.

We have not noticed this problem for Linux 64-bit, nor for other platforms; however if you do, the same workaround applies.

Math fonts

To enhance your proving experience, the eclipse font settings (size, aspect...) are available from the preferences (General > Appearance > Colors and Fonts > Rodin). These settings allow you to modify the properties set on the Event-B Keyboard Text Font which is used in many views of the Proving UI. However, to enjoy these functionalities, you need to install the Brave Sans Mono font on your system. You can download this font from the link here.

Fixed Bugs and Implemented Features

Bugs

Fix bug #838: Overflow of description in tactic profile editor
Fix bug #834: Impossible to type some datatype constructors
Fix bug #833: Clarify error message on invalid input...
Fix bug #835: Inconsistent handling of Proof Control's global input
Fix bug #837: Display issues in new tactic profile dialog
Fix bug #836: ClassCastException on replay of lae when goal changed
Fix bug #831: Issues with DatatypeHelper.computeId
Fix bug #832: Bug in translation of datatypes to set theory

Feature Requests

Fix FR #407: Pattern matching in ae
Fix FR #291: better type synthesis for datatype
Fix FR #410: More automatic proofs about finiteness
Fix FR #409: Avoid startup error when external provers timeout
Fix FR #408: Warn about implication in existential
Fix FR #404: Proofs on bounds of upto
Fix FR #389: Rewrite rule for parallel product
Fix FR #388: Rewrite rule for direct product
Fix FR #405: Keep information about basic constructors

Known Issues

See known bugs on SourceForge.

About

TODO