From ab7900524bb574286b3376f042ebd2a68c86ccb8 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Fri, 6 Dec 2024 12:15:34 -0500
Subject: [PATCH 1/2] use markdown format; move to separate job

---
 .github/workflows/kani.yml | 25 +++++++++++++++++++------
 scripts/run-kani.sh        |  2 +-
 2 files changed, 20 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index b3c8aa3..0633ab6 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -65,17 +65,30 @@ jobs:
       - name: Test Kani script (In Repo Directory)
         working-directory: ${{github.workspace}}/head
         run: scripts/run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr --output-format=terse
-      
-      # Step 4: Run list on the std library and add output to job summary
+   
+  run-kani-list:
+    name: Kani List
+    runs-on: ubuntu-latest
+    steps:
+      # Step 1: Check out the repository
+      - name: Checkout Repository
+        uses: actions/checkout@v4
+        with:
+          path: head
+          submodules: true
+
+      # Step 2: Run list on the std library
       - name: Run Kani List
         run: head/scripts/run-kani.sh --run list --path ${{github.workspace}}/head
-
+      
+      # Step 3: Add output to job summary
       - name: Add Kani List output to job summary
         uses: actions/github-script@v6
         with:
           script: |
             const fs = require('fs');
-            const kaniOutput = fs.readFileSync('${{github.workspace}}/head/kani_list.txt', 'utf8');
+            const kaniOutput = fs.readFileSync('${{github.workspace}}/head/kani-list.md', 'utf8');
             await core.summary
-              .addRaw(kaniOutput)
-              .write();
\ No newline at end of file
+              .addHeading('Kani List Output', 2)
+              .addRaw(kaniOutput, false)
+              .write();
diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
index a576717..ceacda8 100755
--- a/scripts/run-kani.sh
+++ b/scripts/run-kani.sh
@@ -221,7 +221,7 @@ main() {
             --cbmc-args --object-bits 12
     elif [[ "$run_command" == "list" ]]; then
         echo "Running Kani list command..."
-        "$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib ./library --std > $path/kani_list.txt
+        "$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib ./library --std --format markdown
     fi
 }
 

From 5f06c09c3e4554cb9e75ef2f1f5b6ce71083e746 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Fri, 6 Dec 2024 14:46:31 -0500
Subject: [PATCH 2/2] delete test kani job

---
 .github/workflows/kani.yml | 28 ----------------------------
 1 file changed, 28 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 0633ab6..7484c75 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -37,34 +37,6 @@ jobs:
       # Step 2: Run Kani on the std library (default configuration)
       - name: Run Kani Verification
         run: head/scripts/run-kani.sh --path ${{github.workspace}}/head
-
-  test-kani-script:
-    name: Test Kani script
-    runs-on: ${{ matrix.os }}
-    strategy:
-      matrix:
-        os: [ubuntu-latest, macos-latest]
-        include:
-          - os: ubuntu-latest
-            base: ubuntu
-          - os: macos-latest
-            base: macos
-    steps:
-      # Step 1: Check out the repository
-      - name: Checkout Repository
-        uses: actions/checkout@v4
-        with:
-          path: head
-          submodules: true
-
-      # Step 2: Test Kani verification script with specific arguments
-      - name: Test Kani script (Custom Args)
-        run: head/scripts/run-kani.sh -p ${{github.workspace}}/head --kani-args --harness ptr --output-format=terse
-
-      # Step 3: Test Kani verification script in the repository directory
-      - name: Test Kani script (In Repo Directory)
-        working-directory: ${{github.workspace}}/head
-        run: scripts/run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr --output-format=terse
    
   run-kani-list:
     name: Kani List