gh-145000: Run check-html-ids.py in CI (#145632)

Co-authored-by: Hugo van Kemenade <1324225+hugovk@users.noreply.github.com>

.github/workflows/reusable-check-html-ids.yml

@@ -0,0 +1,58 @@
+name: Reusable check HTML IDs
+
+on:
+  workflow_call:
+
+permissions:
+  contents: read
+
+env:
+  FORCE_COLOR: 1
+
+jobs:
+  check-html-ids:
+    name: 'Check for removed HTML IDs'
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    steps:
+      - name: 'Check out base commit'
+        uses: actions/checkout@v6
+        with:
+          persist-credentials: false
+          ref: ${{ github.event.pull_request.base.sha }}
+      - name: 'Set up Python'
+        uses: actions/setup-python@v6
+        with:
+          python-version: '3'
+          cache: 'pip'
+          cache-dependency-path: 'Doc/requirements.txt'
+      - name: 'Install build dependencies'
+        run: make -C Doc/ venv
+      - name: 'Build HTML documentation'
+        run: make -C Doc/ SPHINXOPTS="--quiet" html
+      - name: 'Check out PR head tools'
+        uses: actions/checkout@v6
+        with:
+          persist-credentials: false
+          sparse-checkout: |
+            Doc/tools/check-html-ids.py
+            Doc/tools/removed-ids.txt
+          sparse-checkout-cone-mode: false
+          path: pr-head
+      - name: 'Use PR head tools'
+        run: |
+          cp pr-head/Doc/tools/check-html-ids.py Doc/tools/check-html-ids.py
+          [ -f pr-head/Doc/tools/removed-ids.txt ] && cp pr-head/Doc/tools/removed-ids.txt Doc/tools/removed-ids.txt
+      - name: 'Collect HTML IDs'
+        run: python Doc/tools/check-html-ids.py collect Doc/build/html -o /tmp/html-ids-base.json.gz
+      - name: 'Download PR head HTML IDs'
+        uses: actions/download-artifact@v8
+        with:
+          name: html-ids-head.json.gz
+          path: /tmp
+      - name: 'Check for removed HTML IDs'
+        run: |
+          # shellcheck disable=SC2046
+          python Doc/tools/check-html-ids.py -v check \
+            /tmp/html-ids-base.json.gz /tmp/html-ids-head.json.gz \
+            $([ -f Doc/tools/removed-ids.txt ] && echo "--exclude-file Doc/tools/removed-ids.txt")

.github/workflows/reusable-docs.yml

@@ -75,6 +75,22 @@ jobs:
           --fail-if-regression \
           --fail-if-improved \
           --fail-if-new-news-nit
+    - name: 'Collect HTML IDs'
+      if: github.event_name == 'pull_request'
+      run: python Doc/tools/check-html-ids.py collect Doc/build/html -o Doc/build/html-ids-head.json.gz
+    - name: 'Upload HTML IDs'
+      if: github.event_name == 'pull_request'
+      uses: actions/upload-artifact@v7
+      with:
+        name: html-ids-head
+        path: Doc/build/html-ids-head.json.gz
+        archive: false
+
+  check-html-ids:
+    name: 'Check for removed HTML IDs'
+    needs: build-doc
+    if: github.event_name == 'pull_request'
+    uses: ./.github/workflows/reusable-check-html-ids.yml
 
   # Run "doctest" on HEAD as new syntax doesn't exist in the latest stable release
   doctest:

Doc/tools/check-html-ids.py

@@ -175,6 +175,7 @@ def verbose_print(*args, **kwargs):
             )
             if args.exclude_file:
                 print(f'Alternatively, add them to {args.exclude_file}.')
+            sys.exit(1)
 
 
 if __name__ == '__main__':

Doc/tools/removed-ids.txt

@@ -0,0 +1 @@
+# HTML IDs excluded from the check-html-ids.py check.