* [bug#72755] [WIP][PATCH] guix: Add lean-build-system.
@ 2024-08-22 4:44 Antero Mejr
2024-12-07 7:23 ` Divya Ranjan via Guix-patches via
0 siblings, 1 reply; 4+ messages in thread
From: Antero Mejr @ 2024-08-22 4:44 UTC (permalink / raw)
To: 72755
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
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"))
+ (search-paths '())
+ (native-search-paths '())
+ (tests? #t)
+ (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))
+
+ (define %build-host-inputs
+ #+(input-tuples->gexp build-inputs))
+
+ (define %build-target-inputs
+ (append #$(input-tuples->gexp host-inputs)
+ #+(input-tuples->gexp target-inputs)))
+
+ (define %build-inputs
+ (append %build-host-inputs %build-target-inputs))
+
+ (define %outputs
+ #$(outputs->gexp outputs))
+
+ (lean-build #:name #$name
+ #:source #+source
+ #:system #$system
+ #:phases #$phases
+ #:outputs %outputs
+ #:target #$target
+ #:inputs %build-target-inputs
+ #:native-inputs %build-host-inputs
+ #:search-paths '#$(map search-path-specification->sexp
+ search-paths)
+ #:native-search-paths '#$(map
+ search-path-specification->sexp
+ native-search-paths)
+ #:lean-lake-targets #$lean-lake-targets
+ #:tests? #$tests?
+ #:search-paths '#$(sexp->gexp
+ (map search-path-specification->sexp
+ search-paths))))))
+
+ (mlet %store-monad ((guile (package->derivation (or guile (default-guile))
+ system #:graft? #f)))
+ (gexp->derivation name builder
+ #:system system
+ #:target target
+ #:graft? #f
+ #:substitutable? substitutable?
+ #:guile-for-build guile)))
+
+(define* (lower name
+ #:key source inputs native-inputs outputs system target
+ (lean (default-lean))
+ #:allow-other-keys
+ #:rest arguments)
+ "Return a bag for NAME."
+
+ (define private-keywords
+ '(#:target #:lean #:inputs #:native-inputs #:outputs))
+
+ (bag
+ (name name)
+ (system system)
+ (target target)
+ (build-inputs `(,@(if source
+ `(("source" ,source))
+ '())
+ ,@`(("lean" ,lean))
+ ,@native-inputs
+ ,@(if target '() inputs)
+ ,@(if target
+ ;; Use the standard cross inputs of
+ ;; 'gnu-build-system'.
+ (standard-cross-packages target 'host)
+ '())
+ ;; Keep the standard inputs of 'gnu-build-system'.
+ ,@(standard-packages)))
+ (host-inputs (if target inputs '()))
+ (target-inputs (if target
+ (standard-cross-packages target 'target)
+ '()))
+ (outputs outputs)
+ (build (if target lean-cross-build lean-build))
+ (arguments (strip-keyword-arguments private-keywords arguments))))
+
+(define lean-build-system
+ (build-system
+ (name 'lean)
+ (description
+ "Lean build system, to build Lean 4 packages using Lake")
+ (lower lower)))
diff --git a/guix/build/lean-build-system.scm b/guix/build/lean-build-system.scm
new file mode 100644
index 0000000000..81cb38e597
--- /dev/null
+++ b/guix/build/lean-build-system.scm
@@ -0,0 +1,116 @@
+;;; 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 lean-build-system)
+ #:use-module ((guix build gnu-build-system) #:prefix gnu:)
+ #:use-module (guix build utils)
+ #:use-module (ice-9 match)
+ #:use-module (ice-9 ftw)
+ #:use-module (ice-9 format)
+ #:use-module (srfi srfi-1)
+ #:use-module (srfi srfi-26)
+ #:export (%standard-phases
+ add-installed-lean-path
+ lean-build))
+
+(define (lean-version lean)
+ (let* ((version (last (string-split lean #\-)))
+ (components (string-split version #\.))
+ (major+minor (take components 2)))
+ (string-join major+minor ".")))
+
+(define (lib-dir inputs outputs)
+ "Return the path of the current output's Lean package directory."
+ (let ((out (assoc-ref outputs "out"))
+ (lean (assoc-ref inputs "lean")))
+ (string-append out "/lib/lean" (lean-version lean) "/packages")))
+
+(define (add-installed-lean-path inputs outputs)
+ "Prepend the site-package of OUTPUT to LEAN_PATH. This is useful when
+running checks after installing the package."
+ (let ((path-env (getenv "LEAN_PATH")))
+ (if path-env
+ (setenv "LEAN_PATH" (string-append (lib-dir inputs outputs) ":"
+ path-env))
+ (setenv "LEAH_PATH" (string-append (lib-dir inputs outputs))))))
+
+(define* (build #:key lean-lake-targets #:allow-other-keys)
+ "Build a given Lean 4 package."
+ (let ((call (cons* "lake" "build" lean-lake-targets)))
+ (format #t "running: ~s\n" call)
+ (apply invoke call)))
+
+(define* (check #:key tests? #:allow-other-keys)
+ "Run all the tests"
+ (when tests?
+ (let ((call '("lake" "test")))
+ (format #t "running: ~s\n" call)
+ (apply invoke call))))
+
+(define* (install #:key inputs outputs #:allow-other-keys)
+ "Install a given Lean 4 package."
+ (let ((out (lib-dir inputs outputs)))
+ (format #t "installing Lean library to: ~s\n" out)
+ (copy-recursively ".lake/build/lib" out)))
+
+(define* (wrap #:key inputs outputs #:allow-other-keys)
+ (define (list-of-files dir)
+ (find-files dir (lambda (file stat)
+ (and (eq? 'regular (stat:type stat))
+ (not (wrapped-program? file))))))
+
+ (define bindirs
+ (append-map (match-lambda
+ ((_ . dir)
+ (list (string-append dir "/bin")
+ (string-append dir "/sbin"))))
+ outputs))
+
+ ;; Do not require "bash" to be present in the package inputs
+ ;; even when there is nothing to wrap.
+ ;; Also, calculate (sh) only once to prevent some I/O.
+ (define %sh (delay (search-input-file inputs "bin/bash")))
+ (define (sh) (force %sh))
+
+ (let* ((var `("LEAN_PATH" prefix
+ ,(search-path-as-string->list
+ (or (getenv "LEAN_PATH") "")))))
+ (for-each (lambda (dir)
+ (let ((files (list-of-files dir)))
+ (for-each (cut wrap-program <> #:sh (sh) var)
+ files)))
+ bindirs)))
+
+(define* (add-install-to-lean-path #:key inputs outputs #:allow-other-keys)
+ "A phase that just wraps the 'add-installed-lean-path' procedure."
+ (add-installed-lean-path inputs outputs))
+
+(define %standard-phases
+ (modify-phases gnu:%standard-phases
+ (delete 'bootstrap)
+ (delete 'configure)
+ (replace 'build build)
+ (replace 'check check)
+ (replace 'install install)
+ (add-after 'install 'add-install-to-lean-path add-install-to-lean-path)
+ (add-after 'add-install-to-lean-path 'wrap wrap)))
+
+(define* (lean-build #:key inputs (phases %standard-phases)
+ #:allow-other-keys #:rest args)
+ "Build the given Lean package, applying all of PHASES in order."
+ (apply gnu:gnu-build #:inputs inputs #:phases phases args))
base-commit: a1d367d6ee8c1783ef94cebbc5f2ae3b7a08078d
--
2.45.1
^ permalink raw reply related [flat|nested] 4+ messages in thread* [bug#72755] [WIP][PATCH] guix: Add lean-build-system.
2024-08-22 4:44 [bug#72755] [WIP][PATCH] guix: Add lean-build-system Antero Mejr
@ 2024-12-07 7:23 ` Divya Ranjan via Guix-patches via
2024-12-07 18:03 ` Antero Mejr
0 siblings, 1 reply; 4+ messages in thread
From: Divya Ranjan via Guix-patches via @ 2024-12-07 7:23 UTC (permalink / raw)
To: Antero Mejr; +Cc: 72755
Antero Mejr <mail@antr.me> writes:
> 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
>
> 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"))
> + (search-paths '())
> + (native-search-paths '())
> + (tests? #t)
> + (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))
> +
> + (define %build-host-inputs
> + #+(input-tuples->gexp build-inputs))
> +
> + (define %build-target-inputs
> + (append #$(input-tuples->gexp host-inputs)
> + #+(input-tuples->gexp target-inputs)))
> +
> + (define %build-inputs
> + (append %build-host-inputs %build-target-inputs))
> +
> + (define %outputs
> + #$(outputs->gexp outputs))
> +
> + (lean-build #:name #$name
> + #:source #+source
> + #:system #$system
> + #:phases #$phases
> + #:outputs %outputs
> + #:target #$target
> + #:inputs %build-target-inputs
> + #:native-inputs %build-host-inputs
> + #:search-paths '#$(map search-path-specification->sexp
> + search-paths)
> + #:native-search-paths '#$(map
> + search-path-specification->sexp
> + native-search-paths)
> + #:lean-lake-targets #$lean-lake-targets
> + #:tests? #$tests?
> + #:search-paths '#$(sexp->gexp
> + (map search-path-specification->sexp
> + search-paths))))))
> +
> + (mlet %store-monad ((guile (package->derivation (or guile (default-guile))
> + system #:graft? #f)))
> + (gexp->derivation name builder
> + #:system system
> + #:target target
> + #:graft? #f
> + #:substitutable? substitutable?
> + #:guile-for-build guile)))
> +
> +(define* (lower name
> + #:key source inputs native-inputs outputs system target
> + (lean (default-lean))
> + #:allow-other-keys
> + #:rest arguments)
> + "Return a bag for NAME."
> +
> + (define private-keywords
> + '(#:target #:lean #:inputs #:native-inputs #:outputs))
> +
> + (bag
> + (name name)
> + (system system)
> + (target target)
> + (build-inputs `(,@(if source
> + `(("source" ,source))
> + '())
> + ,@`(("lean" ,lean))
> + ,@native-inputs
> + ,@(if target '() inputs)
> + ,@(if target
> + ;; Use the standard cross inputs of
> + ;; 'gnu-build-system'.
> + (standard-cross-packages target 'host)
> + '())
> + ;; Keep the standard inputs of 'gnu-build-system'.
> + ,@(standard-packages)))
> + (host-inputs (if target inputs '()))
> + (target-inputs (if target
> + (standard-cross-packages target 'target)
> + '()))
> + (outputs outputs)
> + (build (if target lean-cross-build lean-build))
> + (arguments (strip-keyword-arguments private-keywords arguments))))
> +
> +(define lean-build-system
> + (build-system
> + (name 'lean)
> + (description
> + "Lean build system, to build Lean 4 packages using Lake")
> + (lower lower)))
> diff --git a/guix/build/lean-build-system.scm b/guix/build/lean-build-system.scm
> new file mode 100644
> index 0000000000..81cb38e597
> --- /dev/null
> +++ b/guix/build/lean-build-system.scm
> @@ -0,0 +1,116 @@
> +;;; 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 lean-build-system)
> + #:use-module ((guix build gnu-build-system) #:prefix gnu:)
> + #:use-module (guix build utils)
> + #:use-module (ice-9 match)
> + #:use-module (ice-9 ftw)
> + #:use-module (ice-9 format)
> + #:use-module (srfi srfi-1)
> + #:use-module (srfi srfi-26)
> + #:export (%standard-phases
> + add-installed-lean-path
> + lean-build))
> +
> +(define (lean-version lean)
> + (let* ((version (last (string-split lean #\-)))
> + (components (string-split version #\.))
> + (major+minor (take components 2)))
> + (string-join major+minor ".")))
> +
> +(define (lib-dir inputs outputs)
> + "Return the path of the current output's Lean package directory."
> + (let ((out (assoc-ref outputs "out"))
> + (lean (assoc-ref inputs "lean")))
> + (string-append out "/lib/lean" (lean-version lean) "/packages")))
> +
> +(define (add-installed-lean-path inputs outputs)
> + "Prepend the site-package of OUTPUT to LEAN_PATH. This is useful when
> +running checks after installing the package."
> + (let ((path-env (getenv "LEAN_PATH")))
> + (if path-env
> + (setenv "LEAN_PATH" (string-append (lib-dir inputs outputs) ":"
> + path-env))
> + (setenv "LEAH_PATH" (string-append (lib-dir inputs outputs))))))
> +
> +(define* (build #:key lean-lake-targets #:allow-other-keys)
> + "Build a given Lean 4 package."
> + (let ((call (cons* "lake" "build" lean-lake-targets)))
> + (format #t "running: ~s\n" call)
> + (apply invoke call)))
> +
> +(define* (check #:key tests? #:allow-other-keys)
> + "Run all the tests"
> + (when tests?
> + (let ((call '("lake" "test")))
> + (format #t "running: ~s\n" call)
> + (apply invoke call))))
> +
> +(define* (install #:key inputs outputs #:allow-other-keys)
> + "Install a given Lean 4 package."
> + (let ((out (lib-dir inputs outputs)))
> + (format #t "installing Lean library to: ~s\n" out)
> + (copy-recursively ".lake/build/lib" out)))
> +
> +(define* (wrap #:key inputs outputs #:allow-other-keys)
> + (define (list-of-files dir)
> + (find-files dir (lambda (file stat)
> + (and (eq? 'regular (stat:type stat))
> + (not (wrapped-program? file))))))
> +
> + (define bindirs
> + (append-map (match-lambda
> + ((_ . dir)
> + (list (string-append dir "/bin")
> + (string-append dir "/sbin"))))
> + outputs))
> +
> + ;; Do not require "bash" to be present in the package inputs
> + ;; even when there is nothing to wrap.
> + ;; Also, calculate (sh) only once to prevent some I/O.
> + (define %sh (delay (search-input-file inputs "bin/bash")))
> + (define (sh) (force %sh))
> +
> + (let* ((var `("LEAN_PATH" prefix
> + ,(search-path-as-string->list
> + (or (getenv "LEAN_PATH") "")))))
> + (for-each (lambda (dir)
> + (let ((files (list-of-files dir)))
> + (for-each (cut wrap-program <> #:sh (sh) var)
> + files)))
> + bindirs)))
> +
> +(define* (add-install-to-lean-path #:key inputs outputs #:allow-other-keys)
> + "A phase that just wraps the 'add-installed-lean-path' procedure."
> + (add-installed-lean-path inputs outputs))
> +
> +(define %standard-phases
> + (modify-phases gnu:%standard-phases
> + (delete 'bootstrap)
> + (delete 'configure)
> + (replace 'build build)
> + (replace 'check check)
> + (replace 'install install)
> + (add-after 'install 'add-install-to-lean-path add-install-to-lean-path)
> + (add-after 'add-install-to-lean-path 'wrap wrap)))
> +
> +(define* (lean-build #:key inputs (phases %standard-phases)
> + #:allow-other-keys #:rest args)
> + "Build the given Lean package, applying all of PHASES in order."
> + (apply gnu:gnu-build #:inputs inputs #:phases phases args))
>
> base-commit: a1d367d6ee8c1783ef94cebbc5f2ae3b7a08078d
Hello, Antero
I’ve also been involved in packaging Lean4, have you had any more progress on this? I tried to build guix from your patch, but `./pre-inst-env guix build lean` gets stuck at some point after trying to compile things for ~7 hours. I believe it gets stuck at compiling gash. Any clue?
Regards,
Divya Ranjan
^ permalink raw reply [flat|nested] 4+ messages in thread* [bug#72755] [WIP][PATCH] guix: Add lean-build-system.
2024-12-07 7:23 ` Divya Ranjan via Guix-patches via
@ 2024-12-07 18:03 ` Antero Mejr
2024-12-07 22:13 ` Divya Ranjan via Guix-patches via
0 siblings, 1 reply; 4+ messages in thread
From: Antero Mejr @ 2024-12-07 18:03 UTC (permalink / raw)
To: Divya Ranjan; +Cc: 72755
Divya Ranjan <divya@subvertising.org> writes:
> I’ve also been involved in packaging Lean4, have you had any more progress on
> this? I tried to build guix from your patch, but `./pre-inst-env guix build
> lean` gets stuck at some point after trying to compile things for ~7 hours. I
> believe it gets stuck at compiling gash. Any clue?
You shouldn't have to rebuild the entire dependency chain (and things
like gash) to use the above patch - maybe someone on IRC or a maintainer
can help with fixing that?
The above patches should work for building Lean4, but packaging any Lean
library with dependencies (like mathlib) won't work until the lean
developers resolve this issue:
https://github.com/leanprover/lean4/issues/5122
Unfortunately the devs marked it as low priority and seem to be pushing
back against reproducible packaging, which is disappointing. I am
unlikely to continue work on this patch series, as I have switched over
to Coq.
^ permalink raw reply [flat|nested] 4+ messages in thread
* [bug#72755] [WIP][PATCH] guix: Add lean-build-system.
2024-12-07 18:03 ` Antero Mejr
@ 2024-12-07 22:13 ` Divya Ranjan via Guix-patches via
0 siblings, 0 replies; 4+ messages in thread
From: Divya Ranjan via Guix-patches via @ 2024-12-07 22:13 UTC (permalink / raw)
To: Antero Mejr; +Cc: 72755
Antero Mejr <mail@antr.me> writes:
> Divya Ranjan <divya@subvertising.org> writes:
>> I’ve also been involved in packaging Lean4, have you had any more progress on
>> this? I tried to build guix from your patch, but `./pre-inst-env guix build
>> lean` gets stuck at some point after trying to compile things for ~7 hours. I
>> believe it gets stuck at compiling gash. Any clue?
>
> You shouldn't have to rebuild the entire dependency chain (and things
> like gash) to use the above patch - maybe someone on IRC or a maintainer
> can help with fixing that?
Okay, I’ll ask them about it.
> The above patches should work for building Lean4, but packaging any Lean
> library with dependencies (like mathlib) won't work until the lean
> developers resolve this issue:
> https://github.com/leanprover/lean4/issues/5122
>
> Unfortunately the devs marked it as low priority and seem to be pushing
> back against reproducible packaging, which is disappointing. I am
> unlikely to continue work on this patch series, as I have switched over
> to Coq.
Indeed, I saw that. Is there any way around it? How is Nix packaging mathlib et.al?
Regards,
Divya Ranjan
^ permalink raw reply [flat|nested] 4+ messages in thread
end of thread, other threads:[~2024-12-07 22:15 UTC | newest]
Thread overview: 4+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2024-08-22 4:44 [bug#72755] [WIP][PATCH] guix: Add lean-build-system Antero Mejr
2024-12-07 7:23 ` Divya Ranjan via Guix-patches via
2024-12-07 18:03 ` Antero Mejr
2024-12-07 22:13 ` Divya Ranjan via Guix-patches via
Code repositories for project(s) associated with this public inbox
https://git.savannah.gnu.org/cgit/guix.git
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).