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.

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]
# "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"]
# target and optimize are recognized but not yet consumed.

[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" }

The fields:

mode is case-sensitive: "Proof" is rejected. The field is validated on load; an invalid value is an immediate error with the allowed set named in the message. 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. Only [dependencies] and [wasm-dependencies] accept arbitrary keys, because their keys name the dependencies. 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. 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; and the directory names src, out, target, proofs, tests, self, super, crate.

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.

--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.

infs run

infs run builds and then executes the resulting WASM via wasmtime:

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

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 wasmtime cannot execute.
• Always invokes main. Passing --entry-point to anything other than main is rejected with guidance to use single-file mode instead.
• Checks wasmtime availability before starting the build, failing fast if the runtime is absent.
• 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 invoking wasmtime.

In single-file mode (path given), --entry-point (default main) selects which exported function to invoke. main is called with argc=0, argv=0 automatically; other functions receive the trailing arguments from the command line — anything after the first bare token that options did not consume, or after --. 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.

Both modes require wasmtime in PATH. Installation instructions are printed when it is not found.

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: --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)

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, and --wasm-features 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: --wasm-features <list> (if the enclosing manifest requests any;
                                         requires infc ABI ≥ 1.2)

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 requests wasm-features,
    |       infc --abi-version      # the only thing here needing a capability
    |                               # check; 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: --wasm-features <list> (if the enclosing manifest requests any;
                                         requires infc ABI ≥ 1.2)

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.

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

Note: The current ABI version is 1.2.

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.2 (COMPILER_ABI_MAJOR = 1, COMPILER_ABI_MINOR = 2 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, and --wasm-features at minor 2. 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. 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.