Platforms built & tested by our CI, available as binary releases via elan (see below)
- x86-64 Linux with glibc 2.27+
- x86-64 macOS 10.15+
- x86-64 Windows 10+
Platforms cross-compiled but not tested by our CI, available as binary releases
Releases may be silently broken due to the lack of automated testing. Issue reports and fixes are welcome.
- aarch64 Linux with glibc 2.27+
- aarch64 (Apple Silicon) macOS
- x86 (32-bit) Linux
- Emscripten Web Assembly
See also the quickstart instructions for a standard setup with VS Code as the editor.
Release builds for all supported platforms are available at https://github.com/leanprover/lean4/releases.
Instead of downloading these and setting up the paths manually, however, it is recommended to use the Lean version manager
$ elan self update # in case you haven't updated elan in a while
# download & activate latest Lean 4 stable release (https://github.com/leanprover/lean4/releases)
$ elan default leanprover/lean4:stable
Lean 4 comes with a package manager named
lake init foo to initialize a Lean package
foo in the current directory, and
lake build to typecheck and build it as well as all its dependencies. Use
lake help to learn about further commands.
The general directory structure of a package
lakefile.lean # package configuration
lean-toolchain # specifies the lean version to use
Foo.lean # main file, import via `import Foo`
A.lean # further files, import via e.g. `import Foo.A`
A/... # further nesting
.lake/ # `lake` build output directory
lake build you will see a binary named
./.lake/build/bin/foo and when you run it you should see the output:
Changes must be saved to be visible in other files, which must then be invalidated using an editor command (see links above).