File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change 5454 shell : bash # there is no script body, so this is safe to "run" outside landrun.
5555 run : |
5656 # We just populate the env vars for this step to make them viewable in the logs
57+ - name : Generate lean-pr-testing app token
58+ id : lean-pr-testing-token
59+ uses : actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
60+ with :
61+ app-id : ${{ secrets.MATHLIB_LEAN_PR_TESTING_APP_ID }}
62+ private-key : ${{ secrets.MATHLIB_LEAN_PR_TESTING_PRIVATE_KEY }}
63+ owner : leanprover
64+ repositories : lean4
5765 - name : cleanup
5866 shell : bash # This *just* deletes old files, so is safe to run outside landrun.
5967 run : |
@@ -571,11 +579,12 @@ jobs:
571579 exit 1
572580 fi
573581
582+ # The create-github-app-token README states that this token is masked and will not be logged accidentally.
574583 - name : Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
575584 if : always()
576585 shell : bash
577586 env :
578- TOKEN : ${{ secrets.LEAN_PR_TESTING }}
587+ TOKEN : ${{ steps.lean-pr-testing-token.outputs.token }}
579588 GITHUB_CONTEXT : ${{ toJson(github) }}
580589 WORKFLOW_URL : https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}
581590 BUILD_OUTCOME : ${{ steps.build.outcome }}
Original file line number Diff line number Diff line change @@ -88,12 +88,21 @@ jobs:
8888 - name : Cleanup workspace
8989 run : |
9090 sudo rm -rf -- *
91+ - name : Generate lean-pr-testing app token
92+ id : lean-pr-testing-token
93+ uses : actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
94+ with :
95+ app-id : ${{ secrets.MATHLIB_LEAN_PR_TESTING_APP_ID }}
96+ private-key : ${{ secrets.MATHLIB_LEAN_PR_TESTING_PRIVATE_KEY }}
97+ owner : leanprover
98+ repositories : lean4
9199 # Checkout the Lean repository on 'nightly-with-mathlib'
100+ # The create-github-app-token README states that this token is masked and will not be logged accidentally.
92101 - name : Checkout Lean repository
93102 uses : actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
94103 with :
95104 repository : leanprover/lean4
96- token : ${{ secrets.LEAN_PR_TESTING }}
105+ token : ${{ steps.lean-pr-testing-token.outputs.token }}
97106 ref : nightly-with-mathlib
98107 # Merge the relevant nightly.
99108 - name : Fetch tags from 'lean4-nightly', and merge relevant nightly into 'nightly-with-mathlib'
You can’t perform that action at this time.
0 commit comments