From 31aed2a8f1d9a20e3e58fef764fef425e2609116 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Thu, 16 Jan 2025 09:35:03 -0500
Subject: [PATCH] add metrics to the book

---
 .github/workflows/book.yml   | 18 ++++++++++++++++++
 doc/src/SUMMARY.md           |  2 ++
 doc/src/metrics.md           |  3 +++
 doc/src/metrics/kani/kani.md | 10 ++++++++++
 4 files changed, 33 insertions(+)
 create mode 100644 doc/src/metrics.md
 create mode 100644 doc/src/metrics/kani/kani.md

diff --git a/.github/workflows/book.yml b/.github/workflows/book.yml
index 200068be74745..48f5a414b90bd 100644
--- a/.github/workflows/book.yml
+++ b/.github/workflows/book.yml
@@ -10,6 +10,7 @@ on:
     paths:
       - 'doc/**'
       - '.github/workflows/book.yml'
+      - 'scripts/kani-std-analysis/**'
 
 jobs:
   build:
@@ -18,6 +19,23 @@ jobs:
       - name: Checkout
         uses: actions/checkout@v4
 
+      - name: Set up Python
+        uses: actions/setup-python@v4
+        with:
+          python-version: '3.x'
+
+      - name: Install Python dependencies
+        run: |
+          python -m pip install --upgrade pip
+          pip install -r scripts/kani-std-analysis/requirements.txt
+
+      - name: Generate Metrics Graphs
+        run: |
+          cd scripts/kani-std-analysis/
+          python kani_std_analysis.py --plot-only
+          cd ../..
+          mv scripts/kani-std-analysis/*.png doc/src/metrics/kani/
+
       - name: Install mdbook
         run: |
           cargo install mdbook --version "^0.4" --locked
diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md
index e6b2a9c78e598..6b5a60cf43bec 100644
--- a/doc/src/SUMMARY.md
+++ b/doc/src/SUMMARY.md
@@ -9,6 +9,8 @@
 - [Verification Tools](./tools.md)
   - [Kani](./tools/kani.md)
 
+- [Metrics](./metrics.md)
+  - [Kani](./metrics/kani/kani.md)
 
 ---
 
diff --git a/doc/src/metrics.md b/doc/src/metrics.md
new file mode 100644
index 0000000000000..a3b5220635eda
--- /dev/null
+++ b/doc/src/metrics.md
@@ -0,0 +1,3 @@
+# Metrics
+
+Each approved tool can (optionally) publish metrics here about how their tool has been applied to the effort thus far.
\ No newline at end of file
diff --git a/doc/src/metrics/kani/kani.md b/doc/src/metrics/kani/kani.md
new file mode 100644
index 0000000000000..505b817170c86
--- /dev/null
+++ b/doc/src/metrics/kani/kani.md
@@ -0,0 +1,10 @@
+# Kani Metrics
+
+Note that these metrics are for x86-64 architectures.
+
+## `core`
+![Unsafe Metrics](core_unsafe_metrics.png)
+
+![Safe Abstractions Metrics](core_safe_abstractions_metrics.png)
+
+![Safe Metrics](core_safe_metrics.png)