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.

Approach

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.

Possible Solution and Current State of Documentation

The above can 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.

Versioning

The wiki always contains the latest version of the documentation. This presumably covers the latest version of Rodin. There is no easy way to browse an older version of the documentation online. However, this information is accessible through the Eclipse Help System of the corresponding Rodin Version.

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.

Next Steps

We believe that the current approach - Tutorial, FAQ, Reference - is fundamentally a good one. However, there are a number of aspects that we would like to improve. This includes:

• Further validation of the approach: We already talked to a number of users to understand their problems with the documentation better. Please provide us with your feedback. There may be a better approach than what we presented here so far.
• Develop an approach to versioning: Past versions of the documentation should be accessible online as well.
• Improve the structure of the documentation: Granularity of documentation elements should be improved, Navigation should be made easier. Visual cues may be introduced (e.g. icons for "Tip", "Caution", etc.) that are used consistently throughout the documentation
• Improve the content of the documentation: Make sure content builds on top of each other, make sure no steps are omitted, use screenshots, etc.
• Find gaps in the documentation and fill them.
• Rethink the representation of the documentation. The current approach works, but doesn't result in a professional appearance.

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

One possible solution would be to generate HTML and Eclipse Help directly from LaTeX. This can be done with plasTeX. We realized a tiny portion of the documentation using this approach. The following three resulting artefacts were all generated from the same LaTeX-sources:

• HTML Documentation
• Print Documentation (PDF)
• Eclipse Help: Please copy the plugin in the plugin-folder of any Eclipse-Installation. To access the Documentation, open the Help System (Help > Help Contents). You should see the entry "Rodin User Manual v.2.1.1" in the left pane.

It may be possible to add a plasTeX renderer to output mediawiki. It looks like someone already gives a first stab at it — to be investigated. mathieu 14:00, 12 April 2011 (UTC)

pandoc based solution

pandoc advertises a latex to mediawiki conversion — to be investigated. mathieu 14:06, 12 April 2011 (UTC)

Comparing Solutions

The most promising approaches are Wiki (current approach) and plasTex. In the following table, we try to compare them.

Note: We are only talking about the user documentation (less than 20 wiki pages). We are not suggesting to migrate plugin or developer documentation away from the wiki.

	Wiki	plastex
Appearance	Decent HTML look, PDF generation more difficult to get high quality. Eclipse Help works.	High quality PDF. Nice HTML and Eclipse Help thanks to templating.
Contribution	Very easy: Only a Wiki account is necessary, the result is immediately visible in the browser.	Cumbersome: A svn-account is required, a Latex-environment must be set up. The result is not available immediately to other users. (We may set up a nightly build to publish the latest documentation).
Formulas, Graphics	Formulas that are rendered as images will have a low quality in the print documentation. Only bitmap graphics	Formulas will always be high-quality in PDF. Vector images are possible in the PDF and will be rastered for the HTML and Eclipse Help Documentation.
Structure	The hierarchy can be simulated with a naming convention. The scripts generating the Eclipse Help and PDF would have to process it somehow.	Latex structuring mechanisms can be used and will be reflected in HTML and Eclipse Help.
Versioning	Individual pages are versioned. No "tagging" of a basline is possible, However, with the generation of Eclipse Help (and possibly PDF) a snapshot is saved.	Standard SVN-mechanisms for versioning can be used.