Confusing use of ticks in FS0064 warning. #12257
This file contains hidden or 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: Run CLI Commands via PR Comment | |
| on: | |
| issue_comment: | |
| types: [created] | |
| jobs: | |
| parsing_job: | |
| runs-on: ubuntu-latest | |
| permissions: | |
| issues: write # Allow adding a reaction via the comment-pipeline | |
| pull-requests: write | |
| outputs: | |
| command: ${{ steps.parse.outputs.command }} | |
| arg: ${{ steps.parse.outputs.arguments }} | |
| if: github.event.issue.pull_request | |
| steps: | |
| - name: Parse comment | |
| id: parse | |
| uses: dotnet/comment-pipeline@e08a11834acf1e825ac727b732ac9d4cb8120c51 | |
| with: | |
| comment: ${{ toJSON(github.event.comment) }} | |
| commands: | | |
| /run fantomas | |
| /run ilverify | |
| /run xlf | |
| /run test-baseline | |
| github-token: ${{ secrets.GITHUB_TOKEN }} | |
| # This second job by definiton runs user-supplied code - you must NOT elevate its permissions to `write` | |
| # Malicious code could change nuget source URL, build targets or even compiler itself to pass a GH token | |
| # And use it to create branches, spam issues etc. Any write-actions happen in the second job, which does not allow | |
| # user extension points (i.e. plain scripts, must NOT run scripts from within checked-out code) | |
| run-parsed-command: | |
| needs: parsing_job | |
| runs-on: ubuntu-latest | |
| if: needs.parsing_job.outputs.command != '' | |
| steps: | |
| - name: Checkout the repository | |
| uses: actions/checkout@v4 | |
| - name: Checkout PR branch | |
| run: gh auth setup-git && gh pr checkout ${{ github.event.issue.number }} | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| - name: Install dotnet | |
| uses: actions/setup-dotnet@v3 | |
| with: | |
| global-json-file: global.json | |
| - name: Install dotnet tools | |
| run: dotnet tool restore | |
| - name: Setup .NET 9.0.0 Runtime for test execution | |
| if: ${{ needs.parsing_job.outputs.command == '/run test-baseline' }} | |
| uses: actions/setup-dotnet@v4 | |
| with: | |
| dotnet-version: '9.0.x' | |
| - name: Run command | |
| id: run-cmd | |
| env: | |
| TEST_UPDATE_BSL: 1 | |
| continue-on-error: true | |
| run: | | |
| case "${{ needs.parsing_job.outputs.command }}" in | |
| "/run fantomas") dotnet fantomas . ;; | |
| "/run xlf") dotnet build src/Compiler /t:UpdateXlf ;; | |
| "/run ilverify") pwsh tests/ILVerify/ilverify.ps1 || true ;; | |
| "/run test-baseline") dotnet test ./FSharp.Compiler.Service.sln --filter "${{ needs.parsing_job.outputs.arg }}" -c Release || true ;; | |
| *) echo "Unknown command" && exit 1 ;; | |
| esac | |
| - name: Create patch & metadata | |
| id: meta | |
| if: needs.parsing_job.outputs.command | |
| run: | | |
| echo "run_step_outcome=${{ steps.run-cmd.outcome }}" > result | |
| if [[ "${{ steps.run-cmd.outcome }}" == "success" ]]; then | |
| git diff > repo.patch || true | |
| if [ -s repo.patch ]; then echo "hasPatch=true" >> result; else echo "hasPatch=false" >> result; fi | |
| else | |
| echo "hasPatch=false" >> result | |
| fi | |
| cat result | |
| - name: Upload artifacts | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: cli-results | |
| path: | | |
| repo.patch | |
| result | |
| apply-and-report: | |
| needs: [parsing_job, run-parsed-command] | |
| runs-on: ubuntu-latest | |
| permissions: | |
| contents: write | |
| pull-requests: write | |
| if: needs.parsing_job.outputs.command != '' && needs.run-parsed-command.result == 'success' | |
| steps: | |
| - name: Checkout the repository | |
| uses: actions/checkout@v4 | |
| - name: Checkout PR branch | |
| run: gh auth setup-git && gh pr checkout ${{ github.event.issue.number }} | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| - name: Download artifacts | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: cli-results | |
| - name: Read metadata | |
| id: read-meta | |
| run: | | |
| source result | |
| echo "run_step_outcome=$run_step_outcome" >> $GITHUB_OUTPUT | |
| echo "hasPatch=$hasPatch" >> $GITHUB_OUTPUT | |
| - name: Apply and push patch | |
| if: ${{ steps.read-meta.outputs.run_step_outcome == 'success' && steps.read-meta.outputs.hasPatch == 'true' }} | |
| run: | | |
| patch -p1 -s --force < repo.patch || true | |
| git config user.name "GH Actions" | |
| git config user.email "actions@github.com" | |
| git add -u | |
| git commit -m "Apply patch from ${{ needs.parsing_job.outputs.command }}" | |
| upstream=$(git rev-parse --abbrev-ref --symbolic-full-name @{u}) | |
| remote=${upstream%%/*} | |
| branch=${upstream#*/} | |
| echo "Pushing to $remote $branch" | |
| git push "$remote" HEAD:"$branch" | |
| - name: Count stats | |
| id: stats | |
| if: ${{ steps.read-meta.outputs.run_step_outcome == 'success' && steps.read-meta.outputs.hasPatch == 'true' }} | |
| run: | | |
| files=$(git diff --name-only HEAD~1 HEAD | wc -l) | |
| lines=$(git diff HEAD~1 HEAD | wc -l) | |
| echo "files=$files" >> $GITHUB_OUTPUT | |
| echo "lines=$lines" >> $GITHUB_OUTPUT | |
| - name: Generate and publish report | |
| if: always() | |
| env: | |
| COMMAND: ${{ needs.parsing_job.outputs.command }} | |
| OUTCOME: ${{ steps.read-meta.outputs.run_step_outcome }} | |
| PATCH: ${{ steps.read-meta.outputs.hasPatch }} | |
| run: | | |
| # Build the markdown report | |
| report=" | |
| # 🔧 CLI Command Report | |
| - **Command:** \`${COMMAND}\` | |
| - **Outcome:** ${OUTCOME} | |
| " | |
| if [[ "$OUTCOME" == "success" ]]; then | |
| if [[ "$PATCH" == "true" ]]; then | |
| report+="✅ Patch applied: | |
| - Files changed: ${{ steps.stats.outputs.files }} | |
| - Lines changed: ${{ steps.stats.outputs.lines }}" | |
| else | |
| report+="✅ Command succeeded, no changes needed." | |
| fi | |
| else | |
| report+="❌ Command **failed** — no patch applied." | |
| fi | |
| # Output to GitHub Actions UI | |
| echo "$report" >> "$GITHUB_STEP_SUMMARY" | |
| # Store for use in next step | |
| echo "$report" > pr_report.md | |
| - name: Comment on PR | |
| if: always() | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| PR_NUMBER: ${{ env.PR_NUMBER }} | |
| run: | | |
| # Use gh CLI to comment with multi-line markdown | |
| gh pr comment ${{ github.event.issue.number }} \ | |
| --body-file pr_report.md |