(address . guix-patches@gnu.org)
8734mxnp42.fsf@antr.me
Change-Id: I50eb1d2f39573ef8373aa1eb00f0741f4e36f938
---
Work in progress. Updates Lean to 4.10, adds lean-build-system, and a
few of the most common Lean 4 libraries.
What is left to do:
1. mathlib won't build because lake (Lean's package manager/build tool)
tries to fetch dependencies over git. I created an upstream issue to
fix this here: https://github.com/leanprover/lean4/issues/5122
2. test emacs-lean4-mode
3. cleanup and split commits
doc/guix.texi | 8 +
gnu/packages/lean.scm | 309 ++++++++++++++++++++++++++++---
guix/build-system/lean.scm | 181 ++++++++++++++++++
guix/build/lean-build-system.scm | 116 ++++++++++++
4 files changed, 588 insertions(+), 26 deletions(-)
create mode 100644 guix/build-system/lean.scm
create mode 100644 guix/build/lean-build-system.scm
Toggle diff (470 lines)
diff --git a/doc/guix.texi b/doc/guix.texi
index fcaf6b3fbb..5f32ee64b3 100644
--- a/doc/guix.texi
+++ b/doc/guix.texi
@@ -9673,6 +9673,14 @@ Build Systems
are provided.
@end defvar
+@defvar lean-build-system
+This build system is for Lean 4 packages that can be built and tested
+using the Lake build tool. It does not currently build documentation.
+
+Lean library dependencies should be specified in the
+@code{propagated-inputs} field.
+@end defvar
+
@defvar maven-build-system
This variable is exported by @code{(guix build-system maven)}. It implements
a build procedure for @uref{https://maven.apache.org, Maven} packages. Maven
diff --git a/gnu/packages/lean.scm b/gnu/packages/lean.scm
index 1533200426..0b4d506535 100644
--- a/gnu/packages/lean.scm
+++ b/gnu/packages/lean.scm
@@ -4,6 +4,7 @@
;;; Copyright © 2020 Tobias Geerinckx-Rice <me@tobias.gr>
;;; Copyright © 2022 Pradana Aumars <paumars@courrier.dev>
;;; Copyright © 2023 Zhu Zihao <all_but_last@163.com>
+;;; Copyright © 2024 Antero Mejr <mail@antr.me>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -21,60 +22,110 @@
;;; along with GNU Guix. If not, see <http://www.gnu.org/licenses/>.
(define-module (gnu packages lean)
- #:use-module (gnu packages bash)
- #:use-module (gnu packages multiprecision)
#:use-module (guix build-system cmake)
+ #:use-module (guix build-system emacs)
+ #:use-module (guix build-system lean)
#:use-module (guix build-system python)
- #:use-module ((guix licenses) #:prefix license:)
+ #:use-module (guix download)
#:use-module (guix gexp)
- #:use-module (guix packages)
#:use-module (guix git-download)
- #:use-module (guix download)
+ #:use-module (guix packages)
+ #:use-module (guix platform)
+ #:use-module (guix utils)
+ #:use-module ((guix licenses) #:prefix license:)
+ #:use-module (gnu packages base)
#:use-module (gnu packages graphviz)
- #:use-module (gnu packages version-control)
+ #:use-module (gnu packages libevent)
+ #:use-module (gnu packages multiprecision)
+ #:use-module (gnu packages perl)
#:use-module (gnu packages python-build)
#:use-module (gnu packages python-crypto)
#:use-module (gnu packages python-web)
- #:use-module (gnu packages python-xyz))
+ #:use-module (gnu packages python-xyz)
+ #:use-module (gnu packages version-control))
(define-public lean
(package
(name "lean")
- (version "3.51.1")
- (home-page "https://lean-lang.org" )
+ (version "4.10.0") ;TODO: when updating, update mathlib deps as well
(source (origin
(method git-fetch)
(uri (git-reference
- (url "https://github.com/leanprover-community/lean")
+ (url "https://github.com/leanprover/lean4")
(commit (string-append "v" version))))
(file-name (git-file-name name version))
(sha256
(base32
- "17g4d3lqnbl1yfy2pjannf73v8qhc5003d2jkmrqiy05zkqs8d9n"))))
+ "1q0xfg0apzb0dwj71k46w5218hwm2k890cgslwzr4mlyhvrspmcl"))))
(build-system cmake-build-system)
- (inputs
- (list gmp))
(arguments
- (list
- #:build-type "Release" ; default upstream build type
- ;; XXX: Test phases currently fail on 32-bit sytems.
- ;; Tests for those architectures have been temporarily
- ;; disabled, pending further investigation.
- #:tests? (and (not (%current-target-system))
- (let ((arch (%current-system)))
- (not (or (string-prefix? "i686" arch)
- (string-prefix? "armhf" arch)))))
- #:phases
- #~(modify-phases %standard-phases
- (add-before 'configure 'chdir-to-src
- (lambda _ (chdir "src"))))))
+ (list #:build-type "Release" ;default upstream build type
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'unpack 'patch
+ (lambda _
+ (substitute* "stage0/src/CMakeLists.txt"
+ (("set\\(LEAN_PLATFORM_TARGET.*$")
+ (format #f "\
+set(LEAN_PLATFORM_TARGET \"~a-linux-gnu\" CACHE STRING \
+\"LLVM triple of the target platform\")\n"
+ #$(platform-linux-architecture
+ (lookup-platform-by-target-or-system
+ (or (%current-target-system)
+ (%current-system)))))))
+ (substitute* '("src/lean.mk.in"
+ "src/stdlib.make.in"
+ "stage0/src/lean.mk.in"
+ "stage0/src/stdlib.make.in")
+ (("/usr/bin/env bash")
+ (which "bash")))
+ (substitute* "src/lake/examples/reverse-ffi/Makefile"
+ (("cc -o")
+ "gcc -o")))))))
+ (native-search-paths
+ (list (search-path-specification
+ (variable "LEAN_PATH")
+ (files (list (string-append "lib/lean"
+ (version-major+minor version)
+ "/packages"))))))
+ (native-inputs (list diffutils git-minimal perl))
+ (inputs (list gmp libuv))
(synopsis "Theorem prover and programming language")
+ (home-page "https://lean-lang.org")
(description
"Lean is a theorem prover and programming language with a small trusted
core based on dependent typed theory, aiming to bridge the gap between
interactive and automated theorem proving.")
(license license:asl2.0)))
+(define-public lean3
+ (package
+ (inherit lean)
+ (name "lean")
+ (version "3.51.1")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/leanprover-community/lean")
+ (commit (string-append "v" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "17g4d3lqnbl1yfy2pjannf73v8qhc5003d2jkmrqiy05zkqs8d9n"))))
+ (arguments
+ (list #:build-type "Release"
+ ;; XXX: Test phases currently fail on 32-bit sytems.
+ ;; Tests for those architectures have been temporarily
+ ;; disabled, pending further investigation.
+ #:tests? (and (not (%current-target-system))
+ (let ((arch (%current-system)))
+ (not (or (string-prefix? "i686" arch)
+ (string-prefix? "armhf" arch)))))
+ #:phases #~(modify-phases %standard-phases
+ (add-before 'configure 'chdir-to-src
+ (lambda _ (chdir "src"))))))
+ (inputs (list gmp))))
+
(define-public python-mathlibtools
(package
(name "python-mathlibtools")
@@ -108,3 +159,209 @@ (define-public python-mathlibtools
"This package contains @command{leanproject}, a supporting tool for Lean
mathlib, a mathematical library for the Lean theorem prover.")
(license license:asl2.0)))
+
+(define-public emacs-lean4-mode
+ (let ((commit "da7b63d854d010d621e2c82a53d6ae2d94dd53b0") ;no releases
+ (revision "0"))
+ (package
+ (name "emacs-lean4-mode")
+ (version (git-version "0.1.0" revision commit))
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/leanprover-community/lean4-mode")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "0vj9vrfkgm7plp5mvq22fm9sln11j9763g3wd2w6c82rlsk6dhva"))))
+ (build-system emacs-build-system)
+ (home-page "https://github.com/leanprover-community/lean4-mode")
+ (synopsis "Emacs major mode for the Lean 4 theorem prover")
+ (description
+ "This package provides a major mode and utilities for working with the
+Lean 4 theorem prover.")
+ (license license:asl2.0))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Please keep everything below here alphabetized.
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define-public lean-aesop
+ (package
+ (name "lean-aesop")
+ (version "4.10.0") ;matches the version of lean package
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/leanprover-community/aesop")
+ (commit (string-append "v" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "039rdy7lldkvbl8gvln4v912b9pyx0952mqad49g755yvhgq7zw0"))))
+ (build-system lean-build-system)
+ (propagated-inputs (list lean-batteries))
+ (home-page
+ "https://leanprover-community.github.io/mathlib4_docs/Aesop.html")
+ (synopsis "Proof search tactic for the Lean theorem prover")
+ (description
+ "@acronym{Aesop,Automated Extensible Search for Obvious Proofs} is a
+proof search tactic for Lean 4. It is broadly similar to Isabelle's
+@code{auto}.")
+ (license license:asl2.0)))
+
+(define-public lean-batteries
+ (package
+ (name "lean-batteries")
+ (version "4.10.0") ;matches the version of lean package
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/leanprover-community/batteries")
+ (commit (string-append "v" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "0q7wcbx3wl318k8x0hh846bdnh960kiqv9bvs83yzwlnqsvgiiga"))))
+ (build-system lean-build-system)
+ (home-page
+ "https://leanprover-community.github.io/mathlib4_docs/Batteries.html")
+ (synopsis "Extended standard library for the Lean theorem prover")
+ (description
+ "This package provides a a collection of data structures and tactics
+intended for use by both computer-science applications and mathematics
+applications of Lean 4.")
+ (license license:asl2.0)))
+
+(define-public lean-cli
+ (let ((commit "2cf1030dc2ae6b3632c84a09350b675ef3e347d0")
+ (revision "0"))
+ (package
+ (name "lean-cli")
+ (version (git-version "4.10.0" revision commit)) ;matches lean version
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/leanprover/lean4-cli")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "0vj9vrfkgm7plp5mvq22fm9sln11j9763g3wd2w6c82rlsk6dhva"))))
+ (build-system lean-build-system)
+ (home-page "https://github.com/leanprover/lean4-cli")
+ (synopsis "Lean library for creating command-line interfaces")
+ (description
+ "This package provides a Lean library for creating command-line
+interfaces and argument parsing, using a @acronym{DSL, domain-specific
+language}.")
+ (license license:asl2.0))))
+
+(define-public lean-importgraph
+ (package
+ (name "lean-importgraph")
+ (version "4.10.0") ;matches the version of lean package
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/leanprover-community/import-graph")
+ (commit (string-append "v" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "0vj9vrfkgm7plp5mvq22fm9sln11j9763g3wd2w6c82rlsk6dhva"))))
+ (build-system lean-build-system)
+ (propagated-inputs (list lean-batteries lean-cli))
+ (home-page "https://github.com/leanprover-community/import-graph")
+ (synopsis "Lean tool for generating import graphs of Lake packages")
+ (description
+ "This package provides a tool to generate import graphs of packages for
+Lean's Lake package manager.")
+ (license license:asl2.0)))
+
+(define-public lean-mathlib
+ (package
+ (name "lean-mathlib")
+ (version "4.10.0") ;matches the version of lean package
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/leanprover-community/mathlib4")
+ (commit (string-append "v" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "0qxif7ldrcbd8mrmy6rsxig41jbvffhs6vab3bix15pbil5z4x6q"))))
+ (build-system lean-build-system)
+ (propagated-inputs (list lean-aesop
+ lean-batteries
+ lean-importgraph
+ lean-proofwidgets
+ lean-qq))
+ (home-page "https://leanprover-community.github.io/mathlib4_docs/")
+ (synopsis "Math library for the Lean theorem prover")
+ (description
+ "This package provides a Lean library with proofs and tactics for
+programming and mathematics.")
+ (license license:asl2.0)))
+
+(define-public lean-proofwidgets
+ (package
+ (name "lean-proofwidgets")
+ (version "0.0.41")
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/leanprover-community/ProofWidgets4")
+ (commit (string-append "v" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "0vj9vrfkgm7plp5mvq22fm9sln11j9763g3wd2w6c82rlsk6dhva"))))
+ (build-system lean-build-system)
+ (propagated-inputs (list lean-batteries))
+ (home-page
+ "https://leanprover-community.github.io/mathlib4_docs/ProofWidgets.html")
+ (synopsis "User interface library for the Lean theorem prover")
+ (description
+ "This package provides a library of user interface components for Lean
+4. It supports:
+@itemize
+@item{symbolic visualizations of mathematical objects and data structures}
+@item{data visualization}
+@item{interfaces for tactics and tactic modes}
+@item{alternative and domain-specific goal state displays}
+@item{user interfaces for entering expressions and editing proofs}
+@end itemize")
+ (license license:asl2.0)))
+
+(define-public lean-qq
+ (let ((commit "71f54425e6fe0fa75f3aef33a2813a7898392222") ;no tags
+ (revision "0"))
+ (package
+ (name "lean-qq")
+ (version (git-version "4.10.0" revision commit)) ;match lean version
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/leanprover-community/quote4")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "0d5qihwqh17ajld2lxjai2y0s0a5551y19da1y8azihlmy540nc8"))))
+ (build-system lean-build-system)
+ (arguments (list #:tests? #f)) ;no tests
+ (home-page
+ "https://leanprover-community.github.io/mathlib4_docs/Qq.html")
+ (synopsis "Lean library for type-safe expression quotations")
+ (description
+ "This package provides a Lean library for type-safe expression
+quotations, which are a particularly convenient way of constructing
+object-level expressions (Expr) in meta-level code.")
+ (license license:asl2.0))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; New Lean packages should be alphabetized above.
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
diff --git a/guix/build-system/lean.scm b/guix/build-system/lean.scm
new file mode 100644
index 0000000000..4d8519b2c8
--- /dev/null
+++ b/guix/build-system/lean.scm
@@ -0,0 +1,181 @@
+;;; GNU Guix --- Functional package management for GNU
+;;; Copyright © 2024 Antero Mejr <mail@antr.me>
+;;;
+;;; This file is part of GNU Guix.
+;;;
+;;; GNU Guix is free software; you can redistribute it and/or modify it
+;;; under the terms of the GNU General Public License as published by
+;;; the Free Software Foundation; either version 3 of the License, or (at
+;;; your option) any later version.
+;;;
+;;; GNU Guix is distributed in the hope that it will be useful, but
+;;; WITHOUT ANY WARRANTY; without even the implied warranty of
+;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+;;; GNU General Public License for more details.
+;;;
+;;; You should have received a copy of the GNU General Public License
+;;; along with GNU Guix. If not, see <http://www.gnu.org/licenses/>.
+
+(define-module (guix build-system lean)
+ #:use-module (guix search-paths)
+ #:use-module (guix store)
+ #:use-module (guix utils)
+ #:use-module (guix gexp)
+ #:use-module (guix monads)
+ #:use-module (guix packages)
+ #:use-module (guix build-system)
+ #:use-module (guix build-system gnu)
+ #:use-module (ice-9 match)
+ #:use-module (srfi srfi-26)
+ #:export (lean-build-system))
+
+(define (default-lean)
+ "Return the default lean package."
+ ;; Lazily resolve the binding to avoid a circular dependency.
+ (let ((lean (resolve-interface '(gnu packages lean))))
+ (module-ref lean 'lean)))
+
+(define %lean-build-system-modules
+ ;; Build-side modules imported by default.
+ `((guix build lean-build-system)
+ ,@%gnu-build-system-modules))
+
+(define* (lean-build name inputs
+ #:key
+ source
+ (tests? #t)
+ (phases '%standard-phases)
+ (lean-lake-targets ''())
+ (outputs '("out"))
+ (search-paths '())
+ (system (%current-system))
+ (guile #f)
+ (imported-modules %lean-build-system-modules)
+ (modules '((guix build lean-build-system)
+ (guix build utils))))
+ "Build SOURCE using Lean, and with INPUTS."
+ (define builder
+ (with-imported-modules imported-modules
+ #~(begin
+ (use-modules #$@(sexp->gexp modules))
+ (lean-build #:name #$name
+ #:source #+source
+ #:system #$system
+ #:tests? #$tests?
+ #:phases #$phases
+ #:lean-lake-targets #$lean-lake-targets
+ #:outputs #$(outputs->gexp outputs)
+ #:search-paths '#$(sexp->gexp
+ (map search-path-specification->sexp
+ search-paths))
+ #:inputs #$(input-tuples->gexp inputs)))))
+
+ (mlet %store-monad ((guile (package->derivation (or guile (default-guile))
+ system #:graft? #f)))
+ (gexp->derivation name builder
+ #:system system
+ #:guile-for-build guile)))
+
+(define* (lean-cross-build name
+ #:key
+ source target
+ build-inputs target-inputs host-inputs
+ (phases '%standard-phases)
+ (lean-lake-targets '())
+ (outputs '("out"))
This message was truncated. Download the full message here.