# idris2-dev

> Idris2 development guidelines including OOM avoidance, project conventions, and idris2-evm EVM compilation

- Author: shogochiai
- Repository: shogochiai/idris2-magical-utils
- Version: 20260125141900
- Stars: 0
- Forks: 0
- Last Updated: 2026-02-06
- Source: https://github.com/shogochiai/idris2-magical-utils
- Web: https://mule.run/skillshub/@@shogochiai/idris2-magical-utils~idris2-dev:20260125141900

---

---
name: idris2-dev
description: Idris2 development guidelines including OOM avoidance, project conventions, and idris2-evm EVM compilation
triggers:
  - Idris2
  - idris2
  - .idr file
  - .ipkg file
  - pack.toml
  - idris2-evm
  - Yul compilation
  - EVM bytecode
  - OOM
  - memory explosion
---

# Idris2 Development

## Project Policy

**idris2-icwasm / idris2-evm projects are Idris2-complete**

- **IC WASM:** No Rust or C. Use idris2-icwasm only.
- **EVM:** No Solidity, Foundry, Hardhat. Use idris2-evm only (includes Yul codegen).

Minimize external toolchain dependencies. Maximize Idris2 type safety.

## Compilation Targets

Idris2 packages have 4 backend targets:

| Target | Backend | Build | `%foreign` prefix |
|--------|---------|-------|-------------------|
| Native | Chez Scheme | `pack build <pkg>` | (standard) |
| EVM | idris2-evm codegen | `idris2-yul` executable (from idris2-evm package) | `evm:*` |
| IC WASM | idris2-icwasm codegen | `idris2-icwasm` executable | `wasm:*`, `ic0:*` |
| JavaScript | Idris2 built-in | `--cg javascript` / `--cg node` | `javascript:*` |

### Target Detection

Detect target via `%foreign` declarations in source:
- `"evm:*"` -> EVM target. `pack build` will **always fail** (expected behavior)
- `"javascript:*"` -> JS target. ipkg needs `--cg javascript`
- `"wasm:*"` / `"ic0:*"` -> IC WASM target
- none of above -> Native (Chez) target

### Per-Package Build Table

| Package | Target | `pack build` | Correct Build |
|---------|--------|--------------|---------------|
| idris2-textdao | EVM | expected fail | `idris2-yul` executable |
| idris2-ouf | EVM | expected fail | `idris2-yul` executable |
| idris2-subcontract | EVM (lib) | lib only | `idris2-yul` executable |
| oucdashboard | JS | (`--cg javascript` in ipkg) | `pack build` / ipkg opts |
| ouc | IC WASM | tests only | `idris2-icwasm` executable |
| icp-indexer | IC WASM | tests only | `idris2-icwasm` executable |
| lazyweb | Native | OK | `pack build` |
| (other magical-utils) | Native | OK | `pack build` |

### Architecture Table

EVM and IC have symmetric 3-layer structure:

| Layer | EVM | IC |
|-------|-----|-----|
| Low-level types + codegen | idris2-evm (interpreter + Yul codegen, single package) | idris2-icwasm (codegen + IC0 FFI, single package) |
| App framework | idris2-subcontract (UCS/ERC-7546) | idris2-cdk (StableMemory/FR Monad/ICP API) |
| Coverage | idris2-evm-coverage | idris2-dfx-coverage |

**Note:** idris2-yul was merged into idris2-evm. The `idris2-yul` executable is now built from the idris2-evm package (entry point: `YulMain.idr`).

## Memory Explosion Patterns (OOM Avoidance)

Idris2 compilation can explode from ~165MB to 16GB+ RAM:

1. **`{auto prf}` overuse** - Proof search explodes. Demote to runtime verification.
2. **Large Nat pattern matching** - `mkFoo 11155111 = ...` is NG. Use if-else.
3. **Giant single modules** - Split modules over 500 lines. Use re-export facades for compatibility.
4. **Type-level state machines** - If many states, demote to runtime verification.
5. **Existential + multi-branch** - N branches x M functions = NxM expansion. Consolidate to single record.

**Development environment:** 256GB RAM recommended.

Details: `docs/idris2-memory-eater.md`

## Type Ambiguity

Same type name in multiple modules causes compiler backtracking during type inference. Keep packages cleanly separated. Don't duplicate types across packages. If RAM explodes, check for type name collisions first.

## idris2-evm Yul Codegen Known Bugs

### `/=` Operator Reverses Branch Logic
`if x /= 0 then A else B` compiles as `if x == 0 then A else B`.
**Workaround:** Always use `== 0` with swapped branches.

### Closure Parameter Ordering
When the Yul codegen creates closures across many let bindings, parameter order can get shuffled.
**Workaround:** Restructure code to minimize deep closure nesting. Read calldata after state changes.

### Missing EVM.Primitives
`codecopy`, `extcodecopy`, `extcodesize` IO wrapper functions are missing. Constants exist but IO functions don't.

## Git / pack.toml

**Always use SSH URLs for GitHub:**
- `git@github.com:org/repo.git` (correct)
- `https://github.com/org/repo` (wrong - auth issues)

## Generated Files - No Manual Edits

| File | Source | Command |
|------|--------|---------|
| `canister_entry.c` | `can.did` | `idris2-icwasm gen-entry` |
| `*.ttc` (TTC cache) | `*.idr` | `idris2 --build` |
| `build/` directory | Source | Build system |