Difference between pages "Rodin Platform 1.1 Release Notes" and "Switch from CVS to Subversion"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Afuerst
 
imported>Laurent
(Added section "Where Are my Modules")
 
Line 1: Line 1:
 
{{TOCright}}
 
{{TOCright}}
  
== What's New in Rodin 1.1? ==
+
The switch from CVS to Subversion took place Friday 13 March 2009. Before this date, all source code used to be managed in a CVS repository hosted by SourceForge.  After this date, source code is managed in a Subversion repository also hosted by SourceForge.
  
* [[Rodin_Keyboard | Rodin Keyboard]]
+
==How to Access the Repository from Eclipse==
:A new extensible plug-in for the Event-B Keyboard is included. The former one, namely <tt>org.eventb.eventBKeyboard</tt>, translated hard-coded key combos into hard-coded unicode mathematical symbols. There is now one main plug-in, <tt>org.rodinp.keyboard</tt>, that defines a mere extension point <tt>org.rodinp.keyboard.symbols</tt> to define associations between an ASCII sequence and a symbol. It avoids hard-coding anything.
 
:There are currently two extensions of this point:
 
# One in the plug-in <tt>org.eventb.keyboard</tt>, for standard Event-B notation translation.
 
# One in the plug-in <tt>ch.ethz.eventb.keyboard.latex</tt>, for LaTeX notation translation.
 
  
* [[Versioned Reasoners | Versioned Reasoners]]
+
To access the subversion repository, you need to install a Subversion plug-in into your Eclipse development platform.  There is currently two plug-ins that are known to work quite well: [http://subclipse.tigris.org/ Subclipse] and [http://www.eclipse.org/subversive/ Subversive].  We do not recommend yet which plug-in to use, but experience will tell. What is currently known is that it would be a bad idea to install both plug-ins in the same platform as they conflict with each other.
:The reasoners are now tagged with a version, which will evolve along with their behavior.
 
  
* New [[All_Rewrite_Rules | Rewriting rules]] and on prover rules are included:
+
The repository itself is available at URL [https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp  https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp].
# Arithmetic rules (''e.g.'' the form <math>A+B+C-B \defi A+C</math> and a few others)
 
# DEF_IN_UPTO: <math>x \in a \upto b \defi a \leq x \land x \leq b</math>
 
# [http://www.cs.cmu.edu/afs/cs/academic/class/15671-f95/www/handouts/proof/node1.html One point rule]
 
# Goals of the form <math>\exists n \qdot \forall x \qdot x \in S \limp x \leq n</math> when you have a hypothesis that states <math>finite(S)</math>
 
# SIMP_SPECIAL_OVERL
 
# SIMP_FUNIMAGE_LAMBDA
 
  
* [[New Tactic Providers | New Tactic Providers]]
+
==Where Are my Modules==
:A new tactic provider extension API is proposed. It allows tactic providers to give several possible tactic applications, even at the same position in a predicate. This new mechanism is also intended to fit with rule-based provers needs.
 
  
* Proof obligations
+
Just after the switch from CVS to Subversion, certain CVS modules have been moved to clean up the root of the repository. The modules below have been moved to the new <tt>RodinCore</tt> directory:
:The POG does not not generate any longer THM POs for guards when the conditions have already been proved for the abstract event.
+
fr.systerel.explorer
 +
fr.systerel.explorer.tests
 +
org.eventb.core
 +
org.eventb.core.ast
 +
org.eventb.core.ast.tests
 +
org.eventb.core.seqprover
 +
org.eventb.core.seqprover.doc.isv
 +
org.eventb.core.seqprover.tests
 +
org.eventb.core.tests
 +
org.eventb.doc.user
 +
org.eventb.eventBKeyboard
 +
org.eventb.eventBKeyboard.tests
 +
org.eventb.ide
 +
org.eventb.ide-feature
 +
org.eventb.pp
 +
org.eventb.pp.tests
 +
org.eventb.pp.ui
 +
org.eventb.pptrans
 +
org.eventb.pptrans.tests
 +
org.eventb.ui
 +
org.eventb.ui.icons
 +
org.eventb.ui.tests
 +
org.rodinp
 +
org.rodinp-feature
 +
org.rodinp.core
 +
org.rodinp.core.tests
 +
org.rodinp.platform
 +
org.rodinp.platform-feature
 +
org.rodinp.releng
 +
and the following modules have been moved to the new <tt>XProver</tt> directory:
 +
org.eventb.xprover.tptp.core
 +
org.eventb.xprover.tptp.core.tests
 +
org.eventb.xprover.tptp.spass.core
 +
org.eventb.xprover.tptp.spass.core.linux
 +
org.eventb.xprover.tptp.spass.core.macosx
 +
org.eventb.xprover.tptp.spass.core.tests
 +
org.eventb.xprover.tptp.spass.ui
 +
org.eventb.xprover.tptp.ui
 +
and the following modules have been moved to the new <tt>AnimB</tt> directory:
 +
org.animb.animation.stubclient
 +
org.animb.core
 +
org.animb.core.tests
 +
org.animb.eclipseBuilder
 +
org.animb.eclipseBuilder.test
 +
org.animb.eventsexecutor
 +
org.animb.export
 +
org.animb.feature
 +
org.animb.feature-def
 +
org.animb.history
 +
org.animb.ipConnectionTest
 +
org.animb.ipconnection
 +
org.animb.ipconnectionplugin
 +
org.animb.observer
 +
org.animb.server
 +
org.animb.serverplugin
 +
org.animb.site
 +
org.animb.ui.utils
 +
org.animb.updatesite
 +
org.animb.valuation
  
* [[Generated Model Elements | Generated Model Elements]]
+
==How to Move from CVS to Subversion==
:The generated event-B files are tagged. These files cannot be modified.
 
  
* [[Symbol Table | Symbol Table]]
+
The simpler is to create a second workspace on your computer and to launch two Eclipse programs, one on each workspace. For each project checked out in the CVS workspace, just checkout the same project in the Subversion workspace.
:A symbol table view is provided. It contains the mathematical symbols. When clicking on a symbol, it is included at the current position in the text of the Rodin Context/Machine editor.
 
  
* PO Icons
+
If you have some yet uncommitted changes in your CVS workspace, you can select the files and drag and drop them in the appropriate place in the Subversion workspace.  Alternatively, you can create a patch.  For that, select the project(s) that contain uncommitted changes, then select {{menu|Team > Create Patch...}} from the context menu and follow the wizard. Then, in the Subversion workspace, select {{menu|Team > Apply Patch...}} to apply the patch.
:Changed color of 'pending' icon for undischarged POs from red to orange/brown.
 
:Used 'pending_pale' icons for unattempted POs in explorer.
 
  
* Modulo
+
==Procedure Used for Moving CVS History to Subversion==
:Reinforced the WD condition for the modulo operator. We now have exactly the same condition as in classical B: <math>x \bmod b~</math> is well-defined iff <math>0 \leq x \land 0 < y</math>.
 
  
== Requirements ==
+
When switching from CVS to Subversion, we made our best to keep the history of all files. We followed this procedure:
* It is recommended to run the Rodin platform with a Java 1.5 Runtime Environment.  
+
<ol>
* Only a 32-bit version of the Rodin platform is provided. Some optional libraries dedicated to 32-bit support may be required in order to run it on a 64-bit OS. Moreover, you will have to install a 32-bit Java Virtual Machine (JVM), and then to set the -vm option to make sure that Rodin is run with the correct JVM.
+
<li>retrieve a copy of the whole CVS repository into directory <tt>cvs</tt></li>
:''eg.'' <tt>/usr/local/rodin/rodin -vm /usr/lib/jvm/ia32-java-1.5.0-sun/bin/java</tt> (You have to adjust paths to your system.)
+
<li>launch commands</li>
 +
cvs2svn -q --dumpfile=svndump --force-tag=GMF2 --encoding=utf-8 --encoding=latin1 cvs
 +
svndumpfilter exclude CVSROOT < svndump > svndump2
 +
gzip -9 svndump2
 +
<li>upload file <tt>svndump2.gz</tt> to SourceForge</li>
 +
<li>start a shell service on SourceForge and type the following commands</li>
 +
adminrepo --checkout svn
 +
zcat svndump2.gz | svnadmin load /svnroot/rodin-b-sharp
 +
adminrepo --save svn
 +
</ol>
  
== External plug-ins ==
+
Note that the filtering on <tt>CVSROOT</tt> didn't seem to work as expected: this directory still occurred in the SVN trunk and had to be removed manually.
 
 
=== Rodin Update Site ===
 
* [[UML-B_Release_History|UML-B 0.6.0]] 
 
* [[Event-BEMF_ReleaseHistory|Event-B EMF Framework 1.1.2]]
 
* [[Feature_Composition_Release_History|Feature Composition Plug-in 0.0.3]]
 
* [[Refactoring_Framework_Release_History|Refactoring Framework Plug-in 0.0.4]]
 
* [[Shared Event Composition_Release_History|Shared Event Composition Plug-in 1.1.4]]
 
 
 
=== Modularisation Plug-in Update Site ===
 
* [[Modularisation Plug-in|Modularisation Plug-in 1.0.2]]
 
 
 
=== Prob Update Site ===
 
* [[Text_Editor|Camille Texteditor]] 
 
* [http://www.stups.uni-duesseldorf.de/ProB ProB] and ProB Disprover (currently only Mac OS and Linux)
 
* [http://www.stups.uni-duesseldorf.de/BMotionStudio/ BMotion Studio]
 
 
 
=== ETHZ Update Site ===
 
* [[Pattern|Pattern Plug-in 0.8.0]]
 
 
 
== Downloading ==
 
[https://sourceforge.net/projects/rodin-b-sharp/files/Core_%20Rodin%20Platform/1.1/ Download Now!]
 
 
 
== Fixed Bugs and Implemented Feature Requests ==
 
  Bug 1822179: Problem with XML parser
 
  Bug 1830816: Incorrect associativity of function application
 
  Bug 1834722: no horizontal scroll bars
 
  Bug 1926739: Machine Renaming
 
  Bug 2004000: The cursor is not visible at the end of text fields.
 
  Bug 2024804: No typecheck error when missing INITIALISATION
 
  Bug 2616436: SWTException when deleting an element
 
  Bug 2648926: Post-Tactic is invoked after saving
 
  Bug 2782166: Clean & Build
 
  Bug 2804049: Exception on partition sent to ML
 
  Bug 2814047: Refines clause on INITIALISATION event ignored
 
  Bug 2818588: Long formulas not broken across lines
 
  Bug 2821439: functional simplification
 
  Bug 2821449: functional simplification
 
  Bug 2824401: NPE when following a marker
 
  Bug 2829164: exception in navigator
 
  Bug 2830809: parser inconsistent with Mathematical Language Specification
 
  Bug 2840549: Development: Building problem for path with blank
 
  Bug 2841423: use of set comprehension?
 
  Bug 2856893: Impossible to add an element to an event-B component
 
  Bug 2860800: Paths of Plugins (again)
 
  Bug 2864985: Problem with Design of EventBRoot
 
  Bug 2865874: Error when calling ML
 
  Bug 2031274: Rename problem
 
 
 
  FR 1592016: Automatic Completion
 
  FR 1740718: Verification for New Internal Element Wizards
 
  FR 1909636: Arithmetics simplification
 
  FR 1936295: Automatic rule for <+
 
  FR 1942487: Remove membership for range
 
  FR 2140186: prooving when using "lambda expression"
 
  FR 2782135: Pretty Print Font Size
 
  FR 2803368: Versioning reasoners
 
  FR 2817266: Copy of full projects
 
  FR 2864252: Anticipated events in last refinement
 
 
 
== Known Issues ==
 
 
 
* XULRunner 1.9.1 may cause an SWT exception that prevents from opening an editor (as well as any browser-based ui component). To fix it, it is possible to specify XULRunner path to point to 1.9.0: edit "rodin.ini" and add the following line:
 
-Dorg.eclipse.swt.browser.XULRunnerPath=/usr/lib/xulrunner-1.9.0.14
 
where "/usr/lib/xulrunner-1.9.0.14" must be replaced with your actual XULRunner 1.9.0 install directory.
 
 
 
* The list of the currently open bugs is given below:
 
 
 
  Bug 1441596: Tool conflicts caused by identically named files
 
  Bug 1737819: WD properties are not fully propagated
 
  Bug 1743521: Event keyboard : abusive mapping in insertion mode
 
  Bug 1766826: Error messages from math parser incomprehensible
 
  Bug 1813657: Refactoring menu is not related to refactoring
 
  Bug 1818464: Trivial PO does not discharge
 
  Bug 1819316: Existential PO does not discharge
 
  Bug 1820566: Problem with naming in Windows
 
  Bug 1824177: B4free prover translation for <<-> fails
 
  Bug 1824569: Error Markers in Synthesis view do not update
 
  Bug 1841129: Incorrect proof status
 
  Bug 1897572: Error in Proof Obligation Generator
 
  Bug 1919546: P1,PP,M0-M3 not available as post tactic
 
  Bug 1922694: Crazy Copy/Paste
 
  Bug 1948095: importing existing projects
 
  Bug 1949927: newPP is too sensitive to unused hyps
 
  Bug 1954442: Too many handles used by Edit page on Windows
 
  Bug 1977355: Edit tab does not reflect changes made by other programs
 
  Bug 2082375: input file write-protection a problem to Rodin
 
  Bug 2105507: too difficult to work with explicit set expressions
 
  Bug 2174629: No PO generated for unrefined event
 
  Bug 2371318: Unable to apply equality from left to right
 
  Bug 2414463: Builder called on non-Rodin files
 
  Bug 2417801: Simplified hypothesis is not hidden
 
  Bug 2433212: Poor performance under KDE
 
  Bug 2510307: Proof information window empty for grd/WD
 
  Bug 2531738: RODIN crash adding text to note or text box in class diagram
 
  Bug 2573332: Long formulas get truncated
 
  Bug 2630205: reasoning with "finite" clause
 
  Bug 2648946: Predicate Provers (newPP, P0) unable to discharge simple PO
 
  Bug 2656831: saving proofs does not always work
 
  Bug 2657540: Synthesis view: elements inverted
 
  Bug 2694492: proB widget do not display on second proB launch
 
  Bug 2744052: NullPointerException in Builder on cyclic refinement
 
  Bug 2782126: Your platform does not support SWT Browser widget.
 
  Bug 2782243: BraveSansMono
 
  Bug 2815882: Primed identifiers are allowed
 
  Bug 2817523: No paste in root contextual menu of explorer
 
  Bug 2818587: Machine renaming not propagated to extends clauses
 
  Bug 2824204: Change to Rodin Elements not reflected in editor
 
  Bug 2827806: Zombie files in buffer
 
  Bug 2835692: Text Editor exception
 
  Bug 2836774: Text Editor unable to save  (exception)
 
  Bug 2844786: Invisible icons in Proof Control coolbar
 
  Bug 2844797: The Proof Skeleton View does not adapt to the container
 
  Bug 2844813: Turnstile unicode character
 
  Bug 2844889: Plug-in installation in Rodin platform
 
  Bug 2869663: Changing the font in the pretty print view
 
  Bug 2871281: Bad display of marked math symbols
 
  Bug 2871290: Comments are still editable in a generated model
 
  
 +
[[Category:Developer documentation]]
 
[[Category:Rodin Platform]]
 
[[Category:Rodin Platform]]

Revision as of 00:12, 14 March 2009

The switch from CVS to Subversion took place Friday 13 March 2009. Before this date, all source code used to be managed in a CVS repository hosted by SourceForge. After this date, source code is managed in a Subversion repository also hosted by SourceForge.

How to Access the Repository from Eclipse

To access the subversion repository, you need to install a Subversion plug-in into your Eclipse development platform. There is currently two plug-ins that are known to work quite well: Subclipse and Subversive. We do not recommend yet which plug-in to use, but experience will tell. What is currently known is that it would be a bad idea to install both plug-ins in the same platform as they conflict with each other.

The repository itself is available at URL https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp.

Where Are my Modules

Just after the switch from CVS to Subversion, certain CVS modules have been moved to clean up the root of the repository. The modules below have been moved to the new RodinCore directory:

fr.systerel.explorer
fr.systerel.explorer.tests
org.eventb.core
org.eventb.core.ast
org.eventb.core.ast.tests
org.eventb.core.seqprover
org.eventb.core.seqprover.doc.isv
org.eventb.core.seqprover.tests
org.eventb.core.tests
org.eventb.doc.user
org.eventb.eventBKeyboard
org.eventb.eventBKeyboard.tests
org.eventb.ide
org.eventb.ide-feature
org.eventb.pp
org.eventb.pp.tests
org.eventb.pp.ui
org.eventb.pptrans
org.eventb.pptrans.tests
org.eventb.ui
org.eventb.ui.icons
org.eventb.ui.tests
org.rodinp
org.rodinp-feature
org.rodinp.core
org.rodinp.core.tests
org.rodinp.platform
org.rodinp.platform-feature
org.rodinp.releng

and the following modules have been moved to the new XProver directory:

org.eventb.xprover.tptp.core
org.eventb.xprover.tptp.core.tests
org.eventb.xprover.tptp.spass.core
org.eventb.xprover.tptp.spass.core.linux
org.eventb.xprover.tptp.spass.core.macosx
org.eventb.xprover.tptp.spass.core.tests
org.eventb.xprover.tptp.spass.ui
org.eventb.xprover.tptp.ui

and the following modules have been moved to the new AnimB directory:

org.animb.animation.stubclient
org.animb.core
org.animb.core.tests
org.animb.eclipseBuilder
org.animb.eclipseBuilder.test
org.animb.eventsexecutor
org.animb.export
org.animb.feature
org.animb.feature-def
org.animb.history
org.animb.ipConnectionTest
org.animb.ipconnection
org.animb.ipconnectionplugin
org.animb.observer
org.animb.server
org.animb.serverplugin
org.animb.site
org.animb.ui.utils
org.animb.updatesite
org.animb.valuation

How to Move from CVS to Subversion

The simpler is to create a second workspace on your computer and to launch two Eclipse programs, one on each workspace. For each project checked out in the CVS workspace, just checkout the same project in the Subversion workspace.

If you have some yet uncommitted changes in your CVS workspace, you can select the files and drag and drop them in the appropriate place in the Subversion workspace. Alternatively, you can create a patch. For that, select the project(s) that contain uncommitted changes, then select Team > Create Patch... from the context menu and follow the wizard. Then, in the Subversion workspace, select Team > Apply Patch... to apply the patch.

Procedure Used for Moving CVS History to Subversion

When switching from CVS to Subversion, we made our best to keep the history of all files. We followed this procedure:

  1. retrieve a copy of the whole CVS repository into directory cvs
  2. launch commands
  3. cvs2svn -q --dumpfile=svndump --force-tag=GMF2 --encoding=utf-8 --encoding=latin1 cvs svndumpfilter exclude CVSROOT < svndump > svndump2 gzip -9 svndump2
  4. upload file svndump2.gz to SourceForge
  5. start a shell service on SourceForge and type the following commands
  6. adminrepo --checkout svn zcat svndump2.gz | svnadmin load /svnroot/rodin-b-sharp adminrepo --save svn

Note that the filtering on CVSROOT didn't seem to work as expected: this directory still occurred in the SVN trunk and had to be removed manually.