{"id":702,"date":"2021-02-25T17:15:53","date_gmt":"2021-02-25T16:15:53","guid":{"rendered":"https:\/\/wp.software.imdea.org\/cbc\/?page_id=702"},"modified":"2026-02-15T16:34:50","modified_gmt":"2026-02-15T15:34:50","slug":"rodin-installation-and-tips","status":"publish","type":"page","link":"https:\/\/wp.software.imdea.org\/cbc\/rodin-installation-and-tips\/","title":{"rendered":"Rodin: Installation and Basic  Tips"},"content":{"rendered":"\n<h3 class=\"wp-block-heading\">Install Rodin<br><\/h3>\n\n\n\n<div class=\"wp-block-group\"><div class=\"wp-block-group__inner-container is-layout-flow wp-block-group-is-layout-flow\">\n<p class=\"is-style-info\">A tool to develop Event B models and discharge proof obligations using<br>semi-automatic theorem provers.<\/p>\n<\/div><\/div>\n\n\n\n<p class=\"is-style-warning\">I have tested the installation of Rodin 3.9 in Linux, but not in Windows or Mac. If you (try to) install it in a Windows or Mac machine and you experience any errors and\/or find workarounds, please share your experience with your classmates through the class mailing list.<\/p>\n\n\n\n<p><\/p>\n\n\n\n<ul class=\"wp-block-list\">\n<li>Download latest version from <a href=\"https:\/\/sourceforge.net\/projects\/rodin-b-sharp\/files\/Core_Rodin_Platform\/\" target=\"_blank\" rel=\"noreferrer noopener\">https:\/\/sourceforge.net\/projects\/rodin-b-sharp\/files\/Core_Rodin_Platform\/<\/a>\n<ul class=\"wp-block-list\">\n<li>Enter the directory of the last <strong>stable<\/strong> version (3.9, at the time of writing).<\/li>\n\n\n\n<li>Pay attention to the instructions at the bottom of that page.<\/li>\n\n\n\n<li>Download the version corresponding to your OS (ignore <code>org.rodinp.dev-*.zip<\/code> files).<\/li>\n\n\n\n<li>Uncompress, follow instructions.<\/li>\n<\/ul>\n<\/li>\n\n\n\n<li>Start Rodin!<\/li>\n\n\n\n<li>Go to <em>Help<\/em> \u2192 <em>Install New Software<\/em> \u2192 choose <em>Atelier B Provers<\/em> from the <em>Work with<\/em> drop-down menu \u2192 select it \u2192 click <em>Next<\/em>. Follow instructions.<\/li>\n<\/ul>\n\n\n\n<h3 class=\"wp-block-heading\">If Rodin Does Not Start. . .<\/h3>\n\n\n\n<p>Make sure to have Java 1.8 JDK installed (I believe Java JRE is not enough). Oracle Java may be necessary.<\/p>\n\n\n\n<div class=\"wp-block-columns is-layout-flex wp-container-core-columns-is-layout-9d6595d7 wp-block-columns-is-layout-flex\">\n<div class=\"wp-block-column is-layout-flow wp-block-column-is-layout-flow\">\n<h5 class=\"wp-block-heading\">Mac Os X<\/h5>\n\n\n\n<ul class=\"wp-block-list\">\n<li>Change attributes of rodin.app (see instructions in download page).<\/li>\n\n\n\n<li>New M1 , M2, M3 Macs: runtime translation seems to work.<\/li>\n<\/ul>\n<\/div>\n\n\n\n<div class=\"wp-block-column is-layout-flow wp-block-column-is-layout-flow\">\n<h5 class=\"wp-block-heading\">Windows<\/h5>\n\n\n\n<ul class=\"wp-block-list\">\n<li>I can offer little help here.<\/li>\n<\/ul>\n<\/div>\n\n\n\n<div class=\"wp-block-column is-layout-flow wp-block-column-is-layout-flow\">\n<h5 class=\"wp-block-heading\">(Ubuntu) Linux<\/h5>\n\n\n\n<ul class=\"wp-block-list\">\n<li>Rodin 3.9 works out of the box in Ubuntu 25.10.<\/li>\n<\/ul>\n<\/div>\n<\/div>\n\n\n\n<h5 class=\"wp-block-heading\"><br>If everything fails<br><\/h5>\n\n\n\n<ul class=\"wp-block-list\">\n<li>Check Event-B \/ Rodin the mailing lists at <a href=\"https:\/\/sourceforge.net\/p\/rodin-b-sharp\/mailman\/\">https:\/\/sourceforge.net\/p\/rodin-b-sharp\/mailman\/<\/a><\/li>\n\n\n\n<li>Ask in the course mailing list at <a href=\"mailto:cbc@software.imdea.org\">cbc@software.imdea.org<\/a> .<\/li>\n<\/ul>\n\n\n\n<h3 class=\"wp-block-heading\">Using Rodin<\/h3>\n\n\n\n<ul class=\"wp-block-list\">\n<li>Using the theorem prover will be your next task.<\/li>\n\n\n\n<li>To do so: ensure first your installation is working!<\/li>\n<\/ul>\n\n\n\n<p class=\"is-style-warning coblocks-alert-paragraph\">Please import the \u201c<a href=\"https:\/\/wp.software.imdea.org\/cbc\/wp-content\/uploads\/sites\/5\/2021\/02\/IntegerDivision.zip\">integer division<\/a>\u201d example. Check the section \u201c<em>Exporting and Importing Projects<\/em>\u201d below. Click on the project, expand the <code>ID_M0<\/code> component, make sure the \u201c<em>Proof Obligations<\/em>\u201d section has a green icon at its left. <img loading=\"lazy\" decoding=\"async\" width=\"227\" height=\"33\" class=\"wp-image-742\" style=\"width: 150px\" src=\"https:\/\/wp.software.imdea.org\/cbc\/wp-content\/uploads\/sites\/5\/2021\/02\/proof-obligations-green.png\" alt=\"\"><\/p>\n\n\n\n<h3 class=\"wp-block-heading editing\">Editing models<\/h3>\n\n\n\n<ul class=\"wp-block-list\">\n<li>Editing models: right-click on keywords for a drop-down menu with<br>elements to add. <\/li>\n\n\n\n<li>Useful keybindings:<ul><li><code>Alt-G<\/code>: add children element e.g., if in THEN, add action.<\/li><li><code>Alt-T<\/code>: add sibling element e.g., if finished with one guard, add another guard.<\/li><li><code>Ctrl-S<\/code>: save model, run auto-provers, update proof status.<\/li><li><code>Return<\/code> in an editable section: turn edition on an off.<\/li><li><code>TAB<\/code>: go to the next editable section.<\/li><\/ul>\n<ul class=\"wp-block-list\">\n<li><em>Help<\/em> \u2192 <em>Show Active Keybindings<\/em>: more keybindings.<\/li>\n\n\n\n<li><em>Help \u2192 Help Contents \u2192 Rodin Keyboard User Guide \u2192 Introduction<\/em>: list of special symbols and how to insert them using the keyboard. There is also a <em>Symbols<\/em> tab on the bottom right pane that shows symbols that can be clicked to insert them. However, using the keyboard is much faster.<\/li>\n<\/ul>\n<\/li>\n\n\n\n<li>\u201c<em>Explorer window<\/em>\u201d: expand project, machine \/ context, \u201c<em>Proof Obligations<\/em>\u201d to check undischarged proofs: <img loading=\"lazy\" decoding=\"async\" width=\"241\" height=\"28\" class=\"wp-image-712\" style=\"width: 150px\" src=\"https:\/\/wp.software.imdea.org\/cbc\/wp-content\/uploads\/sites\/5\/2021\/02\/proof-obligations-brown.png\" alt=\"\">\n<ul class=\"wp-block-list\">\n<li>Double click on undischarged proof: <img loading=\"lazy\" decoding=\"async\" width=\"264\" height=\"35\" class=\"wp-image-713\" style=\"width: 150px\" src=\"https:\/\/wp.software.imdea.org\/cbc\/wp-content\/uploads\/sites\/5\/2021\/02\/undischarged-proof.png\" alt=\"\"><\/li>\n\n\n\n<li>Switch to \u201c<em>Prover view<\/em>\u201d in icons under menu: <img loading=\"lazy\" decoding=\"async\" width=\"97\" height=\"39\" class=\"wp-image-714\" style=\"width: 97px\" src=\"https:\/\/wp.software.imdea.org\/cbc\/wp-content\/uploads\/sites\/5\/2021\/02\/prover-view-switch.png\" alt=\"\"> (or in <em>Window <em>\u2192<\/em><\/em> <em>Perspective <em>\u2192<\/em> Open Perspective<\/em> in some versions of Rodin).<\/li>\n\n\n\n<li>Switch back to \u201c<em>Event-B view<\/em>\u201d to continue editing.<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n\n\n\n<h3 class=\"wp-block-heading\" id=\"export-import\">Exporting and Importing Projects<\/h3>\n\n\n\n<p><br><strong>Exporting<\/strong> (full reference at <a href=\"https:\/\/www3.hhu.de\/stups\/handbook\/rodin\/current\/html\/sect0032.html\">https:\/\/www3.hhu.de\/stups\/handbook\/rodin\/current\/html\/sect0032.html<\/a>):<\/p>\n\n\n\n<ul class=\"wp-block-list\">\n<li>Select project, right-click and select <em>Export<\/em>.<\/li>\n\n\n\n<li>Select <em>General<\/em> <em>\u2192<\/em> <em>Archive<\/em> File, click <em>Next<\/em>.<\/li>\n\n\n\n<li>Choose path and file name; click <em>Finish<\/em>.<\/li>\n<\/ul>\n\n\n\n<p><br><strong>Importing<\/strong> (full reference at <a href=\"https:\/\/www3.hhu.de\/stups\/handbook\/rodin\/current\/html\/sect0033.html\">https:\/\/www3.hhu.de\/stups\/handbook\/rodin\/current\/html\/sect0033.html<\/a>):<\/p>\n\n\n\n<ul class=\"wp-block-list\">\n<li><em>File<\/em> <em>\u2192<\/em> <em>Import<\/em> from menu.<\/li>\n\n\n\n<li>Select <em>General<\/em> <em>\u2192<\/em> <em>Existing Projects into Workspace<\/em>, click <em>Next<\/em>.<\/li>\n\n\n\n<li>Choose <em>Select archive file<\/em>, then <em>Browse<\/em>.<\/li>\n\n\n\n<li>Find zip file and click <em>Finish<\/em>.<\/li>\n<\/ul>\n\n\n\n<p class=\"aligncenter is-style-warning coblocks-alert-paragraph\"><strong>Note: importing will fail if project names clash.<\/strong><br>You can right-click and <em>Rename<\/em> before exporting (to save under a different name), or before importing (to change name of target project).<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Install Rodin A tool to develop Event B models and discharge proof obligations usingsemi-automatic theorem provers. I have tested the installation of Rodin 3.9 in Linux, but not in Windows or Mac. If you (try to) install it in a Windows or Mac machine and you experience any errors and\/or find workarounds, please share your &hellip; <a href=\"https:\/\/wp.software.imdea.org\/cbc\/rodin-installation-and-tips\/\" class=\"more-link\">Continue reading<span class=\"screen-reader-text\"> &#8220;Rodin: Installation and Basic  Tips&#8221;<\/span><\/a><\/p>\n","protected":false},"author":4,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"_coblocks_attr":"Georgia,Arial,","_coblocks_dimensions":"","_coblocks_responsive_height":"","_coblocks_accordion_ie_support":"","ngg_post_thumbnail":0,"footnotes":""},"class_list":["post-702","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/wp.software.imdea.org\/cbc\/wp-json\/wp\/v2\/pages\/702","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/wp.software.imdea.org\/cbc\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/wp.software.imdea.org\/cbc\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/wp.software.imdea.org\/cbc\/wp-json\/wp\/v2\/users\/4"}],"replies":[{"embeddable":true,"href":"https:\/\/wp.software.imdea.org\/cbc\/wp-json\/wp\/v2\/comments?post=702"}],"version-history":[{"count":98,"href":"https:\/\/wp.software.imdea.org\/cbc\/wp-json\/wp\/v2\/pages\/702\/revisions"}],"predecessor-version":[{"id":1767,"href":"https:\/\/wp.software.imdea.org\/cbc\/wp-json\/wp\/v2\/pages\/702\/revisions\/1767"}],"wp:attachment":[{"href":"https:\/\/wp.software.imdea.org\/cbc\/wp-json\/wp\/v2\/media?parent=702"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}