Docs Site¶

UBCSailbot software team's documentation site. It is meant to be developed in Sailbot Workspace in conjunction with our other software, but doesn't have to be. There are instructions for both cases below.

Setup¶

Setup in Sailbot Workspace¶

Uncomment docs/docker-compose.docs.yml in .devcontainer/devcontainer.json
Uncomment 8000:8000 in .devcontainer/docker-compose.yml
Rebuild the Dev Container

Refer to How to work with containerized applications for more details.

Setup Standalone¶

Manually install social plugin OS dependencies
Install Python dependencies

pip install --upgrade pip pip install -Ur docs/requirements.txt
- Can do this in a Python virtual environment

Run¶

Run in Sailbot Workspace¶

After setup, the Docs site should be running on port 8000.

Refer to How to work with containerized applications for more details.

Run Standalone¶

mkdocs serve

Update Dependencies¶

This site is built using the latest versions of dependencies in docs/requirements.txt at the time of the most recent commit to the main branch. To see exactly how the site will look when deployed, ensure your local dependencies are up to date.

Update Dependencies in Sailbot Workspace¶

Rebuild the Dev Container.

Update Dependencies By Itself¶

pip install -Ur docs/requirements.txt

Maintain¶

Contribute to This Site¶

Read our Markdown Reference Page for the syntax supported by this site.

Delete Docs Versions¶

A version of the docs site is created when a PR is open, and is deleted when it is merged or closed. However, the CI that does this is very finicky, so if 2 PR's are trying to update the site at the exact same time one might fail.

This is especially annoying if this happens to be one that deletes a version, because this means that there is a version still open for a merged/closed PR. To manually clean up these PR's, run the following commands in the docs container (in Docker Desktop, the exec tab):

git config user.name <your github username>
git config user.email <your github email>
mike delete --push pr-<number>

If you get an error that your local copy of the gh-pages branch has diverged from the remote, you can delete it with git branch -D gh-pages and rerun the mike delete command above.

It will probably ask you to login to GitHub: enter your username then a GitHub access token with write permission.