File size: 872 Bytes
0115dcf | 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 | # Contributing
A Lean development shell is provided in the Nix flake. Nix usage is optional.
Any contribution has to pass the pre-commit hooks:
```sh
pre-commit install --install-hooks
```
All commit messages must conform to the Conventional Commits specification.
## Testing
The tests are based on `LSpec`. To run tests, use either
``` sh
nix flake check
```
or
``` sh
lake test
```
You can run an individual test by specifying a prefix
``` sh
lake test -- Frontend/Collect
```
## Formatting
When writing Lean code, follow the guidelines
- Functions should be in `camelCase`
- Theorems and tests should be in `snake_case`
- Write the `|` in a pattern-matching `let` on the next line. This is for visual
distinction with long function arguments.
```lean
let .some result := function
| fail "incorrect"
```
- Each test should be pinpointed and devolatilized.
|