feat: improved export command, namespace aliases
#7614
Workflow file for this run
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: Check for stage0 changes | |
| on: | |
| merge_group: | |
| pull_request: | |
| jobs: | |
| check-stage0-on-queue: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| ref: ${{ github.event.pull_request.head.sha }} | |
| filter: blob:none | |
| fetch-depth: 0 | |
| - name: Find base commit | |
| if: github.event_name == 'pull_request' | |
| run: echo "BASE=$(git merge-base origin/${{ github.base_ref }} HEAD)" >> "$GITHUB_ENV" | |
| - name: Identify stage0 changes | |
| run: | | |
| git diff "${BASE:-HEAD^}..HEAD" --name-only -- stage0 | | |
| grep -v -x -F $'stage0/src/stdlib_flags.h\nstage0/src/lean.mk.in' \ | |
| > "$RUNNER_TEMP/stage0" || true | |
| if test -s "$RUNNER_TEMP/stage0" | |
| then | |
| echo "CHANGES=yes" >> "$GITHUB_ENV" | |
| else | |
| echo "CHANGES=no" >> "$GITHUB_ENV" | |
| fi | |
| shell: bash | |
| - if: github.event_name == 'pull_request' | |
| name: Set label | |
| uses: actions/github-script@v7 | |
| with: | |
| script: | | |
| const { owner, repo, number: issue_number } = context.issue; | |
| if (process.env.CHANGES == 'yes') { | |
| await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['changes-stage0'] }).catch(() => {}); | |
| } else { | |
| await github.rest.issues.removeLabel({ owner, repo, issue_number, name: 'changes-stage0' }).catch(() => {}); | |
| } | |
| - if: env.CHANGES == 'yes' | |
| name: Report changes | |
| run: | | |
| echo "Found changes to stage0/, please do not merge using the merge queue." | tee "$GITHUB_STEP_SUMMARY" | |
| # shellcheck disable=SC2129 | |
| echo '```' >> "$GITHUB_STEP_SUMMARY" | |
| cat "$RUNNER_TEMP/stage0" >> "$GITHUB_STEP_SUMMARY" | |
| echo '```' >> "$GITHUB_STEP_SUMMARY" | |
| - if: github.event_name == 'merge_group' && env.CHANGES == 'yes' | |
| name: Fail when on the merge queue | |
| run: exit 1 |