Add Lean PR comment benchmark

Author: samuelburnham

.envrc

@@ -0,0 +1 @@
+use flake

.github/workflows/bench.yml

@@ -0,0 +1,104 @@
+# Creates a PR benchmark comment with a comparison to main
+name: Benchmark pull requests
+
+on:
+  issue_comment:
+    types: [created]
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
+  cancel-in-progress: true
+
+jobs:
+  setup:
+    name: Comparative PR benchmark comment
+    if:
+      github.event.issue.pull_request
+      && github.event.issue.state == 'open'
+      && (contains(github.event.comment.body, '!benchmark'))
+      && (github.event.comment.author_association == 'MEMBER' || github.event.comment.author_association == 'OWNER')
+    runs-on: ubuntu-latest
+    outputs:
+      benches: ${{ steps.bench-params.outputs.benches }}
+      env-vars: ${{ steps.bench-params.outputs.env-vars }}
+    steps:
+      - uses: actions/checkout@v5
+      - name: Parse PR comment body
+        id: bench-params
+        run: |
+          # Parse `issue_comment` body
+          printf '${{ github.event.comment.body }}' > comment.txt
+          BENCH_COMMAND=$(head -n 1 comment.txt)
+          echo "$BENCH_COMMAND"
+
+          BENCHES=$(echo $BENCH_COMMAND | awk -F'!benchmark ' '{ print $2 }')
+          echo "BENCHES\n$BENCHES"
+          JSON=$(echo $BENCHES | jq -R -c 'split(" ")')
+
+          #echo "benches<<EOF" >> $GITHUB_OUTPUT
+          #echo "$JSON" | tee -a $GITHUB_OUTPUT
+          #echo "EOF" >> $GITHUB_OUTPUT
+          echo "JSON\n$JSON"
+
+          echo "benches=$JSON" | tee -a $GITHUB_OUTPUT
+
+          # Can't persist env vars between jobs, so we pass them as an output and set them in the next job
+          echo "env-vars=$(tail -n +2 comment.txt)" | tee -a $GITHUB_OUTPUT
+
+  benchmark:
+    needs: [ setup ]
+    runs-on: warp-ubuntu-latest-x64-16x
+    strategy:
+      matrix:
+        # Runs a job for each benchmark specified in the `issue_comment` input
+        bench: ${{ fromJSON(needs.setup.outputs.benches) }}
+    steps:
+      - name: Set env vars
+        run: |
+          # Trims newlines that may arise from `$GITHUB_OUTPUT`
+          for var in ${{ inputs.default-env }}
+          do
+            echo "$(echo $var | tr -d '\n')" | tee -a $GITHUB_ENV
+          done
+          # Overrides default env vars with those specified in the `issue_comment` input if identically named
+          for var in ${{ needs.setup.outputs.env-vars }}
+          do
+            echo "$(echo $var | tr -d '\n')" | tee -a $GITHUB_ENV
+          done
+      - uses: actions/checkout@v5
+      # Get base branch of the PR
+      #- uses: xt0rted/pull-request-comment-branch@v2
+      #  id: comment-branch
+      - name: Checkout PR branch
+        run: gh pr checkout $PR_NUMBER
+        env:
+          GH_TOKEN: ${{ github.token }}
+          PR_NUMBER: ${{ github.event.issue.number }}
+      - uses: leanprover/lean-action@v1
+        with:
+          test: false
+      - name: Run bench
+        run: |
+          lake exe ${{ matrix.bench }} | tee out.txt 2>&1
+      - name: Comment on successful run
+        if: success()
+        uses: peter-evans/create-or-update-comment@v4
+        with:
+          issue-number: ${{ github.event.issue.number }}
+          body: |
+            `!${{ needs.setup.outputs.command }}` action succeeded! :rocket:
+
+            Bench output:
+            $(cat out.txt)
+
+            https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}
+
+      - name: Comment on failing run
+        if: failure()
+        uses: peter-evans/create-or-update-comment@v4
+        with:
+          issue-number: ${{ github.event.issue.number }}
+          body: |
+            `!${{ needs.setup.outputs.command }}` action failed :x:
+
+            https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}

.github/workflows/lean_action_ci.yml

@@ -0,0 +1,14 @@
+name: Lean Action CI
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+      - uses: leanprover/lean-action@v1

.gitignore

@@ -1,2 +1,9 @@
-target/
-Cargo.lock
+# Lean
+/.lake
+
+# Rust
+/target
+
+# Nix
+result*
+.direnv/

Benchmarks/Main.lean

@@ -0,0 +1,2 @@
+def main (_args: List String) : IO Unit := do
+  IO.println "Hello bench"

Cargo.lock

@@ -0,0 +1,13 @@
+import Template
+import Ix.Benchmark.Bench
+
+def add (input: Nat): IO Nat := do
+  pure $ input + 1
+
+def addBench := bgroup "Add" [
+ benchIO "add 1" add 1
+] { report := true }
+
+def main : IO Unit := do
+  --IO.println "hello"
+  let _result ← addBench

Main.lean

@@ -0,0 +1 @@
+# template

README.md

@@ -0,0 +1,3 @@
+-- This module serves as the root of the `Template` library.
+-- Import modules here that should be built as part of the library.
+import Template.Basic

Template.lean

@@ -0,0 +1 @@
+def hello := "world"