Types specifying the simplify-implication RPC endpoint
#903
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
| --- | |
| name: Performance Profiling | |
| on: | |
| # Trigger when commenting on an issue or PR, or editing a comment | |
| # Issue/PR MUST already be labeled properly | |
| issue_comment: | |
| types: [created, edited] | |
| jobs: | |
| Prepare: | |
| if: | | |
| contains(github.event.issue.labels.*.name, 'performance') && | |
| ( contains(github.event.comment.body, '.tar.gz)') ) | |
| # Comment must contain something that looks like a link to a | |
| # *.tar.gz in markdown, therefore matching the suffix with ')' | |
| runs-on: [Linux, flyweight] | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| steps: | |
| - name: Check User Org Association | |
| run: | | |
| set -euo pipefail | |
| echo $(pwd) | |
| echo "Testing User Org Relationship: $GITHUB_ACTOR" | |
| gh auth status | |
| if ! gh api -H "Accept: application/vnd.github+json" /orgs/runtimeverification/members/$GITHUB_ACTOR; then | |
| exit 1 | |
| fi | |
| - name: Check File Downloadable | |
| # Note that the reg.ex will only match a URL within parentheses | |
| # (perl reg.ex context) while the guard above uses a simple substring | |
| run: | | |
| set -euo pipefail | |
| DOWNLOAD_URL=$(jq '.comment.body' ${GITHUB_EVENT_PATH} | (grep -oP '(?<=\()https://github\.com/${{ github.repository }}/files/[A-Za-z0-9._~!$&*+,;=@%/-]*\.tar\.gz(?=\))' || echo "No-valid-URL-found") | head -1 ) | |
| echo "Testing whether '${DOWNLOAD_URL}' exists" | |
| curl -sS --head --fail "${DOWNLOAD_URL}" | |
| Profiling: | |
| needs: Prepare | |
| runs-on: [Linux, performance] | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| steps: | |
| - name: Clean _work Folder | |
| run: | | |
| echo "Cleaning Folder" | |
| rm -rf ./* | |
| - name: Determine commit to use | |
| id: determine-commit | |
| run: | | |
| echo "PR_HEAD=$(curl -s ${{ github.event.issue.pull_request.url }} | jq '.head.sha' | xargs echo)" | tee -a $GITHUB_OUTPUT | |
| - name: Check out code | |
| uses: actions/checkout@v3 | |
| with: | |
| ref: '${{ steps.determine-commit.outputs.PR_HEAD }}' | |
| - name: Run Tests | |
| run: | | |
| set -euo pipefail | |
| ISSUE_NUMBER=$(cat ${GITHUB_EVENT_PATH} | jq '.issue.number') | |
| PR_HEAD=${{ steps.determine-commit.outputs.PR_HEAD }} | |
| DOWNLOAD_URL=$(jq '.comment.body' ${GITHUB_EVENT_PATH} | (grep -oP '(?<=\()https://github\.com/${{ github.repository }}/files/[A-Za-z0-9._~!$&*+,;=@%/-]*\.tar\.gz(?=\))' || echo "No-valid-URL-found") | head -1 ) | |
| FILE_NAME=$(basename ${DOWNLOAD_URL}) | |
| gh issue comment ${ISSUE_NUMBER} --body "Running test with ${PR_HEAD:-master} and ${FILE_NAME} as ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}" | |
| echo "Download Test File from ${DOWNLOAD_URL}" | |
| curl -LOsS ${DOWNLOAD_URL} | |
| echo "Starting Test Execution" | |
| mkdir -p profile/tests/$(echo ${FILE_NAME} | cut -d '.' -f 1) | |
| echo "RUNNING PROFILE: ${FILE_NAME}" | |
| nix run .#profile ./${FILE_NAME} | |
| - name: Publish Profile Results | |
| uses: actions/upload-artifact@v3.1.0 | |
| with: | |
| path: ./profile-*.tar.gz | |
| on-success: | |
| needs: Profiling | |
| runs-on: [Linux, flyweight] | |
| if: ${{ always() && contains(join(needs.*.result, ','), 'success') }} | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| steps: | |
| - run: | | |
| ISSUE_NUMBER=$(cat ${GITHUB_EVENT_PATH} | jq '.issue.number') | |
| gh issue -R ${{ github.repository }} comment ${ISSUE_NUMBER} --body "PASSED: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}" | |
| on-failure: | |
| needs: Profiling | |
| runs-on: [Linux, flyweight] | |
| if: ${{ always() && contains(join(needs.*.result, ','), 'failure') }} | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| steps: | |
| - run: | | |
| ISSUE_NUMBER=$(cat ${GITHUB_EVENT_PATH} | jq '.issue.number') | |
| gh issue -R ${{ github.repository }} comment ${ISSUE_NUMBER} --body "FAILED: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}" |