docs / Miri for Agents / The Loop

The Loop

There is one routine to follow, and the miri-lang pack gives it to the agent word for word. This is that section of the pack:

This is the one loop the compiler’s documentation recommends; everything else defers to it. Loop: miri check --format json → edit → miri test (or miri run). Iterate until clean.

  1. miri check — miri check myfile.mi --format json. Each diagnostic has a code, a help and, where one exists, a repair with its edits. A diagnostic without a repair is one you edit yourself.
  2. Edit — miri fix myfile.mi --apply --yes writes every recorded repair in one call. Everything else is an ordinary edit; in a file already in canonical layout, miri patch myfile.mi --replace-in-fn name --old text --new text makes a scoped edit and re-checks before anything reaches disk.
  3. miri test / miri run — miri test --dir <DIR>, miri run myfile.mi; both take --format json. Only a run finds a fault the frontend cannot see.

The loop, step by step

Here is a small program with two mistakes an agent coming from another language might make: && instead of and, and changing a value declared with let.

tally.mi
// Sums the scores between 5 and 10. Written with two mistakes for the compiler to repair.

use system.collections.list

fn main()
    let total = 0
    let scores = List([7, 9, 4])
    for s in scores
        if s > 5 && s < 10
            total = total + s
    println(f"total {total}")

Check. The compiler reports the first problem as JSON. Look for code, help and repair:

$ miri check tally.mi --format json
{
  "schemaVersion": 1,
  "ok": false,
  "command": "check",
  "diagnostics": [
    {
      "severity": "error",
      "code": "MER_PAR_020",
      "message": "'&&' is not a valid operator in Miri",
      "path": "tally.mi",
      "line": 9,
      "column": 18,
      "length": 2,
      "help": "Miri spells logical and as the word `and`: `if a and b`.",
      "fixSafety": "local-edit",
      "repair": {
        "id": "word-operator",
        "summary": "Write `&&` as `and`.",
        "edits": [
          {
            "path": "tally.mi",
            "start": 219,
            "end": 221,
            "replacement": "and"
          }
        ]
      },
      "related": []
    }
  ],
  "exitCode": 1,
  "durationMs": 0
}
exit status 1

Fix. The diagnostic carries a repair, so miri fix can write it:

$ miri fix tally.mi --apply --yes
Applied repairs to tally.mi
exit status 0

Check again. With the syntax fixed, the compiler can now see the next mistake, and it has a repair too:

$ miri check tally.mi --format json
{
  "schemaVersion": 1,
  "ok": false,
  "command": "check",
  "diagnostics": [
    {
      "severity": "error",
      "code": "MER_TYP_042",
      "message": "Cannot assign to immutable variable 'total'",
      "path": "tally.mi",
      "line": 10,
      "column": 13,
      "length": 17,
      "fixSafety": "local-edit",
      "repair": {
        "id": "let-to-var",
        "summary": "Declare the variable with `var` so it can be reassigned.",
        "edits": [
          {
            "path": "tally.mi",
            "start": 135,
            "end": 138,
            "replacement": "var"
          }
        ]
      },
      "related": []
    }
  ],
  "exitCode": 1,
  "durationMs": 23
}
exit status 1

Fix, check, run.

$ miri fix tally.mi --apply --yes
Applied repairs to tally.mi
exit status 0
$ miri check tally.mi --format json
{
  "schemaVersion": 1,
  "ok": true,
  "command": "check",
  "diagnostics": [],
  "exitCode": 0,
  "durationMs": 18
}
exit status 0
$ miri run tally.mi
total 16
exit status 0

Some problems hide others: a syntax error stops the compiler before it checks types. That is why the loop is a loop. Fix what is reported, check again, and stop when ok is true.