Rodin Platform 3.10 Release Notes - Revision history

Idir at 08:53, 6 July 2026

2026-07-06T08:53:01Z

← Older revision		Revision as of 08:53, 6 July 2026
Line 83:		Line 83:
	Fix FR #388: Rewrite rule for direct product		Fix FR #388: Rewrite rule for direct product
	Fix FR #405: Keep information about basic constructors		Fix FR #405: Keep information about basic constructors

			== Known Issues ==
			See [http://sourceforge.net/p/rodin-b-sharp/bugs known bugs on SourceForge].

			== About ==

			TODO

			[[Category:Rodin Platform Release Notes]]

Idir: /* Fixed Bugs and Implemented Features */

2026-07-06T08:52:19Z

Fixed Bugs and Implemented Features

Idir: /* Fixed Bugs and Implemented Features */

2026-07-06T08:51:30Z

Fixed Bugs and Implemented Features

← Older revision		Revision as of 08:51, 6 July 2026
Line 62:		Line 62:

	== Fixed Bugs and Implemented Features ==		== 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

Idir at 08:40, 6 July 2026

2026-07-06T08:40:17Z

← Older revision		Revision as of 08:40, 6 July 2026
Line 47:		Line 47:

	<code>xattr -rc Rodin.app</code>		<code>xattr -rc Rodin.app</code>

			=== Linux specific requirements ===

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

			=== 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: [http://sourceforge.net/projects/rodin-b-sharp/files/DefaultAuto_ML800 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 [http://sourceforge.net/projects/rodin-b-sharp/files/Font_%20Brave%20Sans%20Mono/0.12/ here].

			== Fixed Bugs and Implemented Features ==

Idir at 08:36, 6 July 2026

2026-07-06T08:36:31Z

← Older revision		Revision as of 08:36, 6 July 2026
Line 35:		Line 35:

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

			<code>xattr -rc Rodin.app</code>

Idir at 08:34, 6 July 2026

2026-07-06T08:34:26Z

← Older revision		Revision as of 08:34, 6 July 2026
Line 22:		Line 22:

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

Idir at 08:23, 6 July 2026

2026-07-06T08:23:00Z

← Older revision		Revision as of 08:23, 6 July 2026
Line 5:		Line 5:
	Please note that we only provide 64-bit binary versions of the Rodin platform.		Please note that we only provide 64-bit binary versions of the Rodin platform.

	=== Changes for ~~plug-in~~ developers ===		=== Changes for plugin developers ===

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

	[http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.10/ Download Rodin 3.10 now !]		[http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.10/ 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

Idir at 08:01, 6 July 2026

2026-07-06T08:01:42Z

← Older revision		Revision as of 08:01, 6 July 2026
Line 8:		Line 8:

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

			== Installing ==

			=== Downloading ===

			[http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.10/ Download Rodin 3.10 now !]

Idir: Created page with "== 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 plug-in developers === Rodin 3.10 is built on top of Eclipse 4.38 (2025-12), which requires Java 21."

2026-07-06T07:59:13Z

Created page with "== 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 plug-in developers === Rodin 3.10 is built on top of Eclipse 4.38 (2025-12), which requires Java 21."

New page

== 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 plug-in developers ===

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

← Older revision		Revision as of 08:52, 6 July 2026
Line 64:		Line 64:

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

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