User Documentation Overhaul

From Event-B
Revision as of 07:07, 1 July 2011 by imported>Jastram
Jump to navigationJump to search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

If you have suggestions or wishes regarding the documentation, please add them to the Wish List at the end of this document.

Background

At the Exec Meeting at ETH in 2010 the following was established, amongst other things: "It is clear that the current documentation would not support, say, an engineer in an automotive company to start using the tools without significant support." The effort to improve the documentation is now under way and will be coordinated by Düsseldorf.

After some brainstorming, we came up with the following goal of the project:

Minimize the access to an expert a user of Event-B/Rodin needs to be productive.

Mailinglist

If you would like to stay informed about this project, please subscribe to our mailinglist.

Description of Work and Progress

We maintain a separate page Documentation Overhaul DoW that lists the Description of Work, Work Packages and their progress.

The current state of the documentation can be accessed from our Jenkins Server: http://www.stups.uni-duesseldorf.de/~jenkins/org.rodinp.handbook.feature/build/

Plastex-Scripts on Sourceforge

The scripts for building the documentation and the latex are in Sourceforge at http://rodin-b-sharp.svn.sourceforge.net/viewvc/rodin-b-sharp/trunk/Handbook/

Requirements

By talking to a number of Rodin users we found the following requirements:

  1. Get a new user up to speed.
  2. Find solutions to specific problems.
  3. Find specific information.

Approach and Current State of Documentation

The above will be achieved by:

  1. Providing a Tutorial that covers the essential aspects of Event-B and Rodin.
  2. Providing a FAQ for common problems and issues.
  3. Providing a reference manual.

These three groups of documentation would be interlinked.

These three groups already exist as part of this wiki. This raises the question why the current documentation is not adequate. We believe that this is due to the following reasons, amongst others:

  • The tutorial doesn't make clear what knowledge is expected when starting the tutorial.
  • The tutorial could greatly benefit from screenshots and more detail.
  • The tutorial misses elements that we would consider crucial in a tutorial, e.g. installation (both Rodin and Provers), or configuration of provers.
  • The FAQ contains 17 questions, which covers only a fraction of "frequently asked questions".
  • The reference manual seems fairly complete, but is hard to navigate (mixture of PDFs, links and wiki information, combined with information that is marked as outdated, etc.)

Last, every version of Rodin has its own help system, consisting of a "snapshot" of a subset of the wiki. A script transforms the content to the Eclipse Help System.

Rodin Extensions

Extensions to Rodin will not be part of this effort (e.g. Decomposition). Such efforts will continue to be documented in the Rodin Wiki. However, we can include relevant references in the Rodin documentation. This is mainly due to the fact that we have limited resources and must focus.

Wish List

Please add your personal wishes in this section, one bullet point at a time. We are particularly interested in contributions from the industrial partners.

If you have comments regarding this document, please discuss on the discussion page.

  • Wishlist from ETH
  • Report on Training Experience
  • From SAP:
    • Maybe there is a way to better organize the information, so that navigation becomes easier.
    • You could add an “Event-B/Rodin for Dummies” section, because someone always forgets to install “Atelier-B provers”.
    • The documentation for plug-ins themselves and their compatibilities could be more detailed.
  • Another Suggestion: Video Tutorials
  • Consider adding the proof tactics: Rodin Proof Tactics

plasTeX-based Solution

At the Deploy Plenary meeting in Nice, we decided to implement the new help system using the plasTeX-approach. With this tool, we would generate HTML and Eclipse Help directly from LaTeX.