Markus Himmel f0c190239a

feat: compile against Windows SDK headers under Windows (#5753 )

Breaking changes:

To build Lean from source on Windows, it is now necessary to install the
[Windows
SDK](https://developer.microsoft.com/en-us/windows/downloads/windows-sdk/).
The build instructions have been updated to reflect this. Note that the
Windows SDK is **not** needed to compile Lean programs using a Lean
toolchain obtained using `elan`. The Windows SDK is only needed to build
Lean itself from source.

Furthermore, we are dropping support for Windows versions older than
Windows 10 1903 (released in May 2019).

No Windows version that is still supported by Microsoft as part of
mainstream support is affected by this.

The following Windows versions are still supported by Microsoft as part
of commercial extended support but are no longer supported by Lean:

- Windows 10 Enterprise LTSC 2015
- Windows 10 Enterprise LTSC 2016
- Windows 10 Enterprise LTSC 2019
- Windows Server 2019

2024-10-22 13:00:02 +00:00

2.5 KiB

Raw Blame History

Supported Platforms

Tier 1

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+
aarch64 (Apple Silicon) macOS 10.15+
x86-64 Windows 11 (any version), Windows 10 (version 1903 or higher), Windows Server 2022

Tier 2

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+
x86 (32-bit) Linux
Emscripten Web Assembly

Setting Up Lean

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 instead:

$ 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

`lake`

Lean 4 comes with a package manager named lake. Use 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 foo is

lakefile.lean  # package configuration
lean-toolchain # specifies the lean version to use
Foo.lean       # main file, import via `import Foo`
Foo/
  A.lean       # further files, import via e.g. `import Foo.A`
  A/...        # further nesting
.lake/         # `lake` build output directory

After running lake build you will see a binary named ./.lake/build/bin/foo and when you run it you should see the output:

Hello, world!

Editing

Lean implements the Language Server Protocol that can be used for interactive development in Emacs, VS Code, and possibly other editors.

Changes must be saved to be visible in other files, which must then be invalidated using an editor command (see links above).

2.5 KiB Raw Blame History