idris2-firebox

Make your agents feel at home using Idris 2.

idris2-firebox is a portable, multi-harness plugin bundle designed to make AI coding agents productive in Idris 2. It provides an interactive error decoder, authoring discipline for keeping properties in types, comprehensive guidance on total proof and impossibility, and compiler-driven interactive editing over the Idris 2 IDE protocol.

Installation

Claude Code

Install via the Claude Code plugin marketplace or load this directory into Claude Code.

Codex

Add this repository to Codex using the .codex-plugin/ directory manifest.

Antigravity

Import the plugin into Antigravity using:

agy plugin import claude

What's in it

This bundle provides two skills in skills/:

• idris2: Documentation, authoring discipline, error decoding, totality and impossibility proof patterns, stdlib map, and package setup. Ships the gate script described below.
• idris2-ide-mode: Interactive compiler-driven editing (case splitting, type checking, hole inspection) via the Idris 2 IDE protocol.

The gate

skills/idris2/scripts/idris2-check is the single definition of what "passes" means here, and agents are directed to it rather than to idris2 directly:

python3 skills/idris2/scripts/idris2-check FILE.idr

It runs --check, then --total --check, then a hole query over the IDE protocol. It exists because idris2 --check is weaker than it looks in two ways that do not announce themselves:

• A failing check can exit 0. A missing import prints Error: and exits 0, so a bare $? test reports success on a file the compiler rejected.
• A finished-looking proof can be empty. f n = ?todo exits 0, prints no Error:, and satisfies --total — it is a complete, covering, terminating clause whose right-hand side is unknown.

Holes never fail the gate, since a hole is the honest terminal state when a goal cannot be discharged. They are always listed, and holes remaining means the task is not done.

Pass --json for a machine-readable verdict, or --no-total for plain --check semantics.

Running the tests

Run the unit suite using pytest:

pytest tests/

Run the compiler validation suite, which typechecks every fixture against the installed Idris 2:

python3 tests/run.py

The supported compiler is pinned semantically in tests/idris-version.txt; the exact Pack revision is printed only as a diagnostic. Version-sensitive IDE behavior is exercised directly. Review compiler-message catalog drift separately from the curated decoder:

python3 tests/run.py --coverage

The compiler suites take several minutes because each fixture is checked through every gate phase.

License

This project is licensed under the MIT License — see the LICENSE file for details. Third-party attributions and material derived from Idris 2 are listed in NOTICE.