Skip to content

#lint コマンドを紹介する #402

#lint コマンドを紹介する

#lint コマンドを紹介する #402

Workflow file for this run

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