Add hooks (#495)

This PR adds pre-commit hooks to fix/enforce some conventions like automatically formatting the Agda import block insider `<details>` block. - Closes #491 - Add infrastructure for #448 The hooks are written in Python for ease (also for the CI in the future) and are run using [pre-commit](https://pre-commit.com/). The idea is once you have staged all your changes, you can run (which by default also runs `make check`): ```bash make pre-commit ``` It will automatically fix any formatting issues. In principle, we could also add checks for other conventions in the future, like the ones described in CONVENTIONS.md Oh. I also changed CITATION.md as Github encourages to use the .cff extension. - [x] Update the CI to run pre-commit
UniMath · Mar 9, 2023 · c5ad5a0 · c5ad5a0
1 parent 5adb594
commit c5ad5a0
Show file tree

Hide file tree

Showing 534 changed files with 1,515 additions and 1,409 deletions.
diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml
@@ -55,7 +55,7 @@ jobs:
           restore-keys: |
             ${{ runner.os }}-check-${{ github.ref }}-${{ matrix.agda }}-
             ${{ runner.os }}-check-refs/heads/master-${{ matrix.agda }}-
-            
+
       - name: Typecheck the whole formalisation
         run: |
           cd main
@@ -102,3 +102,10 @@ jobs:
         run: |
           cd main
           make agda-html
+
+  pre-commit:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v3
+      - uses: actions/setup-python@v3
+      - uses: pre-commit/action@v3.0.0
diff --git a/.github/workflows/pages.yaml b/.github/workflows/pages.yaml
@@ -65,24 +65,24 @@ jobs:
         uses: baptiste0928/cargo-install@v1
         with:
           crate: mdbook-katex
-      
+
       - name: MDBook setup
         uses: peaceiris/actions-mdbook@v1
         with:
           mdbook-version: 'latest'
-        
+
       - name: Generate book
         run: |
           cd main
           make website
-          
+
       - name: Setup Pages
         uses: actions/configure-pages@v3
-        
+
       - name: Upload artifact
         uses: actions/upload-pages-artifact@v1
         with:
           path: main/book/html
       - name: Deploy to GitHub Pages
         id: deployment
-        uses: actions/deploy-pages@v1
+        uses: actions/deploy-pages@v1
diff --git a/.gitignore b/.gitignore
@@ -263,6 +263,7 @@ sympy-plots-for-*.tex/
 # pythontex
 *.pytxcode
 pythontex-files-*/
+__pycache__/
 
 # tcolorbox
 *.listing

diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml
@@ -0,0 +1,42 @@
+fail_fast: false
+repos:
+-   repo: https://github.com/pre-commit/pre-commit-hooks
+    rev: v3.2.0
+    hooks:
+    -   id: trailing-whitespace
+    -   id: end-of-file-fixer
+    -   id: check-yaml
+    -   id: check-added-large-files
+    -   id: check-case-conflict
+    -   id: check-merge-conflict
+
+-   repo: local
+    hooks:
+
+    - id: remove-extra-blank-lines
+      name: Remove extra blank lines
+      entry: hooks/remove-extra-blank.py
+      language: python
+      always_run: true
+      verbose: true
+      files: ^src\/.+\.lagda\.md$
+      types_or: [markdown, text]
+      args: []
+      require_serial: false
+
+    - id: fix-imports
+      name: Format Agda imports
+      entry: hooks/fix-imports.py
+      language: python
+      always_run: true
+      verbose: true
+      files: ^src\/.+\.lagda\.md$
+      types_or: [markdown, text]
+      args: []
+      require_serial: false
+
+# - repo: https://github.com/pre-commit/mirrors-prettier
+#   rev: "v3.0.0-alpha.6"
+#   hooks:
+#     - id: prettier
+#       types_or: [css, javascript, markdown,yaml]
diff --git a/CITATION.md → CITATION.cff b/CITATION.md → CITATION.cff
@@ -1,10 +1,6 @@
-## Citing the Agda-UniMath library
-
-```md
 @misc{Agda-UniMath,
   author =     {Egbert Rijke and Elisabeth Bonnevier and Jonathan Prieto-Cubides and others},
   title =     {Univalent mathematics in {Agda}},
   url =         {https://github.com/UniMath/agda-unimath/},
   howpublished = {\url{https://unimath.github.io/agda-unimath/}}
 }
-```
diff --git a/CONVENTIONS.md b/CONVENTIONS.md
@@ -29,3 +29,5 @@ Ideally, the first section of a file explains the idea, then proceeds to give th
       This will be displayed as [UniMath/agda-unimath](https://github.com/UniMath/agda-unimath).
 
 A good reference file for the expected structure of a file is [`foundation.cantor-schroder-bernstein-escardo`](https://raw.githubusercontent.com/UniMath/agda-unimath/master/src/foundation/cantor-schroder-bernstein-escardo.lagda.md).
+
+Please note that some conventions above are checks enforced by our pre-commit hooks, read more about them in [HOWTO-INSTALL.md](HOWTO-INSTALL.md#pre-commit-hooks).
diff --git a/DESIGN-PRINCIPLES.md b/DESIGN-PRINCIPLES.md
@@ -42,4 +42,4 @@ Now we can do a thought experiment. Suppose we have an unorganized library of ma
 
 To resolve those cyclic dependencies, we created two folders for the foundation of the `agda-unimath` library: the `foundation-core` folder containing the basic setup, and the `foundation` folder, containing everything that belongs to the foundation of the library. The `foundation-core` folder contains files that are paired with files of the same name in the `foundation` folder. The corresponding file in the `foundation` folder imports this file from the `foundation-core` folder publicly. Users who are working in areas outside of the foundation can just import files directly from `foundation`, and they don't have to worry that some files might be split in two.
 
-Outside of the `foundation` folder of the library, we stick to the "one-concept-per-file" design principle of our library. If you find, however, that something you were looking for was not in the place you expected it to be (this happens!) please let us know and we will consider it for improvements.
+Outside of the `foundation` folder of the library, we stick to the "one-concept-per-file" design principle of our library. If you find, however, that something you were looking for was not in the place you expected it to be (this happens!) please let us know and we will consider it for improvements.
diff --git a/HOME.md b/HOME.md
@@ -27,8 +27,8 @@ Great, you want to contribute something! The best way to start is to find us in
 
 Once you've decided what you want to contribute, the best way to proceed is to make your own fork of the library. Within your fork, make a separate branch in which you will be making your contributions. Now you're ready to start your project! When you've completed your formalization you can proceed by making a pull request. Then we will review your contributions, and merge it when it is ready for the `agda-unimath` library.
 
-{{#include CITATION.md}}
+{{#include CITATION.cff}}
 
 {{#include SUMMARY.md}}
 
-{{#include CONTRIBUTORS.md}}
+{{#include CONTRIBUTORS.md}}
diff --git a/HOWTO-INSTALL.md b/HOWTO-INSTALL.md
@@ -100,3 +100,21 @@ Menlo, Source Code Pro, Consolas, Monaco, Lucida Console, Liberation Mono, DejaV
 ### After the setup
 
 With Agda installed and emacs correctly set up, you can start using the library. There is no need to install anything further. To compile the library, which is optional, run `make check` from the main folder of the repository. This generates the file `everything.lagda.md`, which imports all the files in the library and subsequently verifies them. You don't need to compile the entire library, however. You can simply open the file you're interested in and load it with Agda. This will verify the file and any prerequisites that are not already compiled.
+
+## Pre-commit hooks
+
+The `agda-unimath` library comes with pre-commit hooks that checks
+that files follow some basic formatting rules. To use these hooks,
+you need to install the `pre-commit` tool. The easiest way to do
+this is to use the Python package manager `pip`:
+
+```shell
+python3 -pip install pre-commit
+```
+
+Once you have installed `pre-commit`, next time before you open a new PR, please stage
+all your changes and run the following command:
+
+```shell
+make pre-commit
+```
diff --git a/MAINTAINERS.md b/MAINTAINERS.md
@@ -14,5 +14,4 @@ Elisabeth is a PhD student at the University of Bergen. Her research is on homot
 
 ### [Jonathan Prieto-Cubides](https://jonaprieto.github.io)
 
-Jonathan is a researcher and a compiler engineer at Heliax designing and implementing the functional programming language Juvix. His research is on graph theory from a univalent point of view.
-
+Jonathan is a researcher and a compiler engineer at Heliax designing and implementing the functional programming language Juvix. His PhD research is on graph theory from a univalent point of view.
diff --git a/Makefile b/Makefile
@@ -12,7 +12,7 @@ AGDAHTMLFLAGS?=--html --html-highlight=code --html-dir=docs --css=Agda.css --onl
 AGDA ?=agda $(AGDAVERBOSE)
 TIME ?=time
 
-METAFILES:=CITATION.md \
+METAFILES:=CITATION.cff \
 			CODINGSTYLE.md \
 			CONTRIBUTORS.md \
 			CONVENTIONS.md \
@@ -83,4 +83,9 @@ graph:
 .PHONY : clean
 clean:
 	rm -Rf _build/
-	find docs -name '*.html' -and -name '*.md' -delete -print0
+	find docs -name '*.html' -and -name '*.md' -delete -print0
+
+.PHONY : pre-commit
+pre-commit:
+	@make check
+	@pre-commit run --all-files
diff --git a/README.md b/README.md
@@ -22,10 +22,10 @@ the library about any topic in mathematics.
 
 ```
 @misc{Agda-UniMath,
-  author =       {Egbert Rijke and 
+  author =       {Egbert Rijke and
                   Elisabeth Bonnevier and
                   Jonathan Prieto-Cubides and others},
   title =        {Univalent mathematics in {Agda}},
   url =          {https://github.com/UniMath/agda-unimath/},
   howpublished = {\url{https://unimath.github.io/agda-unimath/}}
-}
+}
diff --git a/STATEMENT-OF-INCLUSION.md b/STATEMENT-OF-INCLUSION.md
@@ -1,4 +1,4 @@
 
 # Statement of inclusion
 
-There are many reasons to contribute something to a library of formalized mathematics. Some do it just for fun, some do it for their research, some do it to learn something. Whatever your reason is, we welcome your contributions! To keep the experience of contributing something to our library enjoyable for everyone, we strive for an inclusive community of contributors. You can expect from us that we are kind and respectful in discussions, that we will be mindful of your pronouns and use [inclusive language](https://www.apa.org/about/apa/equity-diversity-inclusion/language-guidelines), and that we value your input regardless of your level of experience or status in the community. We're commited to providing a safe and welcoming environment to people of any gender identity, sexual orientation, race, colour, age, ability, ethnicity, background, or fluency in English -- here on GitHub, in online communication channels, and in person. Homotopy type theory is difficult enough without all the barriers that many of us have to face, so we hope to bring some of those down a bit.
+There are many reasons to contribute something to a library of formalized mathematics. Some do it just for fun, some do it for their research, some do it to learn something. Whatever your reason is, we welcome your contributions! To keep the experience of contributing something to our library enjoyable for everyone, we strive for an inclusive community of contributors. You can expect from us that we are kind and respectful in discussions, that we will be mindful of your pronouns and use [inclusive language](https://www.apa.org/about/apa/equity-diversity-inclusion/language-guidelines), and that we value your input regardless of your level of experience or status in the community. We're commited to providing a safe and welcoming environment to people of any gender identity, sexual orientation, race, colour, age, ability, ethnicity, background, or fluency in English -- here on GitHub, in online communication channels, and in person. Homotopy type theory is difficult enough without all the barriers that many of us have to face, so we hope to bring some of those down a bit.
diff --git a/SUMMARY.md b/SUMMARY.md
@@ -11,7 +11,7 @@
     - [Projects using Agda-Unimath](USERS.md)
   - [How-to](HOWTO-INSTALL.md)
     - [Install](HOWTO-INSTALL.md)
-    - [Cite the library](CITATION.md)
+    - [Cite the library](CITATION.cff)
   - [Guidelines](CODINGSTYLE.md)
     - [Structure your file](CONVENTIONS.md)
     - [Library coding style](CODINGSTYLE.md)

diff --git a/agda-unimath.agda-lib b/agda-unimath.agda-lib
@@ -1,3 +1,3 @@
 name: agda-unimath
 include: src
-flags: --without-K --exact-split --no-import-sorts --auto-inline
+flags: --without-K --exact-split --no-import-sorts --auto-inline
diff --git a/grant-acknowledgements.md b/grant-acknowledgements.md
@@ -1,3 +1,3 @@
 # Grant Acknowledgements
 
-- The [TydiForm project](https://tydiform.fmf.uni-lj.si) (2020-Present). Air Force Office of Scientific Research, award number FA9550-21-1-0024.
+- The [TydiForm project](https://tydiform.fmf.uni-lj.si) (2020-Present). Air Force Office of Scientific Research, award number FA9550-21-1-0024.
diff --git a/hooks/README.md b/hooks/README.md
@@ -0,0 +1,14 @@
+
+We have included Python hooks which should run on almost any platform.
+
+Install pre-commit
+
+```
+pip install pre-commit
+```
+
+Next time you commit, pre-commit will run the hooks.
+
+```
+make pre-commit
+```
diff --git a/hooks/__init__.py b/hooks/__init__.py
diff --git a/hooks/fix-imports.py b/hooks/fix-imports.py
@@ -0,0 +1,63 @@
+#!/usr/bin/env python3
+# Run this script:
+# $ python3 hooks/fix-imports.py fileName.lagda.md
+
+import sys
+import utils
+
+status = 0
+
+for fpath in utils.agdaFiles(sys.argv[1:]):
+    with open(fpath, 'r', encoding='UTF-8') as file:
+        contents = file.read()
+        start = contents.find('<details>')
+        end = contents.find('</details>')
+        if start != -1 and end != -1:
+            block = contents[start:end]
+            newBlock = filter(lambda l: l.strip() != '', block.split('\n'))
+            publicImports = []
+            nonPublicImports = []
+            otherStuff = []
+
+            for l in newBlock:
+                if l.startswith('```') or len(l.strip()) == 0:
+                    continue
+                if l.startswith('module') or l.startswith('{-# OPTIONS'):
+                    print(
+                        'Error: module decl./pragmas can not be in the details import block\n\
+                        Please put it in the first Agda block after the first header\n')
+                    sys.exit(1)
+                elif 'open import' in l:
+                    if l.endswith('public'):
+                        publicImports.append(l)
+                    else:
+                        nonPublicImports.append(l)
+                elif 'open' in l:
+                    otherStuff.append(l)
+
+            if len(otherStuff) > 0:
+
+                print(
+                    'Warning: Please review the imports block, it contains non-imports statements:\n\t' + str(fpath) )
+            imports = '\n'.join(
+                map(lambda ls: '\n'.join(sorted(ls)),
+                    filter(lambda ls: len(ls) > 0,
+                           [
+                        publicImports, nonPublicImports, otherStuff])))
+
+            importBlock = '<details><summary>Imports</summary>\n' + \
+                '\n```agda\n' +\
+                imports + \
+                '\n```\n\n'
+
+            newContent = contents[:start] + \
+                importBlock + \
+                contents[end:]
+            with open(fpath, 'w') as file:
+                file.write(newContent)
+        else:
+            agdaBlockStart = utils.find_index(contents,'```agda')
+            if len(agdaBlockStart) > 1:
+                print('Warning: No Agda import block found inside <details> block in:\n\t' + str(fpath))
+                status = 1
+sys.exit(status)
diff --git a/hooks/remove-extra-blank.py b/hooks/remove-extra-blank.py
@@ -0,0 +1,17 @@
+#!/usr/bin/env python3
+# Run this script:
+# $ python3 hooks/remove-extra-blank.py fileName.lagda.md
+
+import sys
+import utils
+import re
+
+for fpath in utils.agdaFiles(sys.argv[1:]):
+    with open(fpath, "r") as f:
+        inputText = f.read()
+    output = re.sub(r"[ \t]+$", "", inputText, flags=re.MULTILINE)
+    output = re.sub(r"\n\s*\n\s*\n", "\n\n", output)
+    with open(fpath, "w") as f:
+        f.write(output)
+
+sys.exit(0)
diff --git a/hooks/utils.py b/hooks/utils.py
@@ -0,0 +1,13 @@
+import pathlib as path
+
+def find_index(s : str, t : str) -> list[int]:
+    return [p for p, c in  enumerate(s) if c == t]
+
+def isAgdaFile(f: path.Path) -> bool:
+    return (f.match('*.lagda.md') and
+            f.exists() and
+            f.is_file())
+
+def agdaFiles(files: list[str]) -> list[path.Path]:
+    return list(filter(isAgdaFile,
+                       map(path.Path, files)))
diff --git a/src/category-theory/endomorphisms-of-objects-categories.lagda.md b/src/category-theory/endomorphisms-of-objects-categories.lagda.md
@@ -63,4 +63,3 @@ module _
   pr1 (pr2 (pr2 monoid-endo-Cat)) = left-unit-law-comp-endo-Cat
   pr2 (pr2 (pr2 monoid-endo-Cat)) = right-unit-law-comp-endo-Cat
 ```
-
diff --git a/...category-theory/homotopies-natural-transformations-large-precategories.lagda.md b/...category-theory/homotopies-natural-transformations-large-precategories.lagda.md
@@ -90,4 +90,3 @@ A homotopy from `α` to `β` can be concatenated with a homotopy from `β` to `
   associative-concat-htpy-natural-transformation-Large-Precat α β γ δ H K L X =
     assoc (H X) (K X) (L X)
 ```
-
diff --git a/src/commutative-algebra/binomial-theorem-commutative-rings.lagda.md b/src/commutative-algebra/binomial-theorem-commutative-rings.lagda.md
@@ -10,6 +10,9 @@ module commutative-algebra.binomial-theorem-commutative-rings where
 open import commutative-algebra.commutative-rings
 open import commutative-algebra.powers-of-elements-commutative-rings
 open import commutative-algebra.sums-commutative-rings
+open import elementary-number-theory.binomial-coefficients
+open import elementary-number-theory.distance-natural-numbers
+open import elementary-number-theory.natural-numbers
 open import foundation.coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.equational-reasoning
@@ -18,9 +21,6 @@ open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.unit-type
 open import foundation.universe-levels
-open import elementary-number-theory.binomial-coefficients
-open import elementary-number-theory.distance-natural-numbers
-open import elementary-number-theory.natural-numbers
 open import linear-algebra.vectors-on-commutative-rings
 open import ring-theory.binomial-theorem-rings
 open import univalent-combinatorics.standard-finite-types

diff --git a/src/commutative-algebra/binomial-theorem-commutative-semirings.lagda.md b/src/commutative-algebra/binomial-theorem-commutative-semirings.lagda.md
@@ -10,6 +10,9 @@ module commutative-algebra.binomial-theorem-commutative-semirings where
 open import commutative-algebra.commutative-semirings
 open import commutative-algebra.powers-of-elements-commutative-semirings
 open import commutative-algebra.sums-commutative-semirings
+open import elementary-number-theory.binomial-coefficients
+open import elementary-number-theory.distance-natural-numbers
+open import elementary-number-theory.natural-numbers
 open import foundation.coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.equational-reasoning
@@ -18,9 +21,6 @@ open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.unit-type
 open import foundation.universe-levels
-open import elementary-number-theory.binomial-coefficients
-open import elementary-number-theory.distance-natural-numbers
-open import elementary-number-theory.natural-numbers
 open import linear-algebra.vectors-on-commutative-semirings
 open import ring-theory.binomial-theorem-semirings
 open import univalent-combinatorics.standard-finite-types