1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153
|
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](https://github.com/agda/agda-stdlib/blob/master/notes/style-guide.md).
How to make changes
-------------------
### Fork and download the repository
1. Create a fork by clicking `Fork` button at the top right of the
[repository](https://github.com/agda/agda-stdlib).
2. 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.
3. On the command line, and in a suitable folder, download your fork by
running the command
```
git clone https://github.com/USER_NAME/agda-stdlib agda-stdlib-fork
```
where `USER_NAME` is your Git username. The folder `agda-stdlib-fork`
should now contain a copy of the standard library.
4. Enter the folder `agda-stdlib-fork` and choose the correct branch of
the library to make your changes on by running the command
```
git checkout X
```
where `X` should be `master` if your changes are compatible with the
current released version of Agda, and `experimental` if your changes
require the development version of Agda.
### Make your changes
5. Make your proposed changes. Please try to obey existing conventions
in the library. See `agda-stdlib-fork/notes/style-guide.md` for a
selection of the most important ones.
6. Document your changes in `agda-stdlib-fork/CHANGELOG.md`.
7. 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.
Your proposed changes MUST pass these tests. 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.
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 `--without-K`. You
can achieve this by placing the following pragma under the header and before
any other line of code (including the module name):
```
{-# OPTIONS --without-K --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`
### Upload your changes
8. Use the `git add X` command to add changes to file `X` to the commit,
or `git add .` to add all the changed files.
9. Run the command:
```
git commit
```
and enter a meaningful description for your changes.
10. Upload your changes to your fork by running the command:
```
git push
```
11. Go to your fork on Github at `https://github.com/USER_NAME/agda-stdlib`
and follow the [official Git instructions](https://help.github.com/en/articles/creating-a-pull-request-from-a-fork)
to open a pull request to the main standard library repository.
12. The library maintainers will then be made aware of your requested
changes and should be in touch soon.
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 directory is not exported in the
`standard-library.agda-lib` file in order to avoid clashing with other people's
README files. This means that by default type-checking a file in the README
directory fails.
* If you wish to type-check a README file, then you will need to change the line:
```
include: src
```
to
```
include: src .
```
in the `standard-library.agda-lib` file.
* Please do not include this change in your pull request.
|