Documentation page and GitHub action

[lukasz-antoniak]

Changes:

1. Redesign structure of gp-pages branch
2. Single GitHub action to publish new documentation after the release

[SiyaoIsHiding]

Nice!

[Copilot]

Pull request overview

This PR restructures the documentation workflow by consolidating GitHub Actions into a single publication workflow and updating the documentation site configuration. The changes eliminate staging workflows in favor of a streamlined approach that publishes versioned documentation directly to the gh-pages branch after releases.

Key changes:

• Adds versioning support using the mike plugin for MkDocs
• Replaces multiple staging/build workflows with a single publish-docs-gp-pages workflow
• Updates MkDocs theme configuration with new branding and navigation features

Reviewed changes

Copilot reviewed 4 out of 6 changed files in this pull request and generated 3 comments.

File	Description
mkdocs.yml	Configures mike plugin for versioned docs, adds logo/favicon, adjusts theme features and TOC depth
.github/workflows/update-docs-staging.yml	Removes the staging branch update workflow
.github/workflows/publish-docs-gp-pages.yml	Adds new workflow to publish versioned docs directly to gh-pages branch
.github/workflows/build-docs-gh-pages.yml	Removes the PR documentation build workflow

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

The TODO comment is unnecessary since workflow_dispatch on line 8 already enables manual triggering. The commented-out push trigger should either be uncommented if automatic triggering on push to 4.x is desired, or removed entirely along with the TODO.

Suggested change

	# TODO: Can we trigger action manually?
	# push:
	# branches:
	# - 4.x

[Copilot]

The workflow name 'publish-docs-gp-pages' uses inconsistent naming conventions. It should either use spaces like 'Publish docs to gh-pages' for display purposes, or maintain the hyphenated format but spell out 'gh-pages' instead of 'gp-pages'.

Suggested change

	name: publish-docs-gp-pages
	name: Publish docs to gh-pages

[Copilot]

This sed command is complex and fragile with nested quotes and escape sequences. Consider using a more maintainable approach such as jq for JSON manipulation or a Python script to modify versions.json, which would be more readable and less error-prone.

Suggested change

	# remove latest tag
	sed -i 's/\"latest\"//g' versions.json
	# remove already present line if exists
	sed -i '/'"$release_version"'/d' versions.json
	# insert new version at the beginning
	sed -i '2s/^/ { "version": "'"$release_version"'", "title": "'"$release_version"'", "aliases": ["latest"] },\'$'\n/g' versions.json
	# update versions.json: remove any existing "latest" aliases and existing entry for this
	# release_version, then insert the new version as the first entry with aliases ["latest"].
	python - << PY
	import json
	from pathlib import Path
	versions_path = Path("versions.json")
	data = json.loads(versions_path.read_text())
	release_version = "${release_version}"
	# Remove "latest" from aliases in all existing entries
	for entry in data:
	aliases = entry.get("aliases")
	if isinstance(aliases, list):
	entry["aliases"] = [alias for alias in aliases if alias != "latest"]
	# Remove any existing entry for this release_version
	data = [entry for entry in data if entry.get("version") != release_version]
	# Insert new version at the beginning
	data.insert(0, {
	"version": release_version,
	"title": release_version,
	"aliases": ["latest"],
	})
	versions_path.write_text(json.dumps(data, indent=2) + "\n")
	PY