Revision 44 as of 2022-09-13 07:42:17

Clear message

Back to developer page.

Git

Our Git workflow

We use Git, following the task-based workflow explained below. All significant development should be in response to an issue in the tracker, let's say issue1000. Then the usual development process involves two roles, "developer" and "reviewer" (usually Malte), and works as follows:

  1. Developer forks the primary Fast Downward repo ("the primary") to their own account (creating "the fork")
  2. Developer creates a new branch issue1000 in the fork, usually branching off the newest revision in main. Note the exact spelling of the branch. Being consistent here allows us to automate some of these steps in the future. The Git commands for this step and the following are shown under Git Commands for Developers below.
  3. Developer resolves the issue in the branch. (Developer does not delete the branch or push any changes to the primary repository.)

  4. Developer adds a short description in CHANGES.md (for examples, see ForDevelopers/ChangelogFormat). Always mention if something changes from a user perspective, such as added functionality or changed command line arguments.

  5. Developer pushes the changes to the fork on GitHub.

  6. Developer makes a pull request on GitHub from the issue1000 branch to the main branch in the primary repository (see ForDevelopers/CodeReview).

  7. Developer adds a link to the pull request to the issue tracker and sets the status of the issue in the tracker to "reviewing".
  8. Reviewer reviews the code and usually makes comments in the pull request. If reviewer is not satisfied, go back to step 3.
  9. Developer makes sure that all code tests pass. We recommend running tox in the misc/tests directory.
  10. Developer merges the issue1000 branch of the fork into the main branch of the primary. There are different workflows that achieve this, including the following:

    1. Developer creates a local clone of the primary ("the clone") with git clone git@github.com:aibasel/downward.git.

    2. Developer checks out the revision from which they branched in the fork in step 2.

    3. Developer adds the fork as a remote repository to the clone with git remote add myfork myforkrepo, where myfork is a unique identifier for the fork and myforkrepo the location of the fork on github (e.g., git@github.com:thomaskeller79/downward.git). This step can be skipped if the fork has been added as a remote repository to the clone before.

    4. Developer fetches the issue branch from fork with git fetch myfork issue1000.

    5. Developer performs the merge with git merge issue1000 --no-ff, then fixes conflicts if necessary.

    6. Developer commits the merge, e.g. with git commit -m "[main] Merge issue1000".

    7. Developer pushes the changes to the primary (git push).

    8. Developer deletes the local branch, both in the fork and the clone (assuming both will be reused). This is done locally using git branch -d issue1000. To delete the branch also remotely, use git push --delete origin issue1000. Note that all users who pulled this branch must delete the branch individually in all their clones.

  11. Developer verifies that the status of the pull request has been automatically set to "Merged". If not, developer changes the status accordingly.
  12. Developer sets the status of the issue to "resolved".

Git Conventions

Commit messages:

Branches:

Git Commands for Developers

Before starting to work on an issue, make sure your working copy is clean and up to date, and that you are on the branch main. 

git pull
git status
git branch

To start working on an issue, create the branch: 

git checkout -b issue1000 main

Fix the issue and commit your changes. If you run experiments, you might also need to create tags. 

git add modified_file
git commit -m "[issue1000] My meaningful commit message."
git tag issue1000-base <rev>
git tag issue1000-v1 <rev>

Then push your changes to GitHub for review. 

git push --set-upstream origin issue1000 --tags

When the issue is ready to be merged, merge it into main, delete the branch and push it to the main repository. 

git checkout main
git merge --no-ff issue1000 -m "[main] Merge issue1000."
git branch -d issue1000
git push

To delete the remote branch, use 

git push --delete origin issue1000

Note that this does not work on our main repository due to branch protection. However, if you haven't pushed your branch to the main repository during development, the main repository does not know about the existence of the branch, so nothing needs to be deleted anyway.

You can fix wrong commit messages in the following way. This modifies history, so the resulting repository is no longer compatible with the main repository. If there is a reason to push this to the primary repository, you have to disable the branch protection and use --force to push. Note that this loses all commits that came after the amended commit, so proceed with caution. 

git commit --amend

Tips and Tricks

Finding a Problem with bisect

Useful aliases

Adding the following to your .gitconfig (or ~/.gitconfig) file enables some useful shortcuts: 

[alias]
ci = commit
st = status
adog = log --all --decorate --oneline --graph
out = !git fetch && git log FETCH_HEAD..
in = !git fetch && git log ..FETCH_HEAD

/!\ I'm not a fan of these "out" and "in" suggestions. The names evoke "hg out" and "hg in", but they are the equivalent of an "hg pull" plus extra stuff. For me, a critical aspect of "hg out"/"hg in" is that they don't change anything. I'd be happier with other names, or if we cannot think of better ones, a warning here that mentions the differences. (I also don't think shortening aliases are all that useful, but if you see value in them, I don't mind. Something like Jendrik's "adog" alias would be genuinely useful to me.)

Ignoring IDE files

To ignore files you create but that should not be ignored in Fast Downward (e.g., files generated by a specific IDE), you can add them tto ~/.gitignore and add the following to ~/.gitconfig: 

[core]
    excludesfile = ~/.gitignore

Configuring meld to work with git

Meld works directly with git but it has to be started with the path to the repository (e.g., meld .).

Alternatively, it can be set up like this in the .gitconfig file: 

[merge]
tool = meld

[mergetool "meld"]
#cmd = meld "$LOCAL" "$BASE" "$REMOTE" --output "$MERGED"
cmd = meld "$LOCAL" "$MERGED" "$REMOTE" --output "$MERGED"

[diff]
tool = meld

[difftool "meld"]
cmd = meld "$LOCAL" "$REMOTE"

[difftool]
prompt = false

[alias]
meld = difftool -d

The workflow for using meld to resolve merge conflicts is as follows:

More information about how to configure the three-way diff can be found in this great answer that inspired above configuration: https://stackoverflow.com/a/34119867

Interact with a Git repo from Mercurial

The hg-git tool allows to pull and push from and to a Git repository with Mercurial, allowing you use Mercurial for working on Git projects. It does so by converting all Git branches to Mercurial bookmarks and vice versa. Here is how to set it up: 

sudo apt install python3-venv

mkdir hg-git
cd hg-git
python3 -m venv --prompt hg-git .venv
pip install -U pip wheel
pip install certifi==2020.6.20 dulwich==0.20.5 hg-git==0.9.0a1 mercurial==5.4.2 pkg-resources==0.0.0 urllib3==1.25.9

# Add to ~/.hgrc file:
[extensions]
hggit =

# Ensure that new Mercurial binary is found before system Mercurial:
sudo ln -s /path/to/hg-git/.venv/bin/hg /usr/local/bin/hg  # or adjust $PATH

(Instead of the last two steps, you could also define a Bash alias that calls the new Mercurial with the hg-git extension enabled, but this breaks tab completion for Mercurial. Details: tab completion breaks if the alias is not named "hg" or if the alias command contains spaces.)

Now you can clone a repository. Remember to update to a bookmark to make it follow your commits: 

hg clone git+ssh://git@github.com/aibasel/downward.git
cd downward
hg update main

[tested with Ubuntu 18.04]

GitHub Configuration