D - infs CLI Reference

infs is the unified command-line interface for the Inference compiler toolchain. It wraps the infc compiler with project management, toolchain installation, and build/run commands.

Compilation Commands

Build Options

When no phase flag is given, infs build runs the full pipeline and writes out/<name>.wasm. The phase flags below stop the pipeline early — supplying one means only that phase (and any required predecessors) runs.

Run Options

Examples

# Full compilation (writes out/example.wasm)
$ infs build example.inf

# Compile with Rocq translation (writes out/example.wasm and out/example.v)
$ infs build example.inf -v

# Build and run
$ infs run example.inf

# Run a specific exported function
$ infs run example.inf --entry-point my_function

Using infc Directly

The underlying infc compiler accepts the same phase and output flags as infs build and can be invoked standalone — useful for embedding into custom build systems or CI without the toolchain wrapper:

$ infc example.inf
$ infc example.inf --parse
$ infc example.inf -v

When no flags are given, infc performs full compilation and writes the WASM binary — equivalent to --codegen -o.

Note

infc currently supports single-file compilation only. Multi-file projects and project file (.infp) support are planned for future releases.

Compilation modes

The compiler has two modes that change how spec blocks and non-deterministic constructs are handled:

• compile (default): produces a release-optimized WASM binary intended for execution. spec blocks are stripped during codegen, so non-deterministic constructs (@, forall, exists, assume, unique) that appear only inside spec blocks do not reach the output.
• proof (implied by -v): keeps spec functions unoptimized so the structure of the source survives into the Rocq translation. The compiler emits both out/<name>.wasm and out/<name>.v. The .v file is a Rocq (Coq) translation suitable for formal verification.

In other words: use the default mode when you want to run the program; pass -v when you want to prove things about it.

Project Management

Creating a New Project

$ infs new myproject

This creates the following project structure:

myproject/
├── Inference.toml
├── src/
│   └── main.inf
├── tests/
└── proofs/

The generated src/main.inf contains a minimal program:

// Entry point for the Inference program

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

Use --no-git to skip git initialization:

$ infs new myproject --no-git

Initializing an Existing Directory

$ infs init

Creates Inference.toml and src/main.inf in the current directory. If a .git directory exists, it also creates .gitignore and .gitkeep files.

Toolchain Management

Installing a Toolchain

# Install latest stable version
$ infs install

# Install a specific version
$ infs install 0.1.0

On first install, infs automatically configures your system PATH:

• Linux/macOS: Adds ~/.inference/bin to your shell profile (~/.bashrc, ~/.zshrc, or ~/.config/fish/config.fish)
• Windows: Updates the user PATH in the registry

After installation, restart your terminal or source your shell profile.

Checking Installation Health

$ infs doctor

This runs diagnostic checks and provides recommendations if anything needs attention.

Other Commands

Compiler Resolution

When running build or run, infs locates the infc compiler using the following priority:

Environment Variables