Merge pull request #9355 from BinderDavid/improve-docs-ci

Do not run CI for documentation changes

.github/workflows/lint.yml

@@ -15,4 +15,4 @@ jobs:
     - uses: haskell-actions/hlint-run@v2
       with:
         path: "."
-        fail-on: suggestion
+        fail-on: suggestion

.github/workflows/validate.skip.yml

@@ -0,0 +1,33 @@
+name: Validate Skip
+
+# 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 without providing any benefit.
+# We therefore use path-filtering in the workflow triggers for the validate jobs, namely
+# "paths_ignore: doc/**". But the "Validate post job" is a required job, therefore a PR cannot
+# be merged unless the "Validate post job" completes succesfully, which it doesn't do if we 
+# filter it out.
+#
+# The solution: We use a second job with the same name which always returns the exit code 0.
+# The logic implemented for "required" workflows accepts if 1) at least one job with that name
+# runs through, AND 2) If multiple jobs of that name exist, then all jobs of that name have to
+# finish successfully.
+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 0

.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.skip.yml" for a description of the problem and the solution provided in that file.
 on:
   push:
+    paths-ignore: 'doc/**'
     branches:
       - master
   pull_request:
+    paths-ignore: 'doc/**'
   release:
     types:
       - created