v0.2.0

Ligare v0.2.0 Released

After over a month of intensive development since v0.1.0, Ligare v0.2.0 is here. The compiler core has grown from 37k to 68k lines (not including 13k lines of std and mathlib). The type system is now logically closed, and the toolchain has been upgraded with a query-driven architecture.

Highlights

Type System Closure

• ! (bottom type): The sole empty type. Diverging functions return !. The compiler automatically derives unreachable branches. Termination checking requires recursive functions to be proved terminating or explicitly marked as returning !.
• Monad System: IO is now a capability-parameterized Monad, making side effects composable and extensible. Effect propagation is automatic. Fine-grained capability constraints like IO FileSystem and IO Network precisely describe side effect scopes.
• Explicit Implicit Arguments: You can now pass implicit arguments explicitly at call sites using {A = Int} to resolve ambiguity in complex scenarios.
• Mature Refinement Types: Definitions like nat = int where (x >= 0) are now standard, with automatic decomposition into base constraint checking and proposition checking, integrated with SMT.

Architectural Overhaul: Query-Driven Compiler

• Query-Driven Architecture: The compiler and LSP are unified into a single reactive query engine. All computations (parsing, type checking, SMT solving, code generation) are modeled as cacheable queries with automatic dependency tracking and precise incremental recomputation.
• LSP Performance: Diagnostics, completions, and hover information now have minimal latency. Only queries truly dependent on a modified line are recomputed. ligls requires no separate compiler process—zero communication overhead.
• Decoupled Kernel: The compiler kernel has been split into six mechanical primitives (invoke, quote, check, reduce, level, register_checker). Each crate has a single responsibility with clear dependency boundaries.
• SCC Lifetime Analysis: The compiler automatically derives value liveness intervals at compile time and inserts deallocation code. Zero runtime overhead, no GC pauses.
• Parallelization: Multi-threaded parallelism via rayon, fully utilizing multi-core CPUs for faster compilation and LSP responses.

Proof & Automation

• Replay SMT: SMT-generated proof terms are cached as query results. Identical inputs skip redundant solving, significantly improving compile performance.
• Extended #[tactic] Macros: Custom proof strategies can be defined by users, combining automated proving with manual intervention.
• Early mathlib: Basic theorems like commutativity and associativity of addition are now provable.

Standard Library & Tooling

• Standard Library std: Includes Option, Result, List, Vec, HashMap, String, basic IO, and more. std is bundled in the release—no extra setup required.
• Editor Support: The ligls LSP server provides intelligent completions, diagnostics, hover info, and go-to-definition. Supports VS Code, Neovim, and Zed.

Platform Support

Platform	Status
Linux	✅ Stable
macOS	✅ Stable
Windows	⚠️ Experimental (WSL recommended)

Installation

Download the archive for your platform from GitHub Releases, extract, and run ligare and ligls directly. The standard library is bundled—no additional setup needed.

Looking Ahead

v0.3.0 will focus on Monad Ecosystem—Result, Option, List, State, and other core standard library types will fully implement the Monad interface, making do blocks the universal syntax for composing computations. v0.4.0 will target package management and toolchain maturity, and v0.5.0 will begin the self-hosting journey.

---

Ligare v0.2.0 — type system closed, query-driven, everything is a term.

v0.1.0

Ligare 0.1.0

First public release of Ligare — a dependently typed systems language that compiles to zero-runtime C.

What's included:

• Full compiler pipeline (parse → constraint check → C code generation)
• Dependent types, refinement types, inductive types
• Effect system (IO isolation, do blocks)
• Module system, namespace, interface methods
• Metaprogramming (quote/splice, #[derive], #[tactic])
• FFI (zero-cost external C functions)
• LSP (diagnostics, completions, hover, go-to-definition)
• Package management, incremental compilation, formatter

Platforms: Linux ✅ · macOS ✅ · Windows ⚠️ experimental

Install:

# Download from assets below, or build from source:
git clone https://github.com/ligare-lang/ligare
cd ligare && cargo build --release

Status: Alpha. APIs may change. Standard library is minimal.