Sharing theories
Rodin 2.0+ with theory plug-in makes it possible to define extensions to the standard mathematical language, that is new operators and datatypes. This page explains how to share your theories with the community and how to get theories developed by other people.
A SourceForge tracker for Theories
A new tracker has been created in the SourceForge site of the Rodin project:
http://sourceforge.net/tracker/?group_id=108850&atid=1558661
This can be viewed as a repository for sharing theories.
Sharing a Theory
Sharing a theory can be achieved the same way as adding an item in any other SourceForge tracker: by clicking the "Add new" link, then filling the form.
As much as possible, non related theories should be provided in different artifacts (tracker items). Before posting a new theory, it is recommended to check if the same or a similar one already exists. In this case, if your theory has something slightly different that you think worth sharing, please do so in the same tracker item, in order to keep related works together (use the upload description field to describe differences).
A theory item is basically made of:
- a relevant title, clearly stating what kind of mathematical extensions are provided;
- a brief description of the contents (in the initial comment);
- a category indicating the area of the theory; if no existing category fits your contribution, leave the field at "None" and indicate in the comment the name of the new category you would like
- a group, indicating which version of Rodin the theory has been developed with
- one or more archives (see Exporting and importing archives containing theories for generating these archives)
Updating a new version
New versions of a given theory shall be uploaded to the same tracker item as the original one, using the upload description field to describe evolutions.
After downloading the desired archive(s) from the list of attached files, import them into your Rodin workspace using one the techniques described in Exporting and importing archives containing theories.
The technique to use depends on how the archive has been generated. In any case, the goal is always the same: to put theory files (.tuf, .dtf, ...) from the archive into the MathExtensions project of your workspace.
