|
| 1 | +# Reusable workflow for daily nanoda verification |
| 2 | +# Users can call this workflow from their repository: |
| 3 | +# |
| 4 | +# name: Daily nanoda verification |
| 5 | +# on: |
| 6 | +# schedule: |
| 7 | +# - cron: '0 0 * * *' |
| 8 | +# workflow_dispatch: |
| 9 | +# jobs: |
| 10 | +# verify: |
| 11 | +# uses: leanprover/lean-action/.github/workflows/nanoda-daily.yml@v1 |
| 12 | +# secrets: |
| 13 | +# webhook-url: ${{ secrets.WEBHOOK_URL }} # optional |
| 14 | +# zulip-api-key: ${{ secrets.ZULIP_API_KEY }} # optional |
| 15 | + |
| 16 | +name: nanoda Daily Verification |
| 17 | + |
| 18 | +on: |
| 19 | + workflow_call: |
| 20 | + inputs: |
| 21 | + allow-sorry: |
| 22 | + description: 'Permit sorryAx axiom' |
| 23 | + type: boolean |
| 24 | + default: true |
| 25 | + notify: |
| 26 | + description: 'Notification method: issue, webhook, zulip, none' |
| 27 | + type: string |
| 28 | + default: 'issue' |
| 29 | + zulip-stream: |
| 30 | + description: 'Zulip stream name (if using zulip notify)' |
| 31 | + type: string |
| 32 | + default: 'ci' |
| 33 | + zulip-topic: |
| 34 | + description: 'Zulip topic (if using zulip notify)' |
| 35 | + type: string |
| 36 | + default: 'nanoda' |
| 37 | + zulip-org-url: |
| 38 | + description: 'Zulip organization URL (required if using zulip notify)' |
| 39 | + type: string |
| 40 | + default: '' |
| 41 | + secrets: |
| 42 | + webhook-url: |
| 43 | + description: 'Slack/Discord webhook URL (optional)' |
| 44 | + required: false |
| 45 | + zulip-api-key: |
| 46 | + description: 'Zulip bot API key (optional)' |
| 47 | + required: false |
| 48 | + |
| 49 | +jobs: |
| 50 | + nanoda-verify: |
| 51 | + runs-on: ubuntu-latest |
| 52 | + steps: |
| 53 | + - name: Checkout repository |
| 54 | + uses: actions/checkout@v4 |
| 55 | + |
| 56 | + - name: Run lean-action with nanoda |
| 57 | + id: lean-action |
| 58 | + uses: leanprover/lean-action@v1 |
| 59 | + with: |
| 60 | + nanoda: true |
| 61 | + nanoda-allow-sorry: ${{ inputs.allow-sorry }} |
| 62 | + |
| 63 | + - name: Create GitHub issue on failure |
| 64 | + if: failure() && inputs.notify == 'issue' |
| 65 | + uses: actions/github-script@v7 |
| 66 | + with: |
| 67 | + script: | |
| 68 | + const runUrl = `${context.serverUrl}/${context.repo.owner}/${context.repo.repo}/actions/runs/${context.runId}`; |
| 69 | + await github.rest.issues.create({ |
| 70 | + owner: context.repo.owner, |
| 71 | + repo: context.repo.repo, |
| 72 | + title: '❌ Daily nanoda verification failed', |
| 73 | + body: `The daily nanoda type checker verification failed.\n\n**Commit:** ${context.sha}\n**Run:** [View workflow run](${runUrl})\n\nPlease investigate and fix any type checking issues.`, |
| 74 | + labels: ['nanoda', 'automated', 'ci-failure'] |
| 75 | + }); |
| 76 | +
|
| 77 | + - name: Send webhook notification |
| 78 | + if: always() && inputs.notify == 'webhook' |
| 79 | + env: |
| 80 | + WEBHOOK_URL: ${{ secrets.webhook-url }} |
| 81 | + run: | |
| 82 | + if [ -z "$WEBHOOK_URL" ]; then |
| 83 | + echo "::error::webhook-url secret is required when notify is set to 'webhook'" |
| 84 | + exit 1 |
| 85 | + fi |
| 86 | + STATUS="${{ job.status }}" |
| 87 | + EMOJI=$([[ "$STATUS" == "success" ]] && echo "✅" || echo "❌") |
| 88 | + RUN_URL="${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}" |
| 89 | +
|
| 90 | + curl --fail -X POST "$WEBHOOK_URL" \ |
| 91 | + -H "Content-Type: application/json" \ |
| 92 | + -d "{ |
| 93 | + \"text\": \"$EMOJI nanoda daily verification: $STATUS\", |
| 94 | + \"blocks\": [ |
| 95 | + { |
| 96 | + \"type\": \"section\", |
| 97 | + \"text\": { |
| 98 | + \"type\": \"mrkdwn\", |
| 99 | + \"text\": \"$EMOJI *nanoda daily verification*: $STATUS\n<$RUN_URL|View run> | Commit: \`${{ github.sha }}\`\" |
| 100 | + } |
| 101 | + } |
| 102 | + ] |
| 103 | + }" |
| 104 | + shell: bash |
| 105 | + |
| 106 | + - name: Validate Zulip configuration |
| 107 | + id: validate-zulip |
| 108 | + if: (success() || failure()) && inputs.notify == 'zulip' |
| 109 | + continue-on-error: true |
| 110 | + env: |
| 111 | + ZULIP_ORG_URL: ${{ inputs.zulip-org-url }} |
| 112 | + ZULIP_API_KEY: ${{ secrets.zulip-api-key }} |
| 113 | + run: | |
| 114 | + if [ -z "$ZULIP_ORG_URL" ]; then |
| 115 | + echo "::error::zulip-org-url input is required when notify is set to 'zulip'" |
| 116 | + exit 1 |
| 117 | + fi |
| 118 | + if [ -z "$ZULIP_API_KEY" ]; then |
| 119 | + echo "::error::zulip-api-key secret is required when notify is set to 'zulip'" |
| 120 | + exit 1 |
| 121 | + fi |
| 122 | +
|
| 123 | + - name: Send Zulip notification on success |
| 124 | + if: success() && inputs.notify == 'zulip' && steps.validate-zulip.outcome == 'success' |
| 125 | + uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 |
| 126 | + with: |
| 127 | + api-key: ${{ secrets.zulip-api-key }} |
| 128 | + email: 'github-bot@${{ inputs.zulip-org-url }}' |
| 129 | + organization-url: 'https://${{ inputs.zulip-org-url }}' |
| 130 | + to: ${{ inputs.zulip-stream }} |
| 131 | + type: 'stream' |
| 132 | + topic: ${{ inputs.zulip-topic }} |
| 133 | + content: | |
| 134 | + ✅ nanoda daily verification [succeeded](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}) on `${{ github.sha }}` |
| 135 | +
|
| 136 | + - name: Send Zulip notification on failure |
| 137 | + if: steps.lean-action.outcome == 'failure' && inputs.notify == 'zulip' && steps.validate-zulip.outcome == 'success' |
| 138 | + uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 |
| 139 | + with: |
| 140 | + api-key: ${{ secrets.zulip-api-key }} |
| 141 | + email: 'github-bot@${{ inputs.zulip-org-url }}' |
| 142 | + organization-url: 'https://${{ inputs.zulip-org-url }}' |
| 143 | + to: ${{ inputs.zulip-stream }} |
| 144 | + type: 'stream' |
| 145 | + topic: '${{ inputs.zulip-topic }} failure' |
| 146 | + content: | |
| 147 | + ❌ nanoda daily verification [failed](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}) on `${{ github.sha }}` |
0 commit comments