A pragmatic, proof-aware test coverage tool for Idris2.
A coverage tool that understands dependent types. It excludes provably unreachable branches (like void cases) from your coverage denominator, so 100% coverage is actually achievable.
$ idris2-cov myproject/
Coverage: 847/901 (94%)
Excluded (unreachable):
- void/absurd patterns: 45
- optimizer artifacts: 12# Build
idris2 --build idris2-coverage.ipkg
# Run on your project
./build/exec/idris2-cov path/to/project/
# Or with an ipkg file
./build/exec/idris2-cov myproject.ipkg
# Show only uncovered functions
./build/exec/idris2-cov --uncovered path/to/project/
# JSON output for CI
./build/exec/idris2-cov --json path/to/project/- Proof-aware: Excludes
impossible/voidbranches from denominator - CRASH classification: Distinguishes bugs from unreachable code
- CI-friendly: Exit codes and JSON output for automation
- Zero compiler changes: Works with vanilla Idris2
| Document | Description |
|---|---|
| Vibe Coding | Why this enables complex software development |
| Getting Started | Installation and first steps |
| User Guide | Full CLI reference and configuration |
| FAQ | Common questions and answers |
| Contributing | Development setup and PR guidelines |
| Architecture | Code structure and design decisions |
| Internals | Technical details (CRASH classification, name mangling) |
idris2 --dumpcases → Parse case trees → Classify branches
↓
Canonical (testable) vs Excluded (void/absurd)
↓
Chez Scheme profiler → Runtime hits → Coverage = executed / canonical
| Code | Meaning |
|---|---|
| 0 | Success (no coverage gaps) |
| 1 | Coverage gaps found |
| 2 | Analysis error |
- Idris2 0.7.0+
- Chez Scheme (for profiling)
- idris2-sos-test-coverage-experiment - Demonstrates how GFR Monad + dependent types reduce System of Systems test complexity from O(2^N) to O(N)
MIT