# Edda — agent setup recipe

You are setting up an Edda project for a user, end to end. Edda is a verified
language that is NOT in your training data — do not guess syntax by analogy to
Rust, Swift, Go, or OCaml; it will not compile. Work these steps in order. The
end state is a small, built, contract-verified project the user can keep as a
reusable starter template.

## 1. Read the reference (before writing any Edda)
Fetch https://edda-lang.org/AGENTS.md and load it in full — the canonical,
always-on language reference. Fetch https://edda-lang.org/guide.md on demand for
special operations (verification tooling, property testing, capability
typestate, distribution). Do not write a line of Edda until AGENTS.md is in
context.

## 2. Install the toolchain
The prebuilt installer bundles the `edda` binary, its runtime, and a vendored
`std` + `runes` — nothing else to fetch, no environment variable to set. Pick
your host:
  - Windows (PowerShell), the verified platform:
      irm https://raw.githubusercontent.com/edda-lang/edda-bootstrap/main/install.ps1 | iex
  - Linux / macOS (archives still rolling out; if there is no release asset for
    your platform yet the installer says so — fall back to a source build per
    the edda-bootstrap README):
      curl -fsSL https://raw.githubusercontent.com/edda-lang/edda-bootstrap/main/install.sh | bash
The installer adds `edda` to PATH, but your CURRENT shell won't see it yet.
Start a new shell, or call the full path for the first check:
      edda version                        (new shell)
      ~/.edda-bootstrap/bin/edda version  (same shell; edda.exe on Windows)
Expect `edda (bootstrap-rust) <version>` and your host target.

## 3. Set up YOUR harness (its native config, not just a dropped file)
Identify which coding agent you are, then create that harness's native project
config so the reference auto-loads every session. Place AGENTS.md at the repo
root in every case — the cross-tool standard 30+ agents read — then add the
harness-native piece:
  - Claude Code:    CLAUDE.md whose first line is  @AGENTS.md  (plus a .claude/ dir).
  - Cursor:         AGENTS.md at root (read directly).
  - OpenAI Codex:   AGENTS.md at root.
  - GitHub Copilot: .github/copilot-instructions.md that points at AGENTS.md.
  - Gemini CLI:     AGENTS.md at root (GEMINI.md also read if present).
  - Windsurf:       .windsurfrules that points at AGENTS.md.
  - Unknown harness: place AGENTS.md at root and create whatever project-memory
    file your harness auto-loads, pointing it at AGENTS.md. Degrade gracefully —
    if there is no such concept, AGENTS.md at root is enough.

## 4. Install the Edda skill (the special-operations tier)
Fetch https://edda-lang.org/skill.md — a short, agent-agnostic skill that points
you at the authoring guide and the compiling examples for anything past everyday
syntax. Render it in your harness's native skill format:
  - Claude Code:   write it to  .claude/skills/edda-authoring/SKILL.md
  - Other harness: save it where your harness discovers skills, or keep it as a
    project doc and read it when a task needs special operations.
Everyday syntax stays in AGENTS.md; the skill is the deeper tier on top.

## 5. Reading-discipline hooks — ASK the user first; never install silently
Edda can enforce a reading discipline mechanically: before editing a .ea file
you first read the compiler-emitted index.toon structure maps down its directory
chain, and oversized reads are capped to a bounded span. Two scripts do it —
toon_gate.py (the gate) and toon_ledger.py (records which maps you have read).

Be honest when you ask: these are currently Claude-Code-shaped (PreToolUse /
PostToolUse hooks that emit JSON deny decisions) and need Python on PATH. They
earn their keep on large, multi-directory codebases and are nearly inert on a
small starter. Offer them only if your harness supports equivalent pre-tool
hooks. Present this and WAIT for a yes / no:

  Optional: I can install two hook scripts that make me read Edda's structure
  maps before editing source and stop me from reading whole oversized files at
  once. Upside: I stay grounded and spend fewer tokens on big codebases. Cost:
  an extra read step per edit, Python on PATH, and a one-time settings change.
  Install them? (yes / no)

If yes: fetch https://edda-lang.org/hooks/toon_gate.py and
https://edda-lang.org/hooks/toon_ledger.py, wire toon_gate to your pre-tool hook
and toon_ledger to your post-tool hook (treat a non-zero gate decision as deny),
and set EDDA_TOON_SUBTREES to your own source directory (e.g. `src`) — the
default targets a monorepo, not a single-package project. If no: skip; nothing
else changes.

## 6. Scaffold a small, real project
Create a package that builds clean and teaches the contract loop — one
capability, one requires/ensures. This matches https://edda-lang.org/get-started.

  package.toml:
    [package]
    name = "hello"
    version = "0.1.0"
    root_namespace = "hello"

    [build]
    default_target = "x86-64-windows-msvc"

  Set default_target to YOUR host triple in dash form (x86-64-linux-gnu,
  aarch64-macos-darwin, ...). `edda version` prints the same triple with
  underscores (x86_64-windows-msvc); it is the same target — package.toml uses
  the dash form.

  src/main.ea:
    module hello.main

    import std.io.stream

    function non_negative(x: i64) -> i64
        requires x >= 0
        ensures result >= 0
    {
        return x
    }

    public function main(out: Stdout) -> ()
        with {out}
    {
        let y = non_negative(7)
        out.print_line(f"non_negative(7) = {y}")
    }

Work from a neutral directory — NOT a sibling of a local edda-stdlibs or edda
monolith checkout, or the compiler may adopt that sibling as the active std and
shadow the bundled one.

## 7. Build, run, and prove verification is real
From the project directory:
      edda check     fast type-only loop
      edda build     typecheck + discharge every contract + emit a binary
      edda run       build, then execute (prints: non_negative(7) = 7)
Now delete the `requires x >= 0` line and run `edda build` again. The compiler
refuses and hands back a concrete counter-example (x = -1) instead of compiling
a bug. Put the line back; the build is green. That refusal is the point of
Edda — the build is the source of truth.

## 8. Leave a reusable template
Tell the user in plain words: this directory is a clean, contract-verified Edda
starter they can copy for any future project, or re-run this recipe to
regenerate. (A `git clone` starter, edda-lang/edda-starter, is planned as a
shortcut.) You are done when `edda build` is green.