Isabelle Community Conventions
This repository contains style guidelines for the development of projects with the Isabelle proof assistant. Many of these guidelines have been adapted from the very successful Lean mathlib contribution guidelines.
We start with the most important rule: Every commit/pull request must comply with the standards listed in this document.
This might seem like a lot of work at first, but experience has shown that a consistent commitment to such rules means:
- High quality of theories due to uniform conventions and documentation
- Easy collaboration due to (1) (searchability, uniformity) and a flexible as well as transparent contribution model
- Quicker development in the mid-term and long-term due (1) and (2)
The guidelines cover the following topics:
- Naming Conventions
- Style Conventions
- Theory Documentation
- Theorem Attributes
- Session Management
- Pull-Request Management
Get Help and Join The Community
This Zulip chat is where some of the Isabelle community, in particular the creators of these guidelines, hang out. We are always happy to help you and try to answer your questions, no matter if they are basic or advanced.