Add metrics documentation generation step in CircleCI & RTD configs

Also rename generated metrics documentation directory `_gen` from `gen`

.circleci/config.yml

@@ -64,7 +64,7 @@ jobs:
           name: Build docs to store
           command: |
             cd docs
-            make html
+            make metrics html
       # Tell Circle to store the documentation output in a folder that we can access later
       - store_artifacts:
           path: docs/build/html/

.gitignore

@@ -27,4 +27,4 @@ htmlcov
 .vscode/
 .pytest_cache
 pip-wheel-metadata
-docs/source/monitoring/gen/
+docs/source/monitoring/_gen/

docs/generate-metrics.py

@@ -30,7 +30,7 @@ class Generator:
         return table_rows
 
     def prometheus_metrics(self):
-        generated_directory = f"{HERE}/source/monitoring"
+        generated_directory = f"{HERE}/source/monitoring/_gen"
         if not os.path.exists(generated_directory):
             os.makedirs(generated_directory)
 

docs/source/conf.py

@@ -220,7 +220,7 @@ if on_rtd:
     # build rest-api, since RTD doesn't run make
     from subprocess import check_call as sh
 
-    sh(['make', 'rest-api'], cwd=docs)
+    sh(['make', 'metrics', 'rest-api'], cwd=docs)
 
 # -- Spell checking -------------------------------------------------------
 

docs/source/monitoring/index.rst

@@ -8,4 +8,4 @@ JupyterHub expose the ``/metrics`` endpoint that returns text describing its cur
 .. toctree::
    :maxdepth: 2
 
-   gen/metrics
+   _gen/metrics