ci: add whitespace check

.github/workflows/whitespace.yml

@@ -0,0 +1,68 @@
+name: Whitespace Check
+
+on:
+  pull_request:
+  push:
+    branches:
+      - master
+
+jobs:
+  whitespace-check:
+    runs-on: ubuntu-latest
+
+    steps:
+    - name: Set commit count
+      shell: bash
+      run: echo "COMMIT_DEPTH=$((1 + ${{ github.event.pull_request.commits }}))" >> $GITHUB_ENV
+
+    - name: Checkout code
+      uses: actions/checkout@v2
+      with:
+        fetch-depth: ${{ env.COMMIT_DEPTH }}
+
+    # TODO: reintroduce this check when the library is cleaned up
+    # - name: Check for trailing whitespace
+    #   run: |
+    #     TRAILING_WHITESPACE=$(git grep -l -z -E '\s+$' | xargs -0 sed -n '/\s$/p')
+    #     if [ -n "$TRAILING_WHITESPACE" ]; then
+    #       echo "Trailing whitespace found. Please fix with:\
+    #       bash ./etc/fix_trailing_whitespace.sh"
+    #       exit 1
+    #     fi
+
+    - name: Check that every file ends correctly
+      run: |
+        while IFS= read -r file; do
+          # Check if the file is a regular file
+          if [ -f "$file" ]; then
+            if [ -n "$(tail -c 1 "$file")" ]; then
+              echo "File $file does not end with a newline. Please fix with:\
+              bash ./etc/fix_end_newlines.sh"
+              exit 1
+            fi
+          fi
+        done < <(git ls-files)
+
+# Get the repo with the commits(+1) in the series.
+# Process `git log --check` output to extract just the check errors.
+
+    - name: git log --check
+      id: check_out
+      run: |
+        log=
+        base_commit=$(git rev-parse FETCH_HEAD)
+        while IFS= read -r line; do
+          log="${log}\n${line}"
+          if [[ $line =~ ^-[^-] ]]; then
+            file_line=$(echo "$line" | cut -c 2-)
+            echo "Whitespace issue: ${file_line}"
+          fi
+        done <<< "$(git diff --check $base_commit ${{ github.sha }} | grep '^-[^-]')"
+
+        if [ -n "${log}" ]; then
+          delimiter=$(openssl rand -hex 8)
+          echo "text<<${delimiter}" >> $GITHUB_OUTPUT
+          echo -e "${log}" >> $GITHUB_OUTPUT
+          echo "${delimiter}" >> $GITHUB_OUTPUT
+          exit 2
+        fi

README.md

@@ -99,4 +99,4 @@ More information can be found in the [Wiki][22].
 [20]: https://code.visualstudio.com/
 [21]: https://github.com/coq-community/vscoq
 
-[22]: https://github.com/HoTT/HoTT/wiki
+[22]: https://github.com/HoTT/HoTT/wiki

etc/fix_end_newlines.sh

@@ -0,0 +1,14 @@
+#!/bin/bash
+
+# This command fixes the end-of-file newlines for all files in the repository.
+
+while IFS= read -r file; do
+  # Check if the file is a regular file
+  if [ -f "$file" ]; then
+    if [ -n "$(tail -c 1 "$file")" ]; then
+      echo "Adding newline to file: $file"
+      echo >> "$file"
+      git add "$file"
+    fi
+  fi
+done < <(git ls-files)

etc/fix_trailing_whitespace.sh

@@ -0,0 +1,5 @@
+#!/bin/bash
+
+# This command removes trailing whitespace from all files in the repository.
+
+git grep -l -z -E '\s+$' | xargs -0 sed -i 's/\s\+$//'

theories/Basics.v

@@ -10,3 +10,4 @@ Require Export Basics.Tactics.
 
 Require Export Basics.Nat.
 Require Export Basics.Numeral.
+

theories/Cubical.v

@@ -2,4 +2,4 @@ Require Export Cubical.DPath.
 Require Export Cubical.PathSquare.
 Require Export Cubical.DPathSquare.
 Require Export Cubical.PathCube.
-Require Export Cubical.DPathCube.
+Require Export Cubical.DPathCube.

theories/Diagrams/ParallelPair.v

@@ -32,4 +32,4 @@ Proof.
   srapply Build_Cocone.
   1: intros []; [exact (q o f) | exact q].
   intros [] [] []; [reflexivity | exact Hq].
-Defined.
+Defined.

theories/Diagrams/Span.v

@@ -33,4 +33,4 @@ Section Span.
       + exact g.
   Defined.
 
-End Span.
+End Span.

theories/Spaces/Int.v

@@ -1,4 +1,4 @@
 Require Export HoTT.Spaces.Int.Core.
 Require Export HoTT.Spaces.Int.Spec.
 Require Export HoTT.Spaces.Int.Equiv.
-Require Export HoTT.Spaces.Int.LoopExp.
+Require Export HoTT.Spaces.Int.LoopExp.

theories/Spaces/Pos.v

@@ -1,2 +1,2 @@
 Require Export HoTT.Spaces.Pos.Core.
-Require Export HoTT.Spaces.Pos.Spec.
+Require Export HoTT.Spaces.Pos.Spec.