Difference between pages "Building Rodin Headless" and "Code Generation Activity"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Nicolas
m (→‎Pre Build Verifications: added verifications about documentation)
 
imported>Andy
 
Line 1: Line 1:
−
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
+
=== Demonstrator Version Release ===
−
# Fetch the sources from Subversion and make a source archive with them.
+
Date: 30 November 2010:
−
# Build the platform headless from this set of sources using Apache Ant.
 
  
−
==Pre Build Verifications==
+
available from: https://sourceforge.net/projects/codegenerationd/files/
  
−
Before building, several checks have to be made in the sources:
+
The WindowsBundles directory contains a Rodin 1.3.1 platform with the Code-Gen plug-ins together with a patch plug-in. The patch plug-in is required to correct a difficulty that we encountered with the org.eventb.emf.persistence plug-in. Simply extract the appropriate zip file into a directory and run the rodin.exe. The plug-ins are pre-installed so no further configuration should be necessary.
−
* the correct Eclipse version is referenced in the p2 configuration (org.rodinp.platform/p2.inf)
 
−
* branding plug-ins display the correct Eclipse version (text information found in several about.properties/plugin.properties files)
 
−
* SVN project org.rodinp.releng is up to date, i.e. all required plug-ins are listed/processed in
 
−
** rodin-core.psf
 
−
** rodin-tests.psf
 
−
** customTargets.xml (copySources)
 
−
** export-RodinCore-src-jars.xml
 
−
* documentation is up to date for /org.rodinp.platform/html/root.html
 
−
* generated documentation matches latest wiki sources for
 
−
** /org.eventb.doc.user/html
 
−
** /org.rodinp.keyboard/doc
 
−
* make a local test within Eclipse:
 
−
** import (binary with linked content) org.eclipse.pde.build into the Eclipse workspace containing Rodin sources
 
−
** run "Build Rodin Product.launch": if everything went well, a directory "${workspace_loc}/../work/result" contains zipped archives for every platform, else errors are reported in the console.
 
  
−
When everything works, any changes to the sources made during this verification process are committed to the Source Forge repository (the below-mentioned Subversion revision is that of this commit).
+
A non-bundled version can be created using the info in the advanced folder using the update site. An example project, and a project forming the basis of a simple tutorial are provided in the accompanying zip file. The content in the zip file is already included in the bundled version.
  
−
==Build Parameters==
+
Mac users - sorry no bundled version available at present, but the update site, install instructions and example projects are available in the advanced directory. We could create a bundled version upon request; meanwhile we are be working on a Rodin 2.0 version, which should be available through the usual update mechanism.
  
−
Three parameters need to be defined for each build:
+
==== A Step by Step tutorial will be available soon ====
−
# the platform version, that is the user-visible version which is displayed in ''About Rodin Platform''.  Example of versions are <tt>1.0</tt> and <tt>1.0RC1</tt>.
 
−
# the Subversion revision number, which permits to know very precisely which source versions are used for the build.
 
−
# the full platform version used for provisioning. This version is made of three digits separated by dots. Example of full versions are <tt>1.0.0</tt> and <tt>1.1.0</tt>.
 
  
−
==Fetching Sources==
+
The SVN repository for code generation resides here:
  
−
Sources are fetched from Subversion using the script below. The script can be run on any Unix machine and takes the first two parameters described above (i.e., platform version and subversion revision). For instance, to build Rodin 1.1, the script was invoked as
+
  svn+ssh://svn.ecs.soton.ac.uk/projects/deploy-exploratory/trunk/CodeGeneration
−
fetchSources 1.1 7661
 
  
−
The script itself is
+
The SVN repository for tagged builds is here:
−
<nowiki>#!/bin/sh
 
−
#
 
−
#  Fetch sources of the Rodin Platform from the Subversion repository on
 
−
#  SourceForge.
 
−
#
 
  
−
SVNROOT=http://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp
+
svn+ssh://svn.ecs.soton.ac.uk/projects/deploy-exploratory/tags/CodeGeneration
−
SVNURL=$SVNROOT/trunk/RodinCore
 
−
export SVNROOT SVNURL
 
  
−
fatal() {
+
=== Completed/Ongoing Work ===
−
    echo "$@" >&2
+
* Demonstration plug-in,
−
    exit 1
+
** ready for deployment.
−
}
+
** deployment/Integration Testing under way.
 +
* The plug-in consists of,
 +
** a tasking Development Generator.
 +
** a tasking Development Editor (Based on an EMF Tree Editor).
 +
** a translator, from Tasking Development to Common Language Model.
 +
** a translator, from the Tasking Development to Event-B model of the implementation.
 +
** a pretty-printer for the Tasking Development.
 +
** a pretty-printer for Common Language Model, which generates Ada Source Code.
  
−
checkRevision() {
+
=== The Demonstration Plug-in Release ===
−
    if expr "$SVNREV" : '^[0-9][0-9]*$' >/dev/null; then
+
The demonstration plug-in is planned for release around November-end 2010, if all goes well. It must be emphasised that the Code Generation (CG) Feature is a demonstration tool; a proof of concept, rather than a prototype. The tool has no static checker and, therefore, there will be a heavy reliance on docs and dialogue to facilitate exploration of the tools and concepts. We will be working on this aspect in due course.
−
: OK
 
−
    else
 
−
fatal "Invalid SVN revision number: $SVNREV"
 
−
    fi
 
−
}
 
  
−
fetchSources() {
+
=== Metamodels ===
−
    mkdir sources || fatal "Some sources have already been checked out."
+
* In the plug-in we define several meta-models:
−
    cd sources
+
** CompositeControl: for the control flow (algorithmic) constructs such as branch, loop and sequence etc. These constructs may be used in the specification of either  sequential or concurrent systems.
−
    fetchProject org.rodinp.releng
+
** Tasking Meta-model: defines the tasking model where we attach tasking specific details, such as task priority, task type. The tasking structures provide the ability to define single tasking or multi-tasking (concurrent) systems. We make use of the composite control plug-in to specify the flow of control.  
−
    cat org.rodinp.releng/rodin-core.psf |
+
** IL1 Meta-model: defines an abstraction of common programming language constructs for use in translations to implementations.
−
sed -e '\,trunk/RodinCore/,!d' \
 
−
    -e 's,.*RodinCore/,,'  \
 
−
    -e 's/,.*//' |
 
−
while read m; do
 
−
    fetchProject "$m"
 
−
done
 
−
}
 
  
−
fetchProject() {
+
=== Translation Rules ===
−
    m="$1"
+
* Tasking to IL1/Event-B translation rules [[http://wiki.event-b.org/images/Translation.pdf]]
−
    echo "Fetching $m"
 
−
    svn -q export -r "$SVNREV" "$SVNURL/$m" "$m"
 
−
}
 
−
 
 
−
 
 
−
[ $# -eq 2 ] || fatal "Usage: $0 <Rodin_version> <SVN_revision>"
 
−
VERSION="$1"
 
−
SVNREV="$2"
 
−
checkRevision
 
−
fetchSources
 
−
zip -q -r "../rodin-${VERSION}-sources.zip" *</nowiki>
 
−
 
 
−
==Installing Eclipse for Headless Build==
 
−
 
 
−
To install Eclipse for headless build, you first need to download two bundles from the Eclipse download site:
 
−
* <tt>eclipse-SDK-${VERSION}-${PLATFORM}.tar.gz</tt>
 
−
* <tt>eclipse-${VERSION}-delta-pack.zip</tt>
 
−
where <tt>VERSION</tt> is the version of Eclipse (e.g., <tt>3.4.2</tt>) and <tt>PLATFORM</tt> specifies the host platform for the build (e.g., <tt>linux-gtk</tt>).
 
−
 
 
−
Once downloaded, you need to extract the first archive, and then the second archive on top of the first. You now have an Eclipse installation able to build binary distribution for all platforms supported by Eclipse.
 
−
 
 
−
==Building the Platform==
 
−
 
 
−
To build the platform, you just need to run the script below after possibly modifying some of the variables at the beginning of it.  The meaning of the variables is
 
−
{| border="1" cellspacing="0" cellpadding="5"
 
−
| <tt>BUILD_ID</tt>
 
−
| Simple platform version (first parameter above)
 
−
|-
 
−
| <tt>SVNREV</tt>
 
−
| Subversion revision number with an <tt>r</tt> prepended
 
−
|-
 
−
| <tt>VERSION</tt>
 
−
| Full platform version used for provisioning (must contain <tt>$SVNREV</tt> as qualifier)
 
−
|-
 
−
| <tt>JAVA_HOME</tt>
 
−
| Absolute path to a Java Runtime Environment
 
−
|-
 
−
| <tt>BUILD_BASE</tt>
 
−
| Absolute path to the directory used for building. As a result of a previous step, this directory must contain a <tt>sources</tt> folder where the Rodin sources have been downloaded.
 
−
|-
 
−
| <tt>ECLIPSE_HOME</tt>
 
−
| Absolute path to the Eclipse installation (including the delta pack) to use for building
 
−
|-
 
−
| <tt>PDE_BUILD</tt>
 
−
| Absolute path to the PDE plug-in in your Eclipse installation.
 
−
|-
 
−
| <tt>BASE_OS</tt>
 
−
| Operating system of the host platform
 
−
|-
 
−
| <tt>BASE_WS</tt>
 
−
| Windowing system of the host platform
 
−
|-
 
−
| <tt>BASE_ARCH</tt>
 
−
| Architecture of the host platform
 
−
|}
 
−
 
 
−
The build script is
 
−
<nowiki>#!/bin/sh
 
−
 
 
−
BUILD_ID=2.0
 
−
SVNREV=9964
 
−
VERSION=$BUILD_ID.r$SVNREV
 
−
 
 
−
JAVA_HOME=/usr/lib/jvm/java-6-sun/jre
 
−
 
 
−
BUILD_BASE=$HOME/Rodin/$BUILD_ID
 
−
BUILD_DIR=$BUILD_BASE/work
 
−
RELENG=$BUILD_BASE/sources/org.rodinp.releng
 
−
 
 
−
ECLIPSE_HOME=$HOME/eclipse-SDK-3.6.1
 
−
PDE_BUILD=$ECLIPSE_HOME/plugins/org.eclipse.pde.build_3.6.1.R36x_v20100823
 
−
ANT_SCRIPT=$PDE_BUILD/scripts/productBuild/productBuild.xml
 
−
 
 
−
BASE_OS=linux
 
−
BASE_WS=gtk
 
−
BASE_ARCH=x86
 
−
 
 
−
$JAVA_HOME/bin/java \
 
−
    -jar $ECLIPSE_HOME/plugins/org.eclipse.equinox.launcher_*.jar \
 
−
    -application org.eclipse.ant.core.antRunner \
 
−
    -buildfile $ANT_SCRIPT \
 
−
    -Dbuilder=$RELENG \
 
−
    -DbuildDirectory=$BUILD_DIR \
 
−
    -DpluginPath=$BUILD_DIR/plugins/org.rodinp.platform \
 
−
    -Dbase=$ECLIPSE_HOME \
 
−
    -DbaseLocation=$ECLIPSE_HOME \
 
−
    -Dbaseos=$BASE_OS \
 
−
    -Dbasews=$BASE_WS \
 
−
    -Dbasearch=$BASE_ARCH \
 
−
    -DbuildId="$BUILD_ID" \
 
−
    -DbuildVersion="$VERSION" \
 
−
    -DforceContextQualifier="r$SVNREV" \
 
−
    -Dconfigs="linux,gtk,x86 & win32,win32,x86 & macosx,cocoa,x86_64"</nowiki>
 
−
 
 
−
==Post Build Verifications==
 
−
 
 
−
When the build worked, the "work/result" directory contains zipped archives for all platforms.
 
−
For each of them, check that:
 
−
* "rodin" binary is an executable file (for Linux and Mac)
 
−
* 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)
 
−
 
 
−
Failures must be manually corrected. Final archives shall match the above requirements.
 
−
 
 
−
[[Category:Developer documentation]]
 
−
[[Category:Rodin Platform]]
 

Revision as of 16:33, 29 November 2010

Demonstrator Version Release

Date: 30 November 2010:

available from: https://sourceforge.net/projects/codegenerationd/files/

The WindowsBundles directory contains a Rodin 1.3.1 platform with the Code-Gen plug-ins together with a patch plug-in. The patch plug-in is required to correct a difficulty that we encountered with the org.eventb.emf.persistence plug-in. Simply extract the appropriate zip file into a directory and run the rodin.exe. The plug-ins are pre-installed so no further configuration should be necessary.

A non-bundled version can be created using the info in the advanced folder using the update site. An example project, and a project forming the basis of a simple tutorial are provided in the accompanying zip file. The content in the zip file is already included in the bundled version.

Mac users - sorry no bundled version available at present, but the update site, install instructions and example projects are available in the advanced directory. We could create a bundled version upon request; meanwhile we are be working on a Rodin 2.0 version, which should be available through the usual update mechanism.

A Step by Step tutorial will be available soon

The SVN repository for code generation resides here: 

svn+ssh://svn.ecs.soton.ac.uk/projects/deploy-exploratory/trunk/CodeGeneration

The SVN repository for tagged builds is here: 

svn+ssh://svn.ecs.soton.ac.uk/projects/deploy-exploratory/tags/CodeGeneration

Completed/Ongoing Work

  • Demonstration plug-in,
    • ready for deployment.
    • deployment/Integration Testing under way.
  • The plug-in consists of,
    • a tasking Development Generator.
    • a tasking Development Editor (Based on an EMF Tree Editor).
    • a translator, from Tasking Development to Common Language Model.
    • a translator, from the Tasking Development to Event-B model of the implementation.
    • a pretty-printer for the Tasking Development.
    • a pretty-printer for Common Language Model, which generates Ada Source Code.

The Demonstration Plug-in Release

The demonstration plug-in is planned for release around November-end 2010, if all goes well. It must be emphasised that the Code Generation (CG) Feature is a demonstration tool; a proof of concept, rather than a prototype. The tool has no static checker and, therefore, there will be a heavy reliance on docs and dialogue to facilitate exploration of the tools and concepts. We will be working on this aspect in due course.

Metamodels

  • In the plug-in we define several meta-models:
    • CompositeControl: for the control flow (algorithmic) constructs such as branch, loop and sequence etc. These constructs may be used in the specification of either sequential or concurrent systems.
    • Tasking Meta-model: defines the tasking model where we attach tasking specific details, such as task priority, task type. The tasking structures provide the ability to define single tasking or multi-tasking (concurrent) systems. We make use of the composite control plug-in to specify the flow of control.
    • IL1 Meta-model: defines an abstraction of common programming language constructs for use in translations to implementations.

Translation Rules

  • Tasking to IL1/Event-B translation rules [[1]]
Retrieved from ‘https://wiki.event-b.org/index.php?title=Building_Rodin_Headless&oldid=1273’