ci(docs): Revamp documentation building, deployment and cleanup (#292)

* Add build-deploy-docs.yml to build the documentation and deploy it to the right folder(s) of TorchJD/documentation repo whenever a pull request is opened, synchronized or reopened, whenever a push is made to the main branch, and whenever a version tag is pushed.
* Add cleanup-pr-docs to delete the documentation contained in a folder of TorchJD/documentation whenever the corresponding PR is closed, and to push the changes to the main branch of TorchJD/documentation.

---------

Co-authored-by: Valérian Rey <31951177+ValerianRey@users.noreply.github.com>
Co-authored-by: Valérian Rey <valerian.rey@gmail.com>

Author: PierreQuinton

.github/workflows/build-deploy-docs.yml

@@ -0,0 +1,68 @@
+name: Build and Deploy Documentation
+
+on:
+  push:
+    branches: [ main ]
+    tags:
+      - 'v[0-9]*.[0-9]*.[0-9]*'
+  pull_request:
+    types: [opened, synchronize, reopened]
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: write
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+
+      - name: Setup PDM
+        uses: pdm-project/setup-pdm@v4
+        with:
+          python-version: '3.13'
+
+      - name: Install dependencies (default & doc)
+        run: pdm install --group doc --frozen-lockfile
+
+      - name: Build Documentation
+        working-directory: docs
+        run: pdm run make dirhtml
+
+      - name: Determine deployment folder
+        id: deploy_folder
+        run: |
+          echo "Determining deployment folder..."
+          if [ "${{ github.event_name }}" = "pull_request" ]; then
+            echo "Deploying to target pr/${{ github.event.number }}"
+            echo "DEPLOY_DIR=pr/${{ github.event.number }}" >> $GITHUB_OUTPUT
+          elif [[ "${{ github.ref }}" == refs/tags/* ]]; then
+            echo "Deploying to target ${{ github.ref_name }}"
+            echo "DEPLOY_DIR=${{ github.ref_name }}" >> $GITHUB_OUTPUT
+          else
+            echo "Deploying to target main"
+            echo "DEPLOY_DIR=main" >> $GITHUB_OUTPUT
+          fi
+
+      - name: Deploy to DEPLOY_DIR of TorchJD/documentation
+        uses: peaceiris/actions-gh-pages@v4
+        with:
+          deploy_key: ${{ secrets.DOCUMENTATION_DEPLOY_KEY }}
+          publish_dir: docs/build/dirhtml
+          destination_dir: ${{ steps.deploy_folder.outputs.DEPLOY_DIR }}
+          external_repository: TorchJD/documentation
+          publish_branch: main
+
+      - name: Deploy to stable of TorchJD/documentation
+        if: startsWith(github.ref, 'refs/tags/')
+        uses: peaceiris/actions-gh-pages@v4
+        with:
+          deploy_key: ${{ secrets.DOCUMENTATION_DEPLOY_KEY }}
+          publish_dir: docs/build/dirhtml
+          destination_dir: stable
+          external_repository: TorchJD/documentation
+          publish_branch: main
+
+      - name: Add documentation link to summary
+        run: |
+          echo "### 📄 [View Deployed Documentation](https://torchjd.github.io/documentation/${{ steps.deploy_folder.outputs.DEPLOY_DIR }})" >> $GITHUB_STEP_SUMMARY

.github/workflows/cleanup-pr-docs.yml

@@ -0,0 +1,32 @@
+name: Cleanup PR Documentation
+
+on:
+  pull_request:
+    types: [closed]
+
+jobs:
+  cleanup:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: write
+    steps:
+      - name: Checkout gh-pages branch
+        uses: actions/checkout@v4
+        with:
+          repository: TorchJD/documentation
+          ref: main
+          ssh-key: ${{ secrets.DOCUMENTATION_DEPLOY_KEY }}
+
+      - name: Remove PR documentation for closed PR
+        run: |
+          PR_NUMBER="${{ github.event.number }}"
+          echo "Removing documentation for PR #${PR_NUMBER}"
+          rm -rf pr/${PR_NUMBER}
+
+      - name: Commit and push cleanup
+        run: |
+          git config user.name "github-actions"
+          git config user.email "github-actions@github.com"
+          git add .
+          git commit -m "Cleanup documentation for closed PR #${{ github.event.number }}" || echo "No changes to commit"
+          git push origin HEAD:main