ci(daily.yml): link to specific step in Zulip message (leanprover-community#31096)

The messages posted by this bot currently link to the workflow page rather than the specific step referenced so it takes some extra clicking to find out what the success / failure is referring to. In fact, even though the bot posts messages for `lean4checker` and `mathlib4_test_executable` in different threads, the overly general URL made even that fact hard to understand:

cf. [#nightly-testing > mathlib test executable failure @ 💬](https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/mathlib.20test.20executable.20failure/near/546141970)

This PR makes the Zulip messages link to the relevant steps in the relevant jobs. It also cleans up some unnecessary steps along the way.

Author: bryangingechen

.github/workflows/daily.yml

@@ -16,29 +16,42 @@ env:
   DEFAULT_BRANCH: master
   TAG_PATTERN: '^nightly-testing-[0-9]{4}-[0-9]{2}-[0-9]{2}$'
 
+permissions:
+  contents: read
+  actions: read
+
 jobs:
   check-lean4checker:
     runs-on: ubuntu-latest
-    if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'
+    if: github.repository == 'leanprover-community/mathlib4'
     strategy:
       matrix:
         branch_type: [master, nightly]
     steps:
-      - name: Cleanup
-        run: |
-          # Delete all but the 5 most recent toolchains.
-          # Make sure to delete both the `~/.elan/toolchains/X` directory and the `~/.elan/update-hashes/X` file.
-          # Skip symbolic links (`-type d`), the current directory (`! -name .`), and `nightly` and `stable`.
-          if cd ~/.elan/toolchains && find . -maxdepth 1 -type d ! -name . -print0 | xargs -0 ls -1td | grep -v 'nightly$' | grep -v 'stable$' | tail -n +6 | xargs -I {} sh -c 'echo {} && rm -rf "{}" && rm "../update-hashes/{}"'; then
-              : # Do nothing on success
-          else
-              : # Do nothing on failure, but suppress errors
-          fi
-
       # Checkout repository, so that we can fetch tags to decide which branch we want.
       - name: Checkout branch or tag
         uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
 
+      # this step needs to be run here while we have `mathlib4` checked out,
+      # or else `gh run view` will try to look for runs in `mathlib4-nightly-testing`
+      - name: Get URLs
+        id: urls
+        env:
+          GH_TOKEN: ${{ github.token }}
+        run: |
+          # adapted from https://cmbuckley.co.uk/blog/2024/04/09/deep-links-to-github-actions-job-logs/
+          lean4checker_url=$(gh run view ${{ github.run_id }} --json jobs --jq '
+            .jobs[] | select(.name == "check-lean4checker (${{ matrix.branch_type }})")
+            | (.url + (.steps[] | select(.name == "Check environments using lean4checker")
+              | "#step:\(.number):1"))')
+          echo "lean4checker_url=$lean4checker_url" | tee -a "$GITHUB_OUTPUT"
+
+          mathlib_test_executable_url=$(gh run view ${{ github.run_id }} --json jobs --jq '
+            .jobs[] | select(.name == "check-lean4checker (${{ matrix.branch_type }})")
+            | (.url + (.steps[] | select(.name == "Run mathlib_test_executable")
+              | "#step:\(.number):1"))')
+          echo "mathlib_test_executable_url=$mathlib_test_executable_url" | tee -a "$GITHUB_OUTPUT"
+
       - name: Fetch latest tags (if nightly)
         if: matrix.branch_type == 'nightly'
         run: |
@@ -68,14 +81,10 @@ jobs:
         with:
           auto-config: false
           use-github-cache: false
-          use-mathlib-cache: false
+          use-mathlib-cache: true
           reinstall-transient-toolchain: true
 
-      - name: Run lake exe cache get
-        run: |
-          lake exe cache get
-
-      - name: Check environments using lean4checker
+      - name: Check environments using lean4checker # make sure this name is consistent with "Get URLs"
         id: lean4checker
         continue-on-error: true
         run: |
@@ -106,7 +115,7 @@ jobs:
           # so we explicitly check Batteries as well here.
           lake env lean4checker/.lake/build/bin/lean4checker Batteries Mathlib
 
-      - name: Run mathlib_test_executable
+      - name: Run mathlib_test_executable # make sure this name is consistent with "Get URLs"
         id: mathlib-test
         continue-on-error: true
         run: |
@@ -123,7 +132,7 @@ jobs:
           type: 'stream'
           topic: 'lean4checker'
           content: |
-            ✅ lean4checker [succeeded](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }})
+            ✅ lean4checker [succeeded](${{ steps.urls.outputs.lean4checker_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }})
 
       - name: Post success message for mathlib_test_executable on Zulip
         if: steps.mathlib-test.outcome == 'success'
@@ -136,7 +145,7 @@ jobs:
           type: 'stream'
           topic: 'mathlib test executable'
           content: |
-            ✅ mathlib_test_executable [succeeded](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }})
+            ✅ mathlib_test_executable [succeeded](${{ steps.urls.outputs.mathlib_test_executable_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }})
 
       - name: Post failure message for lean4checker on Zulip
         if: steps.lean4checker.outcome == 'failure'
@@ -149,7 +158,7 @@ jobs:
           type: 'stream'
           topic: 'lean4checker failure'
           content: |
-            ❌ lean4checker [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }})
+            ❌ lean4checker [failed](${{ steps.urls.outputs.lean4checker_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }})
         continue-on-error: true
 
       - name: Post failure message for mathlib_test_executable on Zulip
@@ -163,5 +172,5 @@ jobs:
           type: 'stream'
           topic: 'mathlib test executable failure'
           content: |
-            ❌ mathlib_test_executable [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }})
+            ❌ mathlib_test_executable [failed](${{ steps.urls.outputs.mathlib_test_executable_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }})
         continue-on-error: true