feat: Add module_doc_lint to CI

.github/workflows/build.yml

@@ -77,6 +77,12 @@ jobs:
         run: |
           bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake exe sorry_lint"
 
+      # Reads the source files directly, so it does not need the build above to have succeeded.
+      - name: module documentation linter
+        if: ${{ !cancelled() }}
+        run: |
+          bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake exe module_doc_lint"
+
       - name: runLinter on Physlib
         if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
         id: lint

AGENTS.md

@@ -18,7 +18,7 @@
 - Make sure that hypotheses are distributed compactly and neatly over new lines, only include new lines when genuinely needed.
 - Do not add lemmas that are trivial rewrites of existing Mathlib or Physlib results, unless they add genuine physics context.
 - Place results in the appropriate existing file; do not create new files without good reason. For example, if you need to prove a general result about derivatives on space in order to prove something in classical mechanics, that result should go in `Space.Derivatives.Basic`, not the classical mechanics file.
-- Include sections which are numbered by `# A. ...`, `## A.1. ...`. See [Physlib/ClassicalMechanics/HarmonicOscillator/Basic.lean](Physlib/ClassicalMechanics/HarmonicOscillator/Basic.lean) for an example.
+- Module documentation (`/-! … -/`) must have the headings: a title `# ...`, followed by a one-line summary of the file; `## i. Overview`; `## ii. Key results`; `## iii. Table of contents`; `## iv. References`; then sections numbered `## A. ...`, `### A.1. ...`, `#### A.1.2. ...`, listed in the table of contents. No heading may end in a full stop. See [Physlib/ClassicalMechanics/HarmonicOscillator/Basic.lean](Physlib/ClassicalMechanics/HarmonicOscillator/Basic.lean) for an example.
 - Every definition must have a docstring.
 - Important lemmas should have a docstring.
 
@@ -58,6 +58,8 @@ When a long proof cannot be split, make sure it contains comments.
 - Check that `lake exe forMathlib_lint` passes: files in `Physlib/Mathematics/ForMathlib/` may only
   import from within that directory, and each must be used outside it.
 - Check `./scripts/lint-style.sh`, but **commit your changes first**; this linter reads committed state.
+- Check that `lake exe module_doc_lint` passes (no build needed). Never add files to
+  `scripts/MetaPrograms/module_doc_no_lint.txt`; fix their module documentation instead.
 - Check that `lake exe auxillary_script_test` passes (needs `Physlib`, `QuantumInfo` and
   `PhyslibAlpha` built).
 - If edited a `PhyslibAlpha` file, check the following:

Physlib/ProbabilisticTheory/Effect/Complement.lean

@@ -10,6 +10,8 @@ public import Physlib.ProbabilisticTheory.Effect.Convex
 /-!
 # Complementary effects
 
+The complement `1 - e` of an effect, its antitonicity and compatibility with mixtures.
+
 ## i. Overview
 
 The complement of an effect `e` is the yes/no test that fires exactly when `e` doesn't: `1 - e`.
@@ -27,6 +29,10 @@ Physically, a state's probability of "no" is always `1` minus its probability of
 - B. Monotonicity of the complement
 - C. The complement and mixtures
 
+## iv. References
+
+* None.
+
 -/
 
 @[expose] public section

Physlib/ProbabilisticTheory/Effect/Convex.lean

@@ -11,6 +11,8 @@ public import Physlib.ProbabilisticTheory.Effect.Basic
 /-!
 # Convexity and mixtures of effects
 
+The effect interval is convex, so effects can be mixed with a given probability.
+
 ## i. Overview
 
 The effect interval `[0, 1]` is convex: randomizing between two effects with some probability
@@ -26,6 +28,10 @@ actually run is itself a legitimate measurement.
 
 - A. Convexity and mixtures of effects
 
+## iv. References
+
+* None.
+
 -/
 
 @[expose] public section

Physlib/ProbabilisticTheory/Effect/Metric.lean

@@ -10,6 +10,8 @@ public import Physlib.ProbabilisticTheory.Effect.Basic
 /-!
 # The metric space of effects
 
+The order-unit metric on effects and their identification with the order-unit-norm ball.
+
 ## i. Overview
 
 Effects sit inside `E`, so pulling back the order-unit norm along the inclusion `Effect E ↪ E`
@@ -28,6 +30,10 @@ Effects also correspond to points of the order-unit-norm ball, by the affine res
 - A. The effect metric
 - B. Effects as points of the order-unit-norm ball
 
+## iv. References
+
+* None.
+
 -/
 
 @[expose] public section

Physlib/ProbabilisticTheory/Effect/Sharp.lean

@@ -11,6 +11,8 @@ public import Physlib.ProbabilisticTheory.Effect.Complement
 /-!
 # Sharp effects
 
+Sharp effects: extreme points of the effect interval, preserved by taking complements.
+
 ## i. Overview
 
 The effect interval `[0, 1]` is convex. A sharp effect is an extreme point of it: one that cannot
@@ -26,6 +28,10 @@ be written as a nontrivial mixture of two distinct effects. Sharp effects genera
 
 - A. Sharp effects
 
+## iv. References
+
+* None.
+
 -/
 
 @[expose] public section

Physlib/Relativity/Fermions/Weyl/DualLeftHanded.lean

@@ -11,7 +11,7 @@ public import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
 public import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
 /-!
 
-## Dual left handed Weyl fermions
+# Dual left handed Weyl fermions
 
 
 In this file we define dual Left handed Weyl fermions.

Physlib/Relativity/Fermions/Weyl/DualRightHanded.lean

@@ -11,7 +11,7 @@ public import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
 public import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
 /-!
 
-## Dual right handed Weyl fermions
+# Dual right handed Weyl fermions
 
 
 In this file we define dual right handed Weyl fermions.

Physlib/Relativity/Fermions/Weyl/LeftHanded.lean

@@ -10,7 +10,7 @@ public import Mathlib.RepresentationTheory.Basic
 public import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
 /-!
 
-## Left handed Weyl fermions
+# Left handed Weyl fermions
 
 
 In this file we define Left handed Weyl fermions.

Physlib/Relativity/Fermions/Weyl/RightHanded.lean

@@ -10,7 +10,7 @@ public import Mathlib.RepresentationTheory.Basic
 public import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
 /-!
 
-## Right handed Weyl fermions
+# Right handed Weyl fermions
 
 
 In this file we define Right handed Weyl fermions.

Physlib/StatisticalMechanics/MicroCanonicalEnsemble/Basic.lean

@@ -8,7 +8,7 @@ module
 public import Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop
 /-!
 
-## The Microcanonical Ensemble
+# The Microcanonical Ensemble
 
 -/
 

Physlib/StatisticalMechanics/MicroCanonicalEnsemble/IdealGas.lean

@@ -9,7 +9,7 @@ public import Physlib.StatisticalMechanics.MicroCanonicalEnsemble.ThermoQuantiti
 public import Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
 /-!
 
-## Ideal gas as a Micro Canonical Ensemble
+# Ideal gas as a Micro Canonical Ensemble
 
 In this module we give the
 -/

Physlib/StatisticalMechanics/MicroCanonicalEnsemble/ThermoQuantities.lean

@@ -9,7 +9,7 @@ public import Physlib.StatisticalMechanics.MicroCanonicalEnsemble.Basic
 public import QuantumInfo.ForMathlib.ComplexLaplaceTransform
 /-!
 
-## The theormodynamical quantities of a microcanonical ensemble
+# The theormodynamical quantities of a microcanonical ensemble
 
 -/
 @[expose] public section

PhyslibAlpha/Basic.lean

@@ -6,12 +6,35 @@ Authors: Joseph Tooby-Smith
 module
 public import Physlib.Meta.TODO.Basic
 /-!
+# PhyslibAlpha
 
-## Overview
+The entry point of PhyslibAlpha, an extension of Physlib with a lighter review process.
+
+## i. Overview
 
 PhyslibAlpha is an extension of Physlib with a lighter review process.
 We expect the file structure to match where possible that of Physlib.
 
+This file contains no declarations; it documents the purpose and review policy of the project.
+
+## ii. Key results
+
+* None: this file contains only documentation.
+
+## iii. Table of contents
+
+- A. Review policy
+
+## iv. References
+
+* None.
+
+-/
+
+/-!
+
+## A. Review policy
+
 The idea is that it sits between the high review standards of Physlib and
 just allowing anything in the project.
 

PhyslibAlpha/ClassicalFieldTheory/Local/Action.lean

@@ -10,6 +10,8 @@ public import PhyslibAlpha.ClassicalFieldTheory.Local.Variation
 /-!
 # Local action functionals
 
+The local action of a field, its value under admissible variations, and critical fields.
+
 ## i. Overview
 
 This module defines the local action functional associated with a local Lagrangian, together with

PhyslibAlpha/ClassicalFieldTheory/Local/EulerLagrange.lean

@@ -9,6 +9,8 @@ public import PhyslibAlpha.ClassicalFieldTheory.Local.Action
 /-!
 # Local Euler-Lagrange operators
 
+The local Euler-Lagrange operator of a local Lagrangian, built componentwise.
+
 ## i. Overview
 
 This module defines the local Euler-Lagrange operator associated with a local Lagrangian.

PhyslibAlpha/ClassicalFieldTheory/Local/EulerLagrangeEquation.lean

@@ -9,6 +9,8 @@ public import PhyslibAlpha.ClassicalFieldTheory.Local.FirstVariation
 /-!
 # Local Euler-Lagrange equations
 
+A named predicate for the local Euler-Lagrange equations and the criticality criteria using it.
+
 ## i. Overview
 
 This module gives a named predicate for fields satisfying the local Euler-Lagrange equations.

PhyslibAlpha/ClassicalFieldTheory/Local/FirstOrder.lean

@@ -9,6 +9,8 @@ public import PhyslibAlpha.ClassicalFieldTheory.Local.FirstVariation
 /-!
 # First-order local field theory
 
+Aliases and projections specializing the local field theory API to first-order jets.
+
 ## i. Overview
 
 This module provides a thin usability layer for first-order local field theory, i.e. the

PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation.lean

@@ -9,6 +9,8 @@ public import PhyslibAlpha.ClassicalFieldTheory.Local.FirstVariation.Criterion
 /-!
 # First variation and the Euler-Lagrange criterion
 
+Public entry point: a field is critical iff its local Euler-Lagrange operator vanishes.
+
 ## i. Overview
 
 This module is the public entry point for the local first-variation theory. The core linearized

PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/Basic.lean

@@ -10,6 +10,8 @@ public import Physlib.Mathematics.VariationalCalculus.Basic
 /-!
 # First variation core objects
 
+The linearized first-variation density and its Euler-Lagrange pairing.
+
 ## i. Overview
 
 This module contains the basic objects used throughout the local first-variation theory:

PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/Criterion.lean

@@ -11,6 +11,8 @@ public import PhyslibAlpha.ClassicalFieldTheory.Local.FirstVariation.Regularity
 /-!
 # First variation criteria
 
+Assembles the first-variation formula into Euler-Lagrange criteria for critical fields.
+
 ## i. Overview
 
 This module assembles the analytic ingredients of the local first-variation proof into the
@@ -25,7 +27,7 @@ facade.
 ## iii. Table of contents
 
 - A. First-variation assembly
-- B. Final Euler-Lagrange criterion
+- B. Intermediate Euler-Lagrange criteria
 
 ## iv. References
 

PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/Density.lean

@@ -10,6 +10,8 @@ public import Mathlib.Analysis.Calculus.ParametricIntegral
 /-!
 # First variation density formulas
 
+Differentiation of the varied action density, pointwise and under the integral sign.
+
 ## i. Overview
 
 This module contains the pointwise and integral first-variation formulas before integration by

PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/IntegrationByParts.lean

@@ -9,6 +9,8 @@ public import PhyslibAlpha.ClassicalFieldTheory.Local.FirstVariation.Support
 /-!
 # First variation integration by parts
 
+Repeated integration by parts for the local first-variation formula.
+
 ## i. Overview
 
 This module contains the repeated integration-by-parts step needed for the local first-variation

PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/Regularity.lean

@@ -9,6 +9,8 @@ public import PhyslibAlpha.ClassicalFieldTheory.Local.FirstVariation.Support
 /-!
 # First variation regularity
 
+Continuity of the Euler-Lagrange operator and smooth regularity from coordinate regularity.
+
 ## i. Overview
 
 This module contains regularity consequences used in the local Euler-Lagrange criterion: continuity

PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/Support.lean

@@ -9,6 +9,8 @@ public import PhyslibAlpha.ClassicalFieldTheory.Local.FirstVariation.Basic
 /-!
 # First variation support lemmas
 
+Support lemmas for the first variation: varied fields, test functions, varied jet coordinates.
+
 ## i. Overview
 
 This module collects the reusable support lemmas used by the analytic part of the local

PhyslibAlpha/ClassicalFieldTheory/Local/JetPoint.lean

@@ -10,6 +10,8 @@ public import Physlib.SpaceAndTime.Space.Derivatives.Iterated
 /-!
 # Coordinate-level jet points
 
+Coordinate-level jet points of fields on `Space d` and the jets of a field at a point.
+
 ## i. Overview
 
 This module introduces the coordinate-level point of the locally trivialized `k`-jet bundle for

PhyslibAlpha/ClassicalFieldTheory/Local/JetPointFiber.lean

@@ -9,6 +9,8 @@ public import PhyslibAlpha.ClassicalFieldTheory.Local.JetPoint
 /-!
 # Fiber directions on jet points
 
+Affine fiber-direction structure on coordinate-level jet points.
+
 ## i. Overview
 
 This module adds the affine fiber-direction structure on coordinate-level jet points.

PhyslibAlpha/ClassicalFieldTheory/Local/JetPointRegularity.lean

@@ -9,6 +9,8 @@ public import PhyslibAlpha.ClassicalFieldTheory.Local.JetPointFiber
 /-!
 # Regularity and support for jet-coordinate maps
 
+Smoothness of jet-coordinate maps of smooth fields and their vanishing outside the support.
+
 ## i. Overview
 
 This module collects the analytic facts about coordinate-level jet maps that are needed later in

PhyslibAlpha/ClassicalFieldTheory/Local/Lagrangian.lean

@@ -10,6 +10,8 @@ public import PhyslibAlpha.ClassicalFieldTheory.Local.TotalDerivative
 /-!
 # Local Lagrangians
 
+Local finite-order Lagrangians on jet points, their regularity, and evaluation along fields.
+
 ## i. Overview
 
 This module defines local Lagrangians of finite order for fields on `Space d` with values in

PhyslibAlpha/ClassicalFieldTheory/Local/TotalDerivative.lean

@@ -9,6 +9,8 @@ public import PhyslibAlpha.ClassicalFieldTheory.Local.JetPoint
 /-!
 # Total derivatives on local jet-dependent functions
 
+Total derivatives of jet-dependent functions, defined via evaluation along fields.
+
 ## i. Overview
 
 This module defines total derivatives of local jet-dependent functions by differentiating their

PhyslibAlpha/ClassicalFieldTheory/Local/TotalDivergence.lean

@@ -9,6 +9,8 @@ public import PhyslibAlpha.ClassicalFieldTheory.Local.FirstOrder
 /-!
 # Total divergences in local classical field theory
 
+Packaged total-divergence Lagrangians and the Euler-Lagrange-triviality property.
+
 ## i. Overview
 
 This module introduces the local coordinate API for total-divergence lagrangians.

PhyslibAlpha/ClassicalFieldTheory/Local/TotalDivergenceEquivalence.lean

@@ -9,6 +9,8 @@ public import PhyslibAlpha.ClassicalFieldTheory.Local.TotalDivergence
 /-!
 # Lagrangian equivalence up to total divergences
 
+Lagrangians differing by a total divergence have the same Euler-Lagrange equations.
+
 ## i. Overview
 
 This module adds the local coordinate API for lagrangians that differ by a total divergence.