Difference between pages "Rodin Platform 3.5 Release Notes" and "Theory Plug-in Developer Documentation"

Revision as of 14:45, 14 June 2021

This page provides some documentation for developers of the Theory plug-in. Documentation for users of the plug-in is available in this page.

Eclipse setup

Clone the git repository from Sourceforge
Import the subdirectories of the git repository in Eclipse (each subdirectory corresponds to an Eclipse project providing an Eclipse feature or plug-in)
Open org.eventb.theory.feature/org.eventb.theory.feature.target and click on Set as Active Target Platform, at the top right of the window; this assumes that the Rodin target platform has been downloaded and put in /var/tmp: if this location is not available, or if another version of Rodin is should be targeted, edit the .target file accordingly

Release checklist

To release a new version of the plug-in:

Tag the last commit with the version number (remember to pass the --tags flag to git push to publish it)
On Sourceforge, create a new folder with the version number in the plug-in's directory and upload the files of the update site there (they are built in org.eventb.theory.repository/target/repository)
Update the composite Eclipse repository that provides the Rodin plug-ins:
- Clone the RodinUpdateSite folder from the Subversion repository and import it in Eclipse
- Open the compSite.xml file, add a <repository> line for the new version and follow the instructions in the file's comments to build the composite repository
- Connect with an SFTP client to web.sourceforge.net (see Sourceforge's documentation) and upload the files built previously (p2.index, compositeArtifacts.jar, compositeContent.jar) in /home/project-web/rodin-b-sharp/htdocs/updates
Publish the release notes in the Theory Plug-in page, update the table in the Rodin Platform Releases page and list the release in Template:Dev News (it is included in the front page)
Announce the release on the Rodin mailing lists rodin-b-sharp-user@lists.sourceforge.net and rodin-b-sharp-announce@lists.sourceforge.net

@@ Line 1: / Line 1: @@
-{{TOCright}}
+This page provides some documentation for developers of the Theory plug-in. Documentation for users of the plug-in is available in [[Theory Plug-in|this page]].
-== Dedication to Ken Robinson ==
+== Eclipse setup ==
-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.
+* Clone the [https://sourceforge.net/p/rodin-b-sharp/theory git repository] from Sourceforge
+* Import the subdirectories of the git repository in Eclipse (each subdirectory corresponds to an Eclipse project providing an Eclipse feature or plug-in)
+* Open <code>org.eventb.theory.feature/org.eventb.theory.feature.target</code> and click on ''Set as Active Target Platform'', at the top right of the window; this assumes that the [https://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.5/org.rodinp.dev-3.5.0-9f39f1653.zip/download Rodin target platform] has been downloaded and put in <code>/var/tmp</code>: if this location is not available, or if another version of Rodin is should be targeted, edit the <code>.target</code> file accordingly
-== What's New in Rodin 3.5? ==
+== Release checklist ==
-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).
+To release a new version of the plug-in:
-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''.
+* Tag the last commit with the version number (remember to pass the <code>--tags</code> flag to <code>git push</code> to publish it)
+* On Sourceforge, create a new folder with the version number in the [https://sourceforge.net/projects/rodin-b-sharp/files/Plugin_Theory/ plug-in's directory] and upload the files of the update site there (they are built in <code>org.eventb.theory.repository/target/repository</code>)
+* Update the composite Eclipse repository that provides the Rodin plug-ins:
+** Clone the <code>RodinUpdateSite</code> folder from the [https://sourceforge.net/p/rodin-b-sharp/svn/HEAD/tree/trunk/RodinUpdateSite/ Subversion repository] and import it in Eclipse
+** Open the <code>compSite.xml</code> file, add a <code>&lt;repository&gt;</code> line for the new version and follow the instructions in the file's comments to build the composite repository
+** Connect with an SFTP client to <code>web.sourceforge.net</code> (see [https://sourceforge.net/p/forge/documentation/SFTP#for-managing-project-web-space Sourceforge's documentation]) and upload the files built previously (<code>p2.index</code>, <code>compositeArtifacts.jar</code>, <code>compositeContent.jar</code>) in <code>/home/project-web/rodin-b-sharp/htdocs/updates</code>
+* Publish the release notes in the [[Theory Plug-in]] page, update the table in the [[Rodin Platform Releases]] page and list the release in [[Template:Dev News]] (it is included in the front page)
+* Announce the release on the Rodin mailing lists rodin-b-sharp-user@lists.sourceforge.net and rodin-b-sharp-announce@lists.sourceforge.net
-Please note that we only provide 64-bit binary versions of the Rodin platform.
+[[Category:Developer documentation]]
-=== 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
-Launching problem with Java 13
-Launching error with Java 11
-Problem with the Rodin proof generator
-Useless local hypotheses in NAT PO
-No information when failing to launch external provers
-Missing refresh in Rodin Editor for event convergence status
-Rodin Handbook URL broken
-Java SE 6 required to run Rodin V3.4 on macOS High Sierra ?
-Editors misinterpret 'generated = false'
-Update VM arguments for Java 9
-crash of Rodin V3.4 when opening workspace
-Proof view: unreadable formulas (white on white)
-AtelierB plug-in 2.2.0 broken
-Statistics columns have non uniform widths
-Generalized Modus Ponens turns goal into "false"
-Null reasoner input
-Dropins folder is available again by default
-Section color preferences are not taken into account
-Tactic Profile Editing very slow performance
-Using 'Open With' context menu on PO does not load the PO
-Proposed name in refine action
-Feature Requests
-Simplify POs for anticipated event further
-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><br/>
-User Release date : 2020/09/11.
-[[Category:Rodin Platform Release Notes]]

Difference between pages "Rodin Platform 3.5 Release Notes" and "Theory Plug-in Developer Documentation"

Revision as of 14:45, 14 June 2021

Eclipse setup

Release checklist

Navigation menu

Page actions

Page actions

Personal tools

Navigation

contribute

Search

Tools