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
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
