build-wiki-pdf.yml

name: Build and add wiki release
# Only run when the wiki is updated
on: gollum
jobs:
  make_pdf:
    runs-on: ubuntu-latest
    steps:
      - uses: technote-space/auto-cancel-redundant-workflow@v1
      - uses: actions/checkout@v2
      - run: sudo apt install pandoc texlive-xetex
      - working-directory: util/wiki
        run: pip3 install -r requirements.txt
      - run: pandoc --version
      - working-directory: util/wiki
        run: |
          git clone https://github.com/utwente-fmt/vercors.wiki.git
          python3 ./generate_wiki_pdf.py -i vercors.wiki --html wiki.html --pdf wiki.pdf
      - working-directory: util/wiki
        run: ls
      - name: Set wiki pdf tag in github repo
        env:
          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
        run: |
          git config --local user.name "Vercors Team"
          git config --local user.email "vercors@lists.utwente.nl"
          git tag --force wiki-generated-doc
          git remote set-url origin https://${GITHUB_TOKEN}@github.com/utwente-fmt/vercors.git
          git push --force --tags
      - name: Create Wiki PDF release
        uses: ncipollo/release-action@v1
        with:
          allowUpdates: true
          artifacts: "util/wiki/wiki.pdf,util/wiki/wiki.html"
          artifactContentType: application/pdf
          body: "These are automatically generated versions of the tutorial on the VerCors wiki. There are two artefacts of interest: the Latex/PDF version, suitable for printing, and the HTML version, suitable for offline viewing."
          name: VerCors Wiki PDF
          prerelease: true
          tag: wiki-generated-doc
          token: ${{ secrets.GITHUB_TOKEN }}
          # instead of secrets.GITHUB_TOKEN, it should be a personal access token from the vercors-bot. So to implement:
          # 1. Create a personal access token from vercors bot
          # 2. add this to the secrets of the vercors repo
          # 3. Replace the GITHUB_TOKEN secret below with the vercors bot personal access token
          # 4. Uncomment this section. I think it should work!
          # - name: Trigger website update
          #   env:
          #     GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
          #   run: |
          #     git clone https://user:$GITHUB_TOKEN@github.com/utwente-fmt/vercors-web-build.git
          #     cd vercors-web-build
          #     git config --local user.name "Vercors Team"
          #     git config --local user.email "vercors@lists.utwente.nl"
          #     git commit --allow-empty -m "Trigger website refresh"
          #     git push