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 disable shallow fetches to fetch all tags and the full
history, so we can calculate a version based on annotated tags.

Also note we check out the repository *twice*, a second time under
_pages/, so the checkout action has a chance to persist the
Action-specific credentials under _pages/. We do it so we have the
credentials we need to push to the "gh-pages" branch later on.

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,31 @@
+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
+        fetch-depth: 0
+    - name: checkout repo under _pages/
+      uses: actions/checkout@main
+      with:
+        ref: gh-pages
+        path: _pages
+    - 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)"