Rodin Platform 3.8 Release Notes - Revision history

Idir: /* Changes for plug-in developers */

2023-04-04T12:00:33Z

Changes for plug-in developers

← Older revision		Revision as of 12:00, 4 April 2023
Line 8:		Line 8:

	Rodin 3.8 is built on top of Eclipse 4.23 (2022-03), which requires Java 11.		Rodin 3.8 is built on top of Eclipse 4.23 (2022-03), which requires Java 11.

	~~There is no API change within Rodin Core.~~

	== Installing ==		== Installing ==

Idir: /* Fixed Bugs and Implemented Features */

2023-04-04T07:19:43Z

Fixed Bugs and Implemented Features

← Older revision		Revision as of 07:19, 4 April 2023
Line 58:		Line 58:

	Bugs		Bugs
	701: Translation occurs unexpectedly		701 Translation occurs unexpectedly
	778: Bad presentation of tactic profiles		778 Bad presentation of tactic profiles
	802: refresh Project Explorer		802 refresh Project Explorer
	803: rule DATATYPE_INDUCTION is unsound		803 rule DATATYPE_INDUCTION is unsound
	804: FormulaExtensionProviderRegistry does not catch exceptions		804 FormulaExtensionProviderRegistry does not catch exceptions
	805: IAE when loading proof		805 IAE when loading proof
	806: Missing UI indicator when running post tactic		806 Missing UI indicator when running post tactic
	807: Proof information view text cut off		807 Proof information view text cut off
	809: store options files in binary plug-ins		809 store options files in binary plug-ins
	811: hypothesis text cut off after instantiation input		811 hypothesis text cut off after instantiation input
	812: dropdown arrow invisible in Event-B editor on macOS		812 dropdown arrow invisible in Event-B editor on macOS
	813: Missing translation in input area of Proof control		813 Missing translation in input area of Proof control
	814: ArrayIndexOutOfBounds when typing extended predicates		814 ArrayIndexOutOfBounds when typing extended predicates
	816: ConcurrentModificationException in editor		816 ConcurrentModificationException in editor
	817: Exception when using external provers with theory...		817 Exception when using external provers with theory...

	Feature Requests		Feature Requests
	170: Bijection and cardinality		170 Bijection and cardinality
	292: Make FiniteHypBoundedGoal smarter		292 Make FiniteHypBoundedGoal smarter
	339: Add auto tactic for not empty set		339 Add auto tactic for not empty set
	343: Generalized Modus Ponens on natural integers		343 Generalized Modus Ponens on natural integers
	342: Generalized Modus Ponens on Boolean expressions		342 Generalized Modus Ponens on Boolean expressions
	365: Proof rule for finiteness of generalized union		365 Proof rule for finiteness of generalized union
	367: extend IParent in ISCContext		367 extend IParent in ISCContext
	371: apply equality and hide it		371 apply equality and hide it
	372: Proof by case on union membership		372 Proof by case on union membership
	376: Min and max definitions		376 Min and max definitions
	377: Apply modus ponens after instantiation		377 Apply modus ponens after instantiation
	382: Get free identifiers from a type environment		382 Get free identifiers from a type environment

	== Known Issues ==		== Known Issues ==

Idir: /* Fixed Bugs and Implemented Features */

2023-04-04T07:18:48Z

Fixed Bugs and Implemented Features

@@ Line 58: / Line 58: @@
 Bugs
-  TO DO
+: Translation occurs unexpectedly
 Feature Requests
-  TO DO
+: Bijection and cardinality
 == Known Issues ==

Idir: Created page with "== What's New in Rodin 3.8? == Rodin 3.8 brings several bug fixes. It also upgrades the underlying Eclipse to 4.23 (2022-03), which can be run by Java 11 Runtimes. Please no..."

2023-04-04T06:47:31Z

Created page with "== What's New in Rodin 3.8? == Rodin 3.8 brings several bug fixes. It also upgrades the underlying Eclipse to 4.23 (2022-03), which can be run by Java 11 Runtimes. Please no..."

New page

== What's New in Rodin 3.8? ==

Rodin 3.8 brings several bug fixes. It also upgrades the underlying Eclipse to 4.23 (2022-03), which can be run by Java 11 Runtimes.

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

=== Changes for plug-in developers ===

Rodin 3.8 is built on top of Eclipse 4.23 (2022-03), which requires Java 11.

There is no API change within Rodin Core.

== Installing ==

=== Downloading ===

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

=== Upgrading from a previous version of Rodin 3.x ===

If you run Rodin 3.1, 3.2, 3.3, 3.4, 3.5, 3.6 or 3.7, then you can upgrade your Rodin Platform by clicking Help > Check for Updates, then select Rodin 3.8 in the popup window and accept the licence terms. Note that the upgrading process can take quite a long time.

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

If you run Rodin 3.0 or prior, you cannot upgrade to 3.8. 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 11 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 ===

The Rodin application is not notarized. This means that when you download it from SourceForge, macOS will quarantine the application and tell you that it is broken. Just run the command <code>xattr -rc Rodin.app</code> in a Terminal to remove the quarantine tag.

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

Bugs
TO DO

Feature Requests
TO DO

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

=== Rodin is not notarized ===

Apple asks that all applications are notarized before they can be run since macOS Mojave. Unfortunately, we did not have time to put this in place for Rodin 3.8. We expect this to be solved for Rodin 3.9. See [[#macOS_specific_requirements|macOS requirements]] for a workaround.

== About ==

TODO

[[Category:Rodin Platform Release Notes]]