Setting up nix and git for mathcomp on HB - math-comp/math-comp GitHub Wiki

Setting up nix & git for mathcomp on HB

Nix setup

Follow the installation procedure documented here: https://github.com/math-comp/math-comp/wiki/Using-nix#nix-installation-pre-requisite-for-the-rest

Github mathcomp repository setup (do only once)

This is one method among many. You can also work with your own setup, just make sure upstream points to math-comp/math-comp. (e.g. git clone [email protected]:math-comp/math-comp -o upstream should suffice if you already registered your ssh-key on github).

https://github.com/math-comp/math-comp/wiki/Creating-and-editing-PRs#github-repository-setup-do-only-once

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

Checkout mathcomp hierarchy-builder branch

  1. Go to your repo, update the remotes

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

  2. Create a worktree for the hierarchy-builder branch and go there

    HB=hierarchy-builder
git worktree add -b $HB ../$HB upstream/$HB && cd ../$HB

  3. Start working.

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

    nix-shell

    from the root of the repository (otherwise you will need to install HB by hand and update it by hand if we need to change it).

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

    cachedMake # you may want to check the cache is there before cleaning your previous .vo
make -C mathcomp clean
cachedMake
make -C mathcomp -t # to touch all .vo in order so that the next call to make does not recompile everything
    • if it starts with these paths will be fetched, you just skipped ~20min of compilation of the current mathcomp port.
    • otherwise, go back to manual compilation: make -j8 -k -C mathcomp, or clean/stash your local modifications and wait for the CI to finish and retry again cachedMake.

  4. 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.

  5. If you make changes to some files, commit before you stop working. Make sure rebase on top of the shared branch now and then.

    git pull -r upstream hierarchy-builder

  6. When you are ready to submit your work,

    • push it 
      git push upstream hierarchy-builder # DO NOT FORCE
    • if this failed, rebase on top of the current state of the branch 
      git pull -r upstream hierarchy-builder
      resolve potential conflicts (they should only occur mathcomp/Make) and try to push again.
    • then go to #733 and tick/untick the appropriate boxes.

ONLY If you need to fix/extend HB

Github hierarchy-builder repository setup (do only once)

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

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.

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

  2. 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.

  3. Fork hierarchy-builder on github:

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

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

  4. Prepare for the install:

    mkdir -p ~/git/hierarchy-builder && cd ~/git/hierarchy-builder
gh repo clone hierarchy-builder master && cd master

    This will clone mathcomp and set the right origin and upstream

  5. Setup local mirroring of PRs:

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

Creating a new PR on HB

  1. Go to your repo, update the remotes

    cd ~/git/hierarchy-builder/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 hierarchy-builder 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 will only work with VS code (or codium) you need to install vscode with the three following extensions:

    • vscoq extension
    • elpi extension
    • coq-elpi 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. Compile and run tests with make inside a nix-shell

  8. You can try it on math-comp/math-comp

    • on the branch hierarchy-builder by running 
      nix-build --argstr bundle "coq-8.13" --argstr job "mathcomp-single"`
      (you can remove --argstr bundle "coq-8.13" to try the three versions of coq at the same time)
    • on another branch by editing .nix/config and replacing 
      mathcomp.override.version = "hierarchy-builder";
      by 
      mathcomp.override.version = "your-branch";

  9. 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>/hierarchy-builder/pull/new/<your-PR>

  • ⚠️ Never ever push directly to upstream master
  • ⚠️ Never use git push without a repo and a branch
Add a custom footer
⚠️ **GitHub.com Fallback** ⚠️