Skip to content

Latest commit

 

History

History
286 lines (213 loc) · 10.1 KB

HACKING.md

File metadata and controls

286 lines (213 loc) · 10.1 KB
Raw

Contributing to the library

Thank you for your interest in contributing to the Agda standard library. Hopefully this guide should make it easy to do so! Feel free to ask any questions on the Agda mailing list. Before you start please read the style-guide.

What is an acceptable contribution?

  • The contribution should be useful in a diverse set of areas.

  • The bar for accepting contributions that use the FFI to depend on external (i.e. Haskell, JavaScript) packages is much higher.

  • If the same concept already exists in the library, there needs to be a very good reason to add a different formalisation.

  • There should be evidence that the code works. Usually this will be proofs, but sometimes for purely computational contributions this will involve adding tests.

  • It should use the minimal set of Agda features, i.e. it should normally use the Agda option pragmas --cubical-compatible and --safe, with the occasional use of --with-K, --sized, --guardedness in certain situations.

In general, if something is in a general undergraduate Computer Science or Mathematics textbook it is probably (!) contributable.

Note on contributions to related/'coupled' modules

Before making changes to a Data module please have a look at related modules and see if they have any content along similar lines. If so, then please follow those conventions (e.g. naming, argument order). For example, if working on Data.Rational, please check Data.Rational.Unnormalised or if working on Data.Vec please check Data.List and vice versa. Likewise, if adding to such modules, please try to make companion additions to the related ones, or at least to make a task-list in the comments on your PR, indicating what outstanding work may be left for subsequent contributions/contributors.

Setup

The typical workflow when contributing to the standard library's repository is to interact with two remote versions of the repository:

  1. agda/agda-stdlib, the official one from which you can pull updates so that your contributions end up on top of whatever the current state is.

  2. USER/agda-stdlib, your fork to which you can push branches with contributions you would like to merge

This tutorial guides you to set up a local copy of agda-stdlib so that you can start contributing. Once things are set up properly, you can stick to only steps 5., 6., 7., 8. and 9. for future contributions.

  1. Fork the agda-stdlib repository

Go to https://github.com/agda/agda-stdlib/ and click the 'Fork' button in the top right corner. This will create a copy of the repository under your username. We assume in the rest of this document that this username is 'USER'.

  1. Double check-line ending settings if not on Linux

If you are on a Mac, make sure that your git options has autocrlf set to input. This can be done by executing

git config --global core.autocrlf input

If you are on Windows, make sure that your editor can deal with Unix format files.

  1. Obtain a local copy of agda/agda-stdlib

Obtain a local copy of the agda-stdlib repository. Here we are going to retrieve it from the agda/agda-stdlib repository so that master always points to the state the official library is in.

git clone git@github.com:agda/agda-stdlib

NB: if you have not added a public key to your github profile to set up git over ssh, you may need to use the https url instead of the git@ one (https://github.com/agda/agda-stdlib)

  1. Add your fork as a secondary remote

As we have mentioned earlier the idea is to pull updates from agda/agda-stdlib and to push branches to your fork. For that to work you will need to explain to git how to refer to your fork. This can be done by declaring a remote like so (again you may need to use the https url if you haven't configured git over ssh)

git remote add USER git@github.com:USER/agda-stdlib

You can check that this operation succeeded by fetching this newly added remote. Git should respond with a list of branches that were found on your fork.

git fetch USER

End of initial setup. When creating a future PRs one should start here..

  1. Create a branch for your new feature

Now that we have a local copy, we can start working on our new feature. The first step is to make sure we start from an up-to-date version of the repo by synchronising master with its current state on agda/agda-stdlib.

git checkout master
git pull

The second step is to create a branch for that feature based off master. Make sure to pick a fresh name in place of new_feature. We promptly push this new branch to our fork using the -u option for push.

git checkout -b new_feature
git push USER -u new_feature
  1. Make your changes

You can then proceed to make your changes. Please follow existing conventions in the library, see style-guide. for details. Document your changes in agda-stdlib-fork/CHANGELOG.md.

If you are creating new modules, please make sure you are having a proper header, and a brief description of what the module is for, e.g.

------------------------------------------------------------------------
-- The Agda standard library
--
-- {PLACE YOUR BRIEF DESCRIPTION HERE}
------------------------------------------------------------------------

If possible, each module should use the options --safe and --cubical-compatible. You can achieve this by placing the following pragma under the header and before any other line of code (including the module name):

{-# OPTIONS --cubical-compatible --safe #-}

If a module cannot be made safe or needs the --with-K option then it should be split into a module which is compatible with these options and an auxiliary one which will either be called SOME/PATH/Unsafe.agda or SOME/PATH/WithK.agda or explicitly declared as either unsafe or needing K in GenerateEverything.hs

  1. [ Optional ] Run test suite locally

NB this step is optional as these tests will be run automatically by our CI infrastructure when you open a pull request on Github, but it can be useful to run it locally to get a faster turn around time when finding problems.

Ensure your changes are compatible with the rest of the library by running the commands

make clean
make test

inside the agda-stdlib-fork folder. Continue to correct any bugs thrown up until the tests are passed. Note that the tests require the use of a tool called fix-whitespace. See the instructions at the end of this file for how to install this.

  1. Add, commit and push your changes to your fork

Use the git add X command to add changes to file X to the commit, or git add . to add all the changed files.

Run the command git commit and enter a meaningful description for your changes.

Upload your changes to your fork by running git push.

  1. Open a PR

Once you're satisfied with your additions, you can make sure they have been pushed to the feature branch by running

git status

and making sure there is nothing left to commit or no local commits to push. You should get something like:

On branch new_feature
Your branch is up-to-date with 'USER/new_feature'.

nothing to commit, working tree clean

You can then go to https://github.com/agda/agda-stdlib/pulls, click on the green 'New pull request' button and then the 'compare across forks' link.

You can then select your fork as the 'head repository' and the corresponding feature branch and click on the big green 'Create pull request' button. The library maintainers will then be made aware of your requested changes and should be in touch soon.

  1. Update the PR

If after opening a PR you realise you have forgotten something, or have received a review asking you to change something, you can simply push more commits to the branch and they will automatically be added to the PR.

How to enforce whitespace policies

Installing fix-whitespace

This tool is kept in the main agda organization. It can be installed by following these instructions:

git clone https://github.com/agda/fix-whitespace --depth 1
cd fix-whitespace/
cabal install

Adding fix-whitespace as a pre-commit hook

You can add the following code to the file .git/hooks/pre-commit to get git to run fix-whitespace before each git commit and ensure you are never committing anything with a whitespace violation:

#!/bin/sh

fix-whitespace --check

Type-checking the README directory

  • By default the README files are not exported in the standard-library.agda-lib file in order to avoid clashing with other people's README files.

  • If you wish to type-check a README file, then you will need to change the present working directory to doc/ where an appropriate standard-library-doc.agda-lib file is present.

Continuous Integration (CI)

Updating the Haskell-CI workflow

The file .github/workflows/haskell-ci.yml tests building the helpers specified in agda-stdlib-utils.cabal. It is autogenerated by the tool haskell-ci but has some custom modification which need to be restored after each regeneration of this workflow.

haskell-ci creates the workflow file from settings in the cabal.haskell-ci file and from the contents of the tested-with field in the agda-stdlib-utils.cabal file. After updating this field, run the following:

haskell-ci regenerate
patch --input=.github/haskell-ci.patch .github/workflows/haskell-ci.yml