I strongly advise you install nix and mathcomp cachix to facilitate and speedup setup.

This is one method among many. You can also work with your own setup, just make sure origin points to your fork GithubUsername/math-comp and upstream to math-comp/math-comp.

However, I will often rely on the git worktree command to avoid duplication of git metadata and objects, and thus save bandwidth and disk space, so I will initialize my repositories with the path ~/git/repo/master and store branches other than master under git/repo/branch.

To perform several github operations from the command line, I will assume that you have either installed the gh utilities via your system package manager, or that you can started nix-shell -p gh to get a shell with gh accessible.

0. Install gh or run nix-shell -p gh

1. Run

   gh auth login -w

   copy the one-time code then press enter, and paste the code in the browser that just opened, identify if required and authorize the app. This will install an ssh-key and remember your username.

2. Fork math-comp on github:

   gh repo fork math-comp/math-comp --clone=false

   (if you already have a fork this is a noop)

3. Prepare for the install:

   mkdir -p ~/git/math-comp && cd ~/git/math-comp
   gh repo clone math-comp master && cd master

   This will clone mathcomp and set the right origin and upstream

4. Setup local mirroring of PRs:

   git config --add remote.upstream.fetch \
     "+refs/pull/*/head:refs/remotes/upstream/pr/*"
   git remote update

1. Go to your repo, update the remotes

   cd ~/git/math-comp/master && git remote update

2. Update you master branch to the latest revision

   git merge --ff-only upstream/master

   If this fails, it means your master branch has diverged from the upstream (math-comp) one, it also means that you might have used your master branch to develop or test something, which is a bad practice.

   • If you want to abandon modifications, do git reset --hard upstream/master ⚠️ this will erase whatever you did on your master branch.
   • Otherwise, you may want to continue this tutorial, keeping in mind that you will then start from your own master rather than math-comp master.

3. Create a new branch (e.g. test-PR), in a new directory of the same name and go there

   git worktree add ../test-PR && cd ../test-PR

4. Start working.

   I strongly advise you work inside mathcomp's dedicated nix-shell by running

   nix-shell

   from the root of the repository.

   Before touching any file, and before compiling, inside the nix-shell, try to run

   cachedMake

   • if it starts with these paths will be fetched, you just skipped ~10min of compilation of mathcomp.
   • otherwise, interrupt and go back to manual compilation: make -j8 -k -C mathcomp

5. Working on a file using one of the three following editors:

   • coqide: if you ran nix-shell it is available, you can start working with it
   • emacs: you can run your own emacs if you installed proof-general and set the coq-prog-name variable to coqtop. Optionally, if you do not have emacs or proof-general installed you can run nix-shell --arg withEmacs true to get a preconfigured emacs (independent from your $HOME configuration).
   • vscode: you can install vscode with the vscoq extension, if you ran it from inside the nix-shell it should be ready to use.

6. If you make changes to some files, commit before you stop working. Make sure rebase on top of upstream master now and then.

   git pull -r upstream master

7. When you are ready to submit a PR, push it to your own fork:

   git push origin test-PR

   and follow the given link to create a new PR. It has the shape https://github.com/<your-github-username>/math-comp/pull/new/<your-PR>

• ⚠️ Never ever push directly to upstream master
• ⚠️ Never use git push without a repo and a branch

0. Check https://github.com/math-comp/math-comp/pulls for a PR you want to try out.

1. Go to your repo, update the remotes

   cd ~/git/math-comp/master && git remote update

2. Create a new branch (e.g. pr-732), in a new directory of the same name and go there

   git worktree add -b pr-732 ../pr-732 pr/732 && cd ../pr-732

3. Work as if you were in your own PR, except you cannot push. Instead you may use the suggestion feature of github (item 6) to suggest your findings to the author.

⚠️ The polite thing to do is to never force push on a branch you did not open without the explicit approval of the author.

0. Go to your repo, update remotes and install/import the hub command

   cd ~/git/math-comp/master
   git remote update
   nix-shell -p hub

   you can the check existing PRs via hub pr list

1. Checkout a pr (e.g. 727) and create a worktree:

   hub pr checkout 727
   PR=$(git branch --show-current)
   git checkout master
   git worktree add -B $PR ../$PR $PR && cd ../$PR

2. I strongly advise you setup push.default git option to current

   git config push.default current

   • I personally set this for all my repositories using the extra --global flag
   • you can now use git push from a PR, but never from master!
   • always try git push -n to do a dry run

3. You can now work as if you were in your own branch, except git push from this branch will now push to the author's branch: use with moderation.