Releases · mimir/mimir · GitHub
Skip to content

Releases: mimir/mimir

Release list

MimIR 0.4

MimIR 0.4 Latest
Latest

Choose a tag to compare

View all tags
@leissa leissa released this 25 Oct 07:49
v0.4
5428557

Covers everything merged since v0.3: 570 commits touching 870 files (+26,194/−16,374).
MimIR now runs in your browser: the playground is mim compiled to WebAssembly, and every Mim snippet in the docs has a run button that opens it there.
On the language side, Mim gained variants with match, nominal types via nom, fully implemented singleton types, and real universe-level inference; option.Opt is now a proper nominal variant.
Under the hood, annexes moved into a lazily imported library World, every RWPhase coerces, n-ary extract/insert subsumes tensor.get/tensor.set, absl is gone, and a round of review passes made the compiler ~7% faster.

Highlights

  • Playground.
    mimir.github.io/playground runs mim as WebAssembly in a Worker, with tabs for the Mim dump, LLVM IR, the log, and a pan/zoom graph view that can pop out into its own window.
    Programs are shared via a compressed #z= link fragment.
    This required building MimIR with statically linked plugins (MIM_STATIC_PLUGINS).
  • Variants and match.
    | Nil | Cons: [Nat, List] is a positional sum type; unlike ∪, nothing is sorted, deduplicated, or flattened.
    T#Cons / T#1 select a case, match l with | Nil => … | Cons (h, t) => … eliminates it, and missing or unreachable arms are diagnosed. 
    rec List = | Nil | Cons: [Nat, List];

lam len (l: List): Nat =
    match l with
        | Nil         => 0
        | Cons (_, t) => core.nat.add (1, len t);
  • Nominal types.
    nom Meter = I32; declares a type that is distinct from every other nom over the same representation, the one place where Mim is not structurally typed.
    e inj Meter wraps and prefix # unwraps; nom Tree (T: *) = | Leaf | Node: [Tree T, T, Tree T] declares a type constructor, and named constructors/fields work directly on a nom.
    The representation is as visible as the nom: a priv nom exported via pub let I = I; is an abstract type.
    noms are erased right before codegen.
  • option.Opt is a nominal variant | None | Some: T, so Opt [] no longer collapses to [] and Opt (Opt T) no longer flattens.
    T is implicit: Opt#Some 23 and Opt#None replace option.some/option.none.
  • Singleton types are complete: «e» is the type whose sole inhabitant is e, ‹e› introduces and # eliminates it, and eliminators resolve singletons on construction.
    wrap/unwrap were renamed to narrow/widen.
  • Universe levels. Univ is now Level, with real level inference: x + k = l is solved, max constraints are postponed and solved per declaration, and remaining level holes default to 0.
  • N-ary extract and insert.
    Arrays and packs fuse — «2; «3; T»» is «2, 3; T» — and t#(i, j) ≡ t#i#j.
    tensor.get/tensor.set and the lower_get_set phase are gone; use t#(i, j) and t#(i, j) ← v on a tensor.buf.
  • Dependent main.
    argv is now mem.Ptr0 «core.idx2nat argc; mem.Ptr0 I8», so its length is tied to argc and the mem.assume casts go away.
    New core.idx2nat (a never-truncating Idx s → Nat) and mem.cstr, which views a C string as a length-indexed array.
    The effect token now lives in core as core.M (re-exported as mem.M), so core no longer depends on mem.

Language & frontend

  • mutual … end groups mutually recursive rec/nom/lam/con/fun declarations (as in Lean) and replaces rec … and; modifiers on mutual apply to every member.
  • Modules are written mod I … end instead of mod I { … }.
  • Arrays without ⊤: the ⊤ wildcard in array types and idx_unsafe are gone; C interop goes through mem.decay/mem.assume.
  • Let-binding type annotations are actually checked now, and so are all members of an identifier group: let (a b: Nat) = (tt, 2) used to be accepted.
  • The AST got dedicated nodes for non-pattern binders («i: n; …», return, match arms) instead of abusing IdPtrn, and AxmDecl is represented faithfully without parser-side expansion.
  • rule declarations track visibility modifiers.
  • --pe-fuel turns potentially endless partial evaluation into an error instead of a stack overflow.
  • The compiler throws proper errors in many places that used to crash or assert.

Core IR & compiler infrastructure

  • Lazy annex library.
    optimize() moves the elaborated World into Driver::library() and imports only the externals back; World::annex imports an annex on first use.
    Phases walk only the program from its externals — no more bootstrapping or annex walks.
    Axioms and non-Lam mutable annexes are opaque; anx lams are rewritten like ordinary code.
  • Coercion in every RWPhase.
    CoercePhase is gone; each rewrite coerces arguments, tuple ops, and bodies to their rewritten expected types, at zero cost when nothing was reshaped.
    Checker → Check with Check::coerce; annotated tuples are always type-checked.
  • Towards an immutable IR: mutables are set only once; InplaceRWPhase is gone again.
  • New phases: contification, aggressive dead-code elimination (removes unused vars even in cycles), and SCCP moved in-tree; BetaRed also inlines Lams that merely shuffle vars or forward constants; BranchNormalize → DispatchNormalize.
  • η-conversion: singleton domains are η-reducible via the new World::inhabitant, and η-chains are reduced at once (with cycle detection).
  • SEO: captured slots in direct-style calls, lea support, liveness tracking, and pinning only the slots a call actually uses; heap2stack now sees through direct-style calls and mem.free.
  • Scalarize is type-directed and handles variants and value telescopes.
  • Proxies no longer contribute to free variables, which killed the costly SEO::find_unknowns.
  • Performance: Vars/Muts on Patricia trees, absl replaced by ankerl::unordered_dense, tuned hash functions, a fixed zonker memo, and fewer locals merges on hash-cons hits (hlo −5.9%, vgg16 −7.1% instructions).
  • Round-trip: both --output-mim and --output-ast dumps re-parse to a byte-identical fixpoint over the whole lit suite, checked in CI (test-roundtrip).
    --dump-local → --mim-local; let patterns drop their types unless --mim-typed-let.
  • The dangerous single-argument Def::proj(i) is gone; cat_tuple/cat_sigma → Tuple::cat/Sigma::cat.
  • Three review passes fixed a long list of folding bugs in core, math, and ll (e.g. bit2 truth table, Idx arithmetic on non-power-of-two sizes, IEEE min/max signed zeros).

Plugins

  • tensor: generate, reduce, numerically stable softmax, conv_grouped (scheduled per group), new reshape/broadcast/transpose normalizers, reassoc sees through transposes, and the schedule travels as one Sched record.
  • btensor: destination-passing style (ops write into a caller-allocated dst), buffer.free, and a free_locals phase that frees local buffers after their last use — several tests now run leak-free under LeakSanitizer.
    map_reduce_post lowering is expressed through a Mim higher-order function.
  • affine: index folding (affine.lower_index) proves divisions in delinearize(linearize(…)) redundant via range analysis, and peels carry-free low parts off the rest.
    Together with ll.novec hints and conv output-channel blocking, the 25 supported KernelBench level-3 models got 1.75× faster (geomean); ShuffleNet went from 17.3 s to 2.3 s.
  • math: inf, neg_inf, nan constants.
  • core: trait.size folds arrays with symbolic element sizes.
  • ll: fixed SIMD extract/insert and vector returns of non-constant lanes.
  • ll_nvptx → nvptx.
  • sexpr moved out of tree to ashiven/sexpr; the old CRTP Emitter is gone.
  • Generated C++/Python bindings escape target-language keywords (annexes may be called and, or, …) and export constructor/field indices.

Tooling, build & CI

  • Builds to WebAssembly via Emscripten with static plugins; the playground is deployed from master.
  • Plugin search paths reworked; Windows (Visual Studio) DLL output path fixed.
  • Python binding generation simplified.

Docs

  • Docs pages run their Mim snippets in the playground; new playground.md.
  • langref.md covers variants, nominal newtypes, singletons, mutual, and universe levels; dev.md documents the new Shape handling.

Contributors

@leissa, @HarithF, @hsqStephenZhang, @ashiven, @fodinabor, @amaebel, and @asindarov.

New Contributors

Full Changelog: v0.3...v0.4

Contributors

fodinabor, leissa, and 5 other contributors
Assets 3
Loading

MimIR 0.3

MimIR 0.3

Choose a tag to compare

View all tags
@leissa leissa released this 13 Sep 23:23
v0.3
66e7e52

Covers everything merged since v0.2: 588 commits touching 821 files (+28,335/−19,142).
This is the largest surface-syntax overhaul since v0.1: the % annex sigil is gone, Mim gained Lua/Rust-style mod/import/use and a full ladder of infix operators, and most of MimIR's utility layer moved out into fe.
On the optimizer side, InplaceRWPhase, static argument optimization, and a %tensor.reassoc matrix-chain phase are new; on the backend side, NVPTX codegen and C runtimes for the LLVM backends landed.

Highlights

  • Modules.
    mod I { ... } groups declarations, import binds a file as a module, use path as I aliases one and use path as * splices its public members into scope.
    Paths are identifier-only (a.b.c); . walks modules and never reads a field out of a value — that stays #.
    Declarations carry visibility (priv/pub, priv by default) that is purely lexical and independent of extern/anx.
  • No more %.
    Annexes are ordinary members of their enclosing module and resolve through the same path lookup as everything else, so %tensor.map_reduce is now tensor.map_reduce.
    An anx modifier marks a declaration as an annex; axm is implicitly anx.
  • Infix operators.
    == != < <= > >= << >> + - * / % and the insert arrow ←/<-, with a precedence ladder shared by parser and dumper.
    Mim gives them no meaning of its own: a op b is sugar for `op (a, b), so let `+ = core.nat.add is what makes 2 + 3 an addition.
    core.ops and math.ops ship ready-made bindings.
    Two consequences worth knowing: f * is a multiplication (write f (*) for the application), and <- is a single token, so a comparison against a negative literal needs x < (-1).
  • Insert is an operator. t#i ← v replaces the old insert axiom and extends recursively through a #-path: t#i#j#k ← v denotes the outer aggregate t.
  • NVPTX. New nvptx (PTX intrinsics) and ll_nvptx (LLVM backend targeting NVIDIA GPUs) plugins.
    ll_nvptx splits the lowered program into a host and a device world, emits <world>.ll and <world>_dev.ll, and on Linux compiles and embeds the device binary into the host module by default.
  • C runtimes for the backends. ll ships mim_rt.c and ll_nvptx ships mim_cuda_rt.c; runtime modules get their own search path (<root>/lib/mim/rt), separate from plugins and imports.
  • Utility layer moved to fe. hash, sets, span, util, vector, log, profile, sys, dl, and link_cut_tree all left mim/util; only dbg.h, gid.h, and types.h remain.
    The CLI switched from lyra to fe::cli, diagnostics to fe::Diag, and Vector<bool> to fe::Bitset.

Language & frontend

  • import/plugin are first-class declarations and accept as I / as *.
  • rec starts a recursive declaration group extended by and; recursive functions use lam/con/fun, whose declared name is in scope inside their own body.
  • Patterns and telescopes were pinned down: () is a pattern and [] a telescope, position decides which, and []-style patterns for lambdas were removed.
  • axm nat.(add, sub): ... declares several axioms at once as members of a module of that name; each tag may carry extra names via = I.
  • Quote and angle-bracket alternatives nobody was using were dropped from the lexer.
  • Implicits got several rounds of work, and the tensor/matrix plugins were rewritten to lean on type inference instead of spelling sizes out.
  • option.none's type parameter is now explicit; vec.first/vec.last return an option.
  • Diagnostics were reworked end to end: --no-snippet, --loc-style={full,rowcol,row,msvc}, std::format-based parser messages, and delimiter recovery through fe's anchoring.

Plugins

  • matrix → btensor, realigned with tensor so every op is the buffer.Buf counterpart of its tensor.* sibling, taking the same groups in the same order and threading mem.M on top.
  • tensor: new splat, gather, scatter, map_reduce_post (epilogue fusion), if_static, fastest_axis, and shape; product_2d/transpose_2d generalized to product_/transpose_; frontend tiling code, symbolic contraction in dot_product, and a first-class loop-nest chooser operand carrying the schedule.
  • %tensor.reassoc: a new phase that reassociates chains of product_ with the classic matrix-chain-order DP, but costed in vector lanes rather than multiplications (-X tensor:reassoc-vec=<n>).
    Extents need not be literal — a cost is a polynomial in the symbolic extents ordered coefficient-wise, which is only a partial order, so up to 4 matrices (-X tensor:reassoc-max=<n>) the surviving bracketings are emitted side by side behind a run-time cost comparison and only the winner's thunk runs.
    Common sub-products are hash-consed across alternatives, keeping code growth well below Catalan(n − 1).
  • gpu: GPU lowering of map_reduce, merged gpu.{auto_}init operations in the backend, HLO work.
  • core: matches on known injections now reduce.
  • ll: vec.zip input count and lane count are distinguished; silent assumptions in the LLVM backend were replaced by proper errors (fixes #9).
  • Plugin arguments via -X <plugin>:<arg>, repeatable, keyed by plugin name and read by a phase through Phase::args; only the first : separates the two halves.
    Plugins declare their arguments and their PluginEnv environment variables next to the code that reads them, and the CLI help tables are generated from those declarations.

Core IR & compiler infrastructure

  • InplaceRWPhase, sharing a new RWBase with RWPhase, for rewrites that don't need a fresh world.
  • Static argument optimization replaces TailRecElim: it seeds on the rightmost Pi domain, freezes the site class, and pools the rest, with a per-site wrapper fallback.
  • Unload phase nukes a plugin together with its annexes, superseding prefix_cleanup.
  • sizeof(Def) shrunk by moving Def::dbg_ into a side table; rebuild, stub, and rewrite now work with DbgKey directly.
  • Def::rebuild and Def::refine removed.
  • mem.add_mem rebuilds mem-placeholder tuples at every occurrence.
  • The world is zonked before optimizing.
  • Performance work on Checker, on the set/optimize machinery, and a general round of profiling fixes.
  • Closure conversion fixes: higher-order returns (#117) and clos-mem.
  • mem.mslot/tensor lowering use mutable continuations to get fresh, distinct memory and avoid buffer aliasing.

Tooling, build & CI

  • Google Test is gone; unit tests moved from gtest/ to test/ and run on doctest (pulled in via fe). googletest and lyra submodules removed.
  • MIM_DEBUG_OPTIMIZE (on by default) compiles Debug builds with -Og instead of -O0; assertions and MIM_ENABLE_CHECKS are unaffected.
  • Three separate search paths for plugins (-P), imports (-I), and runtimes, plus prefix roots via --prefix-path/-R; mim -l prints all three fully resolved.
    A plugin <name>; directive takes its .mim from the directory libmim_<name> was loaded from, so the two halves can never be paired across directories.
  • Python bindings are generated automatically.
  • Stack size raised to 16 MiB at link time; lit timeout raised from 30 s to 120 s; CMake and the CI workflows simplified, and CI wall time cut.

Docs

  • Mim and EBNF syntax highlighting in the generated docs, with fenced-block filtering in docs/fences.py.
  • langref.md substantially rewritten: new Files and Imports, Paths and Modules, Infix Operators, and a Precedence table covering all 16 levels including the Pi/Bot/Err pseudo levels.
  • phases.md extended with RWBase, InplaceRWPhase, sparse fixed-point iteration, and an SSA without Dominance discussion.
  • New why-cpp.md on MimIR's implementation-language choice.
  • Doxygen switched to MathJax.

Contributors

Roland Leißa, Friedrich Tschirpke, Joachim Meyer, Joel Schröder, and hsqStephenZhang.

Full Changelog: v0.2...v0.3

Loading

MimIR 0.2

MimIR 0.2

Choose a tag to compare

View all tags
@leissa leissa released this 18 Jul 10:05
v0.2
ffae556

Changelog

All notable changes to MimIR are documented here.

v0.2

Covers everything merged since v0.1: 1104 commits touching 686 files (+19,800/−8,838). Highlights are Python bindings, a much larger tensor plugin, a new ll backend plugin, GPU codegen support, and a reworked phase/analysis infrastructure (sparse fixpoint iteration, SEO, scalarize).

Highlights

  • Python bindings (py/): brand new nanobind-based bindings (ported from an initial pybind11 prototype) exposing World, Def, Lam, Driver, Flags, Log, the AST Parser, Sym, and Tuple. A higher-level mim package adds jit/callable helpers for calling compiled Mim functions directly from Python, plus bindings for the regex plugin. Comes with its own pytest suite wired into test-all as test-py, gated by the MIM_BUILD_PYTHON CMake option (on by default).
  • Tensor plugin grew substantially: dot_general, map_reduce (and an affine _aff variant), broadcast_in_dim, get/set, reshape, repeat (tiling), slice/flip, pad/concat, shape, 2D conv (+ shape inference), 2D max/sum pooling, and batched matrix multiplication (bmm). Lowering was split into staged phases, backed by a new bufferization pass for constants, padding, and concat.
  • New buffer plugin providing the abstract-matrix-memory/bufferization layer used by tensor lowering.
  • New ll plugin: the textual/LLVM-ish backend that used to live inside core's be/ll.cpp is now its own plugin, following the removal of the hardcoded backend hook from the driver's plugin architecture. (Known limitation carried over: runtime-sized packs still crash this backend's emitter.)
  • direct plugin renamed and rewritten as cps, with a new CPS-conversion implementation.
  • GPU plugin: block/async tags, a unified GPU-launch mechanism, machine-state/sync-usage checks, double-sync removal, and host/device world splitting for backend codegen.
  • S-expression export: new --output-sexpr / --output-sexpr-slotted (with --sexpr-include-types) CLI outputs, formatted for interop with the external slotted-egraphs equality-saturation library.

Core IR & compiler infrastructure

  • Var::mut renamed to Var::binder (binder mutable now lives in Def's union slot).
  • New SEO (symbolic expression optimization) (sea-of-nodes-style) phase for SSA construction over %mem slots + GVN + SCCP in one combined phase.
  • Scalarize phase reworked to flatten nested tuples type-directed by each imm Cn Pi, rather than per Lam.
  • %mem.mslot is now continuation-based instead of direct.
  • Sparse fixpoint iteration for Analysis: split into read (lattice) vs. write (lattice_mut) access, with lattice_force streamlined; writer-dirt tracking plus SEO-driven caller taints and a certifying full round.
  • %opt plugin reorganized; World::sym2annex removed in favor of a more direct symbol/annex mapping.
  • World::app iteration reworked (world-app-iter).
  • Internal code migrated to std::views (range-based Vector::append_range/insert_range) as part of the move to C++23.
  • pack#index now always reduces (previously left un-normalized in some cases).

Bug fixes

  • Fixed argument evaluation order in Rewriter::rewrite_imm_App (rewrite_order).
  • nat.sub now saturates at 0 in the ll backend instead of underflowing.
  • Fixed correctness issues in the new SEO phase.
  • Fixed a lambda-back-not-closed issue caught by %refly.var.
  • Fixed a tuple-pattern parsing issue.
  • Windows CI re-enabled after breakage from a GitHub Windows runner image update (also touched the regex automaton and CLI entry point); Windows venv/pip warnings fixed via ensurepip --upgrade.

Tooling, build & CI

  • Baseline language standard raised to C++23.
  • FileCheck is now built/vendored via the MIM_FILECHECK CMake option instead of assumed to be on PATH, later pinned to a specific release; on Windows, its MinGW runtime DLLs are staged alongside it and its PE header is restamped so msys bash can execute it.
  • All test suites (lit, gtest, and now the Python suite) consolidated under one test-all target.
  • Python bindings switched from pybind11 to nanobind.

Docs

  • Developer docs (docs/phases.md and related) updated to describe the current Phase/RWPhase/PhaseMan pipeline, reflecting the phase-infrastructure and Var/binder work above.

Pull Requests Merged

Read more

Contributors

fodinabor, leissa, and 5 other contributors
Loading

MimIR 0.1

MimIR 0.1

Choose a tag to compare

View all tags
@leissa leissa released this 03 May 22:39
v0.1
6be8bcb

MimIR is a pure, graph-based, higher-order intermediate representation rooted in the Calculus of Constructions.

About This Release

Version 0.1 marks the first official release of MimIR, a compiler IR evolved from the Thorin project. This release represents the stabilization of the core IR, type system, plugin architecture, and tooling after years of development.

Key Features

  • Higher-order IR: First-class functions, type operators, and parametric polymorphism with dependent types
  • Extensible Plugin System: Domain-specific axioms, types, normalizers, and code generation backends
  • Scopeless SSA: A novel IR design based on free-variable nesting instead of dominance, well-suited for higher-order programs
  • Sea-of-Nodes Style: On-the-fly normalization, type checking, and partial evaluation
  • Multi-Platform: Builds and tests on Linux, macOS, and Windows

Ideal For

  • DSL compilers
  • Tensor compilers
  • Automatic differentiation systems
  • Regex engines and other systems requiring high-performance code from high-level abstractions

Documentation

Full documentation is available at mimir.github.io, including the Command-Line Reference, Language Reference, Plugin Guide, and Developer Guide.

Loading