sync.yml

name: sync exercise and solutions

concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}
  cancel-in-progress: true

on:
  pull_request:
    branches:
      - main
  push:
    branches:
      - main
  workflow_dispatch:

permissions:
  contents: write
  pages: write
  id-token: write

jobs:
  sync_exercise:
    runs-on: ubuntu-latest
    steps:
      - name: checkout
        uses: actions/checkout@v4
        with:
          ref: ${{ github.event.pull_request.head.ref }}

      - name: Install elan
        run: |
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
          echo "$HOME/.elan/bin" >> $GITHUB_PATH

      # ファイル名変更により解答と対応しない演習問題が残ることを避けるため、
      # いったん演習ファイルを全て削除している
      - name: run mk_exercise
        run: |
          rm -r LeanByExample/Tutorial/Exercise
          lake exe mk_exercise LeanByExample/Tutorial/Solution LeanByExample/Tutorial/Exercise

      - name: detect diff
        id: diff
        run: |
          git add -N LeanByExample/Tutorial/Exercise
          git diff --name-only --exit-code