Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

The Compiler and LSP

A working day with Argon spends most of its time in two surfaces: the ox CLI in a terminal and the language server in your editor. This chapter is a tour of both — what they do, what flags matter, and what to reach for when something is wrong.

The ox CLI in one page

Eight subcommand families. Most are familiar.

CommandPurposeNotable flags
ox checkType-check + meta-property + package constraints--reason (opt-in reasoning)
ox buildCompile to kernel types + Datalog
ox testRun test blocks--filter <pat>, --verbose, --timings
ox query <name>Run a named query--explain, --standpoint, --as-of-valid, --as-of-tx, --fork, --limit, --format, --arg KEY=VALUE
ox mutate <name>Run a named mutation--principal, --dry-run, --explain, --valid-at, --idempotency-key, --standpoint, --fork, --arg KEY=VALUE
ox diagram [<name>]Render diagrams to SVG / OntoUML--format svg|ontouml, -o <dir> (default diagrams/)
ox install / update / publish / auditPackage managementper-command
ox show <kind>Schema introspection--filter, --sort, --lattice, --limit, --format

A few habits that pay off:

ox check for the editor loop, ox check --reason before commits. The reasoning step is slower; not every save needs it. Save reasoning for moments where you want the invariants verified.

--explain whenever a query result surprises you. It produces a why-tree showing every rule firing that contributed to the result. Most “why is this happening” questions evaporate after one --explain.

--dry-run for any mutation you have not seen run before. It exercises the preconditions and shows you which events would be emitted, without committing. Combine with --explain to see the reasoning chain.

Diagnostic codes

Argon’s diagnostics use a structured naming scheme. Every diagnostic has a code of the form OE/OW/OI + four digits:

  • OE — Errors. The build fails.
  • OW — Warnings. The build proceeds; the issue is flagged.
  • OI — Info. Hints; nothing is wrong.

A few codes you will see often:

CodeMeaning
OE0101Unresolved name
OE0202Property type mismatch
OE0203Non-exhaustive match
OE0207Mixed strict/defeasible strength on the same head

Run ox explain <code> for a longer explanation:

$ ox explain OE0203
   OE0203 — Non-exhaustive match expression.

   A match has no wildcard arm and no guardless arm covering every
   possible subtype of the scrutinee. Every input must reach a body.

   Fix: add a `_ => …` wildcard arm, or add an arm that covers the
   missing subtypes.

The codes are designed to be lookuppable: knowing the code is enough to reach the explanation, the relevant chapter, and (eventually) the relevant decision rationale.

Note: an ox doc command — Argon’s analogue of cargo doc — is on the roadmap. Until it lands, ox explain <code> is the canonical surface for diagnostic-code lookup.

The LSP and editor extension

The language server (ox-lsp) and the VS Code / Cursor extension together provide the editor surface. Open an .ar file in your editor; the extension launches ox-lsp automatically.

Capabilities you will lean on:

  • Hover — type, decidability tier, governing decision, links to documentation. Hover over any identifier to see its full classification.
  • Inlay hints — inferred types, computed metatype values, implicit consequences on rules. Useful for reading rule code; the implicit => FactDerived(H) shows up as a ghosted suffix.
  • Go-to definition / Find references — works across packages.
  • Rename — refactor across the workspace.
  • Code actions — quick fixes for the common diagnostics. OE0203 (non-exhaustive match) inserts a wildcard arm; OE0101 (unresolved name) suggests an use import; OW0813 (deprecated .ol extension) suggests the .ar rename.
  • Diagnostics in real timeOE/OW/OI surfacing as you type; the editor shows them in the gutter and the problems panel.
  • Semantic tokenskind / subkind / role / phase tagged distinctly so syntax highlighting is metatype-aware.
  • Palette commandsArgon: Run query, Argon: Run mutation, Argon: Render diagram, Argon: Run tests. The full ox surface, accessible without leaving the editor.

The InfoView panel

A live-updating side panel that surfaces what the compiler knows about the file under the cursor. Open it from the palette (Argon: Open InfoView) and dock it next to your editor.

Three modes:

  • Module Dashboard — a bird’s-eye view of the active file: every concept, every rule, every test, with their decidability tiers and meta-property classifications. A good starting place when reading an unfamiliar package.
  • Symbol — focuses on whatever symbol your cursor is on. Shows the type, the metatype, the subtype lineage, the rules that mention it, and the tests that exercise it.
  • Metatype — shows the meta-property calculus result for a given metatype. Which axes? Which axiom obligations? Which axes are settled, which are open?

You will find yourself in the Module Dashboard when you arrive in a new file, then drill into Symbol when something specific puzzles you, then jump to Metatype when you want to understand why an item classifies the way it does.

Salsa-incremental everything

Behind the scenes, the compiler is built on Salsa — an incremental computation framework. When you change a file, only the things that depend on what changed are recomputed. In practice this means:

  • The editor loop is fast. Most ox check invocations through the LSP are sub-100ms.
  • ox check --reason reasons over only the rules whose dependencies changed; previously-saturated rules cache.
  • The InfoView updates incrementally. Hover after a change shows the new classification.

You do not configure any of this. It is the default mode of the compiler.

When something is wrong

A small triage tree:

The editor reports a diagnostic you do not understand. ox explain <code>. If the explanation does not name the issue, the diagnostic might be missing — file an issue against the project tracker.

ox check is slow. Run with OX_LOG=trace to see what stages take the time. Most slowdowns are reasoning-heavy rules; consider whether @[budget(N)] on the offending rule helps.

A mutation does not fire. --dry-run --explain. The output shows preconditions and event sequencing; one of them will be off.

A query returns wrong results. --explain. The why-tree shows the rules that fired (and the rules that did not fire when you expected them to).

The LSP stops responding. The output channel under Argon in the editor’s output view shows the LSP’s logs. A restart from the palette (Argon: Restart LSP) usually works.

Exercising the CLI in isolation

The _catalog/cli-ox-*/ workspace family ships one minimal workspace per CLI subcommand, so you can run a single command against a focused fixture and watch the output:

  • cli-ox-check/{passes,fails-OE0101,fails-OE0203,fails-OE0207,fails-OE0805}/ — pinned regressions for the four most common type-check errors.
  • cli-ox-test/{passes,test-with-expect,test-with-assert,multi-frame,negative-no-tests}/ — runs ox test with each test surface in isolation.
  • cli-ox-query/{simple,with-explain,with-standpoint,with-as-of-valid,with-fork}/ — exercises each query flag against a small fixture.
  • cli-ox-mutate/{simple,with-explain,with-dry-run,with-principal,with-idempotency-key}/ — same for mutations.
  • cli-ox-diagram/{single,all,format-ontouml,with-from,negative-bad-source}/ — diagram render paths.

For the LSP surface, _catalog/lsp-{hover,inlay,goto-def,find-refs,rename,code-action}/{minimal,…}/ workspaces ship reproducer source under src/prelude.ar and an EXPECTED.md describing the LSP response the user should see when the file is opened in an ox-lsp-aware editor.

Summary

The CLI is the compile/run surface; the LSP is the editing surface; the InfoView panel is the inspection surface. Diagnostic codes are structured (OE/OW/OI + four digits) and ox explain produces longer explanations. Salsa makes the editor loop incremental. The book’s discipline — ox check in the loop, ox check --reason before commits, --explain whenever something surprises you — produces a fast, debuggable workflow.