For agents

Machine-readable output

Add --json to a brine command and it prints one JSON object per line on stdout instead of text for people. Errors have the same shape from every command, many carry exact text fixes, and the exit code tells you whether the command succeeded. Everything on this page was printed by Brine 0.4.0.

brine check --json
brine check --json src/main.br
brine test --json

Rules for every command

One object per line. Each line is a complete JSON object. Read the output line by line and parse each one; don’t parse it as one document.
stdout only. JSON goes to stdout. With --json, the status lines (Built, Checked, …) are not printed.
Deterministic. The same input gives the same lines in the same order.
Exit codes carry the result:

Exit code	Meaning
`0`	success: the code compiled, every test passed, nothing to format
`1`	compile errors, a failed test, or files that `fmt --check` would change
`2`	the command couldn’t run: a missing file, an unknown error code, bad arguments
`101`	`brine run`: the program panicked
other	`brine run`: the program’s own exit code (`main` returned an `int`, or called `exit`)

Positions are 1-based. line and column mark the first character of the span; end_line and end_column mark the position just after its last character. Columns count characters (Unicode code points), not bytes.
Paths in file are as Brine displays them: relative to the current folder (src/main.br, race.br).

Diagnostics

Every compile error is a diagnostic object, whichever command found it (check, build, run, test, fmt). This is the data race from Race freedom:

brine check --json race.br

{"severity":"error","code":"E0501","message":"cannot assign to `total` inside a `par` body","file":"race.br","line":5,"column":9,"end_line":5,"end_column":14,"label":"would be a data race","related":[],"notes":["`total` is shared by all parallel iterations"],"help":["a `par for` may only write `total[i]` (its own element); to combine values use `par sum(...)`, `par [...]`, or a sequential loop"],"fixes":[]}

The same object, spread out:

{
  "severity": "error",
  "code": "E0501",
  "message": "cannot assign to `total` inside a `par` body",
  "file": "race.br",
  "line": 5,
  "column": 9,
  "end_line": 5,
  "end_column": 14,
  "label": "would be a data race",
  "related": [],
  "notes": ["`total` is shared by all parallel iterations"],
  "help": ["a `par for` may only write `total[i]` (its own element); to combine values use `par sum(...)`, `par [...]`, or a sequential loop"],
  "fixes": []
}

Field	Type	Meaning
`severity`	string	`"error"` for everything in this page; read it rather than assuming
`code`	string	the error code; `brine explain <code>` explains it
`message`	string	the one-line summary (the text after `error[E0501]:`)
`file`, `line`, `column`, `end_line`, `end_column`	string, numbers	the primary span: the code at fault
`label`	string	the note under the primary span (`^^^^^ would be a data race`)
`related`	array	other spans that explain the error, each `{file, line, column, end_line, end_column, label}`
`notes`	array of strings	facts about the error; for proof failures, what the prover knew and needed
`help`	array of strings	how to fix it
`fixes`	array	exact edits that fix it; see Fixes

All the fields are always present, even when the arrays are empty. The text output of brine check shows the same information: each notes entry is a = note: line, each help entry a = help: line, and related spans are the ones underlined with -.

Proof failures

A proof failure has the same shape. related points at the contract that couldn’t be proven:

brine check --json proof.br

{"severity":"error","code":"E0601","message":"cannot prove the precondition of `last`","file":"proof.br","line":7,"column":11,"end_line":7,"end_column":19,"label":"this call might violate `requires len(xs) >= 1`","related":[{"file":"proof.br","line":2,"column":14,"end_line":2,"end_column":26,"label":"precondition declared here"}],"notes":["with the values used here, this is always false"],"help":["add an `assert` before the call to check it at runtime, or a `requires` to this function so its callers must prove it"],"fixes":[]}

When the prover knew some facts but not enough, notes lists them and the goal. This is clamp with its requires lo <= hi missing, which gives one error per return it can’t prove:

fn clamp(x: int, lo: int, hi: int) -> int:
    ensures lo <= result <= hi
    if x < lo:
        return lo
    if x > hi:
        return hi
    return x

fn main():
    print(clamp(5, 0, 10))

{"severity":"error","code":"E0602","message":"cannot prove the postcondition of `clamp`","file":"ens.br","line":4,"column":9,"end_line":4,"end_column":18,"label":"this might return without `lo <= result <= hi` being true","related":[{"file":"ens.br","line":2,"column":13,"end_line":2,"end_column":31,"label":"postcondition declared here"}],"notes":["known facts here: lo > x","to prove: hi >= lo"],"help":["strengthen the function's `requires`, add a loop `invariant`, or check the claim with `assert` before returning"],"fixes":[]}
{"severity":"error","code":"E0602","message":"cannot prove the postcondition of `clamp`","file":"ens.br","line":6,"column":9,"end_line":6,"end_column":18,"label":"this might return without `lo <= result <= hi` being true","related":[{"file":"ens.br","line":2,"column":13,"end_line":2,"end_column":31,"label":"postcondition declared here"}],"notes":["known facts here: x >= lo, x > hi","to prove: hi >= lo"],"help":["strengthen the function's `requires`, add a loop `invariant`, or check the claim with `assert` before returning"],"fixes":[]}

The notes start with known facts here: and to prove:. Here the goal hi >= lo is exactly the missing requires. See Fixing proof failures.

Fixes

Many errors carry one or more edits that fix them. Each fix replaces the text from (line, column) up to (end_line, end_column) with replacement:

fn main():
    let a = true
    let b = false
    if a && b:
        print("both")

{"severity":"error","code":"E0105","message":"`&&` is not an operator in brine","file":"op.br","line":4,"column":10,"end_line":4,"end_column":12,"label":"use `and`","related":[],"notes":[],"help":[],"fixes":[{"file":"op.br","line":4,"column":10,"end_line":4,"end_column":12,"replacement":"and","message":"replace with `and`"}]}

Field	Type	Meaning
`file`, `line`, `column`, `end_line`, `end_column`	string, numbers	the text to replace
`replacement`	string	the new text
`message`	string	what the fix does, for showing to a person

When the start and end are the same, the fix is an insertion. A missing ref at a call:

{"severity":"error","code":"E0402","message":"parameter `xs` is a `ref`; pass the argument with `ref`","file":"stage2.br","line":6,"column":13,"end_line":6,"end_column":15,"label":"the callee may modify this","related":[],"notes":[],"help":["passing by reference is always visible at the call site in brine"],"fixes":[{"file":"stage2.br","line":6,"column":13,"end_line":6,"end_column":13,"replacement":"ref ","message":"add `ref`"}]}

Errors that came with fixes while this page was written:

Code	Fix
E0105	`&&` → `and` (and the other operators from other languages)
E0114	`else if` → `elif`
E0201	a misspelled name → the closest match (`lenn` → `len`)
E0337	insert the missing type (`: int`) under `--typed`
E0402	insert `ref` before an argument

The compiler reports syntax errors before type errors, so applying one round of fixes can uncover more. Check again after applying them.

Errors without a location

When a command can’t run at all, it prints an object with only severity, code (always null) and message, and exits with status 2:

brine check --json nope.br

{"severity":"error","code":null,"message":"file `nope.br` not found"}

brine check

On success, check prints one object and exits with status 0:

{"ok":true,"checks_proven":0,"checks_remaining":1}

Field	Type	Meaning
`ok`	boolean	`true`
`checks_proven`	number	runtime checks (bounds, overflow, division) the prover removed
`checks_remaining`	number	runtime checks that stay in the program

On failure it prints one diagnostic per error and exits with status 1. There is no {"ok":false} line; use the exit code, or look for objects with a severity.

--report adds one object per remaining runtime check before the summary:

brine check --json --report

{"runtime_check":"overflow check","location":"src/main.br:14:24","code":"i * i"}
{"ok":true,"checks_proven":0,"checks_remaining":1}

Field	Type	Meaning
`runtime_check`	string	the kind of check, such as `"overflow check"`
`location`	string	`file:line:column`
`code`	string	the source text being checked

brine build

On success, build prints the path of the binary:

{"built":"target/dev/hello.exe"}

On failure it prints diagnostics and exits with status 1, like check.

brine run

run builds and then runs the program. With --json, compile errors are diagnostics as above. When the build succeeds, it prints no JSON of its own: your program’s stdout and stderr pass through unchanged, and the exit code is the program’s.

brine run --json panic.br

panic: index 3 is out of bounds for an array of length 3
  --> panic.br:4:11

Because program output and diagnostics share stdout, a tool that needs to tell them apart should run brine build --json and then the binary it names.

brine test

test prints one object per test, in the order the tests appear in the source, after they have all finished:

fn double(x: int) -> int:
    return x * 2

fn main():
    print(double(21))

test "doubles":
    assert double(2) == 4

test "prints then fails":
    print("about to check")
    assert double(3) == 7

test "panics":
    let xs: [int] = []
    print(xs[0])

brine test --json failtest.br

{"test":"doubles","ok":true,"seconds":0.023,"output":""}
{"test":"prints then fails","ok":false,"seconds":0.026,"output":"about to check\n\npanic: assertion failed: double(3) == 7\n  --> failtest.br:12:5\n"}
{"test":"panics","ok":false,"seconds":0.015,"output":"\npanic: index 0 is out of bounds for an array of length 0\n  --> failtest.br:16:11\n"}

Field	Type	Meaning
`test`	string	the name from `test "...":`
`ok`	boolean	whether it passed
`seconds`	number	how long it took, to the millisecond
`output`	string	everything the test printed (stdout, then stderr), including the panic message and location

There is no summary line; count the objects. The exit code is 0 if every test passed and 1 otherwise. If the tests don’t compile, test prints diagnostics instead and exits with status 1. A filter works as usual: brine test --json failtest.br doubles prints only the first line.

brine explain

brine explain --json E0601

{"code":"E0601","title":"precondition not proven","explanation":"The function's `requires` clause must hold at every call, and the compiler\nmust be able to prove it from what it knows at the call site. Rules can't be\nbroken, so an unproven claim is an error, not a runtime check.\n\nFix it by giving the prover the facts it needs, for example:\n\n    if 0 <= i and i < len(xs):     # the call is only made when it's safe\n        print(get(xs, i))\n\n    assert 0 <= i < len(xs)        # checked at runtime, then known to the prover\n    print(get(xs, i))\n\nor by adding a `requires` to the calling function, which moves the obligation\nto its callers. The error lists the facts the prover knew and the claim it\nneeded.\n"}

Field	Type	Meaning
`code`	string	the error code
`title`	string	a short name for the error
`explanation`	string	the full explanation, as Markdown-like text with `\n` line breaks

With no code, brine explain --json lists every code, one {code, title} object per line:

{"code":"E0101","title":"invalid literal"}
{"code":"E0102","title":"unterminated string"}
{"code":"E0103","title":"bad indentation"}

An unknown code prints an error without a location and exits with status 2.

Other commands

Command	Output
`brine new --json hello`	`{"created":"hello"}`
`brine fmt --json`	nothing on success; files are rewritten
`brine fmt --check --json`	`{"unformatted":"ugly.br"}` for each file that needs formatting; exit code 1 if there are any
`brine version --json`	`{"version":"0.4.0"}`
`brine doctor --json`	one `{"check":..., "ok":..., "detail":...}` per check

{"check":"brine","ok":true,"detail":"0.4.0 (windows x86_64)"}
{"check":"C compiler","ok":true,"detail":"gcc — gcc (MinGW-W64 x86_64-ucrt-posix-seh, built by Brecht Sanders, r1) 16.2.0"}
{"check":"parallelism","ok":true,"detail":"32 hardware threads"}
{"check":"local sockets","ok":true,"detail":"needed for `brine run --ranks`"}
{"check":"build + run","ok":true,"detail":"compiled and ran a parallel program"}

The optional debugger line of the text output isn’t part of the JSON.

Consuming the output

With jq

# file:line:column: code message, one per error
brine check --json | jq -r 'select(.severity == "error") | "\(.file):\(.line):\(.column): \(.code) \(.message)"'

# the names of failing tests
brine test --json | jq -r 'select(.ok == false) | .test'

# group errors by code
brine check --json | jq -s 'map(select(.code)) | group_by(.code) | map({code: .[0].code, count: length})'

With Python

This script applies every machine fix that brine check offers, checks again until no fixes are left, and prints what remains for a person (or an agent) to fix:

"""Apply the machine fixes from `brine check --json`, then report what's left."""
import json
import subprocess
import sys

def check(target):
    out = subprocess.run(["brine", "check", "--json", *target],
                         capture_output=True, text=True, encoding="utf-8").stdout
    return [json.loads(line) for line in out.splitlines() if line.strip()]

def apply_fixes(diags):
    edits = {}  # file -> [(line, column, end_line, end_column, replacement)]
    for d in diags:
        for f in d.get("fixes", []):
            edits.setdefault(f["file"], []).append(
                (f["line"], f["column"], f["end_line"], f["end_column"], f["replacement"]))
    for path, fixes in edits.items():
        with open(path, encoding="utf-8", newline="") as fh:
            lines = fh.read().split("\n")
        # last fix first, so earlier positions stay valid
        for line, col, end_line, end_col, text in sorted(fixes, reverse=True):
            head = lines[line - 1][:col - 1]
            tail = lines[end_line - 1][end_col - 1:]
            lines[line - 1:end_line] = [head + text + tail]
        with open(path, "w", encoding="utf-8", newline="") as fh:
            fh.write("\n".join(lines))
    return sum(len(v) for v in edits.values())

target = sys.argv[1:]
# syntax errors come before type errors, so fixing can reveal more fixes
for _ in range(10):
    diags = check(target)
    if not any(d.get("fixes") for d in diags):
        break
    print(f"applied {apply_fixes(diags)} fixes")
for d in diags:
    if d.get("ok"):
        print("ok")
    elif d.get("severity") == "error":
        where = f'{d["file"]}:{d["line"]}:{d["column"]}' if "file" in d else "brine"
        print(f'{where}: {d["code"]}: {d["message"]}')
        for h in d.get("help", []):
            print(f"    help: {h}")

Python string indexes count code points, as brine’s columns do, so the slices line up. Run it on this file, which has five mistakes:

fn add_one(ref xs: [int]):
    xs.push(1)

fn main():
    var xs: [int] = []
    add_one(xs)
    let ready = len(xs) > 0 && xs[0] == 1
    if not ready:
        print("empty")
    else if lenn(xs) == 1:
        print("one")
    let n: float = len(xs)
    print(n)

python brine_fix.py demo.br

applied 2 fixes
applied 2 fixes
demo.br:12:20: E0301: mismatched types
    help: convert explicitly with `float(...)`

The first round fixed the syntax errors (&& and else if); the second fixed the missing ref and the misspelled len. The last error needs a decision, float(len(xs)), so it’s left for you.