Enum Commands 

pub enum Commands {
    New {
        name: String,
    },
    Init {
        name: Option<String>,
    },
    Build {
        release: bool,
        verify: bool,
        license: Option<String>,
        lib: bool,
        target: Option<String>,
        native_functions: bool,
        emit: Option<String>,
    },
    Verify {
        license: Option<String>,
    },
    Run {
        release: bool,
        interpret: bool,
        emit: Option<String>,
        args: Vec<String>,
    },
    Check {
        deep: bool,
    },
    Opts {
        file: PathBuf,
        json: bool,
    },
    Publish {
        registry: Option<String>,
        dry_run: bool,
        allow_dirty: bool,
    },
    Login {
        registry: Option<String>,
        token: Option<String>,
    },
    Logout {
        registry: Option<String>,
    },
    Doctor {
        registry: Option<String>,
    },
    Repl {
        logic: bool,
        format: Option<LogicFormat>,
        load: Option<PathBuf>,
    },
    Sat {
        file: PathBuf,
        proof: Option<PathBuf>,
        stats: bool,
    },
    Prove {
        file: Option<PathBuf>,
        trace: bool,
        json: bool,
    },
    Logic {
        sentence: Option<String>,
        file: Option<PathBuf>,
        format: LogicFormat,
        all_readings: bool,
        pragmatic: bool,
        discourse: bool,
    },
    Doc {
        out: Option<PathBuf>,
    },
    Add {
        spec: String,
        path: Option<String>,
        git: Option<String>,
    },
    Remove {
        name: String,
    },
    Fmt {
        paths: Vec<PathBuf>,
        check: bool,
    },
    Emit {
        target: EmitTarget,
        file: Option<PathBuf>,
        output: Option<PathBuf>,
    },
    Clean {
        all: bool,
    },
    Completions {
        shell: Shell,
    },
    Test {
        args: Vec<String>,
    },
}

Available CLI subcommands.

Each variant represents a distinct operation that largo can perform. Commands are grouped into three categories:

Project Management

• New - Create a new project in a new directory
• Init - Initialize a project in the current directory

Build & Run

• Build - Compile the project
• Run - Build and execute
• Check - Type-check without building
• Verify - Run Z3 static verification

Package Registry

• Publish - Upload package to registry
• Login - Authenticate with registry
• Logout - Remove stored credentials

Variants

New

Create a new LOGOS project in a new directory.

Scaffolds a complete project structure including:

• Largo.toml manifest file
• src/main.lg entry point with a “Hello, world!” example
• .gitignore configured for LOGOS projects

Example

largo new my_project
cd my_project
largo run

Fields

name: String

The project name, used for the directory and package name.

Init

Initialize a LOGOS project in the current directory.

Similar to New but works in an existing directory. Creates the manifest and source structure without creating a new folder.

Example

mkdir my_project && cd my_project
largo init

Fields

name: Option<String>

Project name. If omitted, uses the current directory name.

Build

Build the current project.

Compiles the LOGOS source to Rust, then invokes cargo build on the generated code. The resulting binary is placed in target/debug/ or target/release/ depending on the mode.

Verification

When --verify is passed, the build process includes Z3 static verification of logical constraints. This requires:

• A Pro+ license (via --license or LOGOS_LICENSE env var)
• The verification feature enabled at build time

Example

largo build              # Debug build
largo build --release    # Release build with optimizations
largo build --verify     # Build with Z3 verification

Fields

release: bool

Build with optimizations enabled.

verify: bool

Run Z3 static verification after compilation. Requires a Pro+ license.

license: Option<String>

License key for verification. Can also be set via the LOGOS_LICENSE environment variable.

lib: bool

Build as a library instead of an executable. Generates lib.rs with crate-type = ["cdylib"] instead of a binary.

target: Option<String>

Target triple for cross-compilation. Use “wasm” as shorthand for “wasm32-unknown-unknown”.

native_functions: bool

Pre-build every is exported for native function into the AOT-native tier bundle (a cached cdylib per function) under .logos-native/.

emit: Option<String>

Emit target. wasm compiles the project DIRECTLY to a self-contained .wasm module via the built-in backend (no rustc / cargo / wasm-bindgen — milliseconds), written to target/<name>.wasm. wasm-linked additionally links the real logicaffeine_base::BigInt runtime (via rust-lld) so overflowing integer arithmetic computes the exact big number instead of wrapping — needs the Rust toolchain + a wasm32 base build. Omit for the default rustc-based Rust build.

Verify

Run Z3 static verification without building.

Performs formal verification of logical constraints in the project using the Z3 SMT solver. This catches logical errors that would be impossible to detect through testing alone.

Requires a Pro+ license.

Example

largo verify --license sub_xxxxx
# Or with environment variable:
export LOGOS_LICENSE=sub_xxxxx
largo verify

Fields

license: Option<String>

License key for verification. Can also be set via the LOGOS_LICENSE environment variable.

Run

Build and run the current project.

Equivalent to largo build followed by executing the resulting binary. The exit code of the built program is propagated.

With --interpret, skips Rust compilation and uses the tree-walking interpreter for sub-second feedback during development.

Example

largo run              # Debug mode (compile to Rust)
largo run --release    # Release mode
largo run --interpret  # Interpret directly (no compilation)

Fields

release: bool

Build with optimizations enabled.

interpret: bool

Run using the interpreter instead of compiling to Rust. Provides sub-second feedback but lacks full Rust performance.

emit: Option<String>

wasm compiles DIRECTLY to a .wasm (built-in backend, no rustc) and runs it via the emitted host shim (node). wasm-linked links the real BigInt runtime first (exact arbitrary-precision integers; needs the Rust toolchain). Compile-and-run in one step.

args: Vec<String>

Arguments to pass to the program.

Check

Check the project for errors without producing a binary.

Parses and type-checks the LOGOS source without invoking the full build pipeline. Useful for quick validation during development.

Example

largo check

Fields

deep: bool

Also run rustc’s analysis over the generated code (the same deep pass the IDE’s flycheck uses) and translate its findings to LOGOS.

Opts

Report which optimizations actually FIRE when compiling a LOGOS file.

Compiles the file on the AOT, run-path, and VM-compile paths with the firing trace on, and lists the optimizations that genuinely changed the program (not merely the ones that are enabled). Useful for understanding and auditing what the compiler did to a given program.

Example

largo opts src/main.lg
largo opts src/main.lg --json

Fields

file: PathBuf

The .lg source file to analyze.

json: bool

Emit the fired optimizations as JSON (keyword list).

Publish

Publish the package to the LOGOS registry.

Packages the project as a tarball and uploads it to the specified registry. Requires authentication via largo login.

Pre-flight Checks

Before publishing, the command verifies:

• The entry point exists
• No uncommitted git changes (unless --allow-dirty)
• Valid authentication token

Example

largo publish              # Publish to default registry
largo publish --dry-run    # Validate without uploading

Fields

registry: Option<String>

Registry URL. Defaults to registry.logicaffeine.com.

dry_run: bool

Perform all validation without actually uploading. Useful for testing the publish process.

allow_dirty: bool

Allow publishing with uncommitted git changes. By default, publishing requires a clean working directory.

Login

Authenticate with the package registry.

Stores an API token for the specified registry. The token is saved in ~/.config/logos/credentials.toml with restricted permissions.

Token Acquisition

Tokens can be obtained from the registry’s web interface:

1. Visit {registry}/auth/github to authenticate
2. Generate an API token from your profile
3. Provide it via --token or interactive prompt

Example

largo login                       # Interactive prompt
largo login --token tok_xxxxx     # Non-interactive

Fields

registry: Option<String>

Registry URL. Defaults to registry.logicaffeine.com.

token: Option<String>

API token. If omitted, prompts for input on stdin.

Logout

Remove stored credentials for a registry.

Deletes the authentication token from the local credentials file.

Example

largo logout

Fields

registry: Option<String>

Registry URL. Defaults to registry.logicaffeine.com.

Doctor

Diagnose the environment largo runs in.

Checks the Rust toolchain (needed by build/run), the wasm32 target, node (for --emit wasm), the verification flavor, registry reachability and credentials, update freshness, and — inside a project — manifest health. Degradations are warnings; only a broken project fails. Works offline.

Fields

registry: Option<String>

Registry URL to probe (defaults to the LOGOS registry).

Repl

Start the interactive LOGOS REPL.

Two modes in one session: imperative statements against a persistent interpreter session (logos>), and English→FOL logic mode with discourse-aware anaphora (logic>). Type :help inside for the meta-commands (:mode, :format, :readings, :vars, :save, …). Works on a pipe too — no terminal required.

Fields

logic: bool

Start in logic mode (English → FOL).

format: Option<LogicFormat>

Initial logic output format.

load: Option<PathBuf>

Load a saved session/program on startup.

Sat

Solve a DIMACS CNF with the certified SAT engine.

The SAT Competition interface as a largo verb: prints s SATISFIABLE with a v model or s UNSATISFIABLE, optionally exporting a DRAT/DPR/SR refutation for external checkers (drat-trim). Exit codes follow the competition convention: 10 = SAT, 20 = UNSAT, 1 = error.

Fields

file: PathBuf

The DIMACS CNF file to solve.

proof: Option<PathBuf>

Write the UNSAT certificate here (DRAT; DPR/SR for symmetry routes).

stats: bool

Print solver statistics to stderr.

Prove

Prove the theorems in a LOGOS source file (kernel-certified).

Runs ## Theory developments (formal Axiom/Theorem declarations, proved in citation order) and English ## Theorem blocks (Given/Prove/Proof) through the proof engine. Every ✓ is certified by the type-theory kernel — a mere derivation never counts.

Fields

file: Option<PathBuf>

The source file (defaults to the project entry).

trace: bool

Show the rendered derivation tree under each proved theorem.

json: bool

Emit machine-readable JSON results.

Logic

Translate English to First-Order Logic.

Compiles a natural-language sentence to formal logic — the LOGOS logic mode from the terminal. Reads the sentence inline, from --file, or from piped stdin. Prints bare FOL on stdout, so output pipes cleanly into other tools.

Fields

sentence: Option<String>

The English sentence to translate.

file: Option<PathBuf>

Read the sentence (or discourse) from a file.

format: LogicFormat

Output format for the logical form.

all_readings: bool

Show every reading (quantifier scopes + parse forest), numbered.

pragmatic: bool

Enrich with scalar implicature (pragmatic strengthening).

discourse: bool

Treat each input line as one sentence of a discourse with shared anaphora context.

Doc

Generate documentation from the project’s ## blocks.

Renders a markdown reference from the literate structure of the entry file: ## To signatures, type definitions, notes, examples, and formal blocks — in source order. ## Main is omitted.

Fields

out: Option<PathBuf>

Output directory (defaults to target/doc).

Add

Add a dependency to Largo.toml.

Accepts name (any version), name@version, or logos:name (the registry URI form). --path and --git record local and git dependencies. Edits preserve the manifest’s comments and formatting.

Fields

spec: String

The dependency: name, name@version, or logos:name.

path: Option<String>

Use a local path dependency.

git: Option<String>

Use a git dependency.

Remove

Remove a dependency from Largo.toml.

Deletes the named entry from [dependencies], leaving the rest of the manifest byte-identical.

Fields

name: String

The dependency name to remove.

Fmt

Format LOGOS source files.

Applies the canonical style (4-space indentation, no tabs, no trailing whitespace) — the same rules the language server uses. Without paths, formats the whole project; with paths, exactly those files. --check writes nothing and exits 1 if anything would change.

Fields

paths: Vec<PathBuf>

Specific files to format (defaults to all project sources).

check: bool

Check only: list files that need formatting, exit 1 if any.

Emit

Emit compiled code without building a binary.

Prints the generated Rust or C translation of the program, or writes a self-contained .wasm module (built-in backend, no rustc) with its Node.js host shim. Without FILE, uses the current project’s entry; with FILE, works on any standalone .lg/.md source.

Fields

target: EmitTarget

What to emit.

file: Option<PathBuf>

A standalone source file (defaults to the project entry).

output: Option<PathBuf>

Write to this path instead of stdout (rust/c) or the default module path (wasm).

Clean

Remove build artifacts.

Deletes the project’s target/ directory. With --all, also removes the .logos-native/ compiled-function bundle cache produced by largo build --native-functions.

Fields

all: bool

Also remove the .logos-native/ bundle cache.

Completions

Generate shell completions for largo.

Writes a completion script for the given shell to stdout. Source it from your shell’s configuration to get tab completion for every largo command and flag.

Fields

shell: Shell

The shell to generate completions for.

Test

Reserved for the LOGOS test framework (coming in a future release).

Fields

args: Vec<String>

Ignored; the verb is reserved.

Trait Implementations

impl FromArgMatches for Commands

fn from_arg_matches(__clap_arg_matches: &ArgMatches) -> Result<Self, Error>

Instantiate Self from [ArgMatches], parsing the arguments as needed.

fn from_arg_matches_mut( __clap_arg_matches: &mut ArgMatches, ) -> Result<Self, Error>

Instantiate Self from [ArgMatches], parsing the arguments as needed.

fn update_from_arg_matches( &mut self, __clap_arg_matches: &ArgMatches, ) -> Result<(), Error>

Assign values from ArgMatches to self.

fn update_from_arg_matches_mut<'b>( &mut self, __clap_arg_matches: &mut ArgMatches, ) -> Result<(), Error>

Assign values from ArgMatches to self.

impl Subcommand for Commands

fn augment_subcommands<'b>(__clap_app: Command) -> Command

Append to [Command] so it can instantiate Self via [FromArgMatches::from_arg_matches_mut]

fn augment_subcommands_for_update<'b>(__clap_app: Command) -> Command

Append to [Command] so it can instantiate self via [FromArgMatches::update_from_arg_matches_mut]

fn has_subcommand(__clap_name: &str) -> bool

Test whether Self can parse a specific subcommand