Set up GitHub pages for documentation

We use mkdocs and mike for creating documentation:

• Support for multiple languages
• Support for multiple versions.

Create and switch to the branch docs

• If the docs branch does not exist, create using git branch docs
• Switch to the docs branch git checkout docs

Set up the Python environment

We use virtual environment for developing documentation.

• Create the virtual environment in the subfolder venv with the following command python -m venv venv
• Activate the virtual environment source venv/bin/activate
• Download the file docs/venv-requirements.txt, put it at the top-level folder of the repository.
• Install the required package using pip install -r venv-requirements.txt

Initialise the documentation

Locally

• Download the file docs/mkdocs.yml, put it at the top-level folder of the repository.
• Create the docs folder at the top-level folder of the repository.
• Download the file docs/index.en.md, put it in the docs folder.
• Run mike deploy 1.0 to build the first initial version 1.0 (you can replace 1.0 with any version number).
• Run mike set-default 1.0 to set the default version of the 1.0 (or any version that you set above).
• Run mike serve to test the first initial version by pointing your web browser to http://localhost:8000/. The result will look something like this.

Remotely

• Run mike deploy 1.0 -r <your_remote> -b gh-pages -p where <your_remote> is the GitHub remote for deploying the page.
• GitHub action will build the page and your page will be accessible after a few minutes from <organisation/user>.github.io/<repository>
• Check if the pages look OK.

Update an Exiting Version/Create a New Version of the Documentation

• Edit the mkdocs.yml files to update the structure navigation and details of the documentation site.
• Add/Update the Markdown source files accordingly (for each language)
• Test the documentation locally.
  • Run mike deploy <version> to compile the documentation. Here <version> can be an existing version or a new version.
  • (Optionally) Run mike set-default <version> to set the default version (if a new version of the documentation is created).
  • Run mike serve to test the page locally by navigating your browser to http://localhost:8000/.
• Publish the documentation remotely.
  • Run mike deploy <version> -r <remote> -b gh-pages -p.
  • Once GitHub finishes building the page, check the page at <organisation/user>.github.io/<repository> to ensure that the page is correctly displayed.