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,551
- 포크
- 1,044
설치 방법
기본적으로 소스를 먼저 확인하는 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에서 보기