lean-refactor-arena / PyPantograph /src /doc /contributing.md
mikeljl's picture
use pypantograph for checking submitted statements
0115dcf

Contributing

A Lean development shell is provided in the Nix flake. Nix usage is optional. Any contribution has to pass the pre-commit hooks:

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

nix flake check

or

lake test

You can run an individual test by specifying a prefix

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.
let .some result := function
  | fail "incorrect"
  • Each test should be pinpointed and devolatilized.