Contributing
The independently-run Lean Community Zulip chat is the central hub for everything Lean. Whether you are a new or experienced Lean user, it’s a welcoming place to ask questions, share ideas, and collaborate with other Lean users.
Contributing to CSLib
Great that you're interested in contributing to CSLib!
Please read the rest of this document before submitting a pull request. If you have any questions, a good place to ask them is the Lean prover Zulip chat.
Contribution model
To get your code approved, you need to submit a pull request (PR). Each PR needs to be approved by at least one relevant maintainer. You can read the list of current maintainers.
If you are adding something new to cslib and are in doubt about it, you are very welcome to contact us on the Lean prover Zulip chat.
Style and documentation
We generally follow the mathlib style for coding and documentation, so please read that as well. Some things worth mentioning and conventions specific to this library are explained next.
Variable names
Feel free to use variable names that make sense in the domain that you are dealing with. For example, in the Lts library, State is used for types of states and μ is used as variable name for transition labels.
Proof style and golfing
Please try to make proofs easy to follow. Golfing and automation are welcome, as long as proofs remain reasonably readable and compilation does not noticeably slow down.
Notation
The library hosts a number of languages with their own syntax and semantics, so we try to manage notation with reusability and maintainability in mind.
-
If you want notation for a common concept, like reductions or transitions in an operational semantics, try to find an existing typeclass that fits your need.
-
If you define new notation that in principle can apply to different types (e.g., syntax or semantics of other languages), keep it locally scoped or create a new typeclass.
Looking for more support?
Lean community website - A community maintained website that hosts a variety of helpful resources and is the main reference site for working with Mathlib, Lean's extensive community-built library of mathematics.
Lean community YouTube channel - Hosts many instructional videos, lectures and guides recorded from conferences and workshops organized by the Lean community.