Merge branch 'master' of https://github.com/input-output-hk/plutus in…

…to effectfully/builtins/make-all-builtins-strict

.github/workflows/manual-benchmark.yml

@@ -43,13 +43,15 @@ jobs:
         uses: actions/github-script@main
         with:
           script: |
-            const regex = /^\/benchmark\s*(.*?)\s*$/;
+            const regex = /^\/benchmark\s*([^\s]*)\s*(cap=([0-9]+))?\s*$/;
             const comment = context.payload.comment.body;
             const match = comment.match(regex)
-            if (match !== null && match.length == 2)
+            if (match !== null && match.length == 4 && match[1] !== '') {
               core.setOutput('benchmark', match[1]);
-            else
-              core.setFailed(`Unable to extract benchmark name from ${comment}`);
+              core.setOutput('capability_num', match[3] || "");
+            } else {
+              core.setFailed(`Unable to extract benchmark name from comment '${comment}'`);
+            }
 
       - name: Extract Branch Name
         id: extract-branch
@@ -116,6 +118,7 @@ jobs:
           nix develop --no-warn-dirty --accept-flake-config --command bash ./scripts/ci-plutus-benchmark.sh 
         env:
           BENCHMARK_NAME: ${{ steps.extract-benchmark.outputs.benchmark }}
+          CAPABILITY_NUM: ${{ steps.extract-benchmark.outputs.capability_num }}
           PR_NUMBER: ${{ github.event.issue.number }}
           PR_BRANCH: ${{ steps.extract-branch.outputs.head_ref }}
 

plutus-benchmark/bench-compare-markdown

@@ -50,6 +50,7 @@ paste -d " " "$TMP1" "$TMP2" |
           else return (sprintf ("%.1f %s", t, ustr[unit]))
       }
       function percentage_change (t1, t2,    d, sign) {
+          if (t1==0) return ("  -  ")  # Avoid division by zero, just in case
           d = (t2-t1)/t1 * 100
           sign = (d<0) ? "" : ((d==0) ? " " : "+")     # We get the "-" anyway if d<0
           return (sprintf ("%s%.1f%%", sign, d))