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