Merge pull request #1774 from jdchristensen/coqdoc_headings

Fix coqdoc section titles, << >>, and lots more

Makefile.coq.local-early

@@ -6,4 +6,4 @@
 # Makefile.coq.local currently contains additional targets that need
 # access to the variables in Makefile.coq
 COQDOCEXTRAFLAGS?=
-COQDOCFLAGS?=-interpolate -utf8 --no-externals $(COQDOCEXTRAFLAGS)
+COQDOCFLAGS?=--interpolate --utf8 --no-externals --parse-comments $(COQDOCEXTRAFLAGS)

STYLE.md

@@ -44,7 +44,7 @@
   - [1.9. Formatting](#19-formatting)
     - [1.9.1. Location of commands](#191-location-of-commands)
     - [1.9.2. Indentation](#192-indentation)
-    - [1.9.3. Line lengths](#193-line-lengths)
+    - [1.9.3. Line lengths and comments](#193-line-lengths-and-comments)
     - [1.9.4. Tactic scripts](#194-tactic-scripts)
     - [1.9.5. Placement of Arguments and types](#195-placement-of-arguments-and-types)
   - [1.10. Implicit Arguments](#110-implicit-arguments)
@@ -906,14 +906,32 @@ excessive churn in the diff.  If you wish, you can submit a separate
 pull request or commit for the re-indentation, labeled as "only
 whitespace changes" so that no one bothers reading the diff carefully.
 
-### 1.9.3. Line lengths
+### 1.9.3. Line lengths and comments
 
 Lines of code should be of limited width; try to restrict yourself to
 not much more than 70 characters.  Remember that when Coq code is
 often edited in split-screen so that the screen width is cut in half,
 and that not everyone's screen is as wide as yours.
 
-Text in comments, on the other hand, should not contain hard newlines.
+[coqdoc](https://coq.inria.fr/refman/using/tools/coqdoc.html) is used to produce
+a browsable [view of the library](https://hott.github.io/Coq-HoTT/coqdoc-html/toc.html).
+coqdoc treats comments specially, so comments should follow the
+conventions described on the coqdoc page.  The most important ones are
+that Coq expressions within comments are surrounded by square brackets,
+and that headings are indicated with comments of the form
+
+```coq
+(** * This is a top-level section *)
+(** ** This is a subsection *)
+(** *** This is a sub-subsection *)
+```
+
+Section titles should be less than 80 characters, on one line, and not
+end in a period.  Other comments are generally written using the style
+`(** This is a comment. *)` or `(* This is a comment. *)`, with the
+latter generally used for inline comments during a proof.
+
+Text in comments should not contain hard newlines.
 Putting hard newlines in text makes it extremely ugly when viewed in a
 window that is narrower than the width to which you filled it.  If
 editing in Emacs, turn off `auto-fill-mode` and turn on

contrib/HoTTBookExercises.v

@@ -789,15 +789,15 @@ Proof.
 
   (** To obtain the situation of 2.9.4, we rewrite x using
 
-      <<<
+<<
         x = transport (fun A : Type => C A) p^ x
-      >>>
+>>
 
       This equality holds because [(C A) -> (C A)] is contractible, so
 
-      <<<
+<<
         transport (fun A : Type => C A) p^ = idmap
-      >>>
+>>
 
       In both Theorem 3.2.2 and the following result, the hypothesis
       [Contr ((C A) -> (C A))] will follow from the contractibility of [(C A)].

contrib/dune

@@ -2,4 +2,5 @@
  (name HoTT.Contrib)
  (package coq-hott)
  (flags -noinit -indices-matter -color on)
+ (coqdoc_flags :standard --interpolate --utf8 --no-externals --parse-comments)
  (theories HoTT))

test/dune

@@ -1,7 +1,8 @@
 (coq.theory
  (name HoTT.Tests)
  (theories HoTT)
- (flags -noinit -indices-matter -color on))
+ (flags -noinit -indices-matter -color on)
+ (coqdoc_flags :standard --interpolate --utf8 --no-externals --parse-comments))
 
 (include_subdirs qualified)
 

theories/Algebra/Universal/Congruence.v

@@ -21,15 +21,15 @@ Section congruence.
 (** A finitary operation [f : A s1 * A s2 * ... * A sn -> A t]
     satisfies [OpCompatible f] iff
 
-    <<
+<<
       Φ s1 x1 y1 * Φ s2 x2 y2 * ... * Φ sn xn yn
-    >>
+>>
 
     implies
 
-    <<
+<<
       Φ t (f (x1, x2, ..., xn)) (f (y1, y2, ..., yn)).
-    >>
+>>
 
     The below definition generalizes this to infinitary operations.
 *)

theories/Algebra/Universal/Operation.v

@@ -79,7 +79,8 @@ Definition FiniteOperation {σ : Signature} (A : Carriers σ)
 (** A type of curried operations
 <<
 CurriedOperation A [s1, ..., sn] t := A s1 -> ... -> A sn -> A t.
->> *)
+>>
+*)
 
 Fixpoint CurriedOperation {σ} (A : Carriers σ) {n : nat}
   : (FinSeq n (Sort σ)) -> Sort σ -> Type

theories/Algebra/Universal/TermAlgebra.v

@@ -2,9 +2,9 @@
 
     We show that term algebra forms an adjoint functor from the category of hset carriers
 
-    <<
+<<
       {C : Carrier σ | forall s, IsHSet (C s)}
-    >>
+>>
 
     to the category of algebras (without equations) [Algebra σ], where [Carriers σ] is notation for [Sort σ -> Type].  See [ump_term_algebra].
 
@@ -45,9 +45,9 @@ Definition CarriersTermAlgebra_rec {σ : Signature} (C : Carriers σ)
 
 (** A family of relations [R : forall s, Relation (C s)] can be extended to a family of relations on the term algebra carriers,
 
-    <<
+<<
       forall s, Relation (CarriersTermAlgebra C s)
-    >>
+>>
 
     See [ExtendDRelTermAlgebra] and [ExtendRelTermAlgebra] below. *)
 
@@ -318,22 +318,23 @@ End hom_term_algebra.
 (** The next section proves the universal property of the term algebra,
     that [TermAlgebra] is a left adjoint functor
 
-    >>
+<<
       {C : Carriers σ | forall s, IsHSet (C s)} -> Algebra σ,
-    <<
+>>
 
     with right adjoint the forgetful functor. This is stated below as
     an equivalence
 
-    >>
+<<
       Homomorphism (TermAlgebra C) A <~> (forall s, C s -> A s),
-    <<
+>>
 
     given by precomposition with
     
-    >>
+<<
       var_term_algebra C s : C s -> TermAlgebra C s.
-    << *)
+>>
+*)
 
 Section ump_term_algebra.
   Context

theories/Basics/Overture.v

@@ -295,7 +295,8 @@ Module inverseSymmetric (inverse : inverseT).
 End inverseSymmetric.
 
 Module Export symmetric_paths := inverseSymmetric inverse.
->> *)
+>>
+*)
 
 
 (** We define equality concatenation by destructing on both its arguments, so that it only computes when both arguments are [idpath].  This makes proofs more robust and symmetrical.  Compare with the definition of [identity_trans].  *)

theories/Categories/Functor/Composition/Functorial/Core.v

@@ -10,7 +10,7 @@ Set Implicit Arguments.
 Generalizable All Variables.
 Set Asymmetric Patterns.
 
-(** * Construction of the functor [_∘_ : (C → D) × (D → E) → (C → E)] and it's curried variant *)
+(** Construction of the functor [_∘_ : (C → D) × (D → E) → (C → E)] and its curried variant *)
 Section functorial_composition.
   Context `{Funext}.
   Variables C D E : PreCategory.

theories/Categories/Functor/Composition/Laws.v

@@ -97,7 +97,8 @@ Section coherence.
                 \\   //
                  \\ //
                  G ∘ F
->> *)
+>>
+*)
   Lemma triangle C D E (F : Functor C D) (G : Functor D E)
   : (associativity F 1 G @ ap (compose G) (left_identity F))
     = (ap (fun G' : Functor D E => G' o F) (right_identity G)).
@@ -121,7 +122,8 @@ Section coherence.
               ||                      ||
               ||                      ||
       ((K ∘ H) ∘ G) ∘ F ====== (K ∘ (H ∘ G)) ∘ F
->> *)
+>>
+*)
   Lemma pentagon A B C D E
         (F : Functor A B) (G : Functor B C) (H : Functor C D) (K : Functor D E)
   : (associativity F G (K o H) @ associativity (G o F) H K)

theories/Categories/LaxComma/CoreLaws.v

@@ -151,7 +151,8 @@ Module Import LaxCommaCategory.
         repeat (let H := fresh "x" in intro H).
         repeat match goal with H : _ |- _ => revert H end.
         intro.
->> *)
+>>
+*)
 
     Lemma associativity_helper
           {x x0 : PreCategory} {x1 : Functor x0 x}
@@ -269,7 +270,8 @@ Lemma left_identity (s d : object) (m : morphism s d)
         repeat (let H := fresh "x" in intro H).
         repeat match goal with H : _ |- _ => revert H end.
         intro.
->> *)
+>>
+*)
 
     Lemma left_identity_helper
           {x x0 : PreCategory} {x1 : Functor x0 x}
@@ -364,7 +366,8 @@ Lemma left_identity (s d : object) (m : morphism s d)
         repeat (let H := fresh "x" in intro H).
         repeat match goal with H : _ |- _ => revert H end.
         intro.
->> *)
+>>
+*)
 
     Lemma right_identity_helper
           {x x0 : PreCategory} {x1 : Functor x0 x}

theories/Categories/PseudonaturalTransformation/Core.v

@@ -189,7 +189,8 @@ Print PseudonaturalTransformationParts.a_part.
 Print PseudonaturalTransformationParts.b_part.
 Print PseudonaturalTransformationParts.b_id_part.
 Print PseudonaturalTransformationParts.c_part.
->> *)
+>>
+*)
 
 Record PseudonaturalTransformation `{Funext} (X : PreCategory)
        (F G : Pseudofunctor X) :=

theories/Classes/implementations/family_prod.v

@@ -11,9 +11,9 @@ Section family_prod.
 
   (** [FamilyProd F ℓ] is a product type defined by
   
-      <<
+<<
         FamilyProd F [i1;i2;...;in] = F i1 * F i2 * ... * F in * Unit
-      >>
+>>
 
       It is convenient to have the [Unit] in the end.
   *)
@@ -23,10 +23,11 @@ Section family_prod.
 
   (** Map function for [FamilyProd F ℓ],
 
-      <<
+<<
         map_family_prod f (x1, x2, ..., xn, tt)
         = (f x1, f x2, ..., f xn, tt)
-      >> *)
+>>
+*)
 
   Fixpoint map_family_prod {F G : I → Type} {ℓ : list I}
       (f : ∀ i, F i → G i)
@@ -60,9 +61,9 @@ Section family_prod.
   (** If [R : ∀ i, relation (F i)] is a family of relations indexed by
       [i:I] and [R i] is reflexive for all [i], then
 
-      <<
+<<
         for_all_2_family_prod F F R s s
-      >>
+>>
 
       holds. *)
   Lemma reflexive_for_all_2_family_prod (F : I → Type)

theories/Classes/interfaces/ua_algebra.v

@@ -85,9 +85,9 @@ Notation Carriers σ := (Sort σ → Type).
 (** The function [Operation] maps a family of carriers [A : Carriers σ]
     and [w : SymbolType σ] to the corresponding function type.
 
-    <<
+<<
       Operation A [:s1; s2; ...; sn; t:] = A s1 → A s2 → ... → A sn → A t
-    >>
+>>
 
     where [[:s1; s2; ...; sn; t:] : SymbolType σ] is a symbol type
     with domain [[s1; s2; ...; sn]] and codomain [t]. *)
@@ -107,9 +107,9 @@ Defined.
 
 (** Uncurry of an [f : Operation A w], such that
 
-    <<
+<<
       ap_operation f (x1,x2,...,xn) = f x1 x2 ... xn
-    >>
+>>
 *)
 
 Fixpoint ap_operation {σ} {A : Carriers σ} {w : SymbolType σ}
@@ -123,9 +123,9 @@ Fixpoint ap_operation {σ} {A : Carriers σ} {w : SymbolType σ}
 
 (** Funext for uncurried [Operation A w]. If
 
-    <<
+<<
       ap_operation f (x1,x2,...,xn) = ap_operation g (x1,x2,...,xn)
-    >>
+>>
 
     for all [(x1,x2,...,xn) : A s1 * A s2 * ... * A sn], then [f = g]. *)
 

theories/Classes/interfaces/ua_congruence.v

@@ -11,15 +11,15 @@ Section congruence.
 (** An operation [f : A s1 → A s2 → ... → A sn → A t] satisfies
     [OpCompatible f] iff
 
-    <<
+<<
       Φ s1 x1 y1 ∧ Φ s2 x2 y2 ∧ ... ∧ Φ sn xn yn
-    >>
+>>
 
     implies
 
-    <<
+<<
       Φ t (f x1 x2 ... xn) (f y1 y2 ... yn).
-    >>
+>>
 *)
 
   Definition OpCompatible {w : SymbolType σ} (f : Operation A w)

theories/Classes/theory/ua_first_isomorphism.v

@@ -110,9 +110,9 @@ Section first_isomorphism.
 
 (** The homomorphism [def_first_isomorphism] is informally given by
 
-    <<
+<<
       def_first_isomorphism s (class_of _ x) := f s x.
-    >>
+>>
 *)
 
   Definition def_first_isomorphism (s : Sort σ)