PPL

Access the Parma Polyhedra Library Using Git

The Parma Polyhedra Library is currently being maintained on a publicly readable Git repository.

Git is a powerful tool that allows many developers to work on the same source code. This is possible because each developer can clone the entire repository, including the entire development history. Developers then work independently on the cloned repository, on which they have full revision tracking capabilities, without the need of network connection to the server hosting the central repository. When they have made and tested their changes locally, they push them back to the central Git server. The Git server takes care of things like trying to merge the changes coming from different developers. When this is not possible, developers are notified so that they can proceed to a manual merge of the conflicts.

Full read-write access to this repository is of course restricted to recognized developers. Write to us if you want to be involved in the development effort.

We also provide read-only anonymous access to the repository. This allows anyone to easily synchronize their own copy with the development sources.

Git is a powerful and complex system: see below for some Git tips and pointers to further reading.

Read-Only Anonymous Git Access

For this to work you need to install a reasonably recent version of Git on your system.

In order to clone the repository of the PPL sources, issue the command

git clone git://git.cs.unipr.it/ppl/ppl.git

This will put your clone into the ppl directory. If you want the directory to be named differently you can specify the name as in

git clone git://git.cs.unipr.it/ppl/ppl.git my_ppl_repo

The above commands will give you repositories with the complete development history. If you only want the latest revision of anything, use the following command instead:

git clone --depth 1 git://git.cs.unipr.it/ppl/ppl.git my_ppl_no_history_repo

After the initial checkout, you can change into one of the project's directories and execute any Git command that does not require read-write access to the central repository. For example, whenever you want to merge with the latest code changes, cd into your ppl directory and issue the command

git pull

Another repository you may be interested in is the one containing our web pages. To fully clone it, do, e.g.,

git clone git://git.cs.unipr.it/ppl/w3ppl.git

If you are behind a firewall that only allows you access to the outside world via HTTP (possibly with the intermediation of a proxy), you can use the alternative commands

git clone http://www.cs.unipr.it/git/ppl/ppl.git

git clone http://www.cs.unipr.it/git/ppl/w3ppl.git

Read-Write Git Access

If you are a recognized developer, the first thing to do is to let Git know who you are. To do so, you should issue commands like

git config --global user.name "Roberto Bagnara"

git config --global user.email bagnara@cs.unipr.it

These commands will create the file .gitconfig in your home directory. After the commands above, that file should contain

[user]
	name = Roberto Bagnara
	email = bagnara@cs.unipr.it

Full access to the repository requires authenticated access via the SSH protocol. For this to work, an SSH client must be available on your local machine and you must have an account on git.cs.unipr.it. To see if these are the cases, use SSH to enter your myusername account on git.cs.unipr.it: issue the command

ssh git.cs.unipr.it -l myusername

If this does not work there is no point in reading further: solve this problem first.

Issue the command

git clone ssh://myusername@git.cs.unipr.it/git/ppl/ppl.git ppl

git clone ssh://myusername@git.cs.unipr.it/git/ppl/w3ppl.git w3ppl

to clone the PPL source or the PPL web repositories, respectively.

After the initial checkout, you can change into one of the project's directories and execute most Git commands omitting the ssh://myusername@git.cs.unipr.it/git/ppl/ppl.git argument. For example, whenever you want to merge with the latest code changes, cd into your ppl directory and issue

git pull --rebase

This command saves all non-pushed changes made by your commits in a temporary area, updates the local repository with changes done in the central one, and reapplies the saved commits. It is up to you to solve possible conflicts. Pull with rebase permits to have a cleaner linear history for small incremental changes.

Web Pages

Note that when you commit changes to the web pages, these will automatically be checked out into the web server's data area at http://www.cs.unipr.it/ppl/.

Write Access and Responsibility

Always remember the commandments of team membership:

Thou shalt not break the build. Cause not the build team to call down demons upon your workstation.
Thou shalt not wander through thy brother's code changing his parts without first obtaining thy brother's permission. A plague upon those that sow random and wanton destruction through others code.
Thou wilt respond to build and/or bringup problems with haste and thoroughness. Be humble, and serve.
Thou shalt coordinate interface changes and submissions with thy brother developers. Woe be to thee who causes thy brother's code to break.
Thou shalt not unnecessarily change common headers. Woe be the developer who heedeth this not, he shall cause a rebuilding of the world and incur 40 days and 40 nights of compiles.
Thou shalt not covet the false temptress code change past code-freeze. Resist the evil temptation of just one more fix. Thy brother developers and release managers will curse thy name long into the darkness.

Using Git

Documentation

The Git web sites contains all the documentation you can dream of.
Using git without feeling stupid (part 1), by Paolo Bonzini.
Using git without feeling stupid (part 2), by Paolo Bonzini.

Tips

More About Git Configuration

The following command will define a git wup command that you could use before any git push to check what you are about to push to the central repository:

git config --global alias.wup "log -p origin..@{0}"

TODO: explain things such as diff.renames.

Tips from External Sources

Lots of tips on this Basic Git usage page.

CVS Ultra-Quick Reference for the Old, CVS-addicted PPL Developer

For the lazy, here is a rough correspondence between some basic CVS commands and their Git counterparts.

Checkout of the main trunk vs Cloning of the master branch

cvs -d ssh://myusername@git.cs.unipr.it/cvs/ppl checkout ppl
|
+---> git clone ssh://myusername@git.cs.unipr.it/git/ppl/ppl.git

Checkout of a branch vs Cloning of the master branch + Creation of a local branch tracking a remote one

cvs -d ssh://myusername@git.cs.unipr.it/cvs/ppl checkout -r products ppl
|
+---> git clone ssh://myusername@git.cs.unipr.it/git/ppl/ppl.git
      git checkout -b products origin/products

Adding a file vs Staging file content for inclusion in next commit

cvs add file.c
|
+---> git add file.c

Removing a file

cvs rm file.c
|
+---> git rm file.c

Update vs Pull + Rebase

cvs update
|
+---> git pull --rebase

Commit vs Staging modified files content for inclusion + Commit + Push to the central repository

cvs commit
|
+---> git commit -a
      git push

Differences with respect to the central repository

cvs diff
|
+---> git diff

You can also try giving to your shell the command

git --help

or, if you really feel adventurous,

man git

[Page last updated on July 25, 2009, 15:21:56.]