Do not run CI for documentation changes

The github workflows are not run if the
changes are completely contained within
the doc/ subdirectory. The only exception
is the users-guide.yml github action.

.github/workflows/format.yml

@@ -2,6 +2,7 @@ name: Formatting
 
 on:
   pull_request:
+    paths-ignore: 'doc/**'
   push:
     branches: ["master"]
 

.github/workflows/lint.yml

@@ -2,7 +2,9 @@ name: Linting
 
 on:
   pull_request:
+    paths-ignore: 'doc/**'
   push:
+    paths-ignore: 'doc/**'
 
 jobs:
   hlint:
@@ -15,4 +17,4 @@ jobs:
     - uses: haskell/actions/hlint-run@v2
       with:
         path: "."
-        fail-on: suggestion
+        fail-on: suggestion

.github/workflows/validate.patch.yml

@@ -0,0 +1,26 @@
+name: Validate Patch
+
+# This Workflow is special and contains a workaround for a known limitation of GitHub CI.
+#
+# The problem: We don't want to run the "validate" jobs on PRs which contain only changes
+# to the docs, since these jobs take a long time to complete. We therefore use path-filtering
+# in the workflow triggers for the validate jobs, namely "paths_ignore: doc/**".
+# The problem is that the 
+on:
+  push:
+    paths: 'doc/**'
+    branches:
+      - master
+  pull_request:
+    paths: 'doc/**'
+  release:
+    types:
+      - created
+
+jobs:
+  validate-post-job:
+    if: always()
+    name: Validate post job
+    runs-on: ubuntu-latest
+    steps:
+      - run: exit 1

.github/workflows/validate.yml

@@ -11,11 +11,16 @@ concurrency:
   group: ${{ github.ref }}-${{ github.workflow }}
   cancel-in-progress: true
 
+# Note: This workflow file contains the required job "Validate post job". We are using path filtering
+# here to ignore PRs which only change documentation. This can cause a problem, see the workflow file
+# "validate.patch.yml" for a description of the problem and the patch provided in that file.
 on:
   push:
+    paths-ignore: 'doc/**'
     branches:
       - master
   pull_request:
+    paths-ignore: 'doc/**'
   release:
     types:
       - created