cleanup: remove summarize_declarations and tooling for move-decls (…

…#14047)

This PR cleans up the tooling around the `move-decls` label that is now obsolete, thanks to the new `PR summary` comment on PRs.

Here is a short description of what the removed code did:
* the `summarize_declarations` CI step produced a formatted output of `./scripts/no_lost_declarations` that I suspect no one except for me ever looked at;
* `.github/workflows/move_decl.yaml` is the (working) action that adds the output of `./scripts/no_lost_declarations short` to the PR as a comment -- this has been made obsolete by the `PR summary` comment;
* `.github/workflows/move_decl_comment.yml` is a (failed) action that should have posted the short diff on all PRs, but never actually worked -- besides being broken, this has also been made obsolete by the `PR summary` comment.

.github/workflows/bors.yml

@@ -90,23 +90,6 @@ jobs:
       - name: check that workflows were consistent
         run: git diff --exit-code
 
-  summarize_declarations:
-    if: github.repository == 'leanprover-community/mathlib4'
-    name: summarize_declarations
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v4
-        with:
-          ## fetch the whole repository, useful to find a common fork
-          fetch-depth: 0
-      - name: print_lost_declarations
-        run: |
-          ## back and forth to settle a "detached head" (maybe?)
-          git checkout -q master
-          git checkout -q -
-          printf '###  Summary\n\n' > "${GITHUB_STEP_SUMMARY}"
-          ./scripts/no_lost_declarations.sh >> "${GITHUB_STEP_SUMMARY}"
-
   build:
     if: github.repository == 'leanprover-community/mathlib4'
     name: Build

.github/workflows/build.yml

@@ -97,23 +97,6 @@ jobs:
       - name: check that workflows were consistent
         run: git diff --exit-code
 
-  summarize_declarations:
-    if: github.repository == 'leanprover-community/mathlib4'
-    name: summarize_declarations
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v4
-        with:
-          ## fetch the whole repository, useful to find a common fork
-          fetch-depth: 0
-      - name: print_lost_declarations
-        run: |
-          ## back and forth to settle a "detached head" (maybe?)
-          git checkout -q master
-          git checkout -q -
-          printf '###  Summary\n\n' > "${GITHUB_STEP_SUMMARY}"
-          ./scripts/no_lost_declarations.sh >> "${GITHUB_STEP_SUMMARY}"
-
   build:
     if: github.repository == 'leanprover-community/mathlib4'
     name: Build

.github/workflows/build.yml.in

@@ -76,23 +76,6 @@ jobs:
       - name: check that workflows were consistent
         run: git diff --exit-code
 
-  summarize_declarations:
-    if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
-    name: summarize_declarations
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v4
-        with:
-          ## fetch the whole repository, useful to find a common fork
-          fetch-depth: 0
-      - name: print_lost_declarations
-        run: |
-          ## back and forth to settle a "detached head" (maybe?)
-          git checkout -q master
-          git checkout -q -
-          printf '###  Summary\n\n' > "${GITHUB_STEP_SUMMARY}"
-          ./scripts/no_lost_declarations.sh >> "${GITHUB_STEP_SUMMARY}"
-
   build:
     if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
     name: BuildJOB_NAME

.github/workflows/build_fork.yml

@@ -94,23 +94,6 @@ jobs:
       - name: check that workflows were consistent
         run: git diff --exit-code
 
-  summarize_declarations:
-    if: github.repository != 'leanprover-community/mathlib4'
-    name: summarize_declarations
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v4
-        with:
-          ## fetch the whole repository, useful to find a common fork
-          fetch-depth: 0
-      - name: print_lost_declarations
-        run: |
-          ## back and forth to settle a "detached head" (maybe?)
-          git checkout -q master
-          git checkout -q -
-          printf '###  Summary\n\n' > "${GITHUB_STEP_SUMMARY}"
-          ./scripts/no_lost_declarations.sh >> "${GITHUB_STEP_SUMMARY}"
-
   build:
     if: github.repository != 'leanprover-community/mathlib4'
     name: Build (fork)