Add Agda typecheck skill + SessionStart hook for Claude Code on the web#1220
Add Agda typecheck skill + SessionStart hook for Claude Code on the web#1220williamdemeo wants to merge 3 commits into
Conversation
There was a problem hiding this comment.
Pull request overview
Adds Claude Code (web) configuration to provision Nix in remote sessions and document how to typecheck Agda modules via the project’s Nix flake, enabling in-session verification of .lagda.md / .agda edits without changing spec code, build, or CI.
Changes:
- Adds an Agda typecheck skill documenting the
nix develop --command agda <file>workflow and common error triage. - Adds a Claude
SessionStarthook to install/configure Nix + caches and pre-warmnix developin remote (web) sessions. - Wires the hook via
.claude/settings.json.
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 2 comments.
| File | Description |
|---|---|
.claude/skills/agda-typecheck/SKILL.md |
Documents the Nix-flake-based Agda typechecking workflow and local quality gate. |
.claude/settings.json |
Registers a SessionStart hook to run the provisioning script. |
.claude/hooks/session-start.sh |
Installs/configures Nix (flakes + caches) and warms the dev shell for agda in remote sessions. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| grep -q 'cache.iog.io' "$NIX_CONF" 2>/dev/null || cat >> "$NIX_CONF" <<'CONF' | ||
| substituters = https://cache.iog.io https://cache.nixos.org/ | ||
| trusted-public-keys = hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ= cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= | ||
| CONF |
There was a problem hiding this comment.
Fixed in cfa8c63 — switched to extra-substituters / extra-trusted-public-keys so the caches/keys are appended without clobbering any existing config (the cache.iog.io guard keeps it idempotent).
Generated by Claude Code
| if [ -n "${CLAUDE_ENV_FILE:-}" ] && [ -e "$HOME/.nix-profile/etc/profile.d/nix.sh" ]; then | ||
| echo ". \"$HOME/.nix-profile/etc/profile.d/nix.sh\"" >> "$CLAUDE_ENV_FILE" | ||
| fi |
There was a problem hiding this comment.
Fixed in cfa8c63 — the append is now guarded by a grep -qF, so re-running the hook (e.g. on session resume) no longer duplicates the line.
Generated by Claude Code
williamdemeo
force-pushed
the
claude/agda-skill-and-session-hook
branch
from
74b593c to
336ea9d
Compare
The project typechecks only via its Nix flake; there is no system agda. To make Agda checking available to Claude Code (this repo, web sessions): - .claude/skills/agda-typecheck/SKILL.md: documents the `nix develop --command agda <file>` workflow, common Agda error triage, and the project quality gate. - .claude/hooks/session-start.sh + .claude/settings.json: a SessionStart hook that installs nix, enables flakes, points at the cache.nixos.org/cache.iog.io substituters (keys from ci.yml), and pre-warms `nix develop`. Guarded by CLAUDE_CODE_REMOTE; non-fatal and clearly logged if it can't proceed. NETWORK PREREQUISITE: the hook needs the environment network policy to allow nixos.org, cache.nixos.org, cache.iog.io and github.com. The default policy in this session returns 403 for nixos.org and cache.iog.io, so the hook currently logs that and exits 0 without provisioning. Once the policy permits those hosts, the toolchain installs and is cached for subsequent sessions. https://claude.ai/code/session_0174ZBS1RKAGSbBXDsESUwoA
Enabling flakes keyed only on the presence of any experimental-features line, so a bare `experimental-features = nix-command` would skip enabling flakes and `nix develop` would still fail. Check for `flakes` specifically and append via extra-experimental-features, which doesn't clobber an existing setting. https://claude.ai/code/session_0174ZBS1RKAGSbBXDsESUwoA
williamdemeo
force-pushed
the
claude/agda-skill-and-session-hook
branch
from
336ea9d to
2eae3d4
Compare
…append - substituters/trusted-public-keys override (last-one-wins) any existing config; switch to extra-substituters/extra-trusted-public-keys so the caches/keys are added without clobbering the environment's configuration. - the $CLAUDE_ENV_FILE append was unconditional, so re-running the hook (e.g. on session resume) duplicated the line; guard it with a grep so it's idempotent. https://claude.ai/code/session_0174ZBS1RKAGSbBXDsESUwoA
|
Closing this in favor of a lighter-weight approach, per review feedback — thanks, Carlos. The consensus is that a repo-level SessionStart hook is the wrong tool here: it would make every contributor's web session install Nix, and — as it turns out — the upstream installer doesn't run cleanly as root in the managed container anyway. In testing it consistently failed with: so the hook couldn't actually provision the toolchain as written. Replacement, split by where you actually work:
So the Generated by Claude Code |
…ev shell Adds a short "Type-checking while you work" subsection: enter `nix develop` and run `agda <file>` (or `nix develop --command agda <file>`) to type-check a single module — much faster than `nix build` for iterating on a proof — plus a direnv tip to put the toolchain on PATH and launch your editor/agent tooling from that shell. This is the lightweight, no-repo-machinery alternative to a SessionStart hook (see #1220). https://claude.ai/code/session_0174ZBS1RKAGSbBXDsESUwoA
…ev shell Adds a short "Type-checking while you work" subsection: enter `nix develop` and run `agda <file>` (or `nix develop --command agda <file>`) to type-check a single module — much faster than `nix build` for iterating on a proof — plus a direnv tip to put the toolchain on PATH and launch your editor/agent tooling from that shell. This is the lightweight, no-repo-machinery alternative to a SessionStart hook (see #1220). https://claude.ai/code/session_0174ZBS1RKAGSbBXDsESUwoA
Adds Claude Code (web) configuration so cloud sessions can typecheck Agda through the project's Nix flake. Tooling only — no changes to the specification, the build, or CI. Only
.claude/files are added.What this adds
.claude/skills/agda-typecheck/SKILL.md— a skill documenting thenix develop --command agda <file>workflow, common Agda error triage, and the project's Agda quality gate (explicit type signatures, named lemmas,whereoverlet, helper functions overwith, kramdown{.AgdaFunction}spans in prose, no generated artifacts staged, etc.)..claude/hooks/session-start.sh+.claude/settings.json— aSessionStarthook that, in a remote (web) session, installs nix, enables flakes, configures thecache.nixos.org/cache.iog.iosubstituters (public keys taken from.github/workflows/ci.yml), and pre-warmsnix developsonix develop --command agda <file>is ready. It is guarded byCLAUDE_CODE_REMOTE, idempotent, and non-fatal: if it can't proceed it logs a clear message and exits 0 without blocking session startup.Why
Cloud sessions start from a fresh clone with no system
agda(the project pins Agda and its libraries via the flake). Without this, Claude Code on the web can't machine-check.lagda.mdedits. With it, edited modules can be typechecked in-session before pushing.Network prerequisite
The hook needs the environment's Network access to allow
nixos.organdcache.iog.io. Everything else it uses (*.nixos.org, GitHub) is already in the Trusted default allowlist. Configure this per environment (Custom network access + those two domains, keeping the default package-manager list). Until then the hook logs the missing hosts and skips — harmless.Notes for reviewers
master.Checklist
CHANGELOG.md(n/a — no spec changes)🤖 Generated with Claude Code
https://claude.ai/code/session_0174ZBS1RKAGSbBXDsESUwoA
Generated by Claude Code