agda-typecheck-profile

name

agda-typecheck-profile

description

Profile Agda typechecking performance from a cold cache. Supports two modes — project-wide (via `agda --profile=modules`, reporting per-module times and ms-per-line) and single-module (via `agda --profile=definitions`, reporting per-definition times). Can drill from the project-wide report into specific slow modules, and can investigate individual slow definitions by recursively replacing subterms with holes to locate the true hotspot. Use this whenever the user wants to investigate why Agda typechecking is slow, find hot modules or definitions, benchmark typechecking, or hunt down a specific slow hotspot — even if they don't say "profile". Triggers on phrases like "why is Agda slow", "typechecking performance", "profile the build", "which module is slowest", "find the bottleneck", "why does this definition take so long".

Agda typechecking profile

Measures Agda typechecking performance from a cold cache and produces a ranked report. Two modes, and an optional drill-down chain:

• Project-wide → agda --build-library --profile=modules, table of modules sorted by time with ms/line.
• Single module → agda --profile=definitions <file>, table of definitions sorted by time.
• Project-wide → single module: after the project-wide report, offer to drill into the slowest modules (or a user-specified list) using the single-module mode.
• Single module → investigate: after a definitions report, offer to hunt down what's making a specific definition slow via the hole-replacement strategy (see references/investigate-slow.md).

Every Agda invocation goes through one of two wrapper scripts under scripts/. That keeps the Bash command line stable across runs so a single allowlist entry covers every invocation — important for the iterated investigation loop.

Workflow

1. Choose a mode

Pick based on what the user asked for:

• Phrases like "profile the project", "where is time going", "which module is slowest" → project-wide.
• Phrases like "why is this module slow", "profile Foo.agda", "what's slow inside this definition" → single-module. If they named a file or module, use it; otherwise ask.

If it's genuinely ambiguous (e.g., just "profile Agda"), start with project-wide since it's the better default entry point.

2. Shared setup

Applies to both modes. Do this once.

Locate the library directory — the dir containing an .agda-lib file. Check the repo root first:

ls *.agda-lib 2>/dev/null

If not there, look one level down:

find . -maxdepth 3 -name '*.agda-lib' -not -path '*/_build/*' -not -path '*/.git/*'

If exactly one candidate, use it. If multiple or none, ask the user.

Ask about literate line counting — only relevant for project-wide mode. If any source is .lagda.md, ask whether the ms/line denominator should be:

• all — every line in the file (includes prose/markdown).
• code-only — only lines inside ```agda fences (reflects typechecked Agda).

Skip this question in single-module mode — the definitions table doesn't use LOC.

Nix detection is automatic — the wrapper scripts walk up from the lib directory looking for a flake.nix (lib dir, then parent dirs up to /) and, if found, wrap the Agda call in nix develop <flake-dir> --command bash -c "...". You do not need to modify the repo (symlinking flake.nix into the lib dir, copying files, etc.) to make detection work — the wrapper handles nested layouts. If agda still isn't found, set NO_NIX=1 to skip the wrapper, or ask the user how to enter their dev shell.

3a. Project-wide profile

Use the wrapper. It clears _build/ and .agdai files itself (cold cache), runs Agda, and renders the table:

bash ~/.claude/skills/agda-typecheck-profile/scripts/run_modules_profile.sh <lib-dir> <all|code-only>

Real projects can take several minutes. Use a generous timeout (10 min is a reasonable default; raise it for big projects). If it fails partway, the log at /tmp/agda-modules.log still has partial profile data — show the error and ask whether to continue with partial results.

Present the printed table in a fenced code block, then a 1-2 sentence summary of the obvious outliers. Don't speculate about causes — the numbers are the deliverable.

Then offer drill-down. After showing the table, ask the user whether they want to profile specific modules in more detail. Suggest the top 3 by time as defaults, but also let them name their own list. If they say yes, go to 3b for each chosen module in turn (no need to ask for the file again — you already have the module name, just locate its source file under the include paths).

3b. Single-module profile

Need a target file. Accept either a path (src/Data/List.agda) or a dotted module name (Data.List) — if given a module name, resolve it by searching the .agda-lib include paths for <Path>.agda, <Path>.lagda.md, etc. Ask the user if unclear.

Use the wrapper. It renders the top-25 table by default; pass TOP=N env var if you want a different cutoff. Prefix with COLD=1 to clear _build/ and .agdai files before running — needed if you want cold-cache numbers or if dependencies changed.

COLD=1 bash ~/.claude/skills/agda-typecheck-profile/scripts/run_definitions_profile.sh <lib-dir> <file-relative-to-lib-dir>

Note: --profile=definitions reports definitions across every module typechecked to handle the target file, not just the target. That's the useful behavior — the slow definition may live in a dependency that gets unfolded here — but mention it so the user isn't confused when they see definitions from modules they didn't name.

Then offer investigation. Ask the user whether to investigate any specific slow definition by finding the actual hot subterm. If yes, read references/investigate-slow.md and follow the procedure there. That procedure starts by pre-authorizing the one-shot Bash pattern for the whole loop, so the user only confirms once.

4. When to clear the cache

• Project-wide mode — the wrapper clears by default. Set SKIP_CLEAN=1 only if you know what you're doing.
• Single-module mode — clear manually before the first run if you want cold-cache numbers. Don't clear between runs during an investigation; only the edited module needs re-typechecking and dependency interfaces should stay warm.

Cached runs mostly report Miscellaneous time (interface deserialization) and are useless for absolute comparisons.

Reducing permission prompts

Both wrapper scripts are invoked as bash ~/.claude/skills/agda-typecheck-profile/scripts/run_*_profile.sh .... A single allowlist pattern per wrapper covers every invocation regardless of arguments. Suggest these entries (in .claude/settings.local.json) the first time you use the skill in a project:

{
  "permissions": {
    "allow": [
      "Bash(bash ~/.claude/skills/agda-typecheck-profile/scripts/run_modules_profile.sh:*)",
      "Bash(bash ~/.claude/skills/agda-typecheck-profile/scripts/run_definitions_profile.sh:*)"
    ]
  }
}

The investigation workflow (references/investigate-slow.md) lists the additional entries needed for that loop (cp, mv, git diff, git checkout --) and instructs Claude to add them before starting the first iteration.

Note on ~: Claude Code matches permission patterns as literal strings against the command — ~ is not expanded before matching. Always invoke the wrapper as bash ~/.claude/skills/agda-typecheck-profile/scripts/... (the shell expands ~ at exec time); don't pre-resolve it to an absolute path, or the allowlist entry won't match and you'll get prompted on every iteration. If the user's skill is installed somewhere other than ~/.claude/skills/, adapt both the invocation and the allowlist entry consistently.

Output formats

Project-wide:

Module                                Time  Lines  ms/line
--------------------------------  --------  -----  -------
Network.Leios                     62,355ms    392   159.07
Leios.Linear                       4,763ms    316    15.07
...
Total: 100,297ms across 25 modules

Single-module:

Definition                           Time
-----------------------------------  ----
Leios.VRF.LeiosVRF.Dec-canProduceEB  69ms
Leios.VRF.LeiosVRF.Dec-canProduceIB  69ms
...
Total: 21,550ms across 25 definitions

Single-definition (investigation mode) — run_definitions_profile.sh <lib> <file> <def> prints one line:

Axiom.Set.Map.dom-∪⁺  1,234

Tab-separated; easy to parse or diff between iterations.

Interpretation notes

A few things worth mentioning if the user asks:

• Miscellaneous covers typechecking work Agda can't attribute to a single entry (deserialization, interface loading, elaboration at module boundaries). The table excludes it; the gap between the summary total and the sum of table rows tells you its share.
• ms/line is a crude metric. A module with heavy instance search or unification in a few definitions will have much higher ms/line than one with many simple definitions. Treat high ms/line as a hint to investigate, not proof of a problem.
• Cold-cache numbers only. Without clearing the cache, you're measuring deserialization, not typechecking.
• Variance. Expect 5-10% run-to-run variance. A measured "improvement" smaller than that isn't signal.