Back to developer page.
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:
- Developer forks the primary Fast Downward repo to their own account.
Developer creates a new branch issue1000 in their own repository, 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.
- Developer resolves the issue in the branch. (Developer does not delete the branch or push any changes to the primary repository.)
Developer pushes the changes to their fork on GitHub.
Developer makes a pull request on GitHub from the issue1000 branch to the main branch in the primary repository (see ForDevelopers/CodeReview).
- Developer adds a link to the pull request to the issue tracker and sets the status of the issue in the tracker to "reviewing".
- Reviewer reviews the code and usually makes comments in the pull request. If reviewer is not satisfied, go back to step 3.
Reviewer merges the issue1000 branch into the main branch (either locally or on GitHub). When merging on GitHub, make sure that
Your GitHub email address is set up to match the one you usually use to commit and is not set to private.
Your full name is set up in GitHub.
When you merge the pull request, use the message "[main] Merge issue1000." in the first text box (first line of commit message) and leave the second textbox (additional lines of commit message) empty.
Reviewer deletes the issue1000 branch.
- Reviewer pushes merge into the primary repository.
- Reviewer sets the status of the issue to "resolved".
Prepend "[<branch>] " to all commits of the branch <branch> (TODO: developers should copy misc/hooks/commit-msg to .git/hooks/commit-msg)
The first line of the commit message should consist of a self-contained summary and be no longer than 67 characters. All other lines should be below 80 characters. In particular, please avoid very long commit messages without line wrapping.
Please write the summary in the imperative mode (e.g., "Make translator faster." instead of "Made translator faster.", see https://chris.beams.io/posts/git-commit/).
- Use one feature branch for each issue.
Only commit merges of issue branches on main (we make occasional exceptions for small changes like fixing typos).
- Do not squash commits when merging issue branches, i.e., we want to preserve the non-linear history of commits.
- Do not use fast forward merges, i.e., we always want to have a proper merge commit for the integration.
- Delete branches (the pointer) after integration.
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
As a reviewer, if you want to edit or merge the code locally, pull in the issue branch, merge it and push the result to the primary repository
git fetch <URL of issue repository> issue1000 git checkout main git merge --no-ff issue1000 -m "[main] Merge issue1000." git branch -d issue1000 git push
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
- TODO: git bisect with --first-parent etc. (Malte sent a few links)
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
[Silvan] Unfortunately, I haven't found a way for git merge to automatically open meld instead of first doing an incomplete merge and then viewing the failed merge via hg mergetool, which, if configured as above to take $MERGED as the middle file, contains the failed merge in the >>>> ... <<<< ... format, which I really don't like. If anyone finds out how to let git automatically merge what it can and then immediately prompt the user via mergetool instead of requiring this to be called manually, and even better, without showing the failed merge, I would be very happy.
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://firstname.lastname@example.org/aibasel/downward.git cd downward hg update main
[tested with Ubuntu 18.04]
We use GitHub's autolink feature to link from commit messages to the issue tracker (https://help.github.com/en/github/writing-on-github/autolinked-references-and-urls).
- We also decided to protect all branches on the main Fast Downward repository. This means that no force pushes are allowed and branches can't be deleted.