GitHub: Add a GitHub Action to publish docs

Add a GitHub Action to publish docs automatically, whenever someone
pushes against the "main" branch.

Note we have chosen to implement the actual business logic of publishing docs
as part of the Makefile, rather than as part of the GitHub Action
directly. This means we only use the GitHub action to *automate* the
invocation of pre-existing business logic.

This allows us to run the exact same logic both locally and within a
GitHub Action. See here for interesting context:

https://news.ycombinator.com/item?id=33751533

Also note we fetch tags explicitly, because the "checkout" action seems
to have broken semantics. See here for a ton of context:

actions/checkout#1471

Also note we set git-specific environment variables for author and
committer username/email explicitly to make the new commits in the
"gh-pages" branch appear as coming from the GitHub Actions bot.
Otherwise git was complaining that it couldn't determine the identity of
the author and/or committer.
See here for details:

https://github.com/actions/checkout#push-a-commit-using-the-built-in-token
https://github.com/orgs/community/discussions/26560

Finally, ensure the docs-clean target actually depends on having created
the managed Python virtualenv, because it needs Sphinx-provided
commands.

Signed-off-by: Vangelis Koukis <[email protected]>

.github/workflows/docs-publish.yaml

@@ -0,0 +1,27 @@
+name: docs-publish
+
+on:
+  push:
+    branches:
+    - main
+  pull_request:
+    branches:
+    - main
+
+jobs:
+  docs-publish:
+    runs-on: ubuntu-latest
+    steps:
+    - name: checkout repo
+      uses: actions/checkout@main
+      with:
+        fetch-tags: true 
+    - name: fetch all tags explicitly
+      run: git fetch --depth=1 --tags
+    - name: publish docs
+      run: make docs-publish
+      env:
+        GIT_AUTHOR_NAME: "github-actions[bot]"
+        GIT_AUTHOR_EMAIL: "41898282+github-actions[bot]@users.noreply.github.com"
+        GIT_COMMITTER_NAME: "github-actions[bot]"
+        GIT_COMMITTER_EMAIL: "41898282+github-actions[bot]@users.noreply.github.com"

Makefile

@@ -31,8 +31,8 @@ docs: docs-build
 docs-build: venv
 	$(MAKE_VENV) -C docs html
 
-docs-clean:
-	make -C docs clean
+docs-clean: venv
+	$(MAKE_VENV) -C docs clean
 
 # Publish docs: Push to a specific branch at the same origin.
 # We have configured GitHub Pages to serve this branch,
@@ -76,5 +76,6 @@ docs-publish: docs-clean docs-build
 clean: docs-clean
 
 .PHONY: mrproper
-mrproper: clean clean-venv
+mrproper: clean-venv
 	-$(RMDIR) "$(BUILDDIR)"
+	-$(RMDIR) "$(PAGESDIR)"