CONTRIBUTING.md

Contributing to CompPoly

We enthusiastically welcome contributions to CompPoly!

Whether you are fixing bugs, improving documentation, or adding new formalizations, your input is valuable. We particularly encourage contributions that address:

• Active formalizations: Please see the list of active formalization efforts and their blueprints.
• Open Issues: Please see the list of open issues for bugs, requested features, and specific formalization tasks. Issues tagged as good first issue or help wanted are great places to start.
• Roadmap Goals: We maintain a ROADMAP outlining the planned direction and major goals for the library.
• Documentation: Documentation is actively being worked and will be available as soon as possible.

If you are interested in contributing but unsure where to begin, please get in touch.

Large Contributions

For substantial contributions, such as a new proof system, we strongly encourage the development of a blueprint first.

• What is a Blueprint? A blueprint is a document that outlines:
  • The contents of the formalization.
  • The proposed formalization strategy in Lean (key definitions, theorems, assumptions).
  • A dependency graph relating all intermediate results to the final desired result.
  • References to relevant literature.
  • Potential challenges and design choices.
• Why a Blueprint? This helps align the contribution with the project's structure and goals before significant coding and proving effort is invested. It facilitates discussion and feedback from maintainers and the community. It also makes it easier to manage large efforts in a distributed way.
• Process: Please open a new discussion or issue to propose your planned contribution and discuss the blueprint before starting implementation.

Pull Request Guidelines

We follow the specific convention for pull request titles and descriptions used by the Lean community.

Title Format

The title should follow the format:

<type>(<optional-scope>): <subject>

Types:

• feat: New feature
• fix: Bug fix
• doc: Documentation changes
• style: Formatting, missing semicolons, etc.
• refactor: Code refactoring
• test: Adding missing tests
• chore: Maintenance
• perf: Performance improvements
• ci: CI workflow changes

Subject:

• Use imperative, present tense ("change" not "changed" or "changes").
• Do not capitalize the first letter.
• No dot (.) at the end.

Description

The description should include:

• Motivation for the change.
• Contrast with previous behavior.
• References to issues (e.g., Closes #123).

Style and Naming Guidelines

We aim to adhere to the Lean community's contribution guidelines. Our linting script helps enforce some aspects of these guidelines.

Naming Conventions

• Files: UpperCamelCase.lean (e.g., BinarySearch.lean).
• Types and Structures: UpperCamelCase (e.g., MonoidHom, Visualizer).
• Functions and Terms: lowerCamelCase (e.g., binarySearch, isPrime).
• Theorems and Proofs: snake_case (e.g., add_comm, list_reverse_id).
• Acronyms: Treat as words (e.g., HtmlParser not HTMLParser).
• Prop-valued Classes: Use UpperCamelCase. If the class is an adjective, use the Is prefix (e.g., IsCompact, IsPrime). If it is a noun, no prefix is needed (e.g., Group, TopologicalSpace).
• Spelling: Use American English for declaration names (e.g., analyze not analyse, color not colour).
• Dot Notation: Use namespaces to group related definitions (e.g., List.map). This enables dot notation (e.g., l.map f) when the type is known. Use manual dot notation for logical connectives and equality (e.g., And.intro, Eq.refl, Iff.mp).
• Axiomatic Names: Use standard names for properties: refl, symm, trans, comm, assoc, inj (injective), congr.
• Identifiers:
  • Use namespaces for logical properties (e.g., And.comm, Or.intro).
  • Use descriptive names for arithmetic/algebraic properties (e.g., mul_comm, add_assoc).

Theorem Naming Logic

• Hypotheses: Use _of_ to separate hypotheses, listed in the order they appear (e.g., lt_of_succ_le means "less than follows from successor less equal").
• Variants: Use left or right to describe which argument changes or is relevant (e.g., add_le_add_left).
• Structural Lemmas:
  • ext: For extensionality (∀ x, f x = g x → f = g).
  • iff: For bidirectional implications.
  • inj / injective: For injectivity results.
  • mono / antitone: For monotonicity.
• Induction/Recursion:
  • induction_on / recOn: Use when the value comes before the constructions (motive eliminates to Prop / Type).
  • induction / rec: Use when the constructions come before the value.
• Predicates: Generally use prefixes (e.g., isClosed_Icc not Icc_isClosed). Exceptions include property suffixes like _inj, _mono, _injective, _surjective.

Variable Conventions

• u, v, w, ... : Universes
• α, β, γ, ... : Generic types
• a, b, c, ... : Propositions
• x, y, z, ... : Elements of a generic type
• h, h₁, ... : Assumptions/Hypotheses
• p, q, r, ... : Predicates and relations
• m, n, k, ... : Natural numbers
• i, j, k, ... : Integers
• s, t, ... : Sets or Lists

Symbol Naming Dictionary

When translating theorem statements into names, we use standard mappings for symbols:

Logic

Symbol	Name	Symbol	Name	Symbol	Name
∨	or	∧	and	¬	not
→	of / imp	↔	iff	∃	exists
∀	all / forall	=	eq	≠	ne

Sets and Lattices

Symbol	Name	Symbol	Name	Symbol	Name
∈	mem	∉	notMem	⊆	subset
∩	inter	∪	union	\	sdiff
≤	le	<	lt	⊥	bot
⊤	top	⊔	sup	⊓	inf

Algebra

Symbol	Name	Symbol	Name	Symbol	Name
+	add	*	mul	^	pow
-	neg / sub	⁻¹	inv	/	div
∑	sum	∏	prod	•	smul

Note: In adherence with mathlib, we standardize on ≤ (le) and < (lt). Avoid ≥ (ge) and > (gt) in theorem statements unless necessary for argument ordering.

Syntax and Formatting

• Line Length: Keep lines under 100 characters.
• Indentation: Use 2 spaces for indentation.
• Headers: Use standard file headers including copyright, license (Apache 2.0), and authors.

  /-
  Copyright (c) 2024 Author Name. All rights reserved.
  Released under Apache 2.0 license as described in the file LICENSE.
  Authors: Author Name
  -/

• Imports: Group imports at the top of the file.
• Operators: Put spaces on both sides of :, :=, and infix operators. Place them before a line break rather than at the start of the next line.
• Hypotheses: Prefer placing hypotheses to the left of the colon (e.g., (h : P) : Q) rather than using arrows (: P → Q) when the proof introduces them.
• Functions: Prefer fun x ↦ ... over λ x, ....
• Instances: Use the where syntax for defining instances and structures.
• Binders: Use a space after binders (e.g., ∀ x, not ∀x,).
• Tactic Mode: Place by at the end of the line preceding the tactic block. Indent the tactic block.
• Calculations: In calc blocks, align relations.
• Empty Lines: Avoid empty lines inside definitions or proofs.
• Delimiters: Avoid parentheses where possible. Use <| (pipe left) and |> (pipe right) to reduce nesting. Avoid using ; to separate tactics unless writing short, single-line tactic sequences.
• Error Messages: In custom error or trace messages, surround interpolated data with backticks (inline) or place it on a new indented line.

Normal Forms

We aim for consistent representations of equivalent statements:

• Standard Forms: Use established normal forms (e.g., s.Nonempty instead of s ≠ ∅) to enable dot notation and consistency.
• Inequalities with Bottom/Top:
  • In assumptions, use x ≠ ⊥ (easier to check).
  • In conclusions, use ⊥ < x (more powerful result).
  • Similarly for top: x ≠ ⊤ in assumptions, x < ⊤ in conclusions.

Tactic Mode & Performance

• Squeezing Simp: Do not "squeeze" terminal simp calls (replacing simp with simp only [...]) unless necessary for performance or stability. Un-squeezed simp is often more readable and robust to minor library changes.
• Comments: Use -- for inline comments and /- ... -/ for block comments.

Transparency and API Design

• Definitions (def): By default, def creates semireducible definitions. These are usually not unfolded by tactics like rw and simp without explicit instruction. This is preferred for most definitions to keep terms manageable.
• Abbreviations (abbrev): Creates reducible definitions that are always unfolded. Use this for type synonyms or lightweight aliases where the underlying term should be exposed.
• Irreducible: Use irreducible (or structure wrappers) to seal API boundaries when the internal implementation details should not leak.

Deprecation Policy

• Renaming: If you rename a declaration, please ensure you fix any breakage this causes. If that is not possible, keep the old name as a deprecated alias to avoid breaking downstream code immediately.

  @[deprecated (since := "YYYY-MM-DD")] alias oldName := newName

• Removal: For removals, provide a message explaining the transition.

  @[deprecated "Use `better_theorem` instead" (since := "YYYY-MM-DD")]
  theorem old_theorem ...

Documentation Standards

Every definition and major theorem should have a docstring.

• Module Docstrings: Each file should start with a /-! ... -/ block containing a title, summary, notation, and references.
• Sectioning Comments: Use /-! ### Title -/ to structure large files into sections. These appear in the generated documentation.
• Declaration Docstrings: Use /-- ... -/ above definitions.
• Syntax:
  • Use backticks for Lean names: `List.map`.
  • Use LaTeX for math: $ f(x) = y $ (inline) or $$ \sum_{i=0}^n i $$ (display).
• Tactic Documentation: Complete and self-contained descriptions for tactics.

Citation Standards

When referencing papers in Lean docstrings:

• Use citation keys in text: Reference papers with citation keys like [ACFY24] rather than full titles or URLs.

• Include a References section: Each file that cites papers should have a ## References section in its docstring header:

  ## References
  
  * [Arnon, G., Chiesa, A., Fenzi, G., and Yogev, E., *WHIR: Reed–Solomon Proximity Testing
      with Super-Fast Verification*][ACFY24]
  * [Ben-Sasson, E., Carmon, D., Ishai, Y., Kopparty, S., and Saraf, S., *Proximity Gaps
      for Reed-Solomon Codes*][BCIKS20]

  Format: * [Author Last Name, First Initial, *Title*][citation_key].

• Add BibTeX entries: All academic papers must have entries in blueprint/src/references.bib. When adding a new paper, add the BibTeX entry, use the citation key in your Lean file, and list it in the References section.

• Non-academic references: Implementation references (GitHub repos, specifications) may include URLs directly and typically don't need BibTeX entries.

Code of Conduct

To ensure a welcoming and collaborative environment, CompPoly follows the principles outlined in the mathlib Code of Conduct.

By participating in this project (e.g., contributing code, opening issues, commenting in discussions), you agree to abide by its terms. Please treat fellow contributors with respect. Unacceptable behavior can be reported to the project maintainers.

Licensing

Like many other Lean projects, CompPoly is licensed under the terms of the Apache License 2.0 license. The full license text can be found in the LICENSE file.

By contributing to CompPoly, you agree that your contributions will be licensed under this same license. Ensure you are comfortable with these terms before submitting contributions.