Platform documentation

Repository for the documentation of the platform. Each branch corresponds to a different version of the platform, so if you need to update the documentation of a specific version, do not create a separate branch, instead, commit directly to the branch corresponding to the version you're updating.

The documentation features multiple portals, aimed at different audiences (user, admin, ...).

To create a new page (the following example refers to the user portal, but the process for others is equivalent):

• Write a .md file within user/docs
• Add it to the nav element in /user/mkdocs.yml

Commit your changes and the website will automatically be updated within a couple minutes.

Test locally

If you wish to test your changes locally before pushing, the quickest way to do so is:

Install MkDocs and mkdocs-material:

pip install mkdocs
pip install mkdocs-material

Remove custom_dir: ../custom/ from base.yml (this file concerns CSS, so things like colours will be different). If not removed, you may receive an error when performing the next step. Make sure not to include this change in your later commit.

Run the following from the /user (or equivalent for whichever portal you're testing) directory:

mkdocs serve

You can then view the docs at localhost:8000. As the docs on the website are generated by combining multiple portals, you will be missing any portal other than the one you are testing.

Versioned documentation

Different versions of the documentation may be available at once.

The current version of the documentation reflects the most up-to-date state of the main branch, and is updated when new commits to main are made. It can be found under /docs.

Publishing a new branch will generate another documentation portal, named after the branch, under /docs/<branch_name>. Further pushes to this branch will update the corresponding portal.

Adding a portal

The documentation can feature multiple portals, such as User and Admin, aimed at different purposes, which can be accessed from a drop-down menu in the toolbar.

If you wish to add another portal, follow the steps below. This example will configure a new portal, called Example, available under the /example sub-path.

At root level, create a new directory named example. Inside, create a mkdocs.yml file, and a directory called docs, with an index.md file within, as follows:

example/
├── mkdocs.yml
└── docs/
    └── index.md

The contents of mkdocs.yml should be:

INHERIT: ../base.yml
site_url: http://docs/example

extra:
  portal_name: Example

extra_css:
  - !ENV [OTHERS_STYLESHEETS_PORTAL_SELECTION, "../stylesheets/portal_selection.css"]
  - !ENV [OTHERS_STYLESHEETS_COLORS, "../stylesheets/colors.css"]

nav:
  - "index.md"

Of course, you can add more .md files to expand your documentation.

Next, you must edit the base.yml file (found at the root), to expand the extra.portals list with your new portal. Note that name must be the same as portal_name, and path must be the same as the directory you created (prefixed with /).

extra:
  # [...]
  portals:
    - name: User
      path: ""
    - name: Admin
      path: "/admin"
    - name: Example    # Same as portal_name
      path: "/example" # Same as directory's name, prefixed with /

Finally, you must update the .github/workflows/update-docs.yaml file, which defines the GitHub workflow, where some commands must be added.

It may seem complicated, but all you have to do is duplicate the equivalent admin commands and adapt them for your new portal. The example below highlights these sections.

# First here...
git checkout $v
cd user && mkdocs build && cd ..
cd admin && mkdocs build && cd ..
cd example && mkdocs build && cd .. # new line
mkdir -p ./site
[ ! -d user/site ] || mv user/site site/$v
[ ! -d admin/site ] || mv admin/site site/$v/admin
[ ! -d example/site ] || mv example/site site/$v/example # new line

# and then a few lines later...
git checkout main
cd user && mkdocs build && cd ..
cd admin && mkdocs build && cd ..
cd example && mkdocs build && cd .. # new line
[ ! -d user/site ] || mv user/site ./site
[ ! -d admin/site ] || mv admin/site site/admin
[ ! -d example/site ] || mv example/site site/example # new line

Once you commit these changes, your new portal will be available.