Package Request: Lean3 and Lean4 theorem prover

byrongibson commented 3 years ago

Project description

Lean is a functional programming language and interactive theorem prover. Currently Nixpkgs provides the older versions, Lean and Lean2 (broken in 21.11). It appears the maintainer requires Python2, and Lean 3 and 4 are Python 3.

The current stable version is Lean3, but it is EoL'd. All development has moved to Lean4, but it does not have stable release yet and is not backwards compatible with prior versions.

It might be nice to have both Lean3 and Lean4 added to nixpkgs, for more up-to-date experimentation and usage. Fwiw, it appears Lean4 is being developed on NixOS, given the default.nix, flake.nix, and shell.nix files in its repo.

Metadata

homepage URL: https://leanprover.github.io/
source URL: Lean3: https://github.com/leanprover/lean; Lean4: https://github.com/leanprover/lean4
license: Apache 2.0 (both versions)
platforms: unix, linux, darwin

armeenm commented 2 years ago

Hi,

As far as I can tell, nixpkgs currently has support for lean3 as both lean and lean3. Am I mistaken?

divanorama commented 1 year ago

lean3 seems to be is in nixpkgs now. Lean4 has an experimental flake setup in their repo&docs https://leanprover.github.io/lean4/doc/setup.html#nix-setup don't know if it'd be better to package in or leave as is for now

marsam commented 1 year ago

addressed by https://github.com/NixOS/nixpkgs/pull/235517

NixOS / nixpkgs

Package Request: Lean3 and Lean4 theorem prover #141437