Talk:Scenarios for Team-based Development

Required scenarios

Systerel

As an industrial already using Rodin, we are in deep need of support for team-based development inside Rodin. Scenarios (S-2), (S-3) and (S-4) are routinely used here on other projects, and we are trying to build a solution for Rodin (see below).

Another very useful property for team-based development is to be distributed. It is indeed useful for implementing (S-4) but also too allow people to work with history without being connected to a centralized server (which is not always possible).

Some thoughts / Reactions

lock-edit-unlock cycle

is not desirable. We do merging everyday, and we'd like to be able to do the same in Rodin. Lock is too hard a constraint to be useful for us (Systerel).

granularity

In an update-edit-merge cycle, granularity is not a problem. In fact, while merging, the whole project must be taken into account, because two changes made in two separate files may have an impact on the semantic of the whole project. I guess, that the smallest element to be considered is the project itself, and consistency is ensure by people doing the right merge (of course, the process of merging may be alleviate by having the team to follow some predefined rules, and the tool to do most of trivial stuff).

textual merge

I wonder if textual merge (as it was done until now, because computer program were written as text) is the good solution. It looks like there should be means to greatly automate/guide the merging process by taking the XML structure of the Rodin database into account. You may for example have a look at 3dm XML 3-way Merging and Differencing Tool. Knowing the internal database structure (how are event uniquely identified ? How are proof identified ? How do those informations help to differentiate trivial merges from real conflicts...)

version control system

There is nowadays a lot of VCS (SourceSafe, Perforce, CVS, svn, git, mercurial, bazaar, darcs,...). It looks to me that developing a full featured VCS is a several man*year work, and is thus out of the scope of Deploy. As it was proposed by Michael, we should rely on existing VCS, but add plumbing to allow easy merge and preserve database consistency. Ideally we should allow industrialists to use there VCS of choice (even if some of them will certainly be easiest to use with Rodin than others).

database to text translator

How will we translate UML elements into text ? Won't the bi-directional translator becomes more and more complex when the database will bear objects other than event and mathematical formulas ?

DVCS setup

We are in the process of trying a setup of Mercurial with 3dm. 3dm has known shortcomings (notably when there are conflicts), but it does handle gracefully lot of cases (look at the examples in the source distribution). I hope to keep you informed of problems we will encounter, but we'll eventually at least need:

• a way to resolve conflicts without seeing XML (for model and proofs).
• a way to review automated merges (because computers do not understand the model semantic, and may do wrong merges)
• a way to review changes between two database snapshots (in order to browse change history, to see diff between working directory and current heads,... )
• ...

mercurial configuration sample

Mercurial

.hgrc

excerpt:

[merge-tools]
xmlmerge.priority = 10
xmlmerge.executable = tdm
xmlmerge.premerge = False
xmlmerge.args = -m \"$base\" \"$local\" \"$other\" \"$output\"

gvimdiff.args=--nofork -d -g -O $local $other $base
gvimdiff.regkey=Software\Vim\GVim
gvimdiff.regname=path
gvimdiff.premerge=True
gvimdiff.priority=100

bprmerge.priority = 10
bprmerge.executable = $HOME/deploy/merge/prmerge.py
bprmerge.premerge = False
bprmerge.args =  -p other -b \"$base\" -l \"$local\" -o \"$other\" --output \"$output\"

[merge-patterns]
**.bpr = bprmerge
**.bps = internal:local
**.xml = xmlmerge
**.svg = xmlmerge
**.bum = xmlmerge
**.buc = xmlmerge

TDM wrapper script (with some arguments passing tweaks to overcome problems with files having spaces in their name):

#!/bin/sh
rm conflict.log
action=$1
base=`echo $2| tr -d '"' `
local=`echo $3| tr -d '"' `
other=`echo $4| tr -d '"' `
output=`echo $5| tr -d '"' `
echo tdm "$1" "$2" "$3" "$4" "$5"
sed -i -e "s/
/##10;/g" "$output" "$local" "$base" "$other"
java -cp ${HOME}/java/java-getopt-1.0.12.jar:${HOME}/java/xercesImpl.jar:${HOME}/java/xmlParserAPIs.jar:${HOME}/java/3dm.jar tdm.tool.TreeDiffMerge $action  "$base" "$local" "$other" "$output"
#revert tdm side effects
sed -i -e "s/ \/>/\/>/g" -e "s/'/'/g" -e "s/##10;/\
/g"  "$output" "$local" "$base" "$other"

# if merge failed because of conflict
if ! grep -q '<conflictlist />' conflict.log
then
   gvim --nofork -d -g -O "$local" "$other" "$base"
fi
exit 0