compile (default)

Compile Calor source files to C#.

Bash
calor --input <file.calr> --output <file.cs>

Overview

The default calor command (when no subcommand is specified) compiles Calor source files to C#. This is the core functionality of the Calor compiler.

Quick Start

Bash
# Compile a single file
calor --input MyModule.calr --output MyModule.g.cs

# Short form
calor -i MyModule.calr -o MyModule.g.cs

# With verbose output
calor -v -i MyModule.calr -o MyModule.g.cs

Options

OptionShortRequiredDescription
--input-iYesInput Calor source file
--output-oYesOutput C# file path
--verbose-vNoShow detailed compilation output
--verifyNoEnable Z3 static contract verification
--no-cacheNoDisable verification result caching
--clear-cacheNoClear verification cache before compiling
--contract-modeNoContract enforcement mode: full, preconditions, or none

Output Convention

The recommended convention for generated C# files is the .g.cs extension:

Plain Text
MyModule.calr → MyModule.g.cs

This indicates "generated C#" and helps distinguish Calor-generated code from existing C# in your project.

Error Reporting

When compilation fails, errors are reported with file location:

Plain Text
Error in Calculator.calr:12:5
  Undefined variable 'x' in expression

  §R (+ x 1)
       ^

Compilation failed with 1 error

For machine-readable error output, use calor diagnose.

Integration with MSBuild

For automatic compilation during dotnet build, use calor init to set up MSBuild integration.

Exit Codes

CodeMeaning
0Compilation successful
1Compilation failed (syntax errors, validation errors)
2Error (file not found, invalid arguments)

Static Contract Verification

Use --verify to enable Z3 static contract verification:

Bash
calor -i MyModule.calr -o MyModule.g.cs --verify

When enabled, the compiler uses the Z3 SMT solver to attempt proving contracts at compile time. Proven contracts may have their runtime checks elided.

Example output:

Plain Text
Compiling MyModule.calr...
  Function Square: PROVEN - Postcondition (result >= 0)
  Function Divide: UNPROVEN - Postcondition (result >= 0)
Generated MyModule.g.cs

For details on verification categories (Proven, Unproven, Disproven, Unsupported), see Static Contract Verification.

Verification Caching

When using --verify, the compiler caches Z3 verification results to avoid redundant SMT solver invocations on subsequent compilations. This can dramatically improve compile times for projects with stable contracts.

Cache Options

Bash
# Default: caching enabled
calor -i MyModule.calr -o MyModule.g.cs --verify

# Disable caching (useful for CI or debugging)
calor -i MyModule.calr -o MyModule.g.cs --verify --no-cache

# Clear cache before verification
calor -i MyModule.calr -o MyModule.g.cs --verify --clear-cache

See Also