Developing for VerCors

In Summer 2024, Pieter wrote this developer's guide on the internals of VerCors: https://pieter-bos.github.io/vercors-doc/. It provides some useful background on the setup of the project, and how to do certain tasks.

PR/Branch management

Some general guidelines/notes to take into account when developing for VerCors:

• Draft PRs: while a PR is unfinished, mark it as "draft". Once it is ready for merging, unmark it as draft. Please do this even for short-lived PRs, so there is a definitive signal that work on a PR has finished.
• Branches & PRs: if you do work on a branch, it must have a PR. This way we keep track of what everyone is working on.
• PR size: try to keep your PRs small. If it has been open for longer than a month, consider bringing the PR in a state where it can be merged, even though your work might not be finished yet. This ensures we can still try to do bigger refactorings, while keeping churn in long-standing branches minimal.
• Branch naming: we don't really have a guideline for this, proposals welcome. For now: if it's for a specific subsystem (VeyMont, VeSUV, Pallas), include that. If relevant, feel free to include the issue number.
• VerCors repo or fork: obviously, you may open PRs that propose to merge a branch from a VerCors fork. We try to support this workflow in our CI, as long as it doesn't take too much effort. If you're a UT student, FMT employee, or research collaborator, get in touch with us so you can do your development directly in the VerCors repo, if you prefer.
• Branch cleanup: delete your branch after its PR has been merged, unless you plan on continuing development on it. Don't leave it lying around unused.
• Quality control: on the dev & master branch, all tests (except flaky ones) should pass, and all files should be formatted using the auto formatter. On your own branch you can pretty much do whatever you want.

Example workflow

Below you can find a description of what a typical workflow looks like.

1. Determine what you want to fix.
2. If there is an issue for what you want to fix, assign yourself to the issue. This can be done by navigating to the specific page of the issue. Then on the right-hand side there is an "Assignees" header. Beneath this header click on "assign yourself".
3. Ask for permissions to push to the main VerCors repository. We prefer to keep an eye on evolving development by asking contributors to work in branches of the main repository. Alternatively, you can work in your own fork (but e.g. continuous integration will not work).
4. Navigate to the VerCors project on your computer in your terminal.
5. When you're inside the vercors directory, create a new branch by executing the following command: git branch branch_name. Replace branch_name by the name for your branch. This name can reflect what you will fix. For example if you are going to fix issue 1, then you can name the branch "issue1". Or if you add support for automatic generation of invariants, then you can name the branch "automaticInvariants".
6. Then switch to the new branch using the command git checkout branch_name.
7. You can now start working on your problem!
8. When you are done with your fix, commit and push your changed files to the branch. To push to your new branch you can use the following command:git push origin branch_name.
9. Navigate to the main GitHub page of VerCors (https://github.com/utwente-fmt/vercors/).
10. Create a new pull request (see also: https://help.github.com/articles/creating-a-pull-request-from-a-fork/).
11. GitHub will run the tests, check that there are no unresolved comments on the pull request, and verify the tests have run with the most recent upstream changes.
12. As soon as this pull request has been reviewed by at least one person, and is accepted, then your fix can be merged into the master branch. Congratulations you're done with this PR (Pull Request)!