Lean 4: Difference between revisions
m Added heading for references |
|||
| (One intermediate revision by the same user not shown) | |||
| Line 1: | Line 1: | ||
[https://lean-lang.org/ Lean 4] is a pure functional programming language and an interactive theorem prover base on dependent type theory<ref>"The Lean Language Reference", leanprover contributors, https://lean-lang.org/doc/reference/latest/ (Fetched 2026-09-14)</ref>. | |||
== Building Lean 4 projects == | == Building Lean 4 projects == | ||
Use the following<syntaxhighlight lang="nix" line="1"> | Use the following<syntaxhighlight lang="nix" line="1"> | ||
| Line 10: | Line 12: | ||
</syntaxhighlight> | </syntaxhighlight> | ||
== Installing Lean 4 == | |||
Lean4 is available as a package, both on the packages [https://search.nixos.org/packages?channel=26.05&query=lean4#show=lean4 26.05 channel] and the [https://search.nixos.org/packages?channel=unstable&query=lean4#show=lean4 unstable channel], and they may be installed according to their provided instructions. Below is an example of a minimal Lean 4 flake.<syntaxhighlight lang="nix" line="1"> | |||
{ | |||
description = "Minimal Lean 4 flake."; | |||
inputs = { | |||
nixpkgs.url = "github:NixOS/nixpkgs/nixos-26.05"; | |||
}; | |||
outputs = { self, nixpkgs }@inputs: | |||
let | |||
system = "x86_64-linux"; | |||
pkgs = nixpkgs.legacyPackages.${system}; | |||
in | |||
{ | |||
devShells.${system}.default = pkgs.mkShell { | |||
packages = with pkgs; [ | |||
lean4 | |||
]; | |||
}; | |||
}; | |||
} | |||
</syntaxhighlight> | |||
== Text Editors == | |||
Lean provides an official extension for [https://github.com/leanprover/vscode-lean4 VS Code], but community extensions can also be found for other editors such as [https://github.com/leanprover-community/lean4-mode emacs], [https://github.com/Julian/lean.nvim neovim], cursor and so on. Please note, that Lean FRO recommends installing Lean through the officially supported VS Code extension<ref>"Install Lean", Lean FRO, https://lean-lang.org/install/ (Fetched 2026-09-14)</ref>. | |||
=== Lean4-mode - major mode for Emacs === | |||
[https://github.com/leanprover-community leanprover-community] provides a lean major mode for emacs called [https://github.com/leanprover-community/lean4-mode "lean4-mode"]. However, the provided major mode seems to not be receiving updates, and according to community discussions, it has split up into a number of different forks, with different features and support<ref>"lean4-mode - commits", lean4-mode contributors, https://github.com/leanprover-community/lean4-mode/commits/master/ (Fetched 2026-09-14)</ref><ref>Emacs mode discussions, https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs/topic/Meta/near/580208083 (Fetched 2026-09-14)</ref>. While the version provided by leanprover-community supports [https://github.com/emacs-lsp/lsp-mode lsp-mode], the fork by GitHub user [https://github.com/bustercopley bustercopley] supports [https://github.com/joaotavora/eglot eglot] instead<ref>"Use Eglot isntead of lsp-mode", bustercopley, https://github.com/leanprover-community/lean4-mode/commit/b08114632a756e9e2a5b59b89c2b0d79bd6dae6c (Fetched 2026-09-14)</ref>. | |||
== References == | |||
Latest revision as of 10:03, 14 September 2026
Lean 4 is a pure functional programming language and an interactive theorem prover base on dependent type theory[1].
Building Lean 4 projects
Use the following
leanPackages.buildLakePackage {
pname = "my-project";
version = "0.1.0";
src = ./.;
leanDeps = with leanPackages; [ mathlib ];
lakeHash = null; # all deps nix-managed; set to lib.fakeHash for Lake-managed deps
}
Installing Lean 4
Lean4 is available as a package, both on the packages 26.05 channel and the unstable channel, and they may be installed according to their provided instructions. Below is an example of a minimal Lean 4 flake.
{
description = "Minimal Lean 4 flake.";
inputs = {
nixpkgs.url = "github:NixOS/nixpkgs/nixos-26.05";
};
outputs = { self, nixpkgs }@inputs:
let
system = "x86_64-linux";
pkgs = nixpkgs.legacyPackages.${system};
in
{
devShells.${system}.default = pkgs.mkShell {
packages = with pkgs; [
lean4
];
};
};
}
Text Editors
Lean provides an official extension for VS Code, but community extensions can also be found for other editors such as emacs, neovim, cursor and so on. Please note, that Lean FRO recommends installing Lean through the officially supported VS Code extension[2].
Lean4-mode - major mode for Emacs
leanprover-community provides a lean major mode for emacs called "lean4-mode". However, the provided major mode seems to not be receiving updates, and according to community discussions, it has split up into a number of different forks, with different features and support[3][4]. While the version provided by leanprover-community supports lsp-mode, the fork by GitHub user bustercopley supports eglot instead[5].
References
- ↑ "The Lean Language Reference", leanprover contributors, https://lean-lang.org/doc/reference/latest/ (Fetched 2026-09-14)
- ↑ "Install Lean", Lean FRO, https://lean-lang.org/install/ (Fetched 2026-09-14)
- ↑ "lean4-mode - commits", lean4-mode contributors, https://github.com/leanprover-community/lean4-mode/commits/master/ (Fetched 2026-09-14)
- ↑ Emacs mode discussions, https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs/topic/Meta/near/580208083 (Fetched 2026-09-14)
- ↑ "Use Eglot isntead of lsp-mode", bustercopley, https://github.com/leanprover-community/lean4-mode/commit/b08114632a756e9e2a5b59b89c2b0d79bd6dae6c (Fetched 2026-09-14)