ci-log-retrieval
Retrieve and investigate failing Lean CI job logs. Use when a CI job fails and you need to fetch its logs, or when monitoring a CI run for failures.
ソース情報
- リポジトリ
- leanprover/lean4
- ソースの最終更新活動
- 2026年6月10日 11:48
- 検出された SKILL.md の言語
- 英語
- スター
- 9,494
- フォーク
- 1,037
インストール方法
デフォルトでは、最初にソースを確認する Prompt が選択されています。直接コマンドに切り替えるか、ローカルコピーをダウンロードすることもできます。
ソースファイルを確認
インストールを決める前に、SKILL.md と SkillsMP に表示されている付属ファイルをお読みください。
SKILL.md を表示中
SKILL.md
ソースの指示 · 読み取り専用プレビュー- name
- ci-log-retrieval
- description
- Retrieve and investigate failing Lean CI job logs. Use when a CI job fails and you need to fetch its logs, or when monitoring a CI run for failures.
- allowed-tools
- Bash
# CI Log Retrieval
When CI jobs fail, investigate immediately — don't wait for other jobs to complete. Individual job
logs are often available even while other jobs are still running.
Try:
```bash
gh run view <run-id> --log
gh run view <run-id> --log-failed
gh run view <run-id> --job=<job-id> # target the specific failed job
```
Sleeping is fine when asked to monitor CI and no failures exist yet, but once any job fails,
investigate that failure immediately.
GitHubで見る