Agda Translation Efficiency improvements #862
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # This workflows checks for comments in PRs. If the comment has this format: | |
| # /benchmark NAME | |
| # Then this action will run the benchmark with the given NAME, first against | |
| # the current branch and then comparing the results against the master branch. | |
| name: "🚀 Manual Benchmark" | |
| on: | |
| issue_comment: | |
| types: [created] | |
| jobs: | |
| run: | |
| name: Run | |
| runs-on: [self-hosted, plutus-benchmark] | |
| permissions: | |
| pull-requests: write | |
| if: | | |
| startsWith(github.event.comment.body, '/benchmark') && | |
| github.event.issue.pull_request | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@main | |
| with: | |
| # We need at least one commit before master to compare against | |
| fetch-depth: 5 | |
| - name: React With Rocket | |
| uses: actions/github-script@main | |
| with: | |
| script: | | |
| github.rest.reactions.createForIssueComment({ | |
| owner: context.issue.owner, | |
| repo: context.issue.repo, | |
| comment_id: context.payload.comment.id, | |
| content: "rocket" | |
| }); | |
| - name: Extract Benchmark Name | |
| id: extract-benchmark | |
| uses: actions/github-script@main | |
| with: | |
| script: | | |
| 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 == 4 && match[1] !== '') { | |
| core.setOutput('benchmark', match[1]); | |
| core.setOutput('capability_num', match[3] || ""); | |
| } else { | |
| core.setFailed(`Unable to extract benchmark name from comment '${comment}'`); | |
| } | |
| - name: Extract Branch Name | |
| id: extract-branch | |
| uses: actions/github-script@main | |
| with: | |
| script: | | |
| async function isPullRequest() { | |
| const result = await github.rest.issues.get({ | |
| owner: context.issue.owner, | |
| repo: context.issue.repo, | |
| issue_number: context.issue.number | |
| }); | |
| return !!result.data.pull_request; | |
| } | |
| async function getCommentHeadRef() { | |
| const query = ` | |
| query pullRequestDetails($repo:String!, $owner:String!, $number:Int!) { | |
| repository(name: $repo, owner: $owner) { | |
| pullRequest(number: $number) { | |
| headRef { | |
| name | |
| } | |
| } | |
| } | |
| }`; | |
| const result = await github.graphql(query, { | |
| owner: context.issue.owner, | |
| repo: context.issue.repo, | |
| number: context.issue.number | |
| }); | |
| return result.repository.pullRequest.headRef.name; | |
| } | |
| try { | |
| if (!await isPullRequest()) { | |
| core.setFailed("Comment is not on a pull request"); | |
| } else { | |
| core.setOutput("head_ref", await getCommentHeadRef()); | |
| } | |
| } catch (error) { | |
| core.setFailed(`Error: ${error}`); | |
| } | |
| - name: Publish GH Action Link | |
| uses: actions/github-script@main | |
| with: | |
| script: | | |
| async function getJobUrl() { | |
| return `https://github.com/${context.issue.owner}/${context.issue.repo}/actions/runs/${context.runId}`; | |
| } | |
| await github.rest.issues.createComment({ | |
| owner: context.issue.owner, | |
| repo: context.issue.repo, | |
| issue_number: context.issue.number, | |
| body: `Click [here](${await getJobUrl()}) to check the status of your benchmark.` | |
| }); | |
| - name: Run Benchmark | |
| run: | | |
| 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 }} | |
| - name: Publish Results | |
| uses: actions/github-script@main | |
| with: | |
| script: | | |
| const fs = require("fs"); | |
| await github.rest.issues.createComment({ | |
| owner: context.issue.owner, | |
| repo: context.issue.repo, | |
| issue_number: context.issue.number, | |
| // bench-compare-result.log is generated by ci-plutus-benchmark.sh | |
| body: fs.readFileSync("bench-compare-result.log", "utf-8").toString() | |
| }); |