Enforce even indentation and automate some conventions (#635)

Wraps up the last PR on pre-commit stuff. ### Summary - add detection for empty sections at the end of a file - add autoremoval of empty code blocks - add autoremoval of punctuation at the end of headers - fix all uneven indentation in the library - enable enforcing of even indentation - pre-commit now properly fails when a misplaced top-level header is detected
UniMath · May 28, 2023 · b7cff12 · b7cff12
1 parent 6fd8409
commit b7cff12
Show file tree

Hide file tree

Showing 236 changed files with 2,689 additions and 2,312 deletions.
diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml
@@ -50,14 +50,14 @@ repos:
         files: ^src\/.+\.lagda\.md$
         types_or: [markdown, text]
 
-      # - id: indentation-conventions
-      #   name: Agda indentation conventions
-      #   entry: scripts/indentation_conventions.py
-      #   language: python
-      #   always_run: true
-      #   files: ^src\/.+\.lagda\.md$
-      #   types_or: [markdown, text]
-      #   require_serial: true
+      - id: indentation-conventions
+        name: Agda indentation conventions
+        entry: scripts/indentation_conventions.py
+        language: python
+        always_run: true
+        files: ^src\/.+\.lagda\.md$
+        types_or: [markdown, text]
+        require_serial: true
 
       - id: simply-wrappable-long-lines
         name: Fix simply wrappable long lines of Agda code

diff --git a/scripts/indentation_conventions.py b/scripts/indentation_conventions.py
@@ -10,7 +10,7 @@
 
 AGDA_INDENT = '  '
 
-even_indentation_pattern = re.compile(fr'({AGDA_INDENT})*(\S|$)')
+even_indentation_pattern = re.compile(fr'^({AGDA_INDENT})*(\S|$)')
 
 
 def is_even_indentation(line):
@@ -52,7 +52,7 @@ def is_even_indentation(line):
                         if (status == 0):
                             print('Error! Uneven indentation found')
 
-                        print(f'{fpath}:line {i}')
+                        print(f'{fpath}:line {i+1}')
 
                         offender_files[fpath] += 1
                         status |= STATUS_UNEVEN_INDENTATION
@@ -72,6 +72,6 @@ def is_even_indentation(line):
         print(*map(lambda kv: f'  {kv[0]}: {kv[1]} lines',
                    sorted(offender_files.items(), key=lambda kv: kv[1])), sep='\n')
         print(
-            f'\nTotal number of lines in library unevenly indented: {sum(offender_files.values())}.')
+            f'\nTotal number of lines in library unevenly indented: {sum(offender_files.values())}.\n\nUneven indentation means that there is code indented by a non-multiple of the base indentation (2 spaces). If you haven\'t already, we suggest you set up your environment to more easily spot uneven indentation. For instance using VSCode\'s indent-rainbow extension.')
 
     sys.exit(status)
diff --git a/scripts/markdown_conventions.py b/scripts/markdown_conventions.py
@@ -6,9 +6,12 @@
 import utils
 import re
 
-open_tag_pattern = re.compile(r'^```\S+\n', flags=re.MULTILINE)
+open_tag_pattern = re.compile(r'^```\S+.*\n', flags=re.MULTILINE)
 close_tag_pattern = re.compile(r'\n```$', flags=re.MULTILINE)
 
+empty_block_pattern = re.compile(
+    r'^```\S+.*\n(\s*\n)*\n```\s*$(?!\n(\s*\n)*</details>)', flags=re.MULTILINE)
+
 
 def has_well_formed_blocks(mdcode, pos=0):
     """
@@ -50,13 +53,16 @@ def has_well_formed_blocks(mdcode, pos=0):
 top_level_header_after_first_line = re.compile(r'\n#\s', flags=re.MULTILINE)
 
 empty_section_nonincreasing_level = re.compile(
-    r'^((#{2}\s([^\n]*)\n(\s*\n)*#{1,2})|(#{3}\s([^\n]*)\n(\s*\n)*#{1,3})|(#{4}\s([^\n]*)\n(\s*\n)*#{1,4})|(#{5}\s([^\n]*)\n(\s*\n)*#{1,5}))(?!#)', flags=re.MULTILINE)
+    r'^((#{2}\s([^\n]*)\n(\s*\n)*#{1,2})|(#{3}\s([^\n]*)\n(\s*\n)*#{1,3})|(#{4}\s([^\n]*)\n(\s*\n)*#{1,4})|(#{5}\s([^\n]*)\n(\s*\n)*#{1,5})|(#{6}\s([^\n]*)\n(\s*\n)*#{1,6})|(#{7}\s([^\n]*)\n(\s*\n)*#{1,7}))(?!#)', flags=re.MULTILINE)
+
+empty_section_eof = re.compile(
+    r'^(.*\n)*#+\s([^\n]*)\n(\s*\n)*$', flags=re.MULTILINE)
 
 if __name__ == '__main__':
 
     STATUS_UNSPECIFIED_OR_ILL_FORMED_BLOCK = 1
     STATUS_TOP_LEVEL_HEADER_AFTER_FIRST_LINE = 2
-    STATUS_EMPTY_SECTION_NONINCREASING_LEVEL = 4
+    STATUS_EMPTY_SECTION = 4
 
     status = 0
 
@@ -75,13 +81,25 @@ def has_well_formed_blocks(mdcode, pos=0):
         if top_level_header_after_first_line.search(output):
             print(
                 f"Error! File '{fpath}' has a top level header after the first line. Please increase it.")
+            status |= STATUS_TOP_LEVEL_HEADER_AFTER_FIRST_LINE
 
         # TODO: print line numbers
         if empty_section_nonincreasing_level.search(output):
             print(
-                f"Error! File '{fpath}' has an empty section. This may be caused by having a header with the wrong header level. If this was not by mistake, consider including a sentence explaining why the section is empty. For instance, depending on the context, you may write 'This remains to be shown.'")
+                f"Error! File '{fpath}' has an empty section. This may be caused by having a header with the wrong header level. If this was not by mistake, consider removing the section or including a sentence explaining why it is empty. For instance, depending on context, you may write 'This remains to be shown.'")
+
+            status |= STATUS_EMPTY_SECTION
+
+        if empty_section_eof.fullmatch(output):
+            print(
+                f"Error! File '{fpath}' has an empty section at the end of the file. Please consider removing the section or adding  a sentence explaining why it is empty. For instance, depending on context, you may write 'This remains to be shown.'")
+
+            status |= STATUS_EMPTY_SECTION
+
+        output = empty_block_pattern.sub('', output)
 
-            status |= STATUS_EMPTY_SECTION_NONINCREASING_LEVEL
+        output = re.sub(
+            r'(^|\n)(#+\s.*)[\.,:;!?¡¿]\s*($|\n)', r'\1\2\3', output)
 
         if output != inputText:
             with open(fpath, 'w') as f:

diff --git a/src/category-theory/coproducts-precategories.lagda.md b/src/category-theory/coproducts-precategories.lagda.md
@@ -37,10 +37,11 @@ module _
     (z : obj-Precategory C)
     (f : type-hom-Precategory C x z) →
     (g : type-hom-Precategory C y z) →
-    ∃! ( type-hom-Precategory C p z)
-       ( λ h →
-         ( comp-hom-Precategory C h l ＝ f) ×
-         ( comp-hom-Precategory C h r ＝ g))
+    ∃!
+      ( type-hom-Precategory C p z)
+      ( λ h →
+        ( comp-hom-Precategory C h l ＝ f) ×
+        ( comp-hom-Precategory C h r ＝ g))
 
   coproduct-Precategory : obj-Precategory C → obj-Precategory C → UU (l1 ⊔ l2)
   coproduct-Precategory x y =

diff --git a/src/category-theory/exponential-objects-precategories.lagda.md b/src/category-theory/exponential-objects-precategories.lagda.md
@@ -47,11 +47,12 @@ module _
   is-exponential-Precategory x y e ev =
     (z : obj-Precategory C)
     (f : type-hom-Precategory C (object-product-Precategory C p z x) y) →
-    ∃! ( type-hom-Precategory C z e)
-       ( λ g →
-         comp-hom-Precategory C ev
-           ( map-product-Precategory C p g (id-hom-Precategory C)) ＝
-           ( f))
+    ∃!
+      ( type-hom-Precategory C z e)
+      ( λ g →
+        comp-hom-Precategory C ev
+          ( map-product-Precategory C p g (id-hom-Precategory C)) ＝
+          ( f))
 
   exponential-Precategory :
     obj-Precategory C → obj-Precategory C → UU (l1 ⊔ l2)

diff --git a/src/category-theory/functors-large-precategories.lagda.md b/src/category-theory/functors-large-precategories.lagda.md
@@ -110,7 +110,8 @@ preserves-comp-functor-Large-Precategory
     ( hom-functor-Large-Precategory F g)
     ( hom-functor-Large-Precategory F f))
 preserves-id-functor-Large-Precategory (comp-functor-Large-Precategory G F) =
-  ( ap ( hom-functor-Large-Precategory G)
-       ( preserves-id-functor-Large-Precategory F)) ∙
+  ( ap
+    ( hom-functor-Large-Precategory G)
+    ( preserves-id-functor-Large-Precategory F)) ∙
   ( preserves-id-functor-Large-Precategory G)
 ```
diff --git a/src/category-theory/groupoids.lagda.md b/src/category-theory/groupoids.lagda.md
@@ -106,7 +106,7 @@ module _
 
 ## Property
 
-### The type of groupoids with respect to universe levels `l1` and `l2` is equivalent to the type of 1-types in `l1`.
+### The type of groupoids with respect to universe levels `l1` and `l2` is equivalent to the type of 1-types in `l1`
 
 #### The groupoid associated to a 1-type
 

diff --git a/src/category-theory/natural-numbers-object-precategories.lagda.md b/src/category-theory/natural-numbers-object-precategories.lagda.md
@@ -42,9 +42,11 @@ module _
     (x : obj-Precategory C)
     (q : type-hom-Precategory C t x)
     (f : type-hom-Precategory C x x) →
-    ∃! (type-hom-Precategory C n x) λ u →
-       (comp-hom-Precategory C u z ＝ q) ×
-       (comp-hom-Precategory C u s ＝ comp-hom-Precategory C f u)
+    ∃!
+      ( type-hom-Precategory C n x)
+      ( λ u →
+        ( comp-hom-Precategory C u z ＝ q) ×
+        ( comp-hom-Precategory C u s ＝ comp-hom-Precategory C f u))
 
   natural-numbers-object-Precategory : UU (l1 ⊔ l2)
   natural-numbers-object-Precategory =

diff --git a/src/category-theory/natural-transformations-precategories.lagda.md b/src/category-theory/natural-transformations-precategories.lagda.md
@@ -89,10 +89,10 @@ module _
     inv (left-unit-law-comp-hom-Precategory D _)
 
   comp-natural-transformation-Precategory :
-     (F G H : functor-Precategory C D) →
-     natural-transformation-Precategory C D G H →
-     natural-transformation-Precategory C D F G →
-     natural-transformation-Precategory C D F H
+    (F G H : functor-Precategory C D) →
+    natural-transformation-Precategory C D G H →
+    natural-transformation-Precategory C D F G →
+    natural-transformation-Precategory C D F H
   pr1 (comp-natural-transformation-Precategory F G H β α) x =
     comp-hom-Precategory D
       ( components-natural-transformation-Precategory C D G H β x)

diff --git a/src/category-theory/pullbacks-precategories.lagda.md b/src/category-theory/pullbacks-precategories.lagda.md
@@ -57,9 +57,11 @@ module _
     (p₁' : type-hom-Precategory C w' y) →
     (p₂' : type-hom-Precategory C w' z) →
     comp-hom-Precategory C f p₁' ＝ comp-hom-Precategory C g p₂' →
-    ∃! (type-hom-Precategory C w' w) λ h →
-       (comp-hom-Precategory C p₁ h ＝ p₁') ×
-       (comp-hom-Precategory C p₂ h ＝ p₂')
+    ∃!
+      ( type-hom-Precategory C w' w)
+      ( λ h →
+        ( comp-hom-Precategory C p₁ h ＝ p₁') ×
+        ( comp-hom-Precategory C p₂ h ＝ p₂'))
 
   pullback-Precategory :
     (x y z : obj-Precategory C) →

diff --git a/src/category-theory/slice-precategories.lagda.md b/src/category-theory/slice-precategories.lagda.md
@@ -333,15 +333,16 @@ module _
             ( comp-hom-Precategory C p₂ k' ＝ p₂')) →
             k ＝ k'
         σ k' (γ₁ , γ₂) =
-          ap ( pr1 ∘ pr1)
-             ( pr2
-               ( ψ (W' , comp-hom-Precategory C f p₁') (p₁' , refl) (p₂' , α'))
-               ( ( ( k') ,
-                   ( ( ap (comp-hom-Precategory C f) (inv γ₁)) ∙
-                     ( ( inv (associative-comp-hom-Precategory C f p₁ k')) ∙
-                       ( ap (λ l → comp-hom-Precategory C l k') (inv α₁))))) ,
-                 ( eq-hom-Slice-Precategory C A _ _ γ₁) ,
-                 ( eq-hom-Slice-Precategory C A _ _ γ₂)))
+          ap
+            ( pr1 ∘ pr1)
+            ( pr2
+              ( ψ (W' , comp-hom-Precategory C f p₁') (p₁' , refl) (p₂' , α'))
+              ( ( ( k') ,
+                  ( ( ap (comp-hom-Precategory C f) (inv γ₁)) ∙
+                    ( ( inv (associative-comp-hom-Precategory C f p₁ k')) ∙
+                      ( ap (λ l → comp-hom-Precategory C l k') (inv α₁))))) ,
+                ( eq-hom-Slice-Precategory C A _ _ γ₁) ,
+                ( eq-hom-Slice-Precategory C A _ _ γ₂)))
 
     equiv-is-pullback-is-product-Slice-Precategory :
       is-pullback-Precategory C A X Y f g W p₁ p₂ α ≃
@@ -393,21 +394,21 @@ module _
     ( map-pullback-product-Slice-Precategory ∘
       map-inv-pullback-product-Slice-Precategory) ~ id
   issec-map-inv-pullback-product-Slice-Precategory
-     ((Z , .(comp-hom-Precategory C f h₁)) , (h₁ , refl) , (h₂ , β₂) , q) =
+    ((Z , .(comp-hom-Precategory C f h₁)) , (h₁ , refl) , (h₂ , β₂) , q) =
     eq-pair-Σ
       ( refl)
       ( eq-pair-Σ
-         ( refl)
-         ( eq-type-subtype
-            ( λ _ →
-              is-product-Precategory-Prop
-                ( Slice-Precategory C A)
-                ( X , f)
-                ( Y , g)
-                ( _)
-                ( _)
-                ( _))
-            ( refl)))
+        ( refl)
+        ( eq-type-subtype
+          ( λ _ →
+            is-product-Precategory-Prop
+              ( Slice-Precategory C A)
+              ( X , f)
+              ( Y , g)
+              ( _)
+              ( _)
+              ( _))
+          ( refl)))
 
   isretr-map-inv-pullback-product-Slice-Precategory :
     ( map-inv-pullback-product-Slice-Precategory ∘

diff --git a/src/category-theory/yoneda-lemma-precategories.lagda.md b/src/category-theory/yoneda-lemma-precategories.lagda.md
@@ -80,7 +80,7 @@ module _
     sec yoneda-evid-Precategory
   pr1 sec-yoneda-evid-Precategory = yoneda-extension-Precategory
   pr2 sec-yoneda-evid-Precategory =
-    htpy-eq (preserves-id-functor-Precategory C (Set-Precategory _) F c)
+    htpy-eq (preserves-id-functor-Precategory C (Set-Precategory l1) F c)
 
   retr-yoneda-evid-Precategory :
     retr yoneda-evid-Precategory

diff --git a/src/commutative-algebra/commutative-rings.lagda.md b/src/commutative-algebra/commutative-rings.lagda.md
@@ -541,10 +541,11 @@ module _
 
   preserves-concat-add-list-Commutative-Ring :
     (l1 l2 : list type-Commutative-Ring) →
-    Id ( add-list-Commutative-Ring (concat-list l1 l2))
-       ( add-Commutative-Ring
-         ( add-list-Commutative-Ring l1)
-         ( add-list-Commutative-Ring l2))
+    Id
+      ( add-list-Commutative-Ring (concat-list l1 l2))
+      ( add-Commutative-Ring
+        ( add-list-Commutative-Ring l1)
+        ( add-list-Commutative-Ring l2))
   preserves-concat-add-list-Commutative-Ring =
     preserves-concat-add-list-Ring ring-Commutative-Ring
 ```
diff --git a/src/commutative-algebra/euclidean-domains.lagda.md b/src/commutative-algebra/euclidean-domains.lagda.md
@@ -631,10 +631,11 @@ module _
 
   preserves-concat-add-list-Euclidean-Domain :
     (l1 l2 : list type-Euclidean-Domain) →
-    Id ( add-list-Euclidean-Domain (concat-list l1 l2))
-       ( add-Euclidean-Domain
-         ( add-list-Euclidean-Domain l1)
-         ( add-list-Euclidean-Domain l2))
+    Id
+      ( add-list-Euclidean-Domain (concat-list l1 l2))
+      ( add-Euclidean-Domain
+        ( add-list-Euclidean-Domain l1)
+        ( add-list-Euclidean-Domain l2))
   preserves-concat-add-list-Euclidean-Domain =
     preserves-concat-add-list-Integral-Domain
       integral-domain-Euclidean-Domain
@@ -680,7 +681,7 @@ module _
           ( y))
         ( remainder-euclidean-division-Euclidean-Domain x y p)))
   equation-euclidean-division-Euclidean-Domain x y p =
-     pr1 (pr2 (pr2 is-euclidean-domain-Euclidean-Domain x y p))
+    pr1 (pr2 (pr2 is-euclidean-domain-Euclidean-Domain x y p))
 
   remainder-condition-euclidean-division-Euclidean-Domain :
     ( x y : type-Euclidean-Domain) →
@@ -691,5 +692,5 @@ module _
       ( remainder-euclidean-division-Euclidean-Domain x y p) <
     ( euclidean-valuation-Euclidean-Domain y))
   remainder-condition-euclidean-division-Euclidean-Domain x y p =
-     pr2 (pr2 (pr2 is-euclidean-domain-Euclidean-Domain x y p))
+    pr2 (pr2 (pr2 is-euclidean-domain-Euclidean-Domain x y p))
 ```
diff --git a/src/commutative-algebra/ideals-generated-by-subsets-commutative-rings.lagda.md b/src/commutative-algebra/ideals-generated-by-subsets-commutative-rings.lagda.md
@@ -62,10 +62,11 @@ module _
 
   preserves-concat-ev-formal-combination-subset-Commutative-Ring :
     (u v : formal-combination-subset-Commutative-Ring) →
-    Id ( ev-formal-combination-subset-Commutative-Ring (concat-list u v))
-       ( add-Commutative-Ring R
-         ( ev-formal-combination-subset-Commutative-Ring u)
-         ( ev-formal-combination-subset-Commutative-Ring v))
+    Id
+      ( ev-formal-combination-subset-Commutative-Ring (concat-list u v))
+      ( add-Commutative-Ring R
+        ( ev-formal-combination-subset-Commutative-Ring u)
+        ( ev-formal-combination-subset-Commutative-Ring v))
   preserves-concat-ev-formal-combination-subset-Commutative-Ring =
     preserves-concat-ev-formal-combination-subset-Ring
       ( ring-Commutative-Ring R)
@@ -81,10 +82,11 @@ module _
   preserves-mul-ev-formal-combination-subset-Commutative-Ring :
     (r : type-Commutative-Ring R)
     (u : formal-combination-subset-Commutative-Ring) →
-    Id ( ev-formal-combination-subset-Commutative-Ring
-         ( mul-formal-combination-subset-Commutative-Ring r u))
-       ( mul-Commutative-Ring R r
-         ( ev-formal-combination-subset-Commutative-Ring u))
+    Id
+      ( ev-formal-combination-subset-Commutative-Ring
+        ( mul-formal-combination-subset-Commutative-Ring r u))
+      ( mul-Commutative-Ring R r
+        ( ev-formal-combination-subset-Commutative-Ring u))
   preserves-mul-ev-formal-combination-subset-Commutative-Ring =
     preserves-mul-ev-formal-combination-subset-Ring
       ( ring-Commutative-Ring R)

diff --git a/src/commutative-algebra/integral-domains.lagda.md b/src/commutative-algebra/integral-domains.lagda.md
@@ -600,10 +600,11 @@ module _
 
   preserves-concat-add-list-Integral-Domain :
     (l1 l2 : list type-Integral-Domain) →
-    Id ( add-list-Integral-Domain (concat-list l1 l2))
-       ( add-Integral-Domain
-         ( add-list-Integral-Domain l1)
-         ( add-list-Integral-Domain l2))
+    Id
+      ( add-list-Integral-Domain (concat-list l1 l2))
+      ( add-Integral-Domain
+        ( add-list-Integral-Domain l1)
+        ( add-list-Integral-Domain l2))
   preserves-concat-add-list-Integral-Domain =
     preserves-concat-add-list-Commutative-Ring
       commutative-ring-Integral-Domain

diff --git a/src/commutative-algebra/maximal-ideals-commutative-rings.lagda.md b/src/commutative-algebra/maximal-ideals-commutative-rings.lagda.md
@@ -18,3 +18,5 @@ module commutative-algebra.maximal-ideals-commutative-rings where
 ideal `J` such that `I ⊆ J` satisfies `1 ∉ J ⇒ I ＝ J`.
 
 ## Definition
+
+This remains to be defined.
diff --git a/src/commutative-algebra/powers-of-elements-commutative-semirings.lagda.md b/src/commutative-algebra/powers-of-elements-commutative-semirings.lagda.md
@@ -68,7 +68,7 @@ module _
     power-add-Semiring (semiring-Commutative-Semiring A)
 ```
 
-### If `x` commutes with `y`, then powers distribute over the product of `x` and `y`.
+### If `x` commutes with `y`, then powers distribute over the product of `x` and `y`
 
 ```agda
 module _