Rodin Platform 3.5 Release Notes - Revision history

Laurent: /* About */

2020-09-11T13:09:28Z

About

← Older revision		Revision as of 13:09, 11 September 2020
Line 126:		Line 126:
	== About ==		== About ==

	Rodin Platform with git commit: <code>~~d6d7f86fa~~</code><br/>		Rodin Platform with git commit: <code>74e0e4188</code><br/>
	User Release date : 2020/09/11.		User Release date : 2020/09/11.

	[[Category:Rodin Platform Release Notes]]		[[Category:Rodin Platform Release Notes]]

Laurent: /* macOS specific requirements */

2020-09-11T13:06:41Z

macOS specific requirements

← Older revision		Revision as of 13:06, 11 September 2020
Line 51:		Line 51:

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

			The Atelier B provers (not part of Rodin Platform, but very useful) do not work on macOS Catalina and newer. This is because they use a 32-bit binary program.

	=== Linux specific requirements ===		=== Linux specific requirements ===

Laurent: /* About */

2020-09-11T13:03:36Z

About

← Older revision		Revision as of 13:03, 11 September 2020
Line 124:		Line 124:
	== About ==		== About ==

	Rodin Platform with git commit: <code>~~bb0b4ee2e~~</code><br/>		Rodin Platform with git commit: <code>d6d7f86fa</code><br/>
	User Release date : 2020/09/11.		User Release date : 2020/09/11.

	[[Category:Rodin Platform Release Notes]]		[[Category:Rodin Platform Release Notes]]

Laurent: /* Disclaimer */

2020-09-11T09:35:25Z

Disclaimer

← Older revision		Revision as of 09:35, 11 September 2020
Line 107:		Line 107:

	See [http://sourceforge.net/p/rodin-b-sharp/bugs/785 Bug 785].		See [http://sourceforge.net/p/rodin-b-sharp/bugs/785 Bug 785].

			== Thanks ==

			A big thank you to
			* Yamine Ait-Ameur (IRIT) who lead the Event-B-Rodin-Plus initiative for resuming work on the Theory plug-in and the Rodin Platform.
			* Thai Son Hoang (University of Southampton) who made the port to Eclipse 2020-06.
			* Colin Snook (University of Southampton) and Michael Leuschel (University of Dusseldorf) for making sure that their plug-ins work with Rodin 3.5 and useful feedback.
			* Marc Pantel (IRIT) for bringing the macOS workaround.
			* Ilya Shchepetkov (Ivannikov Institute for System Programming) and Fredrik Öhrström for their useful feedback on the release candidate.
			* All users and contributors that I have forgotten to remember.

	== Disclaimer ==		== Disclaimer ==

	Since Rodin is continuously maintained, several unsoundness bugs which have been encountered were investigated and fixed. However, despite the total commitment of our teams to ensure the soundness of the platform, some unexpected and unknown soundness issues could remain. We would be grateful if you would report these issues to the [mailto:rodin-b-sharp-devel@lists.sourceforge.net development mailing list].		Since Rodin is continuously maintained, several unsoundness bugs which have been encountered were investigated and fixed. However, despite the total commitment of our teams to ensure the soundness of the platform, some unexpected and unknown soundness issues could remain. We would be grateful if you would report these issues to the [mailto:rodin-b-sharp-devel@lists.sourceforge.net development mailing list].

Laurent: /* Dedication */

2020-09-11T08:37:42Z

Dedication

← Older revision		Revision as of 08:37, 11 September 2020
Line 1:		Line 1:
	{{TOCright}}		{{TOCright}}

	== Dedication ==		== Dedication to Ken Robinson ==

	This release of the Rodin Platform is dedicated to the memory of Ken Robinson (University of New South Wales) who passed away the 5th of September 2020. Ken was a vibrant member of the Event-B community and an important user of the Rodin platform: he did not hesitate to complain loudly when the platform was not running as he expected. His regular feedback allowed us to greatly improve Rodin for the great good of the whole community. Ken was also the author of the [https://www3.hhu.de/stups/handbook/rodin/current/html/files/EventB-Summary.pdf Event-B Cheat Sheet] available with the Rodin handbook.		This release of the Rodin Platform is dedicated to the memory of Ken Robinson (University of New South Wales) who passed away the 5th of September 2020. Ken was a vibrant member of the Event-B community and an important user of the Rodin platform: he did not hesitate to complain loudly when the platform was not running as he expected. His regular feedback allowed us to greatly improve Rodin for the great good of the whole community. Ken was also the author of the [https://www3.hhu.de/stups/handbook/rodin/current/html/files/EventB-Summary.pdf Event-B Cheat Sheet] available with the Rodin handbook.

Laurent at 08:37, 11 September 2020

2020-09-11T08:37:12Z

← Older revision		Revision as of 08:37, 11 September 2020
Line 1:		Line 1:
	{{TOCright}}		{{TOCright}}

			== Dedication ==

			This release of the Rodin Platform is dedicated to the memory of Ken Robinson (University of New South Wales) who passed away the 5th of September 2020. Ken was a vibrant member of the Event-B community and an important user of the Rodin platform: he did not hesitate to complain loudly when the platform was not running as he expected. His regular feedback allowed us to greatly improve Rodin for the great good of the whole community. Ken was also the author of the [https://www3.hhu.de/stups/handbook/rodin/current/html/files/EventB-Summary.pdf Event-B Cheat Sheet] available with the Rodin handbook.

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

Laurent: /* About */

2020-09-11T08:05:18Z

About

← Older revision		Revision as of 08:05, 11 September 2020
Line 108:		Line 108:

	== About ==		== About ==
	~~TODO~~
	Rodin Platform with git commit: ~~6980ca1~~<br/>		Rodin Platform with git commit: <code>bb0b4ee2e</code><br/>
	User Release date : ~~2018~~/03/07.		User Release date : 2020/09/11.

	[[Category:Rodin Platform Release Notes]]		[[Category:Rodin Platform Release Notes]]

Laurent: /* Rodin is not notarized */

2020-09-11T08:02:38Z

Rodin is not notarized

← Older revision		Revision as of 08:02, 11 September 2020
Line 98:		Line 98:
	=== Rodin is not notarized ===		=== 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.5. We expect this to be solved for Rodin 3.6.		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.5. We expect this to be solved for Rodin 3.6. See [[#macOS_specific_requirements\|macOS requirements]] for a workaround.

	=== macOS in dark mode ===		=== macOS in dark mode ===

Laurent: /* Requirements - Compatibility */

2020-09-11T07:58:03Z

Requirements - Compatibility

← Older revision		Revision as of 07:58, 11 September 2020
Line 33:		Line 33:
	== Requirements - Compatibility ==		== Requirements - Compatibility ==

	* Configurations supported (and for which binaries are provided)		=== Supported operating systems ===
	** Linux 64-bit
	** Windows 64-bit
	** macOS 64-bit

	* ~~You need to have a~~ 64-bit ~~Java JRE (8 or later) installed on your computer. The Rodin application will not work with a previous version or with a 32~~-bit ~~JRE.~~		Rodin will work on the following operating systems
			* macOS 64-bit
			* Linux 64-bit
			* Windows 64-bit

	* 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].		=== Java Runtime requirement ===

	* Linux 64-bit:		You need to have a 64-bit Java JRE (version 8 or later) installed on your computer. The Rodin application will not work with a previous version or with a 32-bit JRE.
	~~: 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 64-bit:		=== macOS specific requirements ===
	: Atelier B provers 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.~~

	* macOS 64-~~bit:~~		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.

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

	== External plug-ins ==		== External plug-ins ==

Laurent: /* Requirements - Compatibility */

2020-09-11T07:43:29Z

Requirements - Compatibility

← Older revision		Revision as of 07:43, 11 September 2020
Line 52:		Line 52:
	* macOS 64-bit:		* macOS 64-bit:

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

	== External plug-ins ==		== External plug-ins ==