Postprocess test suite metrics into GitHub summary

.github/workflows/ci.yml

@@ -182,6 +182,13 @@ jobs:
       - name: show the current environment
         run: src/ci/scripts/dump-environment.sh
 
+      # Pre-build citool before the following step uninstalls rustup
+      # Build is into the build directory, to avoid modifying sources
+      - name: build citool
+        run: |
+          cd src/ci/citool
+          CARGO_TARGET_DIR=../../../build/citool cargo build
+
       - name: run the build
         # Redirect stderr to stdout to avoid reordering the two streams in the GHA logs.
         run: src/ci/scripts/run-build-from-ci.sh 2>&1
@@ -218,6 +225,16 @@ jobs:
         # erroring about invalid credentials instead.
         if: github.event_name == 'push' || env.DEPLOY == '1' || env.DEPLOY_ALT == '1'
 
+      - name: postprocess metrics into the summary
+        run: |
+          if [ -f build/metrics.json ]; then
+            ./build/citool/debug/citool postprocess-metrics build/metrics.json ${GITHUB_STEP_SUMMARY}
+          elif [ -f obj/build/metrics.json ]; then
+            ./build/citool/debug/citool postprocess-metrics obj/build/metrics.json ${GITHUB_STEP_SUMMARY}
+          else
+            echo "No metrics.json found"
+          fi
+
       - name: upload job metrics to DataDog
         if: needs.calculate_matrix.outputs.run_type != 'pr'
         env: