Projects & the infs Toolchain

Motivation

infc is a single-file compiler. Given one .inf source file it parses, type-checks, analyses, and emits a WASM binary. That model is fine for self-contained examples, but real codebases need more: a place to declare external .wasm dependencies, a way to express whether a build is meant to produce an executable or a Rocq proof, and a project root that tools can agree on so artifacts land in predictable locations.

infs is the unified toolchain entry point that provides all of this. It discovers a project, reads its manifest, resolves the configuration, and spawns infc with the right arguments and working directory. The split is deliberate: infc stays a pure compiler that knows nothing about project structure; infs is the orchestrator that wraps it.

Project Layout

infs new myproject scaffolds the following structure:

myproject/
+-- Inference.toml       # manifest
+-- src/
|   +-- main.inf         # entry point (project mode always compiles this)
+-- out/                 # created by the first build (gitignored)
|   +-- main.wasm
+-- tests/
|   +-- .gitkeep
+-- proofs/              # proof-mode artifacts land here by default
|   +-- .gitkeep
+-- .gitignore

The layout mirrors Cargo's conventions: manifest at the root, sources under src/, build outputs under out/. The out/ directory is not committed; it is created automatically by infc (relative to its working directory, which infs sets to the project root). proofs/ is tracked via .gitkeep so that curated hand-authored proof sources stay in version control even when generated .wasm/.v artifacts are gitignored by extension. What coqc writes when one of those proofs is checked — a .vo, a .glob, a .<module>.aux — is gitignored too, and anywhere in the project rather than only under proofs/: a .v can be hand-authored, so its location decides whether it is output, while coqc's products never are and land beside whichever source it is given.

The Manifest (Inference.toml)

Inference.toml is the project manifest. Only [package] is required; all other sections default if absent.

[package]
name = "myproject"
version = "0.1.0"
infc_version = "0.1.0"

# Optional package fields:
# description = "A brief description"
# authors = ["Name <email@example.com>"]
# license = "MIT"

[build]
# The runtime the module is built for; "wasm32" (the default) is generic
# WebAssembly, "stellar" builds a Soroban smart contract, and "spacewasm"
# builds for the SpaceWasm flight interpreter. Validated on load: an
# unrecognized name is an error.
# target = "wasm32"
# "compile" (default) or "proof"
mode = "compile"
# Post-MVP WebAssembly proposals to opt into; empty (the default) keeps the
# output pure WebAssembly 1.0. Currently supported: "bulk-memory".
# wasm-features = ["bulk-memory"]
# "all" (default) keeps every array bounds guard; "omit-proven" drops the
# guards the analysis proved can never fire.
# bounds-checks = "all"
# optimize is recognized but not yet consumed.

# [memory]
# Linear memory of the emitted module; any key may be given alone. The memory
# is fixed at `pages` unless `max-pages` lets a linked module or the host grow it.
# `import = true` imports it from the host as `env.memory` instead of defining
# it, for the `wasm32` target only, and not in a proof build.
# pages = 1
# max-pages = 1
# stack-size = 65536
# import = false

[verification]
# Output directory for proof artifacts (honored only in proof mode).
# Defaults to "proofs/" if this section is omitted.
# output-dir = "proofs/"

[wasm-dependencies]
# Logical module name -> compiled .wasm, resolved relative to this file.
arith = { path = "libs/arith.wasm" }

# [host-imports]
# The host functions the program may bind, one array per import module; a
# header with no keys admits none. Omit the table to apply no policy.
# fprime_core = ["telemetry", "command"]
# env = ["clock_ms"]

The fields:

target and mode are case-sensitive: "Wasm32", "SpaceWasm" and "Proof" are all rejected, and neither key trims whitespace. The wire spelling of every target name is one lower-case word, so "space-wasm" and "space_wasm" are rejected too. Both are validated on load; an invalid value is an immediate error with the allowed set named in the message, never a fall back to the default. target names the same vocabulary as infc --target and is rejected with the same wording; "soroban", the former name of "stellar", earns a message redirecting to the current spelling rather than the generic unknown-target one.

target = "stellar" narrows the rest of the manifest. It cannot be combined with a [build.wasm-opt] table — that pairing is itself a load error, because whether an external Binaryen preserves a contract's value-ABI wrappers and its contractenvmetav0 section depends on a version nothing here pins — it admits no wasm-features, mode = "proof" is a load error too, and infs run refuses the project outright, since a contract is invoked by a Soroban host and not by a plain WebAssembly runtime. What an exported function may declare is narrowed too; see Compilation Targets. A [memory] that imports its memory (import = true) is not narrowed on load, here or at "spacewasm": the manifest loads, and the compiler refuses the build, naming the setting to remove (see Importing the memory).

target = "spacewasm" narrows it less, and the difference is instructive. It admits no wasm-features and no mode = "proof", on load, for the same reason — the interpreter decodes neither the post-MVP families nor the custom 0xfc instructions. But it keeps [build.wasm-opt], because what that refusal protects is a contract's wrappers and its contractenvmetav0 section, and this target's module has neither, and it keeps infs run, which executes the build in process under the SpaceWasm interpreter itself rather than under wasmtime. Nothing narrows what an exported function may declare: the bytes are the "wasm32" build's. The same load-time strictness applies to keys: every fixed-schema table rejects a key it does not recognize, naming the offending key and the fields the table accepts — a misspelled wasm_features fails the build rather than silently shipping a differently-configured artifact. Three tables accept arbitrary keys, because their keys are the data: [dependencies] and [wasm-dependencies], whose keys name dependencies, and [host-imports], whose keys name the import modules an embedder registers host functions under. wasm-features entries are WebAssembly proposal names ("bulk-memory"), not instruction names, and the setting is honored in project builds, single-file builds, and single-file infs run. [wasm-dependencies] entries have the same reach: project build, project run, single-file build, and single-file run all forward every declared entry to infc, and all four forward a [host-imports] table too. The unknown-key refusal first shipped in v0.0.6, though: a release through v0.0.5 reads past a root table it does not know with no diagnostic, and for [host-imports] that means building under no policy at all, so a project that relies on its allowlist has to be built with an infs that knows the table. See apps/infs/docs/inference-toml.md for the full reference.

Reserved Project Names

Project names must start with a letter or underscore and contain only alphanumeric characters, underscores, or hyphens. Names that match Inference language keywords or conventional directory names are reserved and rejected (case-insensitively). The reserved set includes: fn, let, mut, if, else, match, return, type, struct, impl, trait, pub, use, mod, ndet, assume, assert, forall, exists, spec, requires, ensures, invariant, const, enum, loop, break, continue, external, unique, unit; and the directory names src, out, target, proofs, tests, self, super, crate.

Reserved Module Segment

A module name has one reservation of its own, separate from the project-name set above and applied in a different position: host as the first segment of a use … from clause names the embedder, not a module this build links. So use { clock_ms } from host::env; binds a host import of the module env, and a [wasm-dependencies] key whose first segment is host — host, or host::io — is refused on every build and run route before infc is asked to build, because no linked module can be named under it; a host import needs no dependency entry at all, and belongs under [host-imports] if the project keeps an allowlist. The match is exact and first-segment only: hostlib, Host and a::host are ordinary module names. Contrast the path grammar's reserved root, which names the entry file in use root; and shadows a literal src/root.inf — root is reserved among the files of this project, host among the modules outside it. See What host reserves, and what it does not.

Real Manifest Examples

From scratch/raytracing-in-one-weekend/Inference.toml (single WASM dependency):

[package]
name = "raytracing-in-one-weekend"
version = "0.1.0"
infc_version = "0.1.0"

[wasm-dependencies]
fixmath = { path = "libs/fixmath.wasm" }

From scratch/linker-e2e/Inference.toml (multiple dependencies):

[package]
name = "linker-e2e"
version = "0.1.0"
infc_version = "0.1.0"

[wasm-dependencies]
arith = { path = "libs/arith.wasm" }
memlib = { path = "libs/memlib.wasm" }
sortlib = { path = "libs/sortlib.wasm" }

Neither example sets [build] or [verification] — those sections are omitted when all values are at their defaults.

Project Discovery

When infs build or infs run receives no path argument, it walks up the directory tree from the current working directory looking for Inference.toml. The nearest ancestor containing the file wins — the same convention Cargo uses, so a nested project's manifest shadows an outer one. The walk stops at the filesystem root; if no manifest is found, the command errors with a remediation message naming infs new and infs init.

After discovery, infc is spawned with its working directory set to the project root. This means out/ always lands at the root regardless of where the command was invoked from inside the project tree, and all source-relative paths in .inf files resolve from the same stable base.

~/projects/myproject/src/utils/
$ infs build           # walks up, finds ~/projects/myproject/Inference.toml
                       # infc CWD = ~/projects/myproject/
                       # artifact  = ~/projects/myproject/out/main.wasm

infs build

infs build has two modes of operation:

infs build                           # project mode: discovers Inference.toml, compiles src/main.inf
infs build path/to/file.inf          # single-file mode: compiles that file directly

Flags:

Mode resolution (precedence, highest first):

1. CLI --mode when present.
2. Manifest [build] mode = "proof" — forwards --mode proof to infc.
3. Manifest [build] mode = "compile" (explicit or defaulted) — forwards nothing, leaving infc's own -v ↔ proof implication intact.

The rule about forwarding nothing for compile mode is deliberate: infc's normalize_args function owns the -v ↔ --mode proof implication as its single source of truth. If infs also forwarded --mode compile it would suppress that implication for users who pass only -v, turning a spec-aware proof build into a spec-stripped one.

A manifest with [memory] import = true has no proof artifact, so infc refuses every build of it that writes a .v: -v, --mode proof, and the --mode proof that infs passes for a project whose manifest sets [build] mode = "proof". Build the imported-memory module with infs build --mode compile, which overrides the manifest's proof mode. infs has no per-build override for [memory] import, so a project builds the proof of the same program with import set to false or removed. That proof is about the defined-memory module. It carries over to the imported-memory one only under premises that are documented rather than proved, and only for a program that binds no host import, since infc refuses a .v for every host-import program whichever way its memory is built (see An Imported Memory Has No Proof Artifact).

--out-dir and [verification] output-dir: in effective proof mode (CLI --mode proof or manifest mode = "proof"), infs reads [verification] output-dir (defaulting to proofs/), normalizes it to a project-relative path, and forwards it to infc as --out-dir. This relocates both .wasm and .v artifacts to that directory. In compile mode, [verification] output-dir is ignored entirely — the compile artifact must always land under out/.

Forwarding --out-dir requires infc ABI ≥ 1.1 (see Relationship to infc below). Using a non-default output-dir with an older infc is a hard error with remediation.

Artifacts per Mode

In single-file mode (infs build path/to/file.inf) the output always goes to out/ relative to infc's inherited CWD (the invoking shell's current directory), with no manifest output-dir forwarded.

A build that writes a .v names the Rocq module after the source file's stem, so in single-file mode the stem has to be usable as one. infs build term.inf -v is refused in infc's words, with no artifact, because term is a name the proof contract declares and the module record would shadow it for any proof that imports the .v after the contract library; the message says to rename the file to term_module.inf. Refused: a stem that is not a legal Rocq identifier (my-prog, café), one containing __ or longer than 255 characters, one ending in _ when the program has a spec, a Rocq keyword or curated prelude name, a preamble helper, a contract name, or ho; a stem that is not valid UTF-8 is refused too. The infc README lists the rules in full. The same file builds without -v or --mode proof, since the .wasm has no Rocq name. Project mode compiles src/main.inf, whose stem main is never reserved. The rule and its rationale are in Reserved names.

infs run

infs run builds and then executes the resulting WASM where the build's [build] target says: a wasm32 build under wasmtime, and a spacewasm build in process under the SpaceWasm interpreter, with the F´ (F Prime) reference host functions and no wasmtime at all (see Running a SpaceWasm build). A stellar build is refused before anything is built.

infs run                                 # project mode: build + invoke main
infs run program.inf                     # single-file: compile and invoke main
infs run program.inf --entry-point helper  # single-file: invoke helper()
infs run program.inf -L libs             # single-file: search libs/ for external .wasm
infs run --fuel 1000000                  # spacewasm: stop after 10^6 interpreter instructions

Flags:

In single-file mode, -L and the other options must appear before the first bare trailing token: infs run program.inf -L libs 1 parses -L libs and passes 1 to the invoked function, while infs run program.inf 1 -L libs passes 1 -L libs verbatim as two trailing arguments, parsing no -L at all. Use -- to pass arguments that themselves look like flags.

In project mode (no path given):

• Always builds in compile mode, regardless of [build] mode in the manifest. Proof-mode WASM embeds custom non-deterministic opcodes (0xfc family) that neither wasmtime nor the SpaceWasm interpreter can decode. The one thing [build] mode can still do to run is stop it before it starts: mode = "proof" paired with a target that has no proof mode is a load error for every command, run included — a value run would ignore can still refuse to be read.
• Always invokes main, with no arguments, so a main that takes any runs only in single-file mode: one that declares parameters, and one that returns a struct or array, which takes a hidden result address (see below). Such a main is refused before it is invoked, on either runtime, naming what it takes and the single-file command that passes it. Passing --entry-point to anything other than main is rejected with guidance to use single-file mode instead.
• For a wasm32 build, checks wasmtime availability before starting the build, failing fast if the runtime is absent; a spacewasm build never looks for it.
• Resolves the manifest's [wasm-dependencies] and forwards any -L directories the same way project build does, anchored to the invocation directory, so a project binding use { … } from <module> runs without a separate link step.
• out/main.wasm is the expected artifact; if the build succeeds but the file is absent, run errors before executing anything.
• Judges the imports of the artifact it built — after [build.wasm-opt], so the bytes it asks about are the ones that would run — before anything runs. A wasm32 artifact that imports any function is refused: run registers no host function under wasmtime, and does not let wasmtime stand in for the embedder a program binding use { … } from host::… is written for — not even for the WASI functions the wasmtime CLI provides on its own. The refusal names each import and, when every one is an F´ reference host at its reference signature, the spacewasm target that provides them. The wasmtime check above still comes first, so a machine without the runtime is told to install it before it can hear this refusal. A spacewasm artifact may import the F´ reference hosts at their reference signatures and nothing else, and one that imports anything else is refused before the interpreter decodes a byte of it. Single-file run refuses the same way, naming out/<stem>.wasm.
• Supplies the memory a wasm32 artifact imports, the one import it does supply under wasmtime. A project built with [memory] import = true produces a module that imports env.memory, and the wasmtime command line provides no such memory, so the module would not instantiate. run reads the limits of the import off the artifact itself — after linking and [build.wasm-opt], so they are the limits of the bytes that run, not the manifest's — writes a small module that defines and exports one memory at exactly those limits beside the artifact, under a name that is this run's own (out/main.wasm.<pid>-0.memory), and invokes wasmtime with --preload env=out/main.wasm.<pid>-0.memory ahead of --invoke. The file is removed when wasmtime returns, whether the run succeeded or failed, and because each run creates its own, two runs of one artifact that overlap never share or remove each other's. An artifact that imports a function as well as its memory is still refused, for the function. Single-file run supplies the memory the same way, beside out/<stem>.wasm. Nothing else touches that memory and no other module shares it, and a project's main takes no argument and returns no struct or array, so a project's run meets the embedder contract by construction. A single-file run of an entry point that takes or returns a struct or array does not: the supplied memory has no pages above the module's, so the addresses typed on its command line, which run passes on unchecked, can only point into the module's own pages.
• As in infs build, which shares this step, holds [build.wasm-opt] to the memory import the compiler wrote. Binaryen output that adds, removes, renames or re-limits it is refused, as output importing a function the compiler's artifact did not already import is: the build fails, the optimized output is discarded, and the artifact infc wrote stays in place. The import is a contract with the host, not an interface the optimizer may narrow. infs never passes Binaryen's --zero-filled-memory, because a memory the host supplies is not zero-filled and the flag would let the optimizer drop the zero bytes of the constants segment the module writes into it.

In single-file mode (path given), --entry-point (default main) selects which exported function to invoke, and that function receives the trailing arguments from the command line — anything after the first bare token that options did not consume, or after --. main is no exception: each argument becomes the matching parameter of the compiled function, so infs run program.inf 41 hands 41 to a pub fn main(x: i32). Under wasmtime the arguments are handed to wasmtime as written, and it parses them; under the SpaceWasm interpreter run reads each as the parameter's i32 or i64, in its signed or its unsigned range, and refuses a count that differs. Those parameters are the ones the source declares, with two differences that apply to every function, main included. A struct or array parameter is a memory address. A function that returns a struct or array takes the address to write its result to as a hidden first parameter and returns nothing, so pub fn main() -> [i32; 4] needs that address on the command line and prints no value. run passes these addresses as numbers and checks none of them. Single-file run also resolves the enclosing manifest's [wasm-dependencies] and forwards any -L directories verbatim: infc inherits the invoking shell's working directory here, so a relative -L already means what it meant at the shell, with no anchoring step needed.

A wasm32 build requires wasmtime in PATH, in both modes, and installation instructions are printed when it is not found. A spacewasm build requires no runtime at all: the interpreter is part of infs.

Scaffolding

infs new <name> creates a new project directory with the layout shown above and optionally initializes a git repository (pass --no-git to skip).

infs init [name] initializes the current directory as a project — it writes Inference.toml and src/main.inf without creating a new parent directory. The name defaults to the current directory's name. If .git/ is present, infs init also creates .gitignore and .gitkeep files without overwriting anything that already exists.

Both commands scaffold src/main.inf with a minimal entry point:

// Entry point for the Inference program

pub fn main() -> i32 {
    return 0;
}

Toolchain Management

Project workflow is only half of infs's surface. The other half is a rustup-style toolchain manager — the part that makes "install Inference" a one-command operation and lets several compiler versions coexist:

Toolchains live under INFERENCE_HOME (default ~/.inference), and the release manifest is fetched from the distribution server (overridable via INFS_DIST_SERVER). infs build and infs run resolve the infc they spawn through this installation — the resolution order is described in the next section.

Relationship to infc

infs is a thin orchestrator. It does not link, parse, or type-check anything itself — all of that is infc's responsibility. The relationship:

infs build / infs run (project mode)
    |
    +-- discover_and_load(Inference.toml)
    |
    +-- find_infc_with_source()  # INFC_PATH > sibling of infs > system PATH > managed toolchain
    |
    +-- compatibility handshake
    |       infc --commit-hash    # short-circuit: same-build binaries always compatible
    |                             # sibling tier only: differing commits warn (stale neighbour)
    |       infc --abi-version    # major mismatch → hard error; minor mismatch → warning
    |
    +-- spawn infc
            CWD = <project root>
            arg: src/main.inf
            arg: -v                     (if .v requested; `run` never requests it)
            arg: --mode proof           (if effective proof mode; `run` never requests it)
            arg: --out-dir <dir>        (if effective proof mode + ABI ≥ 1.1; `run` never requests it)
            arg: --wasm-lib-dir <dir>   (one per -L/--wasm-lib-dir; a relative
                                         dir is anchored to the invocation
                                         directory, since infc runs at the root —
                                         `build` and `run` both pass their own
                                         `-L` flags through here)
            arg: --wasm-dep name=path   (one per [wasm-dependencies] entry; the
                                         declared path resolved against the root)
            arg: --target <name>        (if [build] target names a non-default
                                         target; gated on that name's own minor)
            arg: --wasm-features <list> (if [build] wasm-features requests any;
                                         requires infc ABI ≥ 1.2. Applies in both
                                         modes — a `.v` describing a different
                                         instruction set than the shipped `.wasm`
                                         would be worthless)
            arg: --bounds-checks <policy> (if [build] bounds-checks is
                                         "omit-proven"; ABI ≥ 1.9; both modes)
            arg: --memory-pages <n>     (if [memory] declares `pages`; ABI ≥ 1.3)
            arg: --max-memory-pages <n> (if [memory] declares `max-pages`;
                                         ABI ≥ 1.10)
            arg: --stack-size <n>       (if [memory] declares `stack-size`; ABI ≥ 1.3)
            arg: --import-memory        (if [memory] sets `import = true`;
                                         ABI ≥ 1.11)
            arg: --adopt-external-specs (if [verification] asks for it on a
                                         proof-artifact build; ABI ≥ 1.4; `run`
                                         never requests it)
            arg: --host-imports=<list>  (if a [host-imports] table is declared,
                                         as one argument — `--host-imports=` for
                                         a table with no keys; requires infc
                                         ABI ≥ 1.8)

Project run forces compile mode (mode = None) and never requests --out-dir, so the -v/--mode proof/--out-dir lines above never fire for it — but it shares this exact spawn otherwise, including the -L and [wasm-dependencies] forwarding.

Single-file build <path> and run <path> spawn infc directly instead of through the shared project-build helper, and — unlike the two project-mode paths above — they do not send infc the same argument list: build forwards only what the user explicitly passed, leaning on infc's own phase-flag default for the rest, while run always requests the full pipeline explicitly, because it needs the finished WASM artifact in hand to execute it. What they do agree on: neither sets current_dir, so infc inherits the invocation directory; every -L is forwarded verbatim, with no anchoring step; and whichever of --wasm-lib-dir, --wasm-dep, --target, --wasm-features, --bounds-checks, the memory flags and --host-imports a given invocation sends, they appear in that same relative order.

infs build <path> (single-file mode)
    |
    +-- enclosing_manifest(path)   # walk up from the source file; optional
    |
    +-- compatibility handshake     # unconditional — always runs, before any
    |       infc --commit-hash      # flag below is decided (unlike `run`,
    |       infc --abi-version      # which only handshakes when wasm-features
    |                               # are requested)
    |
    +-- spawn infc
            CWD = inherited from the invoking shell
            arg: <path>
            arg: -v                     (if `-v` was passed; `run` never sends it)
            arg: --mode <mode>          (if `--mode` was passed; `run` never
                                         sends it)
            arg: --wasm-lib-dir <dir>   (one per -L/--wasm-lib-dir, forwarded
                                         verbatim; no anchoring step runs)
            arg: --wasm-dep name=path   (one per [wasm-dependencies] entry from
                                         the enclosing manifest, if any)
            arg: --target <name>        (as the project route sends it)
            arg: --wasm-features <list> (if the enclosing manifest requests any;
                                         requires infc ABI ≥ 1.2)
            arg: --bounds-checks <policy> (as the project route sends it)
            arg: --memory-pages <n>     (as the project route sends them)
            arg: --max-memory-pages <n>
            arg: --stack-size <n>
            arg: --import-memory
            arg: --host-imports=<list>  (if the enclosing manifest declares a
                                         [host-imports] table; one argument;
                                         requires infc ABI ≥ 1.8)

build never adds --parse, --codegen, or -o: with no phase flag at all, infc's own default — full compilation, WASM written to disk — already does what build wants.

infs run <path> (single-file mode)
    |
    +-- enclosing_manifest(path)   # walk up from the source file; optional
    |
    +-- compatibility handshake     # conditional — runs only when the
    |       infc --commit-hash      # enclosing manifest asks for something an
    |       infc --abi-version      # older infc could not honor: a target,
    |                               # wasm-features, bounds-checks =
    |                               # "omit-proven", a [memory] table, or a
    |                               # [host-imports] table (present, even
    |                               # empty); skipped entirely otherwise,
    |                               # unlike `build`
    |
    +-- spawn infc
            CWD = inherited from the invoking shell
            arg: <path>
            arg: --parse                (always; `build` never sends it)
            arg: --codegen              (always; `build` never sends it)
            arg: -o                     (always; `build` never sends it)
            arg: --wasm-lib-dir <dir>   (one per -L/--wasm-lib-dir, forwarded
                                         verbatim; no anchoring step runs)
            arg: --wasm-dep name=path   (one per [wasm-dependencies] entry from
                                         the enclosing manifest, if any)
            arg: --target <name>        (as the project route sends it)
            arg: --wasm-features <list> (if the enclosing manifest requests any;
                                         requires infc ABI ≥ 1.2)
            arg: --bounds-checks <policy> (as the project route sends it)
            arg: --memory-pages <n>     (as the project route sends them)
            arg: --max-memory-pages <n>
            arg: --stack-size <n>
            arg: --import-memory
            arg: --host-imports=<list>  (if the enclosing manifest declares a
                                         [host-imports] table; one argument;
                                         requires infc ABI ≥ 1.8)

run always requests --parse --codegen -o explicitly rather than relying on infc's default, and neither -v nor --mode is ever part of its argv: the RunArgs struct (apps/infs/src/commands/run.rs) carries no such flags. Once infc exits, both run routes read the imports off the artifact they are about to execute before anything runs: a wasm32 artifact that imports any function is refused before wasmtime is invoked, since run registers no host function there, while one that imports only its memory has that memory supplied; and a spacewasm artifact importing anything but the F´ reference hosts at their reference signatures is refused before the interpreter decodes it — see infs run.

infc flags confirmed against core/cli/src/parser.rs:

Note: The current ABI version is 1.11.

The default behavior when no phase flag is supplied is full compilation with WASM output written to disk — equivalent to --codegen -o.

ABI Versioning and the --out-dir Gate

infs and infc communicate their compatibility through two probes run before every project build. First, infc --commit-hash is compared with infs's build commit: a match means the two binaries came from the same tree and are guaranteed compatible, skipping further checks. Otherwise, infc --abi-version is parsed as <major>.<minor>:

• Major mismatch: hard error with remediation (rebuild or set INFC_PATH).
• Minor mismatch: warning only; compilation proceeds.
• Unknown/old (infc exits non-zero or prints unknown): silent; treated as graceful skip, equivalent to ABI unknown.

The current ABI is 1.11 (COMPILER_ABI_MAJOR = 1, COMPILER_ABI_MINOR = 11 in core/compiler-interface/src/lib.rs). Each additive flag is gated at the minor it was introduced at, independently: --out-dir landed at minor 1, --wasm-features at minor 2, --memory-pages and --stack-size at minor 3, --adopt-external-specs at minor 4, --target at minor 5, --host-imports at minor 8, --bounds-checks at minor 9, --max-memory-pages at minor 10, and --import-memory at minor 11. infs forwards each only to an infc that reports an ABI minor at or above the flag's own (or matches by commit hash) — an infc that reports minor 1, for instance, supports --out-dir but not --wasm-features. --host-imports is forwarded from the [host-imports] table, and only from a declared one, so a project without the table puts no minor-8 floor under its compiler; a project with one is refused against an older infc rather than built without the flag, because that compiler would admit every host import the program binds and write an artifact identical to the one the table exists to police. --target is gated on the name rather than on the flag: each target became requestable at its own minor (wasm32 at 5, stellar at 6, spacewasm at 7), and an infc that parses the flag but predates a name would accept it and build for the default runtime — a wrong artifact rather than a refusal. That is true even where the two builds are the same bytes: dropping spacewasm produces the module a wasm32 build produces and drops the target's acceptance envelope with it, so what the name was written for never runs. The default target is never forwarded at all, so a project that names none puts no floor under its compiler. [memory] is gated per key for the same reason: pages and stack-size need minor 3 and max-pages minor 10, so a project that declares no maximum puts no minor-10 floor under its compiler, and one that does is refused against an older infc rather than built with a fixed memory. import = true needs minor 11 on its own, and its gate is the one that matters most: built without the flag, the module defines its own memory, and an embedder that resolves imports by name, as the JavaScript API and wasmtime's Linker do, ignores the env.memory it supplies and the module never asks for. The module instantiates, and the host then reads and writes a memory the module never touches, with nothing to say so. import = false forwards nothing and gates nothing, so a project that sets only the numbers builds against minor 3 or 10 as before. Pairing a manifest with a non-default [verification] output-dir against an older infc is a hard error:

error: the resolved infc does not support `--out-dir` (requires infc ABI ≥ 1.1);
       update the toolchain or remove `[verification] output-dir` from Inference.toml.

Compiler Resolution

infs locates infc by checking, in order:

1. INFC_PATH environment variable — an explicit override, useful for development and CI.
2. The infc sitting in the same directory as the running infs. A driver and its companion tools ship as one unit, so adjacency identifies the paired compiler — the same rule clang and rustc use to find theirs. Nothing about the directory is inspected, only that the two binaries share it, so this holds for a cargo build under any CARGO_TARGET_DIR, --target-dir, profile, or target triple, and for an unpacked release tarball alike.
3. System PATH (which infc).
4. The managed toolchain directory (~/.inference/toolchains/<version>/infc).

Step 2 assumes a pairing rather than proving one, so the handshake checks it: when the sibling tier resolved the compiler and infc --commit-hash disagrees with the commit infs was built from, the build warns and names both. The other three tiers stay silent on a commit mismatch, because for an explicitly pinned, system-installed, or managed infc a differing commit is the normal state — only adjacency claims the two binaries are a pair. The check sees cross-commit drift only: two binaries built from one commit with different working trees report the same hash.

INFERENCE_HOME overrides the managed toolchain root (default ~/.inference). INFS_VERBOSE traces which of the four resolved, and reports when step 2 found no neighbour and fell through.

Comparison with Cargo

The parallels to Cargo are intentional:

Where Inference is deliberately simpler: there are no build profiles beyond the compile/proof axis (debug vs. release optimization is not yet user-configurable via the manifest), no workspace support, and no package registry — external .wasm modules are referenced by filesystem path.

Current Limitations

• Fixed entry point in project mode. Project mode always compiles src/main.inf and invokes main. Custom entry files and custom exported functions are only available in single-file mode.
• Single entry file. infc follows the import-reachable closure from src/main.inf; there is no mechanism to specify additional top-level files.
• No workspaces. A single Inference.toml defines one project. Multi-crate workspace support is not yet implemented.
• No package registry. [wasm-dependencies] accepts only local filesystem paths. Version-pinned or registry-sourced dependencies are reserved for a future manifest extension.

Related Resources

• Compilation Targets — compile vs. proof modes, optimization levels, and the WASM target matrix; the --mode flag is specified in detail there.
• External Functions and WASM Linking — how use { f } from <module>; binds to [wasm-dependencies] entries and how the linker merges them.
• The WASM Linker — the static merge algorithm that folds external .wasm bodies into the output module.
• Module Hierarchy and Multi-File Compilation — how infc follows imports across files within a project.