Event-B - User contributions [en-gb]

Template:Main Page/Community

2026-01-09T16:17:06Z

Laurent:

<noinclude>
== Displayed as follow on the Main Page ==
<div style="margin:0;width:43%;border:1px solid #AAAAAA;background:#FFFFFF">
</noinclude>
[https://wiki.event-b.org/index.php/Rodin_Workshop_2026 Rodin 2026 -- The 13th Rodin User and Developer Workshop on 18-19 May 2026 (co-located with ABZ2026 and FM2026).]

[https://wiki.event-b.org/index.php/Rodin_Workshop_2025 Rodin 2025 -- The 12th Rodin User and Developer Workshop on 10 June 2025 (co-located with ABZ2025).]

[https://wiki.event-b.org/index.php/Rodin_Workshop_2024 Rodin 2024 -- The 11th Rodin User and Developer Workshop on 25 June 2024 (co-located with ABZ2024).]

[https://wiki.event-b.org/index.php/Rodin_Workshop_2023 Rodin 2023 -- The 10th Rodin User and Developer Workshop on 30 May 2023 (co-located with ABZ2023).]

[https://wiki.event-b.org/index.php/Rodin_Workshop_2021 Rodin 2021 -- The 9th Rodin User and Developer Workshop on 8 June 2021 (co-located with ABZ2021).]

[http://wiki.event-b.org/index.php/Rodin_Workshop_2020 Rodin 2020 (POSTPONED TO 2021) -- The 8th Rodin User and Developer Workshop on 26 May 2020 (co-located with ABZ2020).]

[http://research.nii.ac.jp/eventb2016/ The Event-B Day at NII. November 21, 2016. NII, Tokyo, Japan.]

[http://wiki.event-b.org/index.php/Rodin_Workshop_2016 Rodin 2016 Workshop on 23-24 May 2016 co-located with ABZ2016.]

[http://www.cdcc.faw.jku.at/ABZ2016/ ABZ 2016: The 5th International ABZ Conference, for ASM, Alloy, B, TLA, VDM, Z May 23-27, 2016 Linz, Austria]

[http://research.nii.ac.jp/eventb2014/ The Event-B Day at NII. October 31, 2014. NII, Tokyo, Japan.]

[http://wiki.event-b.org/index.php/Rodin_Workshop_2014 Rodin 2014 Workshop on 2+3 June 2014 co-located with ABZ2014.]

[http://link.springer.com/book/10.1007/978-3-642-33170-1/page/1 The DEPLOY book was published by Springer in July 2013: Industrial deployment of system engineering methods providing high dependability and productivity, A. Romanovsky, M. Thomas (Eds). ISBN: 978-3-642-33169-5]


----

[[Mailing lists]] - Rodin related mailing lists.

[[Rodin Platform Releases]] - Track releases.

[[Bugs and Feature Requests]] - Report a bug or request a new feature.

[[Plug-in_Wishlist|Plug-in Wishlist]]

[http://www.fm4industry.org FAQ about the use and the impact of formal engineering methods in Industry]

----

''Do not hesitate to improve this wiki.'' You may find some help within the following pages:

[[Help:Contents|Wiki Help]] - Some technical documentation about this wiki.

[[EB:VP|Village Pump]] - Ask your questions and keep track of the main wiki events.

[[Special:Recentchanges|Recent Changes]] - Monitor the wiki activity.

[[Test area|Test Area]] - Wiki editing is simple. Try by yourself.
<noinclude>
</div>
[[Category:Main page templates|Community]]
</noinclude>

Rodin Workshop 2024

2024-01-18T09:13:48Z

Laurent: /* Organisers */

==11th Rodin User and Developer Workshop==

The 11th Rodin User and Developer Workshop, 25th June, 2024, Bergamo, Italy

Event-B is a formal method for system-level modelling and analysis. The
Rodin Platform is an Eclipse-based toolset for Event-B that provides
effective support for modelling and automated proof. The platform is open
source and is further extendable with plug-ins. A range of plug-ins have
already been developed.

The 11th Rodin workshop will be collocated with the [https://abz-conf.org/site/2024/ ABZ 2024 Conference].

The purpose of this workshop is to bring together existing and potential
users and developers of the Rodin toolset and to foster a broader community
of Rodin users and developers.

For Rodin users the workshop will provide an opportunity to share tool
experiences and to gain an understanding of on-going tool developments.
For plug-in developers the workshop will provide an opportunity to showcase
their tools and to achieve better coordination of tool development effort.

== Call For Papers ==
If you are interested in giving a presentation or plug-in demonstration at the Rodin workshop please submit an abstract. We will endeavour to accommodate all submissions that are clearly relevant to Rodin and Event-B.
The proceedings of the workshop will be available as a technical report at the University of Southampton.

;Submission deadline : 31st May 2024
;Submission to: rodin@ecs.soton.ac.uk
;Submission format : extended abstract (1 to 2 page description with title and authors and references - PDF)
;Submission Instructions: Please indicate within the text whether the submission is about tool usage or tool development.

==Registration==
To register for the workshop, please follow the instructions on the [https://abz-conf.org/site/2024/registration/ ABZ 2024 registration page].

== Organisers ==
[https://www.southampton.ac.uk/people/5xb2d2/doctor-asieh-salehi-fathabadi Asieh Salehi Fathabadi], Senior Research Fellow, University of Southampton
[https://tnda.eu/en/the-team/ Guillaume Verdier], Université de Paris-Est Créteil
[https://www.cs.hhu.de/lehrstuehle-und-arbeitsgruppen/softwaretechnik-und-programmiersprachen/unser-team/team/rutenkolk Kristin Rutenkolk], Heinrich Heine University Düsseldorf
[https://sites.google.com/site/singhnne/ Neeraj Kumar Singh], Associate Professor, INPT-ENSEEIHT / IRIT, University of Toulouse
[https://www.jku.at/en/institute-of-software-systems-engineering/about-us/team/sebastian-stock/ Sebastian Stock], Junior Researcher, Johannes Kepler University
Laurent Voisin, R&D Manager, [https://www.systerel.fr/en/ Systerel]

Rodin Workshop 2024

2024-01-18T09:13:17Z

Laurent: /* Organisers */ Added Kristin

==11th Rodin User and Developer Workshop==

The 11th Rodin User and Developer Workshop, 25th June, 2024, Bergamo, Italy

Event-B is a formal method for system-level modelling and analysis. The
Rodin Platform is an Eclipse-based toolset for Event-B that provides
effective support for modelling and automated proof. The platform is open
source and is further extendable with plug-ins. A range of plug-ins have
already been developed.

The 11th Rodin workshop will be collocated with the [https://abz-conf.org/site/2024/ ABZ 2024 Conference].

The purpose of this workshop is to bring together existing and potential
users and developers of the Rodin toolset and to foster a broader community
of Rodin users and developers.

For Rodin users the workshop will provide an opportunity to share tool
experiences and to gain an understanding of on-going tool developments.
For plug-in developers the workshop will provide an opportunity to showcase
their tools and to achieve better coordination of tool development effort.

== Call For Papers ==
If you are interested in giving a presentation or plug-in demonstration at the Rodin workshop please submit an abstract. We will endeavour to accommodate all submissions that are clearly relevant to Rodin and Event-B.
The proceedings of the workshop will be available as a technical report at the University of Southampton.

;Submission deadline : 31st May 2024
;Submission to: rodin@ecs.soton.ac.uk
;Submission format : extended abstract (1 to 2 page description with title and authors and references - PDF)
;Submission Instructions: Please indicate within the text whether the submission is about tool usage or tool development.

==Registration==
To register for the workshop, please follow the instructions on the [https://abz-conf.org/site/2024/registration/ ABZ 2024 registration page].

== Organisers ==
[https://www.southampton.ac.uk/people/5xb2d2/doctor-asieh-salehi-fathabadi Asieh Salehi Fathabadi], Senior Research Fellow, University of Southampton
[https://tnda.eu/en/the-team/ Guillaume Verdier], Université de Paris-Est Créteil
[https://www.cs.hhu.de/lehrstuehle-und-arbeitsgruppen/softwaretechnik-und-programmiersprachen/unser-team/team/rutenkolk Kristin Rutenkolk], Heinrich Heine University Düsseldorf, Germany
[https://sites.google.com/site/singhnne/ Neeraj Kumar Singh], Associate Professor, INPT-ENSEEIHT / IRIT, University of Toulouse
[https://www.jku.at/en/institute-of-software-systems-engineering/about-us/team/sebastian-stock/ Sebastian Stock], Junior Researcher, Johannes Kepler University
Laurent Voisin, R&D Manager, [https://www.systerel.fr/en/ Systerel]

How to create Rodin projects programmatically

2023-08-21T15:19:43Z

Laurent:

The code snippets on this page are derived from the UML-B plugin 'ac.soton.umlb.eventB', package 'generator'.
You can find this package in the Rodin projects sourceforge SVN repository : https://sourceforge.net/p/rodin-b-sharp/svn/HEAD/tree/trunk/UML-B/ac.soton.umlb.eventB/src/ac/soton/umlb/eventB/generator/

[Some of the code could be improved wrt the use of monitors. An explanation of some of the parameters in the Rodin API could be added]

== How to create a Rodin Project ==
Here is a method to create a Rodin project of a given name. (This method overwrites any existing Rodin project of that name).
The project handle is retrieved from the rodin database. if the project does not exist, it is created using the handle.
The project is opened. The project is given the Rodin 'nature' (if not already).
The project is set to derived (this is not strictly necessary but it can be used to distinguish projects that the user has created from ones that have been created programmatically).

public static IRodinProject createRodinProject(final String projectName) {
final IWorkspace workspace = ResourcesPlugin.getWorkspace();
try {
final IRodinDB rodinDB = RodinCore.valueOf(workspace.getRoot());
final IRodinProject rodinProject = rodinDB.getRodinProject(projectName);
final IProject project = rodinProject.getProject();
if (!project.exists()) project.create(null);
project.open(null);

// add the rodin nature if it isn't already there
final IProjectDescription description = project.getDescription();
final String[] natures = description.getNatureIds();
boolean alreadyRodin = false;
for (int i = 0; i < natures.length; ++i)
if (RodinCore.NATURE_ID.equals(natures[i])) {
alreadyRodin = true;
break;
}
if (!alreadyRodin) { // Add the Rodin nature
final String[] newNatures = new String[natures.length + 1];
System.arraycopy(natures, 0, newNatures, 0, natures.length);
newNatures[natures.length] = RodinCore.NATURE_ID;
description.setNatureIds(newNatures);
project.setDescription(description, null);
}
project.setDerived(true); // mark the project as derived (this could be used to distinguish user editable projects
return rodinProject;
} catch (final CoreException e) {
.... exception code ....
}
}

Once you have created a Rodin Project you may want to call its save method to save it. Since this method makes changes to the workspace, you need to call it from a WorkspaceRunnable.
For Example:-

RodinCore.run(new IWorkspaceRunnable() {
public void run(final IProgressMonitor monitor) throws CoreException{
monitor.beginTask("",10);
rodinProject=createRodinProject(projectName);
rodinProject.save(null, true);
monitor.done();
}
},null);

==How to create a Rodin File construct (e.g. Machine, Context)==
Here is a method to create a new Rodin File construct of a given filename in the given Rodin project and with a given comment.
Note that the filename should include the correct extension (e.g. ".bum" for a Machine).
The handle is retrieved from the Rodin project and used to create the new Rodin file.
The corresponding resource is set to derived to indicate that it was generated programmatically.
The comment is added to the Rodin File.

public static IRodinFile createRodinConstruct(final String filename, final IRodinProject rProject, final String comment) {
if (rProject == null)
return null;
try {
final IRodinFile rodinFile = rProject.getRodinFile(filename);
rodinFile.create(true, null);
rodinFile.getResource().setDerived(true); // mark the file as derived
if (rodinFile instanceof ICommentedElement)
if (comment != null && !comment.trim().equals(""))
((ICommentedElement) rodinFile).setComment(comment, null);
return rodinFile;
} catch (final Exception e) {
.... exception code ....
}
}

As with the Rodin project above, if you want to save the created construct, you should do this from a WorkspaceRunnable.

==How to create a Rodin element==
Here is a method to create a new Rodin element of a given type and name in the given Rodin element and Rodin File and with a given comment.
The handle is retrieved from the parent element and used to create the new Rodin element. Depending on the type of the new Rodin element, the name is used as the
label, identifier, or abstract event label. The comment is set if the element type owns a comment.

public static IInternalElement createRodinElement(
final IInternalElementType type,
final String name,
final IInternalElement parent,
final IRodinFile rodinFile,
final String comment) {
if (parent == null) return null;
try {
final IInternalElement rodinEl = parent.getInternalElement(type, name)
rodinEl.create(null, null);
if (rodinEl instanceof ILabeledElement)
((ILabeledElement) rodinEl).setLabel(name, null);
if (rodinEl instanceof IIdentifierElement)
((IIdentifierElement) rodinEl).setIdentifierString(name, null);
if (rodinEl instanceof ICommentedElement)
if (comment != null)
((ICommentedElement) rodinEl).setComment(comment,null);
if (rodinEl instanceof IRefinesEvent)
((IRefinesEvent) rodinEl).setAbstractEventLabel(name, null);
return rodinEl;
} catch (final Exception e) {
.... exception code ....
}
}

This method is called passing the appropriate element type which can be obtained from the Rodin element class. For example an Invariant can be created like this:-

IInvariant invariant = (IInvariant) createRodinElement(IInvariant.ELEMENT_TYPE, invariantName, rodinFile, rodinFile, comment);

==How to set attributes of a Rodin Element==

To set attributes of a Rodin Element, use the appropriate methods of the element (depending on the element type).
For example:-

invariant.setPredicateString(myPredicateString,null);

[[Category:Developer documentation]]
[[Category:Rodin Platform]]

Rodin Workshop 2023

2023-03-09T14:48:55Z

Laurent: /* Organisers */ Add Neeraj

==10th Rodin User and Developer Workshop==

The 10th Rodin User and Developer Workshop, 30th May, 2023, Nancy, France

Event-B is a formal method for system-level modelling and analysis. The
Rodin Platform is an Eclipse-based toolset for Event-B that provides
effective support for modelling and automated proof. The platform is open
source and is further extendable with plug-ins. A range of plug-ins have
already been developed.

The 10th Rodin workshop will be collocated with the [https://abz2023.loria.fr/ ABZ 2023 Conference].

The purpose of this workshop is to bring together existing and potential
users and developers of the Rodin toolset and to foster a broader community
of Rodin users and developers.

For Rodin users the workshop will provide an opportunity to share tool
experiences and to gain an understanding of on-going tool developments.
For plug-in developers the workshop will provide an opportunity to showcase
their tools and to achieve better coordination of tool development effort.

==Call for Abstracts==

If you are interested in giving a presentation at the Rodin workshop or have a plug-in to demonstrate, send a short abstract (1 or 2 pages PDF) to [mailto:rodin@ecs.soton.ac.uk?subject=RodinWorkshop2023%20Contribution rodin@ecs.soton.ac.uk] by 28th April 2023 with subject '''[RodinWorkshop2023] Contribution''', indicating whether it is a tool usage or tool development presentation.

We will endeavour to accommodate all submissions that are clearly relevant to Rodin and Event-B.

The proceedings of the workshop will be available as a technical report at the University of Southampton.

=== Organisers ===
Dana Dghaym, University of Southampton, UK
Neeraj Kumar Singh, INPT-ENSEEIHT / IRIT, University of Toulouse, France
Laurent Voisin, Systerel, France
Fabian Vu, Heinrich Heine University Düsseldorf, Germany

Rodin Platform 3.5.0 External Plug-ins

2021-02-10T14:20:41Z

Laurent: /* Atelier B Update Site */

==== Rodin Update Site ====

Available from http://rodin-b-sharp.sourceforge.net/updates

{{SimpleHeader}}
|-
! scope=col | || Plug-in name || Version || Status || MCV* || Release Date || Contact || Additional info
|-
| || [[SMT_Plug-in | SMT Solvers ]] || 1.4.0 || available || || 15th March 2016|| [mailto:lvoisin@users.sourceforge.net Laurent Voisin] || Automatic prover using SMT solvers
|-
| || Relevance Filter || 1.1.1 || available || ?.x.x || || || Improves chance of automatic proof by selecting relevant hypotheses
|-
| || [[B2Latex | B2Latex export]] || 0.7.0 || available || 2.5.x || 27th May 2015 || [mailto:lvoisin@users.sourceforge.net Laurent Voisin] || generates a Latex documentation of the Event-B
|-
| [[Image:Rose.gif|30px]]||[[Rose_(Structured)_Editor|Rose editor]] || 1.7.0 || available || 3.x.x || 4 Nov 2018 || [mailto:umlb@soton.ac.uk umlb] || Tree-structured editor for Event-B EMF that handles extensions without modification. Mainly useful for Plug-in developers.
|-
| CODA || CODA Component Diagrams || 6.0.1 || available || 3.x.x || ? || [mailto:umlb@soton.ac.uk umlb] || Component diagrams with timed channels. ('''Not compatible with latest UML-B.''' Will be up-issued on Soton update site.)
|-
| CODA || CODA Simulator for Component Diagrams || 3.0.1 || available || 3.x.x || ? || [mailto:umlb@soton.ac.uk umlb] || Component based simulation. ('''Not compatible with latest UML-B.''' Will be up-issued on Soton update site.)
|-
| [[Image:Project diagram icon s.png|30px]]||[[Project_Diagram|Project Diagram]]|| 1.0.1 || available || 3.x.x || 1st Feb. 2015 || [mailto:umlb@soton.ac.uk umlb] || Machine - Context relationship diagram. ('''Not compatible with latest UML-B.''' Will be up-issued on Soton update site.)
|-
| [[Image:Cmp_mch_obj.gif|20px]] ||[[Parallel_Composition_using_Event-B | Shared Event Composition]] || 1.7.1 || not checked || || 5th July 2017 || [mailto:umlb@soton.ac.uk umlb] || Compatible with Rodin 3.x.x
|-
| [[Image:DecompositionPlug-in_logo.png|30px]] || [[Decomposition Plug-in User Guide | Decomposition]] || 1.3.1 || not checked || || 4th July 2017 || [mailto:umlb@soton.ac.uk umlb] || Compatible with Rodin 3.x.x
|-
| ||[[Refactoring Framework | Refactory ]]|| 1.3.0 || not checked|| 3.x.x || 6th May 2014 || [mailto:umlb@soton.ac.uk umlb] || Compatible with Rodin 3.0.x.
|-
| || [[Theory Plug-in| Theory Plug-in]] || 3.0.0 || not checked|| || 17th Dec 2014|| [mailto:lvoisin@users.sourceforge.net Laurent] ||
|-.x
| || [[Code Generation Activity | Code Generation]] || 0.2.5 || not checked|| || 29th Aug. 2013|| [mailto:umlb@soton.ac.uk umlb] || For Java, Ada, and OpenMP C code
|-.x
|-
| || [[Isabelle for Rodin]] || || not checked || 2.x.x || || ||
|-
| || [[Pattern | Pattern]] || 0.9.0 || not checked || 3.x.x || 13th March 2015 || [mailto:tshoang@users.sourceforge.net Thai Son Hoang] ||
|-
| || [[Event-B Qualitative Probability User Guide | Qualitative Probability]] || 0.2.3 || not working || 3.x.x || 9th October 2015 || [mailto:tshoang@users.sourceforge.net Thai Son Hoang] || Needs updating to be compatible with changes in Rodin 3.5
|-
| || [[Generic Instantiation Plug-in User Guide | Generic Instantiation (Soton)]] || 1.0.1 || not checked || || 05th March 2013 || [mailto:asf08r@ecs.soton.ac.uk Asieh] ||
|-
| ||[[Records|Records]] || 2.0.0 || not checked || 2.x.x || 16th Oct. 2010 || [mailto:umlb@soton.ac.uk umlb] || no longer supported - use CamilleX instead
|-
| ||[[EMF_Compare_Editor_installation|Teamwork]] || 1.2.0 || not checked || 3.2.x || 5th Sept. 2016 || [mailto:umlb@soton.ac.uk umlb] || No longer supported - use CamilleX instead. Provides a synchronised copy of Machines and Contexts for committing into a repository.
|-
| [[Image:Umlb32.gif|30px]] || [[UML-B|UML-B]] || 2.3.0 || not checked || 3.x.x || 18th Oct. 2014 || [mailto:umlb@soton.ac.uk umlb] || no longer supported - use new UML-B from Soton update site instead
|-
| [[Image:Umlb32.gif|30px]] ||[[UML-B_-_Statemachine_Animation|UML-B Statemachine Animation]] || 1.3.0 || not checked || 3.x.x || 18th Oct. 2014 || [mailto:umlb@soton.ac.uk umlb] || no longer supported - use new UML-B from Soton update site instead
|-
| [[Image:IUMLB_big.png|30px]] ||iUML-B plugins || || not checked || 3.x.x || || [mailto:umlb@soton.ac.uk umlb] || New versions are now available on the Soton Update Site.
|}

==== Atelier B Update Site ====

Available from http://methode-b.com/update_site/atelierb_provers

{{SimpleHeader}}
|-
! scope=col | || Plug-in name || Version || Status || MCV* || Release Date || Contact || Additional info
|-
| || Atelier B provers || 2.3.0 || available || 3.3.0 || 2 Dec 2020 || ||
|}

==== ProB Update Site ====

Available from http://www.stups.hhu.de/prob_updates_rodin3

{{SimpleHeader}}
|-
! scope=col | || Plug-in name || Version || Status || MCV* || Release Date || Contact || Additional info
|-
| || ProB || 3.0.10 || available || 3.5.0 || 4 Sep 2020 || || The ProB animator and model checker
|-
| || ProB (Dis)Prover || 3.0.9 || available || 3.5.0 || 4 Sep 2020 || || The ProB counter-example finder and prover
|-
| || ProB Symbolic constants support || 3.0.9 || available || 3.5.0 || 4 Sep 2020 || ||
|}

==== Southampton Releases Update Site ====

Available from http://eventb-soton.github.io/updateSite/releases
{{SimpleHeader}}
|-
! scope=col | || Plug-in name || Version || Status || MCV* || Release Date || Contact || Additional info
|-
| [[Image:CamilleX.png|CmX]] || [[CamilleX|CamilleX]] || 2.0.2 || new release || 3.4.x || 21 Jan 2021 || [mailto:T.S.Hoang@ecs.soton.ac.uk Thai Son Hoang] || CamilleX provides text editors for Event-B models and support modelling mechanisms such as machine inclusion.
|-
| [[Image:IUMLB_big.png|30px]] || [[Event-B_Classdiagrams|UML-B Class Diagrams]] || 3.0.0 || new release || 3.x.x || 11 Sept 2020 || [mailto:umlb@soton.ac.uk umlb] || UML-B Class diagrams translate into Event-B Machines.
|-
| [[Image:IUMLB_big.png|30px]] || [[Event-B_Statemachines|UML-B State-machines]] || 4.0.1 || new release || 3.x.x || 13 Aug 2020 || [mailto:umlb@soton.ac.uk umlb] || UML-B State-machines translate into Event-B Machines.
|-
| [[Image:IUMLB_big.png|30px]] ||[[Event-B_Statemachines|UML-B State-machine Animation]] || 3.0.0 || new release || 3.x.x || 13 Aug 2020 || [mailto:umlb@soton.ac.uk umlb] || Animate UML-B State-machines. Compatible with UML-B statemachines 4.x.x and ProB 3.0.x.
|-
| [[Image:IUMLB_big.png|30px]] ||[[Scenario Checker|Scenario Checker]] || 0.0.0 || new release || 3.4.x || 31 July 2020 || [mailto:umlb@soton.ac.uk umlb] || Validation tool for recording and replaying scenarios
|}

The following framework plug-ins are also provided on the Southampton Releases Update Site. These plugins are installed automatically when required and are not usually installed explicitly by users.
{{SimpleHeader}}
|-
! scope=col | || Plug-in name || Version || Status || MCV* || Release Date || Contact || Additional info
|-
| ||[[EMF_framework_for_Event-B|Event-B EMF framework]] || 6.1.0 || new release || 3.x.x || 4 July 2020 || [mailto:umlb@soton.ac.uk umlb] || Provided for plug-in developers. End users should not need to install this framework. It will be installed automatically by other plug-ins as required.
|-
| ||[[Generic_Event-B_EMF_extensions|Event-B EMF extensions]] || 6.1.0 || new release || 3.x.x || 4 July 2020 || [mailto:umlb@soton.ac.uk umlb] || Provided for plug-in developers. End users should not need to install this framework. It will be installed automatically by other plug-ins as required.
|-
| ||[[Generic_Event-B_EMF_extensions|UML-B diagrams]] || 8.0.1 || new release || 3.2.x || 13 Aug 2020 || [mailto:umlb@soton.ac.uk umlb] || Provided for plug-in developers. End users should not need to install this framework. It will be installed automatically by other plug-ins as required.
|-
| ||[[ProB Support|ProB Support]] || 0.0.0 || new release || 3.4.x || 28 July 2020 || [mailto:umlb@soton.ac.uk umlb] || Provided for plug-in developers. End users should not need to install this framework. It will be installed automatically by other plug-ins as required.
|}

Building Rodin Headless

2020-09-11T15:50:27Z

Laurent: /* Last operations to perform */

This page documents the procedure followed for building the binary packages of the Rodin platform that are distributed on SourceForge. The build is done in two steps
# Fetch the sources from the repository and make a source archive with them.
# Build the platform headless from this set of sources using Apache Ant.

==Requirements==
* [http://maven.apache.org/ Apache Maven 3] should be installed on the platform that will run the build.

==Pre Build Verifications==

Before building, several checks have to be made in the sources:
* clean build all RodinCore plug-ins, so that generated files are regenerated using repository sources
* JUnit tests are OK
* versions of plug-ins, features and product obey [http://wiki.eclipse.org/Version_Numbering Eclipse versioning policy]
* API Tooling build against previous Rodin release produces no errors on any plug-in
* Rodin build process is managed using Apache maven and Tycho. One should verify that maven artifact versions match the plug-in versions (defined in plug-in MANIFEST.MF files)
* the correct Eclipse version is referenced in the p2 configuration (org.rodinp.platform/Rodin.p2.inf)

addRepository(type:0,location:http${#58}//download.eclipse.org/releases/neon,name:Neon Update Site);\
addRepository(type:1,location:http${#58}//download.eclipse.org/releases/neon,name:Neon Update Site);\

and matches the one defined whithin the parent pom file (<tt>org.eventb.parent/pom.xml</tt>) :

<repository>
<id>oxygen-4.7</id>
<layout>p2</layout>
<url>http://download.eclipse.org/eclipse/updates/4.7/</url>
</repository>

* the correct link for the Rodin Handbook is provided in the parent pom file (<tt>org.eventb.parent/pom.xml</tt>) :
<repository>
<id>handbook</id>
<layout>p2</layout>
<url>http://handbook.event-b.org/updatesite</url>
</repository>

* branding plug-ins display the correct Eclipse version (text information found in several about.properties/plugin.properties files)
* documentation is up to date for /org.rodinp.platform/html/root.html
* generated documentation matches latest wiki sources for <tt>org.eventb.keyboard/doc</tt>
* make sure a valid destination folder is specified in <tt>org.eventb.parent/pom.xml</tt>. This destination folder will host the built platforms, the update-site and the development target platform.
Example :
<www-basedir>/tmp/rodin-build/rodin-3.0</www-basedir>

The variable used in Maven scripts is then <tt>${www-basedir}</tt>

When everything works, any changes to the sources made during this verification process are pushed to the Source Forge repository.

'''N.B.''' Several information are defined and manipulated for each build. Here below is a memo to help understand them :
# the platform version which defines a milestone identifier for the Rodin platform. Example of platform versions are <tt>1.0</tt> and <tt>2.3RC1</tt>.
# the Git commit number which permits to know very precisely which source versions are used for the build.
# the Git branch from which the commit can be checked out
# the full platform version used for provisioning, and which is the user-visible version which is displayed in ''About Rodin Platform''. This version is made of the platform version and the commit number, separated by a dot. Example of full versions are <tt>2.8RC1.bh1420</tt> and <tt>2.8.1.hgf52f65</tt>.

==Fetching Sources==

Create a directory that will contain the sources and be used to build the platform. 
Example :
mkdir Rodin3.0BuildDirectory

and go to this directory :
cd Rodin3.0BuildDirectory

Fetch sources from Git in the current directory :
<nowiki>git clone git://git.code.sf.net/p/rodin-b-sharp/rodincore .</nowiki>

==Building the Platform==

To build the platform, you just need to run the script below (available from org.rodinp.releng/scripts/run-maven.sh) :

<nowiki> #!/bin/sh
###############################################################################
# Copyright (c) 2013 Systerel and others.
# All rights reserved. This program and the accompanying materials
# are made available under the terms of the Eclipse Public License v1.0
# which accompanies this distribution, and is available at
# http://www.eclipse.org/legal/epl-v10.html
#
# Contributors:
# Systerel - initial API and implementation
###############################################################################
SCRIPT=`readlink -m -n $0`
SCRIPTS_DIR=`dirname $SCRIPT`
MAIN_DIR=`readlink -m -n $SCRIPTS_DIR/../..`

cd $MAIN_DIR

GIT_COMMIT=`git log -1 --format='%h'`
echo "Building Rodin with Maven for git commit: $GIT_COMMIT"
mvn clean install -Dgit-commit=$GIT_COMMIT $@ # -DskipTests -fae </nowiki>

==Post Build Verifications==

When the build worked, the destination directory (defined by variable <tt>${www-basedir}</tt>) contains zipped archives for all platforms, the update site, and the target platform for plug-in development.
For each of them, check that:
* "rodin" binary is an executable file (for Linux and Mac)
* the version appearing in ''About Rodin platform'' is correctly defined
* a directory "dropins" exists at the root (under "rodin", among "features", plugins", ...)
* in "configuration/org.eclipse.equinox.simpleconfigurator/bundles.info", plug-in "org.eclipse.equinox.p2.reconciler.dropins" is configured with auto start mode ("true" at the end of the line)

==Last operations to perform==
*Copy the build update site into a dedicated folder onto SourceForge (e.g., <code>/home/pfs/project/rodin-b-sharp/Core_Update_Site/3.5/</code>)
*Ensure that the download of the uploaded version of Rodin is here by default
*Update the main wiki page:
**http://wiki.event-b.org/index.php/Main_Page
**The image "out now" is to be changed
**The link "learn more" should point to the release notes
**The link "download now" should point to the SF repository
*The Platform releases page should be updated:
**http://wiki.event-b.org/index.php/Rodin_Platform_Releases
*The 64 bits page should be updated:
**http://wiki.event-b.org/index.php/Rodin_64_bit
*In the Bug and Feature Request trackers, complete the milestone for the new release, create a new milestone for the following one, and move any remaining ticket between these two milestones.
*A mail is sent on the user + announce rodin SF lists.

[[Category:Developer documentation]]
[[Category:Rodin Platform]]

Template:Dev News

2020-09-11T15:34:25Z

Laurent: /* Displayed as follow on the Main Page */

<noinclude>
[http://wiki.event-b.org/index.php?title=Template:Dev_News/Archives&action=edit Edit Archives]
== Displayed as follow on the Main Page ==
<div style="margin:0;width:50%;border:1px solid #AAAAAA;background:#FFFFFF;">
</noinclude>
<div style="font-size:90%;">
{| border="0"
|-
|Rodin 3.5 is out   
||[[Rodin Platform 3.5 Release Notes | +Learn more... ]]
[http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.5/ Download now]
|-
|}
* 11/09/20 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.5/ Release 3.5] of Rodin is now available [[Rodin Platform 3.5 Release Notes | +Learn more]]
* 07/03/18 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.4/ Release 3.4] of Rodin is now available [[Rodin Platform 3.4 Release Notes | +Learn more]]
* 13/04/17 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.3/ Release 3.3] of Rodin is now available [[Rodin Platform 3.3 Release Notes | +Learn more]]
* 22/06/15 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.2/ Release 3.2] of Rodin is now available [[Rodin Platform 3.2 Release Notes | +Learn more]]
* 17/12/14 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.1/ Release 3.1] of Rodin is now available [[Rodin Platform 3.1 Release Notes | +Learn more]]
* 25/03/14 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.0/ Release 3.0] of Rodin is now available [[Rodin_Platform_3.0_Release_Notes | +Learn more]]
* 18/10/13 : [[SMT_Solvers_Plug-in]] SMT 1.1 is now available
* 20/06/13 : [https://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.8/ Release 2.8] of Rodin is now available [[Rodin_Platform_2.8_Release_Notes | +Learn more]]
* 03/06/13 : [[SMT_Solvers_Plug-in]] SMT 1.0 is now available
* 06/11/12 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.7/ Release 2.7] of Rodin is now available
* 03/08/12 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.6/ Release 2.6] of Rodin is now available
* 02/05/12 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.5/ Release 2.5] of Rodin is now available
* 03/02/12 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.4/ Release 2.4] of Rodin is now available
* 01/12/11 : [[Rodin_Editor | Rodin Editor]] plug-in v0.6 released for Rodin 2.3
* 04/10/11 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.3/ Release 2.3] of Rodin is now available
* 01/08/11 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.2.2/ Release 2.2.2] of Rodin is now available
* 13/07/11 : [[Rodin_Editor | Rodin Editor]] plug-in released for Rodin 2.2.x
* 01/06/11 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.2/ Release 2.2] of Rodin is now available

</div>
<noinclude>
</div>
[[Category:Main page templates]]
</noinclude>

Template:Dev News

2020-09-11T15:32:55Z

Laurent: /* Displayed as follow on the Main Page */

<noinclude>
[http://wiki.event-b.org/index.php?title=Template:Dev_News/Archives&action=edit Edit Archives]
== Displayed as follow on the Main Page ==
<div style="margin:0;width:50%;border:1px solid #AAAAAA;background:#FFFFFF;">
</noinclude>
<div style="font-size:90%;">
{| border="0"
|-
|Rodin 3.5 is out
||[[Rodin Platform 3.5 Release Notes | +Learn more... ]]
[http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.5/ Download now]
|-
|}
* 11/09/20 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.5/ Release 3.5] of Rodin is now available [[Rodin Platform 3.5 Release Notes | +Learn more]]
* 07/03/18 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.4/ Release 3.4] of Rodin is now available [[Rodin Platform 3.4 Release Notes | +Learn more]]
* 13/04/17 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.3/ Release 3.3] of Rodin is now available [[Rodin Platform 3.3 Release Notes | +Learn more]]
* 22/06/15 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.2/ Release 3.2] of Rodin is now available [[Rodin Platform 3.2 Release Notes | +Learn more]]
* 17/12/14 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.1/ Release 3.1] of Rodin is now available [[Rodin Platform 3.1 Release Notes | +Learn more]]
* 25/03/14 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.0/ Release 3.0] of Rodin is now available [[Rodin_Platform_3.0_Release_Notes | +Learn more]]
* 18/10/13 : [[SMT_Solvers_Plug-in]] SMT 1.1 is now available
* 20/06/13 : [https://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.8/ Release 2.8] of Rodin is now available [[Rodin_Platform_2.8_Release_Notes | +Learn more]]
* 03/06/13 : [[SMT_Solvers_Plug-in]] SMT 1.0 is now available
* 06/11/12 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.7/ Release 2.7] of Rodin is now available
* 03/08/12 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.6/ Release 2.6] of Rodin is now available
* 02/05/12 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.5/ Release 2.5] of Rodin is now available
* 03/02/12 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.4/ Release 2.4] of Rodin is now available
* 01/12/11 : [[Rodin_Editor | Rodin Editor]] plug-in v0.6 released for Rodin 2.3
* 04/10/11 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.3/ Release 2.3] of Rodin is now available
* 01/08/11 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.2.2/ Release 2.2.2] of Rodin is now available
* 13/07/11 : [[Rodin_Editor | Rodin Editor]] plug-in released for Rodin 2.2.x
* 01/06/11 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.2/ Release 2.2] of Rodin is now available

</div>
<noinclude>
</div>
[[Category:Main page templates]]
</noinclude>

Rodin Platform 3.5.0 External Plug-ins

2020-09-11T15:30:39Z

Laurent: /* Atelier B Update Site */

==== Rodin Update Site ====

Available from http://rodin-b-sharp.sourceforge.net/updates

{{SimpleHeader}}
|-
! scope=col | || Plug-in name || Version || Status || MCV* || Release Date || Contact || Additional info
|-
| [[Image:IUMLB_big.png|30px]] || [[Event-B_Classdiagrams|Event-B Class Diagrams]] || 2.0.0 || new release || 3.x.x || 4 Nov 2018 || [mailto:cfs@ecs.soton.ac.uk email] || Class diagrams contained in Event-B Machines.
|-
| ||[[EMF_framework_for_Event-B|Event-B EMF framework]] || 6.0.0 || new release || 3.x.x || 4 Nov 2018 || [mailto:cfs@ecs.soton.ac.uk email] || Provided for plug-in developers. End users should not need to install this framework. It will be installed automatically by other plug-ins as required.
|-
| ||[[Generic_Event-B_EMF_extensions|Event-B EMF support for extensions]] || 6.0.0 || new release || 3.x.x || 17th Dec 2015 || [mailto:cfs@ecs.soton.ac.uk email] || Provided for plug-in developers. End users should not need to install this framework. It will be installed automatically by other plug-ins as required.
|-
| ||[[Generic_Event-B_EMF_extensions|Event-B EMF support for diagrams]] || 7.0.0 || new release || 3.2.x || 17th Dec 2015 || [mailto:cfs@ecs.soton.ac.uk email] || Provided for plug-in developers. End users should not need to install this framework. It will be installed automatically by other plug-ins as required.
|-
| [[Image:Rose.gif|30px]]||[[Rose_(Structured)_Editor|Rose editor]] || 1.7.0 || new release || 3.x.x || 4 Nov 2018 || [mailto:cfs@ecs.soton.ac.uk email] || Mainly useful for Plug-in developers. Tree-structured editor for Event-B EMF that handles extensions without modification
|-
| [[Image:Project diagram icon s.png|30px]]||[[Project_Diagram|Project Diagram]]|| 1.0.1 || not checked || 3.x.x || 1st Feb. 2015 || [mailto:vs2@ecs.soton.ac.uk email] || Machine - Context relationship diagram
|-
| [[Image:Umlb32.gif|30px]] || [[UML-B|UML-B]] || 2.3.0 || not checked || 3.x.x || 18th Oct. 2014 || [mailto:cfs@ecs.soton.ac.uk email] || Original UML-B modelling environment
|-
| [[Image:Umlb32.gif|30px]] ||[[UML-B_-_Statemachine_Animation|UML-B Statemachine Animation]] || 1.3.0 || not checked || 3.x.x || 18th Oct. 2014 || [mailto:vs2@ecs.soton.ac.uk email] || Compatible with UML-B 2.3 and ProB 3.0
|-
| ||[[EMF_Compare_Editor_installation|Teamwork]] || 1.2.0 || not checked || 3.2.x || 5th Sept. 2016 || [mailto:cfs@ecs.soton.ac.uk email] || Provides a synchronised copy of Machines and Contexts for committing into a repository. It is recommended to also install the Rose editor, EMF compare 3.1.0 and a recent repository client (e.g. Egit 4.1.4).
|-
| [[Image:Cmp_mch_obj.gif|20px]] ||[[Parallel_Composition_using_Event-B | Shared Event Composition]] || 1.7.1 || not checked || || 5th July 2017 || [mailto:cfs@ecs.soton.ac.uk email] || Compatible with Rodin 3.x.x (checked by cfs 5/05/17)
|-
| [[Image:DecompositionPlug-in_logo.png|30px]] || [[Decomposition Plug-in User Guide | Decomposition]] || 1.3.1 || not checked || || 4th July 2017 || [mailto:cfs@ecs.soton.ac.uk email] || Compatible with Rodin 3.x.x (checked by cfs 4/05/17)
|-
| ||[[Refactoring Framework | Refactory ]]|| 1.3.0 || not checked|| 3.x.x || 6th May 2014 || [mailto:asf08r@ecs.soton.ac.uk email] || Compatible with Rodin 3.0.x.
|-
| || [[Theory Plug-in| Theory Plug-in]] || 3.0.0 || not checked|| || 17th Dec 2014|| [mailto:asf08r@ecs.soton.ac.uk email] ||
|-.x
| || [[Code Generation Activity | Code Generation]] || 0.2.5 || not checked|| || 29th Aug. 2013|| [mailto:ae2@ecs.soton.ac.uk email] || For Java, Ada, and OpenMP C code
|-.x
|-
| || Relevance Filter || 1.1.1 || available || ?.x.x || || ||
|-
| || [[Isabelle for Rodin]] || || not checked || 2.x.x || || ||
|-
| || [[SMT_Plug-in | SMT Solvers ]] || 1.4.0 || available || || 15th March 2016|| [mailto:lvoisin@users.sourceforge.net Laurent Voisin] ||
|-
| || [[Pattern | Pattern]] || 0.9.0 || not checked || 3.x.x || 13th March 2015 || [mailto:tshoang@users.sourceforge.net Thai Son Hoang] ||
|-
| || [[Event-B Qualitative Probability User Guide | Qualitative Probability]] || 0.2.3 || available || 3.x.x || 9th October 2015 || [mailto:tshoang@users.sourceforge.net Thai Son Hoang] ||
|-
| || [[B2Latex | B2Latex export]] || 0.7.0 || available || 2.5.x || 27th May 2015 || [mailto:lvoisin@users.sourceforge.net Laurent Voisin] ||
|-
| || [[Generic Instantiation Plug-in User Guide | Generic Instantiation (Soton)]] || 1.0.1 || not checked || || 05th March 2013 || [mailto:asf08r@ecs.soton.ac.uk email] ||
|-
| ||[[Records|Records]] || 2.0.0 || available || 2.x.x || 16th Oct. 2010 || [mailto:cfs@ecs.soton.ac.uk email] ||
|}

==== Atelier B Update Site ====

Available from http://methode-b.com/update_site/atelierb_provers

{{SimpleHeader}}
|-
! scope=col | || Plug-in name || Version || Status || MCV* || Release Date || Contact || Additional info
|-
| || Atelier B provers || 2.2.1 || available || 3.3.0 || 7 Aug 2017 || || Does not work with macOS Catalina!
|}

==== ProB Update Site ====

Available from http://www.stups.hhu.de/prob_updates_rodin3

{{SimpleHeader}}
|-
! scope=col | || Plug-in name || Version || Status || MCV* || Release Date || Contact || Additional info
|-
| || ProB || 3.0.10 || available || 3.5.0 || 4 Sep 2020 || || The ProB animator and model checker
|-
| || ProB (Dis)Prover || 3.0.9 || available || 3.5.0 || 4 Sep 2020 || || The ProB counter-example finder and prover
|-
| || ProB Symbolic constants support || 3.0.9 || available || 3.5.0 || 4 Sep 2020 || ||
|}

==== Southampton Releases Update Site ====

Available from http://eventb-soton.github.io/updateSite/releases

{{SimpleHeader}}
|-
! scope=col | || Plug-in name || Version || Status || MCV* || Release Date || Contact || Additional info
|-
| [[Image:CamilleX.png|CmX]] || [[CamilleX|CamilleX]] || 2.0.0 || new release || 3.4.0 || 29 Jul 2020 || [mailto:T.S.Hoang@ecs.soton.ac.uk Thai Son Hoang] || CamilleX provides text editors for Event-B models and support modelling mechanisms such as machine inclusion.
|-
| [[Image:IUMLB_big.png|30px]] || [[Event-B_Statemachines|Event-B State-machines]] || 4.0.1 || new release || 3.x.x || 13 Aug 2020 || [mailto:cfs@ecs.soton.ac.uk Colin Snook] || State-machines contained in Event-B Machines.
|-
| [[Image:IUMLB_big.png|30px]] ||[[Event-B_Statemachines|Event-B State-machine Animation]] || 3.0.0 || new release || 3.x.x || 13 Aug 2020 || [mailto:cfs@ecs.soton.ac.uk Colin Snook] || Compatible with Event-B statemachines 4.x.x and ProB 3.0.x.
|}

Rodin Platform 3.5.0 External Plug-ins

2020-09-11T13:12:11Z

Laurent:

==== Rodin Update Site ====

Available from http://rodin-b-sharp.sourceforge.net/updates

{{SimpleHeader}}
|-
! scope=col | || Plug-in name || Version || Status || MCV* || Release Date || Contact || Additional info
|-
| [[Image:IUMLB_big.png|30px]] || [[Event-B_Classdiagrams|Event-B Class Diagrams]] || 2.0.0 || new release || 3.x.x || 4 Nov 2018 || [mailto:cfs@ecs.soton.ac.uk email] || Class diagrams contained in Event-B Machines.
|-
| ||[[EMF_framework_for_Event-B|Event-B EMF framework]] || 6.0.0 || new release || 3.x.x || 4 Nov 2018 || [mailto:cfs@ecs.soton.ac.uk email] || Provided for plug-in developers. End users should not need to install this framework. It will be installed automatically by other plug-ins as required.
|-
| ||[[Generic_Event-B_EMF_extensions|Event-B EMF support for extensions]] || 6.0.0 || new release || 3.x.x || 17th Dec 2015 || [mailto:cfs@ecs.soton.ac.uk email] || Provided for plug-in developers. End users should not need to install this framework. It will be installed automatically by other plug-ins as required.
|-
| ||[[Generic_Event-B_EMF_extensions|Event-B EMF support for diagrams]] || 7.0.0 || new release || 3.2.x || 17th Dec 2015 || [mailto:cfs@ecs.soton.ac.uk email] || Provided for plug-in developers. End users should not need to install this framework. It will be installed automatically by other plug-ins as required.
|-
| [[Image:Rose.gif|30px]]||[[Rose_(Structured)_Editor|Rose editor]] || 1.7.0 || new release || 3.x.x || 4 Nov 2018 || [mailto:cfs@ecs.soton.ac.uk email] || Mainly useful for Plug-in developers. Tree-structured editor for Event-B EMF that handles extensions without modification
|-
| [[Image:Project diagram icon s.png|30px]]||[[Project_Diagram|Project Diagram]]|| 1.0.1 || not checked || 3.x.x || 1st Feb. 2015 || [mailto:vs2@ecs.soton.ac.uk email] || Machine - Context relationship diagram
|-
| [[Image:Umlb32.gif|30px]] || [[UML-B|UML-B]] || 2.3.0 || not checked || 3.x.x || 18th Oct. 2014 || [mailto:cfs@ecs.soton.ac.uk email] || Original UML-B modelling environment
|-
| [[Image:Umlb32.gif|30px]] ||[[UML-B_-_Statemachine_Animation|UML-B Statemachine Animation]] || 1.3.0 || not checked || 3.x.x || 18th Oct. 2014 || [mailto:vs2@ecs.soton.ac.uk email] || Compatible with UML-B 2.3 and ProB 3.0
|-
| ||[[EMF_Compare_Editor_installation|Teamwork]] || 1.2.0 || not checked || 3.2.x || 5th Sept. 2016 || [mailto:cfs@ecs.soton.ac.uk email] || Provides a synchronised copy of Machines and Contexts for committing into a repository. It is recommended to also install the Rose editor, EMF compare 3.1.0 and a recent repository client (e.g. Egit 4.1.4).
|-
| [[Image:Cmp_mch_obj.gif|20px]] ||[[Parallel_Composition_using_Event-B | Shared Event Composition]] || 1.7.1 || not checked || || 5th July 2017 || [mailto:cfs@ecs.soton.ac.uk email] || Compatible with Rodin 3.x.x (checked by cfs 5/05/17)
|-
| [[Image:DecompositionPlug-in_logo.png|30px]] || [[Decomposition Plug-in User Guide | Decomposition]] || 1.3.1 || not checked || || 4th July 2017 || [mailto:cfs@ecs.soton.ac.uk email] || Compatible with Rodin 3.x.x (checked by cfs 4/05/17)
|-
| ||[[Refactoring Framework | Refactory ]]|| 1.3.0 || not checked|| 3.x.x || 6th May 2014 || [mailto:asf08r@ecs.soton.ac.uk email] || Compatible with Rodin 3.0.x.
|-
| || [[Theory Plug-in| Theory Plug-in]] || 3.0.0 || not checked|| || 17th Dec 2014|| [mailto:asf08r@ecs.soton.ac.uk email] ||
|-.x
| || [[Code Generation Activity | Code Generation]] || 0.2.5 || not checked|| || 29th Aug. 2013|| [mailto:ae2@ecs.soton.ac.uk email] || For Java, Ada, and OpenMP C code
|-.x
|-
| || Relevance Filter || 1.1.1 || available || ?.x.x || || ||
|-
| || [[Isabelle for Rodin]] || || not checked || 2.x.x || || ||
|-
| || [[SMT_Plug-in | SMT Solvers ]] || 1.4.0 || available || || 15th March 2016|| [mailto:lvoisin@users.sourceforge.net Laurent Voisin] ||
|-
| || [[Pattern | Pattern]] || 0.9.0 || not checked || 3.x.x || 13th March 2015 || [mailto:tshoang@users.sourceforge.net Thai Son Hoang] ||
|-
| || [[Event-B Qualitative Probability User Guide | Qualitative Probability]] || 0.2.3 || available || 3.x.x || 9th October 2015 || [mailto:tshoang@users.sourceforge.net Thai Son Hoang] ||
|-
| || [[B2Latex | B2Latex export]] || 0.7.0 || available || 2.5.x || 27th May 2015 || [mailto:lvoisin@users.sourceforge.net Laurent Voisin] ||
|-
| || [[Generic Instantiation Plug-in User Guide | Generic Instantiation (Soton)]] || 1.0.1 || not checked || || 05th March 2013 || [mailto:asf08r@ecs.soton.ac.uk email] ||
|-
| ||[[Records|Records]] || 2.0.0 || available || 2.x.x || 16th Oct. 2010 || [mailto:cfs@ecs.soton.ac.uk email] ||
|}

==== Atelier B Update Site ====

Available from http://methode-b.com/update_site/atelierb_provers

{{SimpleHeader}}
|-
! scope=col | || Plug-in name || Version || Status || MCV* || Release Date || Contact || Additional info
|-
| || Atelier B provers || 2.2.1 || available || 3.3.0 || 7 Aug 2017 || || Provers from Atelier B
|}

==== ProB Update Site ====

Available from http://www.stups.hhu.de/prob_updates_rodin3

{{SimpleHeader}}
|-
! scope=col | || Plug-in name || Version || Status || MCV* || Release Date || Contact || Additional info
|-
| || ProB || 3.0.10 || available || 3.5.0 || 4 Sep 2020 || || The ProB animator and model checker
|-
| || ProB (Dis)Prover || 3.0.9 || available || 3.5.0 || 4 Sep 2020 || || The ProB counter-example finder and prover
|-
| || ProB Symbolic constants support || 3.0.9 || available || 3.5.0 || 4 Sep 2020 || ||
|}

==== Southampton Releases Update Site ====

Available from http://eventb-soton.github.io/updateSite/releases

{{SimpleHeader}}
|-
! scope=col | || Plug-in name || Version || Status || MCV* || Release Date || Contact || Additional info
|-
| [[Image:CamilleX.png|CmX]] || [[CamilleX|CamilleX]] || 2.0.0 || new release || 3.4.0 || 29 Jul 2020 || [mailto:T.S.Hoang@ecs.soton.ac.uk Thai Son Hoang] || CamilleX provides text editors for Event-B models and support modelling mechanisms such as machine inclusion.
|-
| [[Image:IUMLB_big.png|30px]] || [[Event-B_Statemachines|Event-B State-machines]] || 4.0.1 || new release || 3.x.x || 13 Aug 2020 || [mailto:cfs@ecs.soton.ac.uk Colin Snook] || State-machines contained in Event-B Machines.
|-
| [[Image:IUMLB_big.png|30px]] ||[[Event-B_Statemachines|Event-B State-machine Animation]] || 3.0.0 || new release || 3.x.x || 13 Aug 2020 || [mailto:cfs@ecs.soton.ac.uk Colin Snook] || Compatible with Event-B statemachines 4.x.x and ProB 3.0.x.
|}

Rodin Platform 3.5.0 External Plug-ins

2020-09-11T13:10:38Z

Laurent:

==== Rodin Update Site ====

Available from http://rodin-b-sharp.sourceforge.net/updates

{{SimpleHeader}}
|-
! scope=col | || Plug-in name || Version || Status || MCV* || Release Date || Contact || Additional info
|-
| [[Image:IUMLB_big.png|30px]] || [[Event-B_Classdiagrams|Event-B Class Diagrams]] || 2.0.0 || new release || 3.x.x || 4 Nov 2018 || [mailto:cfs@ecs.soton.ac.uk email] || Class diagrams contained in Event-B Machines.
|-
| ||[[EMF_framework_for_Event-B|Event-B EMF framework]] || 6.0.0 || new release || 3.x.x || 4 Nov 2018 || [mailto:cfs@ecs.soton.ac.uk email] || Provided for plug-in developers. End users should not need to install this framework. It will be installed automatically by other plug-ins as required.
|-
| ||[[Generic_Event-B_EMF_extensions|Event-B EMF support for extensions]] || 6.0.0 || new release || 3.x.x || 17th Dec 2015 || [mailto:cfs@ecs.soton.ac.uk email] || Provided for plug-in developers. End users should not need to install this framework. It will be installed automatically by other plug-ins as required.
|-
| ||[[Generic_Event-B_EMF_extensions|Event-B EMF support for diagrams]] || 7.0.0 || new release || 3.2.x || 17th Dec 2015 || [mailto:cfs@ecs.soton.ac.uk email] || Provided for plug-in developers. End users should not need to install this framework. It will be installed automatically by other plug-ins as required.
|-
| [[Image:Rose.gif|30px]]||[[Rose_(Structured)_Editor|Rose editor]] || 1.7.0 || new release || 3.x.x || 4 Nov 2018 || [mailto:cfs@ecs.soton.ac.uk email] || Mainly useful for Plug-in developers. Tree-structured editor for Event-B EMF that handles extensions without modification
|-
| [[Image:Project diagram icon s.png|30px]]||[[Project_Diagram|Project Diagram]]|| 1.0.1 || not checked || 3.x.x || 1st Feb. 2015 || [mailto:vs2@ecs.soton.ac.uk email] || Machine - Context relationship diagram
|-
| [[Image:Umlb32.gif|30px]] || [[UML-B|UML-B]] || 2.3.0 || not checked || 3.x.x || 18th Oct. 2014 || [mailto:cfs@ecs.soton.ac.uk email] || Original UML-B modelling environment
|-
| [[Image:Umlb32.gif|30px]] ||[[UML-B_-_Statemachine_Animation|UML-B Statemachine Animation]] || 1.3.0 || not checked || 3.x.x || 18th Oct. 2014 || [mailto:vs2@ecs.soton.ac.uk email] || Compatible with UML-B 2.3 and ProB 3.0
|-
| ||[[EMF_Compare_Editor_installation|Teamwork]] || 1.2.0 || not checked || 3.2.x || 5th Sept. 2016 || [mailto:cfs@ecs.soton.ac.uk email] || Provides a synchronised copy of Machines and Contexts for committing into a repository. It is recommended to also install the Rose editor, EMF compare 3.1.0 and a recent repository client (e.g. Egit 4.1.4).
|-
| [[Image:Cmp_mch_obj.gif|20px]] ||[[Parallel_Composition_using_Event-B | Shared Event Composition]] || 1.7.1 || not checked || || 5th July 2017 || [mailto:cfs@ecs.soton.ac.uk email] || Compatible with Rodin 3.x.x (checked by cfs 5/05/17)
|-
| [[Image:DecompositionPlug-in_logo.png|30px]] || [[Decomposition Plug-in User Guide | Decomposition]] || 1.3.1 || not checked || || 4th July 2017 || [mailto:cfs@ecs.soton.ac.uk email] || Compatible with Rodin 3.x.x (checked by cfs 4/05/17)
|-
| ||[[Refactoring Framework | Refactory ]]|| 1.3.0 || not checked|| 3.x.x || 6th May 2014 || [mailto:asf08r@ecs.soton.ac.uk email] || Compatible with Rodin 3.0.x.
|-
| || [[Theory Plug-in| Theory Plug-in]] || 3.0.0 || not checked|| || 17th Dec 2014|| [mailto:asf08r@ecs.soton.ac.uk email] ||
|-.x
| || [[Code Generation Activity | Code Generation]] || 0.2.5 || not checked|| || 29th Aug. 2013|| [mailto:ae2@ecs.soton.ac.uk email] || For Java, Ada, and OpenMP C code
|-.x
|-
| || Relevance Filter || 1.1.1 || available || ?.x.x || || ||
|-
| || [[Isabelle for Rodin]] || || not checked || 2.x.x || || ||
|-
| || [[SMT_Plug-in | SMT Solvers ]] || 1.4.0 || available || || 15th March 2016|| [mailto:lvoisin@users.sourceforge.net Laurent Voisin] ||
|-
| || [[Pattern | Pattern]] || 0.9.0 || not checked || 3.x.x || 13th March 2015 || [mailto:tshoang@users.sourceforge.net Thai Son Hoang] ||
|-
| || [[Event-B Qualitative Probability User Guide | Qualitative Probability]] || 0.2.3 || available || 3.x.x || 9th October 2015 || [mailto:tshoang@users.sourceforge.net Thai Son Hoang] ||
|-
| || [[B2Latex | B2Latex export]] || 0.7.0 || available || 2.5.x || 27th May 2015 || [mailto:lvoisin@users.sourceforge.net Laurent Voisin] ||
|-
| || [[Generic Instantiation Plug-in User Guide | Generic Instantiation (Soton)]] || 1.0.1 || not checked || || 05th March 2013 || [mailto:asf08r@ecs.soton.ac.uk email] ||
|-
| ||[[Records|Records]] || 2.0.0 || available || 2.x.x || 16th Oct. 2010 || [mailto:cfs@ecs.soton.ac.uk email] ||
|}

==== Atelier B Update Site ====

Available from http://methode-b.com/update_site/atelierb_provers

{{SimpleHeader}}
|-
! scope=col | || Plug-in name || Version || Status || MCV* || Release Date || Contact || Additional info
|-
| || Atelier B provers || 2.2.1 || available || 3.3.0 || 7 Aug 2017 || || Provers from Atelier B
|}

==== ProB Update Site ====

Available from http://www.stups.hhu.de/prob_updates_rodin3

{{SimpleHeader}}
|-
! scope=col | || Plug-in name || Version || Status || MCV* || Release Date || Contact || Additional info
|-
| || ProB || 3.0.10 || available || 3.5.0 || 4 Sep 2020 || || The ProB animator and model checker
|-
| || ProB (Dis)Prover || 3.0.9 || available || 3.5.0 || 4 Sep 2020 || || The ProB counter-example finder and prover
|-
| || ProB Symbolic constants support || 3.0.9 || available || 3.5.0 || 4 Sep 2020 || ||
|}

==== Southampton Releases Update Site ====
Available from http://eventb-soton.github.io/updateSite/releases

{{SimpleHeader}}
|-
! scope=col | || Plug-in name || Version || Status || MCV* || Release Date || Contact || Additional info
|-
| [[Image:CamilleX.png|CmX]] || [[CamilleX|CamilleX]] || 2.0.0 || new release || 3.4.0 || 29 Jul 2020 || [mailto:T.S.Hoang@ecs.soton.ac.uk Thai Son Hoang] || CamilleX provides text editors for Event-B models and support modelling mechanisms such as machine inclusion.
|-
| [[Image:IUMLB_big.png|30px]] || [[Event-B_Statemachines|Event-B State-machines]] || 4.0.1 || new release || 3.x.x || 13 Aug 2020 || [mailto:cfs@ecs.soton.ac.uk Colin Snook] || State-machines contained in Event-B Machines.
|-
| [[Image:IUMLB_big.png|30px]] ||[[Event-B_Statemachines|Event-B State-machine Animation]] || 3.0.0 || new release || 3.x.x || 13 Aug 2020 || [mailto:cfs@ecs.soton.ac.uk Colin Snook] || Compatible with Event-B statemachines 4.x.x and ProB 3.0.x.
|}

Rodin Platform 3.5 Release Notes

2020-09-11T13:09:28Z

Laurent: /* About */

{{TOCright}}

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

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

Rodin 3.5 brings lexicographical variants and several bug fixes. It also upgrades the underlying Eclipse to 2020-06, which can be run by all modern Java Runtimes (Java 8 up to 13).

The new lexicographical variant feature means that from now on a machine can contain several variant elements, which are to be understood as a tuple combination (in order of appearance). For instance, if a machine contains the two variants ''V1'' and ''V2'' declared in that order, then a converging event must either decrease ''V1'', or not modify ''V1'' and decrease ''V2''.

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

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

Rodin 3.5 is built on top of Eclipse 4.16 (2020-06), which requires Java 8, just as the previous versions.

There is no API change within Rodin Core.

Following to the introduction of lexicographical variants, a machine can now contain several variant elements. Moreover, variant elements now carry a label attribute. The Rodin tools contain a compatibility layer that allows to read existing machine containing a single unlabelled variant and present it with the new API (using the hardcoded label <code>vrn</code> available from the <code>org.eventb.core.IVariant.DEFAULT_LABEL</code> constant).

== Installing ==

=== Downloading ===

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

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

If you run Rodin 3.1, 3.2, 3.3, or 3.4, then you can upgrade your Rodin Platform by clicking Help > Check for Updates, then select Rodin 3.5 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.5 brings a new version of Eclipse. This means that once you have opened a workspace with Rodin 3.5, you will not be able to open it with a prior version of Rodin anymore. Please consider copying your workspace for Rodin 3.5 to avoid any disaster.

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

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

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 ==
{{:Rodin_Platform_3.5.0_External_Plug-ins}}

== Fixed Bugs and Implemented Features ==

Bugs
783 Launching problem with Java 13
782 Launching error with Java 11
781 Problem with the Rodin proof generator
780 Useless local hypotheses in NAT PO
779 No information when failing to launch external provers
777 Missing refresh in Rodin Editor for event convergence status
776 Rodin Handbook URL broken
774 Java SE 6 required to run Rodin V3.4 on macOS High Sierra ?
775 Editors misinterpret 'generated = false'
773 Update VM arguments for Java 9
772 crash of Rodin V3.4 when opening workspace
771 Proof view: unreadable formulas (white on white)
770 AtelierB plug-in 2.2.0 broken
769 Statistics columns have non uniform widths
765 Generalized Modus Ponens turns goal into "false"
756 Null reasoner input
754 Dropins folder is available again by default
753 Section color preferences are not taken into account
741 Tactic Profile Editing very slow performance
698 Using 'Open With' context menu on PO does not load the PO
618 Proposed name in refine action

Feature Requests
355 Simplify POs for anticipated event further
314 Lexicographic variant

== 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.5. We expect this to be solved for Rodin 3.6. See [[#macOS_specific_requirements|macOS requirements]] for a workaround.

=== macOS in dark mode ===

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

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

== About ==

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

[[Category:Rodin Platform Release Notes]]

Rodin Platform 3.5 Release Notes

2020-09-11T13:06:41Z

Laurent: /* macOS specific requirements */

{{TOCright}}

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

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

Rodin 3.5 brings lexicographical variants and several bug fixes. It also upgrades the underlying Eclipse to 2020-06, which can be run by all modern Java Runtimes (Java 8 up to 13).

The new lexicographical variant feature means that from now on a machine can contain several variant elements, which are to be understood as a tuple combination (in order of appearance). For instance, if a machine contains the two variants ''V1'' and ''V2'' declared in that order, then a converging event must either decrease ''V1'', or not modify ''V1'' and decrease ''V2''.

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

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

Rodin 3.5 is built on top of Eclipse 4.16 (2020-06), which requires Java 8, just as the previous versions.

There is no API change within Rodin Core.

Following to the introduction of lexicographical variants, a machine can now contain several variant elements. Moreover, variant elements now carry a label attribute. The Rodin tools contain a compatibility layer that allows to read existing machine containing a single unlabelled variant and present it with the new API (using the hardcoded label <code>vrn</code> available from the <code>org.eventb.core.IVariant.DEFAULT_LABEL</code> constant).

== Installing ==

=== Downloading ===

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

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

If you run Rodin 3.1, 3.2, 3.3, or 3.4, then you can upgrade your Rodin Platform by clicking Help > Check for Updates, then select Rodin 3.5 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.5 brings a new version of Eclipse. This means that once you have opened a workspace with Rodin 3.5, you will not be able to open it with a prior version of Rodin anymore. Please consider copying your workspace for Rodin 3.5 to avoid any disaster.

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

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

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 ==
{{:Rodin_Platform_3.5.0_External_Plug-ins}}

== Fixed Bugs and Implemented Features ==

Bugs
783 Launching problem with Java 13
782 Launching error with Java 11
781 Problem with the Rodin proof generator
780 Useless local hypotheses in NAT PO
779 No information when failing to launch external provers
777 Missing refresh in Rodin Editor for event convergence status
776 Rodin Handbook URL broken
774 Java SE 6 required to run Rodin V3.4 on macOS High Sierra ?
775 Editors misinterpret 'generated = false'
773 Update VM arguments for Java 9
772 crash of Rodin V3.4 when opening workspace
771 Proof view: unreadable formulas (white on white)
770 AtelierB plug-in 2.2.0 broken
769 Statistics columns have non uniform widths
765 Generalized Modus Ponens turns goal into "false"
756 Null reasoner input
754 Dropins folder is available again by default
753 Section color preferences are not taken into account
741 Tactic Profile Editing very slow performance
698 Using 'Open With' context menu on PO does not load the PO
618 Proposed name in refine action

Feature Requests
355 Simplify POs for anticipated event further
314 Lexicographic variant

== 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.5. We expect this to be solved for Rodin 3.6. See [[#macOS_specific_requirements|macOS requirements]] for a workaround.

=== macOS in dark mode ===

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

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

== About ==

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

[[Category:Rodin Platform Release Notes]]

Rodin Platform 3.5 Release Notes

2020-09-11T13:03:36Z

Laurent: /* About */

{{TOCright}}

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

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

Rodin 3.5 brings lexicographical variants and several bug fixes. It also upgrades the underlying Eclipse to 2020-06, which can be run by all modern Java Runtimes (Java 8 up to 13).

The new lexicographical variant feature means that from now on a machine can contain several variant elements, which are to be understood as a tuple combination (in order of appearance). For instance, if a machine contains the two variants ''V1'' and ''V2'' declared in that order, then a converging event must either decrease ''V1'', or not modify ''V1'' and decrease ''V2''.

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

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

Rodin 3.5 is built on top of Eclipse 4.16 (2020-06), which requires Java 8, just as the previous versions.

There is no API change within Rodin Core.

Following to the introduction of lexicographical variants, a machine can now contain several variant elements. Moreover, variant elements now carry a label attribute. The Rodin tools contain a compatibility layer that allows to read existing machine containing a single unlabelled variant and present it with the new API (using the hardcoded label <code>vrn</code> available from the <code>org.eventb.core.IVariant.DEFAULT_LABEL</code> constant).

== Installing ==

=== Downloading ===

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

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

If you run Rodin 3.1, 3.2, 3.3, or 3.4, then you can upgrade your Rodin Platform by clicking Help > Check for Updates, then select Rodin 3.5 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.5 brings a new version of Eclipse. This means that once you have opened a workspace with Rodin 3.5, you will not be able to open it with a prior version of Rodin anymore. Please consider copying your workspace for Rodin 3.5 to avoid any disaster.

If you run Rodin 3.0 or prior, you cannot upgrade to 3.5. 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 8 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].

== External plug-ins ==
{{:Rodin_Platform_3.5.0_External_Plug-ins}}

== Fixed Bugs and Implemented Features ==

Bugs
783 Launching problem with Java 13
782 Launching error with Java 11
781 Problem with the Rodin proof generator
780 Useless local hypotheses in NAT PO
779 No information when failing to launch external provers
777 Missing refresh in Rodin Editor for event convergence status
776 Rodin Handbook URL broken
774 Java SE 6 required to run Rodin V3.4 on macOS High Sierra ?
775 Editors misinterpret 'generated = false'
773 Update VM arguments for Java 9
772 crash of Rodin V3.4 when opening workspace
771 Proof view: unreadable formulas (white on white)
770 AtelierB plug-in 2.2.0 broken
769 Statistics columns have non uniform widths
765 Generalized Modus Ponens turns goal into "false"
756 Null reasoner input
754 Dropins folder is available again by default
753 Section color preferences are not taken into account
741 Tactic Profile Editing very slow performance
698 Using 'Open With' context menu on PO does not load the PO
618 Proposed name in refine action

Feature Requests
355 Simplify POs for anticipated event further
314 Lexicographic variant

== 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.5. We expect this to be solved for Rodin 3.6. See [[#macOS_specific_requirements|macOS requirements]] for a workaround.

=== macOS in dark mode ===

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

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

== About ==

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

[[Category:Rodin Platform Release Notes]]

Building Rodin Headless

2020-09-11T10:31:39Z

Laurent: /* Last operations to perform */

This page documents the procedure followed for building the binary packages of the Rodin platform that are distributed on SourceForge. The build is done in two steps
# Fetch the sources from the repository and make a source archive with them.
# Build the platform headless from this set of sources using Apache Ant.

==Requirements==
* [http://maven.apache.org/ Apache Maven 3] should be installed on the platform that will run the build.

==Pre Build Verifications==

Before building, several checks have to be made in the sources:
* clean build all RodinCore plug-ins, so that generated files are regenerated using repository sources
* JUnit tests are OK
* versions of plug-ins, features and product obey [http://wiki.eclipse.org/Version_Numbering Eclipse versioning policy]
* API Tooling build against previous Rodin release produces no errors on any plug-in
* Rodin build process is managed using Apache maven and Tycho. One should verify that maven artifact versions match the plug-in versions (defined in plug-in MANIFEST.MF files)
* the correct Eclipse version is referenced in the p2 configuration (org.rodinp.platform/Rodin.p2.inf)

addRepository(type:0,location:http${#58}//download.eclipse.org/releases/neon,name:Neon Update Site);\
addRepository(type:1,location:http${#58}//download.eclipse.org/releases/neon,name:Neon Update Site);\

and matches the one defined whithin the parent pom file (<tt>org.eventb.parent/pom.xml</tt>) :

<repository>
<id>oxygen-4.7</id>
<layout>p2</layout>
<url>http://download.eclipse.org/eclipse/updates/4.7/</url>
</repository>

* the correct link for the Rodin Handbook is provided in the parent pom file (<tt>org.eventb.parent/pom.xml</tt>) :
<repository>
<id>handbook</id>
<layout>p2</layout>
<url>http://handbook.event-b.org/updatesite</url>
</repository>

* branding plug-ins display the correct Eclipse version (text information found in several about.properties/plugin.properties files)
* documentation is up to date for /org.rodinp.platform/html/root.html
* generated documentation matches latest wiki sources for <tt>org.eventb.keyboard/doc</tt>
* make sure a valid destination folder is specified in <tt>org.eventb.parent/pom.xml</tt>. This destination folder will host the built platforms, the update-site and the development target platform.
Example :
<www-basedir>/tmp/rodin-build/rodin-3.0</www-basedir>

The variable used in Maven scripts is then <tt>${www-basedir}</tt>

When everything works, any changes to the sources made during this verification process are pushed to the Source Forge repository.

'''N.B.''' Several information are defined and manipulated for each build. Here below is a memo to help understand them :
# the platform version which defines a milestone identifier for the Rodin platform. Example of platform versions are <tt>1.0</tt> and <tt>2.3RC1</tt>.
# the Git commit number which permits to know very precisely which source versions are used for the build.
# the Git branch from which the commit can be checked out
# the full platform version used for provisioning, and which is the user-visible version which is displayed in ''About Rodin Platform''. This version is made of the platform version and the commit number, separated by a dot. Example of full versions are <tt>2.8RC1.bh1420</tt> and <tt>2.8.1.hgf52f65</tt>.

==Fetching Sources==

Create a directory that will contain the sources and be used to build the platform. 
Example :
mkdir Rodin3.0BuildDirectory

and go to this directory :
cd Rodin3.0BuildDirectory

Fetch sources from Git in the current directory :
<nowiki>git clone git://git.code.sf.net/p/rodin-b-sharp/rodincore .</nowiki>

==Building the Platform==

To build the platform, you just need to run the script below (available from org.rodinp.releng/scripts/run-maven.sh) :

<nowiki> #!/bin/sh
###############################################################################
# Copyright (c) 2013 Systerel and others.
# All rights reserved. This program and the accompanying materials
# are made available under the terms of the Eclipse Public License v1.0
# which accompanies this distribution, and is available at
# http://www.eclipse.org/legal/epl-v10.html
#
# Contributors:
# Systerel - initial API and implementation
###############################################################################
SCRIPT=`readlink -m -n $0`
SCRIPTS_DIR=`dirname $SCRIPT`
MAIN_DIR=`readlink -m -n $SCRIPTS_DIR/../..`

cd $MAIN_DIR

GIT_COMMIT=`git log -1 --format='%h'`
echo "Building Rodin with Maven for git commit: $GIT_COMMIT"
mvn clean install -Dgit-commit=$GIT_COMMIT $@ # -DskipTests -fae </nowiki>

==Post Build Verifications==

When the build worked, the destination directory (defined by variable <tt>${www-basedir}</tt>) contains zipped archives for all platforms, the update site, and the target platform for plug-in development.
For each of them, check that:
* "rodin" binary is an executable file (for Linux and Mac)
* the version appearing in ''About Rodin platform'' is correctly defined
* a directory "dropins" exists at the root (under "rodin", among "features", plugins", ...)
* in "configuration/org.eclipse.equinox.simpleconfigurator/bundles.info", plug-in "org.eclipse.equinox.p2.reconciler.dropins" is configured with auto start mode ("true" at the end of the line)

==Last operations to perform==
*Copy the build update site into a dedicated folder onto SourceForge (e.g., <code>/home/pfs/project/rodin-b-sharp/Core_Update_Site/3.5/</code>)
*Ensure that the download of the uploaded version of Rodin is here by default
*Update the main wiki page:
**http://wiki.event-b.org/index.php/Main_Page
**The image "out now" is to be changed
**The link "learn more" should point to the release notes
**The link "download now" should point to the SF repository
*The Platform releases page should be updated:
**http://wiki.event-b.org/index.php/Rodin_Platform_Releases
*The 64 bits page should be updated:
**http://wiki.event-b.org/index.php/Rodin_64_bit
*A group for the new release is available on Bug and Feature Request trackers.
*A mail is sent on the user + announce rodin SF lists.

[[Category:Developer documentation]]
[[Category:Rodin Platform]]

Rodin Platform Releases

2020-09-11T10:26:55Z

Laurent:

{{TOCright}}

== Current Release ==
The current version of Rodin release is [[Rodin Platform 3.5 Release Notes|3.5]]. It has been published on 2020-09-11. Installation and Release Notes can be found [http://wiki.event-b.org/index.php/Rodin_Platform_3.5_Release_Notes here]

== Current plug-ins ==
{{:Rodin_Platform_3.5.0_External_Plug-ins}}

== Previous Releases ==

{{SimpleHeader}}
|-
! scope=col | Version || Release Date
|-
|[[Rodin Platform 3.4 Release Notes|3.4]] || 2018/02/23
|-
|[[Rodin Platform 3.3 Release Notes|3.3]] || 2017/04/05
|-
|[[Rodin Platform 3.2 Release Notes|3.2]] || 2015/09/22
|-
|[[Rodin Platform 3.1 Release Notes|3.1]] || 2014/12/17
|-
|[[Rodin Platform 3.0 Release Notes|3.0]] || 2014/03/25
|-
|[[Rodin Platform 2.8 Release Notes|2.8]] || 2013/06/20
|-
|[[Rodin Platform 2.7 Release Notes|2.7]] || 2012/11/06
|-
|[[Rodin Platform 2.6 Release Notes|2.6]] || 2012/08/03
|-
|[[Rodin Platform 2.5 Release Notes|2.5]] || 2012/05/02
|-
|[[Rodin Platform 2.4 Release Notes|2.4]] || 2011/01/31
|-
|[[Rodin Platform 2.3 Release Notes|2.3]] || 2011/10/04
|-
|[[Rodin Platform 2.2.2 Release Notes|2.2.2]] || 2011/08/01
|-
|[[Rodin Platform 2.2 Release Notes|2.2]] || 2011/06/01
|-
|[[Rodin Platform 2.1.1 Release Notes|2.1.1]] || 2011/03/15
|-
|[[Rodin Platform 2.1 Release Notes|2.1]] || 2011/02/08
|-
|[[Rodin Platform 2.0.1 Release Notes|2.0.1]] || 2010/11/16
|-
|[[Rodin Platform 2.0 Release Notes|2.0]] || 2010/10/08
|-
|[[Rodin Platform 1.3.1 Release Notes|1.3.1]] || 2010/06/15
|-
|[[Rodin Platform 1.3 Release Notes|1.3]] || 2010/05/05
|-
|[[Rodin Platform 1.2 Release Notes|1.2]] || 2010/02/05
|-
|[[Rodin Platform 1.1 Release Notes|1.1]] || 2009/10/15
|-
|[https://sourceforge.net/projects/rodin-b-sharp/files/Core_%20Rodin%20Platform/1.0/ 1.0] || 2009/07/01
|}

== Release Policy ==
* The Rodin platform is released on an irregular basis.
* The code is frozen during the 2 weeks preceding each release.
* Each release is announced on the [[Mailing_lists | Devel]] mailing list. Two days later, the information is broadcasted on the [[Mailing_lists | Announce]] and [[Mailing_lists | User]] mailing lists.
* The [http://wiki.eclipse.org/index.php/Version_Numbering Eclipse versioning policy] is enforced.
* The optional plug-ins shall strive to meet the release date: the release will not be held back.
* The news related to the optional plug-ins are spread on the [[Mailing_lists | Announce]] and [[Mailing_lists | User]] mailing lists.
* A wiki page is dedicated to each release. Select a version from the lists below to see the corresponding release notes.
* The maintainers of the optional plug-ins shall update the ''External Plug-ins'' page of the concerned release once they have ensured the compatibility of their plug-ins with the Rodin platform.
: To indicate that the plug-in is released and compatible with the current platform, please use the following template:
<nowiki>| [[Image:My_plug-in_logo|30px]] || [[My plug-in info page link | My plug-in]] || version || available || || contact address || Additional notes about the plugin</nowiki>
: To indicate that the plug-in is not yet available and will be released at a later date, please use the following template:
<nowiki>| [[Image:My_plug-in_logo|30px]] || [[My plug-in info page link | My plug-in]] || version || not available || expected_release_date || contact address || Additional notes</nowiki>
: To indicate that the plug-in is no longer maintained for the next version:
<nowiki>| [[Image:My_plug-in_logo|30px]] || [[My plug-in info page link | My plug-in]] || version || not maintained || || contact address|| Additional notes</nowiki>
* The compatibility is preserved upwardly throught model and proof upward compatibility. However, this compatibility is ensured on models and proofs (not on plaform preferences, etc.).
Also, only the latest version is maintained (i.e. there is no maintenance of old releases).

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

Rodin 64 bit

2020-09-11T10:20:51Z

Laurent:

Since [[Rodin_Platform_2.4_Release_Notes|release 2.4]], Rodin is available for 64 bit platforms (Windows, Linux, Mac).

Since [[Rodin_Platform_3.4_Release_Notes|release 3.4]], Rodin is no longer available for 32 bit platforms.

Check the latest download:

http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.5/

Rodin Platform 3.5 Release Notes

2020-09-11T09:35:25Z

Laurent: /* Disclaimer */

{{TOCright}}

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

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

Rodin 3.5 brings lexicographical variants and several bug fixes. It also upgrades the underlying Eclipse to 2020-06, which can be run by all modern Java Runtimes (Java 8 up to 13).

The new lexicographical variant feature means that from now on a machine can contain several variant elements, which are to be understood as a tuple combination (in order of appearance). For instance, if a machine contains the two variants ''V1'' and ''V2'' declared in that order, then a converging event must either decrease ''V1'', or not modify ''V1'' and decrease ''V2''.

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

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

Rodin 3.5 is built on top of Eclipse 4.16 (2020-06), which requires Java 8, just as the previous versions.

There is no API change within Rodin Core.

Following to the introduction of lexicographical variants, a machine can now contain several variant elements. Moreover, variant elements now carry a label attribute. The Rodin tools contain a compatibility layer that allows to read existing machine containing a single unlabelled variant and present it with the new API (using the hardcoded label <code>vrn</code> available from the <code>org.eventb.core.IVariant.DEFAULT_LABEL</code> constant).

== Installing ==

=== Downloading ===

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

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

If you run Rodin 3.1, 3.2, 3.3, or 3.4, then you can upgrade your Rodin Platform by clicking Help > Check for Updates, then select Rodin 3.5 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.5 brings a new version of Eclipse. This means that once you have opened a workspace with Rodin 3.5, you will not be able to open it with a prior version of Rodin anymore. Please consider copying your workspace for Rodin 3.5 to avoid any disaster.

If you run Rodin 3.0 or prior, you cannot upgrade to 3.5. 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 8 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].

== External plug-ins ==
{{:Rodin_Platform_3.5.0_External_Plug-ins}}

== Fixed Bugs and Implemented Features ==

Bugs
783 Launching problem with Java 13
782 Launching error with Java 11
781 Problem with the Rodin proof generator
780 Useless local hypotheses in NAT PO
779 No information when failing to launch external provers
777 Missing refresh in Rodin Editor for event convergence status
776 Rodin Handbook URL broken
774 Java SE 6 required to run Rodin V3.4 on macOS High Sierra ?
775 Editors misinterpret 'generated = false'
773 Update VM arguments for Java 9
772 crash of Rodin V3.4 when opening workspace
771 Proof view: unreadable formulas (white on white)
770 AtelierB plug-in 2.2.0 broken
769 Statistics columns have non uniform widths
765 Generalized Modus Ponens turns goal into "false"
756 Null reasoner input
754 Dropins folder is available again by default
753 Section color preferences are not taken into account
741 Tactic Profile Editing very slow performance
698 Using 'Open With' context menu on PO does not load the PO
618 Proposed name in refine action

Feature Requests
355 Simplify POs for anticipated event further
314 Lexicographic variant

== 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.5. We expect this to be solved for Rodin 3.6. See [[#macOS_specific_requirements|macOS requirements]] for a workaround.

=== macOS in dark mode ===

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

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

== About ==

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

[[Category:Rodin Platform Release Notes]]

Rodin Platform 3.5.0 External Plug-ins

2020-09-11T09:15:12Z

Laurent: Created page with "==== Rodin Update Site ==== Available from http://rodin-b-sharp.sourceforge.net/updates <!-- Please use one of the following templates for the Status column <span st..."

==== Rodin Update Site ====

Available from http://rodin-b-sharp.sourceforge.net/updates



{{SimpleHeader}}
|-
! scope=col | || Plug-in name || Version || Status || MCV* || Release Date || Contact || Additional info
|-
| [[Image:CamilleX.png|CmX]] || [[CamilleX|CamilleX]] || 1.0.0 || available || 3.4.0 || 12 Nov 2018 || [mailto:T.S.Hoang@ecs.soton.ac.uk Thai Son Hoang] || CamilleX provides text editors for Event-B models.
|-
| [[Image:IUMLB_big.png|30px]] || [[Event-B_Classdiagrams|Event-B Class Diagrams]] || 2.0.0 || new release || 3.x.x || 4 Nov 2018 || [mailto:cfs@ecs.soton.ac.uk email] || Class diagrams contained in Event-B Machines.
|-
| [[Image:IUMLB_big.png|30px]] || [[Event-B_Statemachines|Event-B State-machines]] || 4.0.0 || new release || 3.x.x || 4 Nov 2018 || [mailto:cfs@ecs.soton.ac.uk email] || State-machines contained in Event-B Machines.
|-
| [[Image:IUMLB_big.png|30px]] ||[[Event-B_Statemachines|Event-B State-machine Animation]] || 2.4.0 || new release || 3.x.x || 4 Nov 2018 || [mailto:vs2@ecs.soton.ac.uk email] || Compatible with Event-B statemachines 3.x.x and ProB 3.0.x.
|-
| ||[[EMF_framework_for_Event-B|Event-B EMF framework]] || 6.0.0 || new release || 3.x.x || 4 Nov 2018 || [mailto:cfs@ecs.soton.ac.uk email] || Provided for plug-in developers. End users should not need to install this framework. It will be installed automatically by other plug-ins as required.
|-
| ||[[Generic_Event-B_EMF_extensions|Event-B EMF support for extensions]] || 6.0.0 || new release || 3.x.x || 17th Dec 2015 || [mailto:cfs@ecs.soton.ac.uk email] || Provided for plug-in developers. End users should not need to install this framework. It will be installed automatically by other plug-ins as required.
|-
| ||[[Generic_Event-B_EMF_extensions|Event-B EMF support for diagrams]] || 7.0.0 || new release || 3.2.x || 17th Dec 2015 || [mailto:cfs@ecs.soton.ac.uk email] || Provided for plug-in developers. End users should not need to install this framework. It will be installed automatically by other plug-ins as required.
|-
| [[Image:Rose.gif|30px]]||[[Rose_(Structured)_Editor|Rose editor]] || 1.7.0 || new release || 3.x.x || 4 Nov 2018 || [mailto:cfs@ecs.soton.ac.uk email] || Mainly useful for Plug-in developers. Tree-structured editor for Event-B EMF that handles extensions without modification
|-
| [[Image:Project diagram icon s.png|30px]]||[[Project_Diagram|Project Diagram]]|| 1.0.1 || not checked || 3.x.x || 1st Feb. 2015 || [mailto:vs2@ecs.soton.ac.uk email] || Machine - Context relationship diagram
|-
| [[Image:Umlb32.gif|30px]] || [[UML-B|UML-B]] || 2.3.0 || not checked || 3.x.x || 18th Oct. 2014 || [mailto:cfs@ecs.soton.ac.uk email] || Original UML-B modelling environment
|-
| [[Image:Umlb32.gif|30px]] ||[[UML-B_-_Statemachine_Animation|UML-B Statemachine Animation]] || 1.3.0 || not checked || 3.x.x || 18th Oct. 2014 || [mailto:vs2@ecs.soton.ac.uk email] || Compatible with UML-B 2.3 and ProB 3.0
|-
| ||[[EMF_Compare_Editor_installation|Teamwork]] || 1.2.0 || not checked || 3.2.x || 5th Sept. 2016 || [mailto:cfs@ecs.soton.ac.uk email] || Provides a synchronised copy of Machines and Contexts for committing into a repository. It is recommended to also install the Rose editor, EMF compare 3.1.0 and a recent repository client (e.g. Egit 4.1.4).
|-
| [[Image:Cmp_mch_obj.gif|20px]] ||[[Parallel_Composition_using_Event-B | Shared Event Composition]] || 1.7.1 || not checked || || 5th July 2017 || [mailto:cfs@ecs.soton.ac.uk email] || Compatible with Rodin 3.x.x (checked by cfs 5/05/17)
|-
| [[Image:DecompositionPlug-in_logo.png|30px]] || [[Decomposition Plug-in User Guide | Decomposition]] || 1.3.1 || not checked || || 4th July 2017 || [mailto:cfs@ecs.soton.ac.uk email] || Compatible with Rodin 3.x.x (checked by cfs 4/05/17)
|-
| ||[[Refactoring Framework | Refactory ]]|| 1.3.0 || not checked|| 3.x.x || 6th May 2014 || [mailto:asf08r@ecs.soton.ac.uk email] || Compatible with Rodin 3.0.x.
|-
| || [[Theory Plug-in| Theory Plug-in]] || 3.0.0 || not checked|| || 17th Dec 2014|| [mailto:asf08r@ecs.soton.ac.uk email] ||
|-.x
| || [[Code Generation Activity | Code Generation]] || 0.2.5 || not checked|| || 29th Aug. 2013|| [mailto:ae2@ecs.soton.ac.uk email] || For Java, Ada, and OpenMP C code
|-.x
|-
| || Relevance Filter || 1.1.1 || available || ?.x.x || || ||
|-
| || [[Isabelle for Rodin]] || || not checked || 2.x.x || || ||
|-
| || [[SMT_Plug-in | SMT Solvers ]] || 1.4.0 || available || || 15th March 2016|| [mailto:lvoisin@users.sourceforge.net Laurent Voisin] ||
|-
| || [[Pattern | Pattern]] || 0.9.0 || not checked || 3.x.x || 13th March 2015 || [mailto:tshoang@users.sourceforge.net Thai Son Hoang] ||
|-
| || [[Event-B Qualitative Probability User Guide | Qualitative Probability]] || 0.2.3 || available || 3.x.x || 9th October 2015 || [mailto:tshoang@users.sourceforge.net Thai Son Hoang] ||
|-
| || [[B2Latex | B2Latex export]] || 0.7.0 || available || 2.5.x || 27th May 2015 || [mailto:lvoisin@users.sourceforge.net Laurent Voisin] ||
|-
| || [[Generic Instantiation Plug-in User Guide | Generic Instantiation (Soton)]] || 1.0.1 || not checked || || 05th March 2013 || [mailto:asf08r@ecs.soton.ac.uk email] ||
|-
| ||[[Records|Records]] || 2.0.0 || available || 2.x.x || 16th Oct. 2010 || [mailto:cfs@ecs.soton.ac.uk email] ||
|}

==== Atelier B Update Site ====

Available from http://methode-b.com/update_site/atelierb_provers

{{SimpleHeader}}
|-
! scope=col | || Plug-in name || Version || Status || MCV* || Release Date || Contact || Additional info
|-
| || Atelier B provers || 2.2.1 || available || 3.3.0 || 7 Aug 2017 || || Provers from Atelier B
|}

==== ProB Update Site ====

Available from http://www.stups.hhu.de/prob_updates_rodin3

{{SimpleHeader}}
|-
! scope=col | || Plug-in name || Version || Status || MCV* || Release Date || Contact || Additional info
|-
| || ProB || 3.0.10 || available || 3.5.0 || 4 Sep 2020 || || The ProB animator and model checker
|-
| || ProB (Dis)Prover || 3.0.9 || available || 3.5.0 || 4 Sep 2020 || || The ProB counter-example finder and prover
|-
| || ProB Symbolic constants support || 3.0.9 || available || 3.5.0 || 4 Sep 2020 || ||
|}

Rodin Platform 3.5 Release Notes

2020-09-11T08:37:42Z

Laurent: /* Dedication */

{{TOCright}}

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

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

Rodin 3.5 brings lexicographical variants and several bug fixes. It also upgrades the underlying Eclipse to 2020-06, which can be run by all modern Java Runtimes (Java 8 up to 13).

The new lexicographical variant feature means that from now on a machine can contain several variant elements, which are to be understood as a tuple combination (in order of appearance). For instance, if a machine contains the two variants ''V1'' and ''V2'' declared in that order, then a converging event must either decrease ''V1'', or not modify ''V1'' and decrease ''V2''.

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

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

Rodin 3.5 is built on top of Eclipse 4.16 (2020-06), which requires Java 8, just as the previous versions.

There is no API change within Rodin Core.

Following to the introduction of lexicographical variants, a machine can now contain several variant elements. Moreover, variant elements now carry a label attribute. The Rodin tools contain a compatibility layer that allows to read existing machine containing a single unlabelled variant and present it with the new API (using the hardcoded label <code>vrn</code> available from the <code>org.eventb.core.IVariant.DEFAULT_LABEL</code> constant).

== Installing ==

=== Downloading ===

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

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

If you run Rodin 3.1, 3.2, 3.3, or 3.4, then you can upgrade your Rodin Platform by clicking Help > Check for Updates, then select Rodin 3.5 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.5 brings a new version of Eclipse. This means that once you have opened a workspace with Rodin 3.5, you will not be able to open it with a prior version of Rodin anymore. Please consider copying your workspace for Rodin 3.5 to avoid any disaster.

If you run Rodin 3.0 or prior, you cannot upgrade to 3.5. 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 8 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].

== External plug-ins ==
{{:Rodin_Platform_3.5.0_External_Plug-ins}}

== Fixed Bugs and Implemented Features ==

Bugs
783 Launching problem with Java 13
782 Launching error with Java 11
781 Problem with the Rodin proof generator
780 Useless local hypotheses in NAT PO
779 No information when failing to launch external provers
777 Missing refresh in Rodin Editor for event convergence status
776 Rodin Handbook URL broken
774 Java SE 6 required to run Rodin V3.4 on macOS High Sierra ?
775 Editors misinterpret 'generated = false'
773 Update VM arguments for Java 9
772 crash of Rodin V3.4 when opening workspace
771 Proof view: unreadable formulas (white on white)
770 AtelierB plug-in 2.2.0 broken
769 Statistics columns have non uniform widths
765 Generalized Modus Ponens turns goal into "false"
756 Null reasoner input
754 Dropins folder is available again by default
753 Section color preferences are not taken into account
741 Tactic Profile Editing very slow performance
698 Using 'Open With' context menu on PO does not load the PO
618 Proposed name in refine action

Feature Requests
355 Simplify POs for anticipated event further
314 Lexicographic variant

== 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.5. We expect this to be solved for Rodin 3.6. See [[#macOS_specific_requirements|macOS requirements]] for a workaround.

=== macOS in dark mode ===

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

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

== About ==

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

[[Category:Rodin Platform Release Notes]]

Rodin Platform 3.5 Release Notes

2020-09-11T08:37:12Z

Laurent:

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

Rodin 3.5 brings lexicographical variants and several bug fixes. It also upgrades the underlying Eclipse to 2020-06, which can be run by all modern Java Runtimes (Java 8 up to 13).

The new lexicographical variant feature means that from now on a machine can contain several variant elements, which are to be understood as a tuple combination (in order of appearance). For instance, if a machine contains the two variants ''V1'' and ''V2'' declared in that order, then a converging event must either decrease ''V1'', or not modify ''V1'' and decrease ''V2''.

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

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

Rodin 3.5 is built on top of Eclipse 4.16 (2020-06), which requires Java 8, just as the previous versions.

There is no API change within Rodin Core.

Following to the introduction of lexicographical variants, a machine can now contain several variant elements. Moreover, variant elements now carry a label attribute. The Rodin tools contain a compatibility layer that allows to read existing machine containing a single unlabelled variant and present it with the new API (using the hardcoded label <code>vrn</code> available from the <code>org.eventb.core.IVariant.DEFAULT_LABEL</code> constant).

== Installing ==

=== Downloading ===

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

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

If you run Rodin 3.1, 3.2, 3.3, or 3.4, then you can upgrade your Rodin Platform by clicking Help > Check for Updates, then select Rodin 3.5 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.5 brings a new version of Eclipse. This means that once you have opened a workspace with Rodin 3.5, you will not be able to open it with a prior version of Rodin anymore. Please consider copying your workspace for Rodin 3.5 to avoid any disaster.

If you run Rodin 3.0 or prior, you cannot upgrade to 3.5. 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 8 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].

== External plug-ins ==
{{:Rodin_Platform_3.5.0_External_Plug-ins}}

== Fixed Bugs and Implemented Features ==

Bugs
783 Launching problem with Java 13
782 Launching error with Java 11
781 Problem with the Rodin proof generator
780 Useless local hypotheses in NAT PO
779 No information when failing to launch external provers
777 Missing refresh in Rodin Editor for event convergence status
776 Rodin Handbook URL broken
774 Java SE 6 required to run Rodin V3.4 on macOS High Sierra ?
775 Editors misinterpret 'generated = false'
773 Update VM arguments for Java 9
772 crash of Rodin V3.4 when opening workspace
771 Proof view: unreadable formulas (white on white)
770 AtelierB plug-in 2.2.0 broken
769 Statistics columns have non uniform widths
765 Generalized Modus Ponens turns goal into "false"
756 Null reasoner input
754 Dropins folder is available again by default
753 Section color preferences are not taken into account
741 Tactic Profile Editing very slow performance
698 Using 'Open With' context menu on PO does not load the PO
618 Proposed name in refine action

Feature Requests
355 Simplify POs for anticipated event further
314 Lexicographic variant

== 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.5. We expect this to be solved for Rodin 3.6. See [[#macOS_specific_requirements|macOS requirements]] for a workaround.

=== macOS in dark mode ===

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

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

== About ==

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

[[Category:Rodin Platform Release Notes]]

Rodin Platform 3.5 Release Notes

2020-09-11T08:05:18Z

Laurent: /* About */

{{TOCright}}

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

Rodin 3.5 brings lexicographical variants and several bug fixes. It also upgrades the underlying Eclipse to 2020-06, which can be run by all modern Java Runtimes (Java 8 up to 13).

The new lexicographical variant feature means that from now on a machine can contain several variant elements, which are to be understood as a tuple combination (in order of appearance). For instance, if a machine contains the two variants ''V1'' and ''V2'' declared in that order, then a converging event must either decrease ''V1'', or not modify ''V1'' and decrease ''V2''.

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

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

Rodin 3.5 is built on top of Eclipse 4.16 (2020-06), which requires Java 8, just as the previous versions.

There is no API change within Rodin Core.

Following to the introduction of lexicographical variants, a machine can now contain several variant elements. Moreover, variant elements now carry a label attribute. The Rodin tools contain a compatibility layer that allows to read existing machine containing a single unlabelled variant and present it with the new API (using the hardcoded label <code>vrn</code> available from the <code>org.eventb.core.IVariant.DEFAULT_LABEL</code> constant).

== Installing ==

=== Downloading ===

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

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

If you run Rodin 3.1, 3.2, 3.3, or 3.4, then you can upgrade your Rodin Platform by clicking Help > Check for Updates, then select Rodin 3.5 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.5 brings a new version of Eclipse. This means that once you have opened a workspace with Rodin 3.5, you will not be able to open it with a prior version of Rodin anymore. Please consider copying your workspace for Rodin 3.5 to avoid any disaster.

If you run Rodin 3.0 or prior, you cannot upgrade to 3.5. 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 8 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].

== External plug-ins ==
{{:Rodin_Platform_3.5.0_External_Plug-ins}}

== Fixed Bugs and Implemented Features ==

Bugs
783 Launching problem with Java 13
782 Launching error with Java 11
781 Problem with the Rodin proof generator
780 Useless local hypotheses in NAT PO
779 No information when failing to launch external provers
777 Missing refresh in Rodin Editor for event convergence status
776 Rodin Handbook URL broken
774 Java SE 6 required to run Rodin V3.4 on macOS High Sierra ?
775 Editors misinterpret 'generated = false'
773 Update VM arguments for Java 9
772 crash of Rodin V3.4 when opening workspace
771 Proof view: unreadable formulas (white on white)
770 AtelierB plug-in 2.2.0 broken
769 Statistics columns have non uniform widths
765 Generalized Modus Ponens turns goal into "false"
756 Null reasoner input
754 Dropins folder is available again by default
753 Section color preferences are not taken into account
741 Tactic Profile Editing very slow performance
698 Using 'Open With' context menu on PO does not load the PO
618 Proposed name in refine action

Feature Requests
355 Simplify POs for anticipated event further
314 Lexicographic variant

== 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.5. We expect this to be solved for Rodin 3.6. See [[#macOS_specific_requirements|macOS requirements]] for a workaround.

=== macOS in dark mode ===

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

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

== About ==

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

[[Category:Rodin Platform Release Notes]]

Rodin Platform 3.5 Release Notes

2020-09-11T08:02:38Z

Laurent: /* Rodin is not notarized */

{{TOCright}}

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

Rodin 3.5 brings lexicographical variants and several bug fixes. It also upgrades the underlying Eclipse to 2020-06, which can be run by all modern Java Runtimes (Java 8 up to 13).

The new lexicographical variant feature means that from now on a machine can contain several variant elements, which are to be understood as a tuple combination (in order of appearance). For instance, if a machine contains the two variants ''V1'' and ''V2'' declared in that order, then a converging event must either decrease ''V1'', or not modify ''V1'' and decrease ''V2''.

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

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

Rodin 3.5 is built on top of Eclipse 4.16 (2020-06), which requires Java 8, just as the previous versions.

There is no API change within Rodin Core.

Following to the introduction of lexicographical variants, a machine can now contain several variant elements. Moreover, variant elements now carry a label attribute. The Rodin tools contain a compatibility layer that allows to read existing machine containing a single unlabelled variant and present it with the new API (using the hardcoded label <code>vrn</code> available from the <code>org.eventb.core.IVariant.DEFAULT_LABEL</code> constant).

== Installing ==

=== Downloading ===

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

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

If you run Rodin 3.1, 3.2, 3.3, or 3.4, then you can upgrade your Rodin Platform by clicking Help > Check for Updates, then select Rodin 3.5 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.5 brings a new version of Eclipse. This means that once you have opened a workspace with Rodin 3.5, you will not be able to open it with a prior version of Rodin anymore. Please consider copying your workspace for Rodin 3.5 to avoid any disaster.

If you run Rodin 3.0 or prior, you cannot upgrade to 3.5. 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 8 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].

== External plug-ins ==
{{:Rodin_Platform_3.5.0_External_Plug-ins}}

== Fixed Bugs and Implemented Features ==

Bugs
783 Launching problem with Java 13
782 Launching error with Java 11
781 Problem with the Rodin proof generator
780 Useless local hypotheses in NAT PO
779 No information when failing to launch external provers
777 Missing refresh in Rodin Editor for event convergence status
776 Rodin Handbook URL broken
774 Java SE 6 required to run Rodin V3.4 on macOS High Sierra ?
775 Editors misinterpret 'generated = false'
773 Update VM arguments for Java 9
772 crash of Rodin V3.4 when opening workspace
771 Proof view: unreadable formulas (white on white)
770 AtelierB plug-in 2.2.0 broken
769 Statistics columns have non uniform widths
765 Generalized Modus Ponens turns goal into "false"
756 Null reasoner input
754 Dropins folder is available again by default
753 Section color preferences are not taken into account
741 Tactic Profile Editing very slow performance
698 Using 'Open With' context menu on PO does not load the PO
618 Proposed name in refine action

Feature Requests
355 Simplify POs for anticipated event further
314 Lexicographic variant

== 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.5. We expect this to be solved for Rodin 3.6. See [[#macOS_specific_requirements|macOS requirements]] for a workaround.

=== macOS in dark mode ===

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

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

== About ==
TODO
Rodin Platform with git commit: 6980ca1 
User Release date : 2018/03/07.

[[Category:Rodin Platform Release Notes]]

Rodin Platform 3.5 Release Notes

2020-09-11T07:58:03Z

Laurent: /* Requirements - Compatibility */

{{TOCright}}

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

Rodin 3.5 brings lexicographical variants and several bug fixes. It also upgrades the underlying Eclipse to 2020-06, which can be run by all modern Java Runtimes (Java 8 up to 13).

The new lexicographical variant feature means that from now on a machine can contain several variant elements, which are to be understood as a tuple combination (in order of appearance). For instance, if a machine contains the two variants ''V1'' and ''V2'' declared in that order, then a converging event must either decrease ''V1'', or not modify ''V1'' and decrease ''V2''.

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

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

Rodin 3.5 is built on top of Eclipse 4.16 (2020-06), which requires Java 8, just as the previous versions.

There is no API change within Rodin Core.

Following to the introduction of lexicographical variants, a machine can now contain several variant elements. Moreover, variant elements now carry a label attribute. The Rodin tools contain a compatibility layer that allows to read existing machine containing a single unlabelled variant and present it with the new API (using the hardcoded label <code>vrn</code> available from the <code>org.eventb.core.IVariant.DEFAULT_LABEL</code> constant).

== Installing ==

=== Downloading ===

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

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

If you run Rodin 3.1, 3.2, 3.3, or 3.4, then you can upgrade your Rodin Platform by clicking Help > Check for Updates, then select Rodin 3.5 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.5 brings a new version of Eclipse. This means that once you have opened a workspace with Rodin 3.5, you will not be able to open it with a prior version of Rodin anymore. Please consider copying your workspace for Rodin 3.5 to avoid any disaster.

If you run Rodin 3.0 or prior, you cannot upgrade to 3.5. 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 8 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].

== External plug-ins ==
{{:Rodin_Platform_3.5.0_External_Plug-ins}}

== Fixed Bugs and Implemented Features ==

Bugs
783 Launching problem with Java 13
782 Launching error with Java 11
781 Problem with the Rodin proof generator
780 Useless local hypotheses in NAT PO
779 No information when failing to launch external provers
777 Missing refresh in Rodin Editor for event convergence status
776 Rodin Handbook URL broken
774 Java SE 6 required to run Rodin V3.4 on macOS High Sierra ?
775 Editors misinterpret 'generated = false'
773 Update VM arguments for Java 9
772 crash of Rodin V3.4 when opening workspace
771 Proof view: unreadable formulas (white on white)
770 AtelierB plug-in 2.2.0 broken
769 Statistics columns have non uniform widths
765 Generalized Modus Ponens turns goal into "false"
756 Null reasoner input
754 Dropins folder is available again by default
753 Section color preferences are not taken into account
741 Tactic Profile Editing very slow performance
698 Using 'Open With' context menu on PO does not load the PO
618 Proposed name in refine action

Feature Requests
355 Simplify POs for anticipated event further
314 Lexicographic variant

== 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.5. We expect this to be solved for Rodin 3.6.

=== macOS in dark mode ===

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

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

== About ==
TODO
Rodin Platform with git commit: 6980ca1 
User Release date : 2018/03/07.

[[Category:Rodin Platform Release Notes]]

Rodin Platform 3.5 Release Notes

2020-09-11T07:43:29Z

Laurent: /* Requirements - Compatibility */

{{TOCright}}

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

Rodin 3.5 brings lexicographical variants and several bug fixes. It also upgrades the underlying Eclipse to 2020-06, which can be run by all modern Java Runtimes (Java 8 up to 13).

The new lexicographical variant feature means that from now on a machine can contain several variant elements, which are to be understood as a tuple combination (in order of appearance). For instance, if a machine contains the two variants ''V1'' and ''V2'' declared in that order, then a converging event must either decrease ''V1'', or not modify ''V1'' and decrease ''V2''.

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

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

Rodin 3.5 is built on top of Eclipse 4.16 (2020-06), which requires Java 8, just as the previous versions.

There is no API change within Rodin Core.

Following to the introduction of lexicographical variants, a machine can now contain several variant elements. Moreover, variant elements now carry a label attribute. The Rodin tools contain a compatibility layer that allows to read existing machine containing a single unlabelled variant and present it with the new API (using the hardcoded label <code>vrn</code> available from the <code>org.eventb.core.IVariant.DEFAULT_LABEL</code> constant).

== Installing ==

=== Downloading ===

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

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

If you run Rodin 3.1, 3.2, 3.3, or 3.4, then you can upgrade your Rodin Platform by clicking Help > Check for Updates, then select Rodin 3.5 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.5 brings a new version of Eclipse. This means that once you have opened a workspace with Rodin 3.5, you will not be able to open it with a prior version of Rodin anymore. Please consider copying your workspace for Rodin 3.5 to avoid any disaster.

If you run Rodin 3.0 or prior, you cannot upgrade to 3.5. You need to download the platform from SourceForge and reinstall your external plugins.

== Requirements - Compatibility ==

* Configurations supported (and for which binaries are provided)
** 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.

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

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

== External plug-ins ==
{{:Rodin_Platform_3.5.0_External_Plug-ins}}

== Fixed Bugs and Implemented Features ==

Bugs
783 Launching problem with Java 13
782 Launching error with Java 11
781 Problem with the Rodin proof generator
780 Useless local hypotheses in NAT PO
779 No information when failing to launch external provers
777 Missing refresh in Rodin Editor for event convergence status
776 Rodin Handbook URL broken
774 Java SE 6 required to run Rodin V3.4 on macOS High Sierra ?
775 Editors misinterpret 'generated = false'
773 Update VM arguments for Java 9
772 crash of Rodin V3.4 when opening workspace
771 Proof view: unreadable formulas (white on white)
770 AtelierB plug-in 2.2.0 broken
769 Statistics columns have non uniform widths
765 Generalized Modus Ponens turns goal into "false"
756 Null reasoner input
754 Dropins folder is available again by default
753 Section color preferences are not taken into account
741 Tactic Profile Editing very slow performance
698 Using 'Open With' context menu on PO does not load the PO
618 Proposed name in refine action

Feature Requests
355 Simplify POs for anticipated event further
314 Lexicographic variant

== 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.5. We expect this to be solved for Rodin 3.6.

=== macOS in dark mode ===

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

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

== About ==
TODO
Rodin Platform with git commit: 6980ca1 
User Release date : 2018/03/07.

[[Category:Rodin Platform Release Notes]]

Rodin Platform 3.5 Release Notes

2020-09-11T07:42:01Z

Laurent: /* Upgrading from a previous version of Rodin 3.x */

{{TOCright}}

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

Rodin 3.5 brings lexicographical variants and several bug fixes. It also upgrades the underlying Eclipse to 2020-06, which can be run by all modern Java Runtimes (Java 8 up to 13).

The new lexicographical variant feature means that from now on a machine can contain several variant elements, which are to be understood as a tuple combination (in order of appearance). For instance, if a machine contains the two variants ''V1'' and ''V2'' declared in that order, then a converging event must either decrease ''V1'', or not modify ''V1'' and decrease ''V2''.

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

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

Rodin 3.5 is built on top of Eclipse 4.16 (2020-06), which requires Java 8, just as the previous versions.

There is no API change within Rodin Core.

Following to the introduction of lexicographical variants, a machine can now contain several variant elements. Moreover, variant elements now carry a label attribute. The Rodin tools contain a compatibility layer that allows to read existing machine containing a single unlabelled variant and present it with the new API (using the hardcoded label <code>vrn</code> available from the <code>org.eventb.core.IVariant.DEFAULT_LABEL</code> constant).

== Installing ==

=== Downloading ===

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

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

If you run Rodin 3.1, 3.2, 3.3, or 3.4, then you can upgrade your Rodin Platform by clicking Help > Check for Updates, then select Rodin 3.5 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.5 brings a new version of Eclipse. This means that once you have opened a workspace with Rodin 3.5, you will not be able to open it with a prior version of Rodin anymore. Please consider copying your workspace for Rodin 3.5 to avoid any disaster.

If you run Rodin 3.0 or prior, you cannot upgrade to 3.5. You need to download the platform from SourceForge and reinstall your external plugins.

== Requirements - Compatibility ==

* Configurations supported (and for which binaries are provided)
** 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.

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

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

== External plug-ins ==
{{:Rodin_Platform_3.5.0_External_Plug-ins}}

== Fixed Bugs and Implemented Features ==

Bugs
783 Launching problem with Java 13
782 Launching error with Java 11
781 Problem with the Rodin proof generator
780 Useless local hypotheses in NAT PO
779 No information when failing to launch external provers
777 Missing refresh in Rodin Editor for event convergence status
776 Rodin Handbook URL broken
774 Java SE 6 required to run Rodin V3.4 on macOS High Sierra ?
775 Editors misinterpret 'generated = false'
773 Update VM arguments for Java 9
772 crash of Rodin V3.4 when opening workspace
771 Proof view: unreadable formulas (white on white)
770 AtelierB plug-in 2.2.0 broken
769 Statistics columns have non uniform widths
765 Generalized Modus Ponens turns goal into "false"
756 Null reasoner input
754 Dropins folder is available again by default
753 Section color preferences are not taken into account
741 Tactic Profile Editing very slow performance
698 Using 'Open With' context menu on PO does not load the PO
618 Proposed name in refine action

Feature Requests
355 Simplify POs for anticipated event further
314 Lexicographic variant

== 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.5. We expect this to be solved for Rodin 3.6.

=== macOS in dark mode ===

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

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

== About ==
TODO
Rodin Platform with git commit: 6980ca1 
User Release date : 2018/03/07.

[[Category:Rodin Platform Release Notes]]

Rodin Platform 3.5 Release Notes

2020-09-08T14:37:49Z

Laurent:

{{TOCright}}

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

Rodin 3.5 brings lexicographical variants and several bug fixes. It also upgrades the underlying Eclipse to 2020-06, which can be run by all modern Java Runtimes (Java 8 up to 13).

The new lexicographical variant feature means that from now on a machine can contain several variant elements, which are to be understood as a tuple combination (in order of appearance). For instance, if a machine contains the two variants ''V1'' and ''V2'' declared in that order, then a converging event must either decrease ''V1'', or not modify ''V1'' and decrease ''V2''.

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

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

Rodin 3.5 is built on top of Eclipse 4.16 (2020-06), which requires Java 8, just as the previous versions.

There is no API change within Rodin Core.

Following to the introduction of lexicographical variants, a machine can now contain several variant elements. Moreover, variant elements now carry a label attribute. The Rodin tools contain a compatibility layer that allows to read existing machine containing a single unlabelled variant and present it with the new API (using the hardcoded label <code>vrn</code> available from the <code>org.eventb.core.IVariant.DEFAULT_LABEL</code> constant).

== Installing ==

=== Downloading ===

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

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

TODO CHECK IS THIS IS TRUE

The only way to upgrade is to download the new platform.
You may then point it to your usual workspace(s).
This restriction is due to the Eclipse switch.

For those who are annoyed to install their Rodin plug-ins once more by downloading from the update site, it might be worth installing them directly from your older Rodin installation:
* run the new Rodin
* File > Import... > Install/From Existing Installation
* Point to your older Rodin installation
* Select the features you want to install
* Proceed with the Next button, the following is just as a usual install

== Requirements - Compatibility ==

* Configurations supported (and for which binaries are provided)
** 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.

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

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

== External plug-ins ==
{{:Rodin_Platform_3.5.0_External_Plug-ins}}

== Fixed Bugs and Implemented Features ==

Bugs
783 Launching problem with Java 13
782 Launching error with Java 11
781 Problem with the Rodin proof generator
780 Useless local hypotheses in NAT PO
779 No information when failing to launch external provers
777 Missing refresh in Rodin Editor for event convergence status
776 Rodin Handbook URL broken
774 Java SE 6 required to run Rodin V3.4 on macOS High Sierra ?
775 Editors misinterpret 'generated = false'
773 Update VM arguments for Java 9
772 crash of Rodin V3.4 when opening workspace
771 Proof view: unreadable formulas (white on white)
770 AtelierB plug-in 2.2.0 broken
769 Statistics columns have non uniform widths
765 Generalized Modus Ponens turns goal into "false"
756 Null reasoner input
754 Dropins folder is available again by default
753 Section color preferences are not taken into account
741 Tactic Profile Editing very slow performance
698 Using 'Open With' context menu on PO does not load the PO
618 Proposed name in refine action

Feature Requests
355 Simplify POs for anticipated event further
314 Lexicographic variant

== 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.5. We expect this to be solved for Rodin 3.6.

=== macOS in dark mode ===

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

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

== About ==
TODO
Rodin Platform with git commit: 6980ca1 
User Release date : 2018/03/07.

[[Category:Rodin Platform Release Notes]]

Rodin Platform 3.5 Release Notes

2020-09-08T14:14:37Z

Laurent: /* Fixed Bugs and Implemented Features */

{{TOCright}}

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

Rodin 3.5 brings several bug fixes, and upgrades the underlying Eclipse to 2020-06.

Please note that we no longer provide 32-bit binary versions of the Rodin platform, since they are almost not downloaded anymore (as per the statistics on SourceForge), everyone is now running a 64-bit OS. Nonetheless, if needed, it is still possible for you to build 32-bit binaries from the source (see [[Building Rodin Headless]], you may also ask for [https://sourceforge.net/projects/rodin-b-sharp/support support]).

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

Rodin 3.5 is built on top of Eclipse 4.16 (2020-06), which requires Java 8, just as the previous versions.

There is no API change within Rodin Core.

TODO Several variants in the same machine

== Installing ==

=== Downloading ===

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

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

TODO CHECK IS THIS IS TRUE

The only way to upgrade is to download the new platform.
You may then point it to your usual workspace(s).
This restriction is due to the Eclipse switch.

For those who are annoyed to install their Rodin plug-ins once more by downloading from the update site, it might be worth installing them directly from your older Rodin installation:
* run the new Rodin
* File > Import... > Install/From Existing Installation
* Point to your older Rodin installation
* Select the features you want to install
* Proceed with the Next button, the following is just as a usual install

== Requirements - Compatibility ==

* Configurations supported (and for which binaries are provided)
** Linux 64-bit
** Windows 64-bit
** Mac OS X 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.

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

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

== External plug-ins ==
{{:Rodin_Platform_3.5.0_External_Plug-ins}}

== Fixed Bugs and Implemented Features ==

Bugs
783 Launching problem with Java 13
782 Launching error with Java 11
781 Problem with the Rodin proof generator
780 Useless local hypotheses in NAT PO
779 No information when failing to launch external provers
777 Missing refresh in Rodin Editor for event convergence status
776 Rodin Handbook URL broken
774 Java SE 6 required to run Rodin V3.4 on macOS High Sierra ?
775 Editors misinterpret 'generated = false'
773 Update VM arguments for Java 9
772 crash of Rodin V3.4 when opening workspace
771 Proof view: unreadable formulas (white on white)
770 AtelierB plug-in 2.2.0 broken
769 Statistics columns have non uniform widths
765 Generalized Modus Ponens turns goal into "false"
756 Null reasoner input
754 Dropins folder is available again by default
753 Section color preferences are not taken into account
741 Tactic Profile Editing very slow performance
698 Using 'Open With' context menu on PO does not load the PO
618 Proposed name in refine action

Feature Requests
355 Simplify POs for anticipated event further
314 Lexicographic variant

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

=== Rodin is not notarized ===

TODO

=== macOS in dark mode ===

TODO

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

== About ==
TODO
Rodin Platform with git commit: 6980ca1 
User Release date : 2018/03/07.

[[Category:Rodin Platform Release Notes]]

Rodin Platform 3.5 Release Notes

2020-09-08T12:35:04Z

Laurent: /* Fixed Bugs and Implemented Features */

{{TOCright}}

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

Rodin 3.5 brings several bug fixes, and upgrades the underlying Eclipse to 2020-06.

Please note that we no longer provide 32-bit binary versions of the Rodin platform, since they are almost not downloaded anymore (as per the statistics on SourceForge), everyone is now running a 64-bit OS. Nonetheless, if needed, it is still possible for you to build 32-bit binaries from the source (see [[Building Rodin Headless]], you may also ask for [https://sourceforge.net/projects/rodin-b-sharp/support support]).

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

Rodin 3.5 is built on top of Eclipse 4.16 (2020-06), which requires Java 8, just as the previous versions.

There is no API change within Rodin Core.

TODO Several variants in the same machine

== Installing ==

=== Downloading ===

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

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

TODO CHECK IS THIS IS TRUE

The only way to upgrade is to download the new platform.
You may then point it to your usual workspace(s).
This restriction is due to the Eclipse switch.

For those who are annoyed to install their Rodin plug-ins once more by downloading from the update site, it might be worth installing them directly from your older Rodin installation:
* run the new Rodin
* File > Import... > Install/From Existing Installation
* Point to your older Rodin installation
* Select the features you want to install
* Proceed with the Next button, the following is just as a usual install

== Requirements - Compatibility ==

* Configurations supported (and for which binaries are provided)
** Linux 64-bit
** Windows 64-bit
** Mac OS X 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.

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

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

== External plug-ins ==
{{:Rodin_Platform_3.5.0_External_Plug-ins}}

== Fixed Bugs and Implemented Features ==

Bugs
TODO
783 Launching problem with Java 13
782 Launching error with Java 11
781 Problem with the Rodin proof generator
780 Useless local hypotheses in NAT PO
779 No information when failing to launch external provers
777 Missing refresh in Rodin Editor for event convergence status
775 Editors misinterpret 'generated = false'
773 Update VM arguments for Java 9
756 Null reasoner input
754 Dropins folder is available again by default
698 Using 'Open With' context menu on PO does not load the PO
618 Proposed name in refine action

Feature Requests
355 Simplify POs for anticipated event further
314 Lexicographic variant

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

=== Rodin is not notarized ===

TODO

=== macOS in dark mode ===

TODO

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

== About ==
TODO
Rodin Platform with git commit: 6980ca1 
User Release date : 2018/03/07.

[[Category:Rodin Platform Release Notes]]

Rodin Platform 3.5 Release Notes

2020-09-08T12:31:12Z

Laurent: /* Fixed Bugs and Implemented Features */

{{TOCright}}

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

Rodin 3.5 brings several bug fixes, and upgrades the underlying Eclipse to 2020-06.

Please note that we no longer provide 32-bit binary versions of the Rodin platform, since they are almost not downloaded anymore (as per the statistics on SourceForge), everyone is now running a 64-bit OS. Nonetheless, if needed, it is still possible for you to build 32-bit binaries from the source (see [[Building Rodin Headless]], you may also ask for [https://sourceforge.net/projects/rodin-b-sharp/support support]).

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

Rodin 3.5 is built on top of Eclipse 4.16 (2020-06), which requires Java 8, just as the previous versions.

There is no API change within Rodin Core.

TODO Several variants in the same machine

== Installing ==

=== Downloading ===

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

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

TODO CHECK IS THIS IS TRUE

The only way to upgrade is to download the new platform.
You may then point it to your usual workspace(s).
This restriction is due to the Eclipse switch.

For those who are annoyed to install their Rodin plug-ins once more by downloading from the update site, it might be worth installing them directly from your older Rodin installation:
* run the new Rodin
* File > Import... > Install/From Existing Installation
* Point to your older Rodin installation
* Select the features you want to install
* Proceed with the Next button, the following is just as a usual install

== Requirements - Compatibility ==

* Configurations supported (and for which binaries are provided)
** Linux 64-bit
** Windows 64-bit
** Mac OS X 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.

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

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

== External plug-ins ==
{{:Rodin_Platform_3.5.0_External_Plug-ins}}

== Fixed Bugs and Implemented Features ==

Bugs
TODO
783 Launching problem with Java 13
782 Launching error with Java 11
781 Problem with the Rodin proof generator
779 No information when failing to launch external provers
777 Missing refresh in Rodin Editor for event convergence status
775 Editors misinterpret 'generated = false'
773 Update VM arguments for Java 9
756 Null reasoner input
754 Dropins folder is available again by default
698 Using 'Open With' context menu on PO does not load the PO
618 Proposed name in refine action

Feature Requests
355 Simplify POs for anticipated event further
314 Lexicographic variant

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

=== Rodin is not notarized ===

TODO

=== macOS in dark mode ===

TODO

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

== About ==
TODO
Rodin Platform with git commit: 6980ca1 
User Release date : 2018/03/07.

[[Category:Rodin Platform Release Notes]]

Rodin Platform 3.5 Release Notes

2020-09-08T09:55:25Z

Laurent: Created page with "{{TOCright}} == What's New in Rodin 3.5? == Rodin 3.5 brings several bug fixes, and upgrades the underlying Eclipse to 2020-06. Please note that we no longer provide 32-bit..."

{{TOCright}}

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

Rodin 3.5 brings several bug fixes, and upgrades the underlying Eclipse to 2020-06.

Please note that we no longer provide 32-bit binary versions of the Rodin platform, since they are almost not downloaded anymore (as per the statistics on SourceForge), everyone is now running a 64-bit OS. Nonetheless, if needed, it is still possible for you to build 32-bit binaries from the source (see [[Building Rodin Headless]], you may also ask for [https://sourceforge.net/projects/rodin-b-sharp/support support]).

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

Rodin 3.5 is built on top of Eclipse 4.16 (2020-06), which requires Java 8, just as the previous versions.

There is no API change within Rodin Core.

TODO Several variants in the same machine

== Installing ==

=== Downloading ===

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

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

TODO CHECK IS THIS IS TRUE

The only way to upgrade is to download the new platform.
You may then point it to your usual workspace(s).
This restriction is due to the Eclipse switch.

For those who are annoyed to install their Rodin plug-ins once more by downloading from the update site, it might be worth installing them directly from your older Rodin installation:
* run the new Rodin
* File > Import... > Install/From Existing Installation
* Point to your older Rodin installation
* Select the features you want to install
* Proceed with the Next button, the following is just as a usual install

== Requirements - Compatibility ==

* Configurations supported (and for which binaries are provided)
** Linux 64-bit
** Windows 64-bit
** Mac OS X 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.

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

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

== External plug-ins ==
{{:Rodin_Platform_3.5.0_External_Plug-ins}}

== Fixed Bugs and Implemented Features ==

Bugs
TODO
777 Missing refresh in Rodin Editor for event convergence status

Feature Requests
TODO
None

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

=== Rodin is not notarized ===

TODO

=== macOS in dark mode ===

TODO

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

== About ==
TODO
Rodin Platform with git commit: 6980ca1 
User Release date : 2018/03/07.

[[Category:Rodin Platform Release Notes]]