Comment on pull request with performance data

Author: ttuegel

.github/workflows/performance.yml

@@ -29,9 +29,13 @@ jobs:
           skipPush: true
 
       - name: Build
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
         run: |
           ./scripts/test-statistics.sh ./. test/regression-evm >pull-request.json
           git fetch origin
           git worktree add kore-master master
           ./scripts/test-statistics.sh ./kore-master test/regression-evm >master.json
-          ./scripts/join-statistics.sh master.json pull-request.json
+          ./scripts/join-statistics.sh master.json pull-request.json \
+            | ./scripts/format-statistics.sh >comment.md
+          gh pr comment ${{ github.event.pull_request.number }} -F comment.md

scripts/format-statistics.sh

@@ -0,0 +1,4 @@
+#!/usr/bin/env nix-shell
+#!nix-shell ../test.nix -i bash
+
+mlr --ijson --omd cut -o -f name,allocated_bytes,diff_allocated_bytes,max_live_bytes,diff_max_live_bytes