Lean4+Mathlib4の組み合わせで証明が出来上がるとレポジトリをGithubで公開したくなります。この時にGithub Actionsを使ってCI (Continuous Integration)を設定しておくと、利用者がレポジトリをダウンロードしてから利用を開始する体験を向上できます。この記事は
GitHub - leanprover/lean-action: GitHub action for standard CI in Lean projects
を参考にして書き直しました。コメントでこちらを教えていただいた北窓さんに感謝です！！
やることは次の通りです。
1. レポジトリのトップに.githubというフォルダを作成し、その中にworkflowsというフォルダを作成します。そしてその中にci.ymlというファイルを配置します。このファイルの中身も上記リンクで紹介されていますが、以下の通りです。
name: CI
on:
push:
branches: ["main"] # replace "main" with the default branch
pull_request:
branches: ["main"]
workflow_dispatch:jobs:
build:
runs-on: ubuntu-lateststeps:
- uses: actions/checkout@v4
# uses lean standard action with all default input values
- uses: leanprover/lean-action@v1
このファイルの追加をローカルレポジトリで行った場合にはリモートにプッシュしてGithub上に反映されていることを確認してください。
2. Githubのリモートレポジトリにアクセスし、レポジトリの設定を開きます。左側に縦にCode and automationの中にActionsがあるのでそれをクリックし、さらにGeneralをクリックしてActionsの設定画面を開きます。以下の設定にしてください（デフォルトではなっていると思います）。
- Actions permissionsはAllow all actions and reusable workflowsが選択されていること。
- Workflow permissionsはRead repository contents and packages permissionsが選択されていること。
- 設定を変更した場合はSaveを押すこと。
これでCIが正しく動作するように設定が済みました。レポジトリにコードをプッシュすると文法チェックが行われ、それがパスするとビルドが走り、その際の成果物がキャッシュされるようです。
3. 最後にREADME.mdを書き換えて、使い方の準備として以下のような記載を追加します。
レポジトリをダウンロードして解凍してください。そのフォルダの中で以下のコマンドを実行してください。
% lake exe cache get
% lake build
上記終了後フォルダをVSCodeで開き、作業を開始できます。ファイルによっては「ヘッダが古いのでRestart Fileボタンを押して」というメッセージが出ることがあります。その際にはInfoViewの中のRestart Fileを押してください。しばらくするとエラーが消えます。
CIバッジ
CIバッジとはCIが成功しているか失敗しているかを示すアイコンで、CIが走るたびに自動更新されます。CIバッジの取得と貼り方はネットで簡単に調べられます。うまく貼れれば下記のようなバッジが表示されます。
