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-access}
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-access}
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 you have been granted full access to git.cs.unipr.it
you should
obtain a shell prompt. Otherwise, if SSH connection works, you will get
the following message
fatal: What do you think I am? A shell? Connection to git.cs.unipr.it closed.
In both cases (i.e., you obtain either a shell prompt or the message
What do you think I am? A shell?
) connection to git.cs.unipr.it
via
SSH works. Otherwise there is no point in reading further: solve this
problem first.
Issue the command
git clone ssh://git@git.cs.unipr.it/ppl/ppl
git clone ssh://git@git.cs.unipr.it/ppl/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://git@git.cs.unipr.it/ppl/ppl
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}
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://git@git.cs.unipr.it/ppl/ppl
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://git@git.cs.unipr.it/ppl/ppl
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