User Documentation Overhaul
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://handbook.event-b.org
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:
- Get a new user up to speed.
- Find solutions to specific problems.
- Find specific information.
Approach and Current State of Documentation
The above will be achieved by:
- Providing a Tutorial that covers the essential aspects of Event-B and Rodin.
- Providing a FAQ for common problems and issues.
- 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.
PlasTeX Performance
With a version of dvipng before 1.14, plastex is slow and creates zombies while it runs. To fix this, you need to install dvipng 1.14. Here are the instructions for Ubuntu 11.04:
- sudo apt-get install texinfo
- sudo apt-get install libkpathsea-dev
- sudo apt-get install libgd-dev
- sudo apt-get install libgd2-xpm-dev
- Download http://sourceforge.net/projects/dvipng/ and unpack it
- ./configure
- make
- sudo make install
That should do the trick. To check, run dvipng without arguments, it should print the version.
