[bug#72755] [WIP][PATCH] guix: Add lean-build-system.

[Antero Mejr <mail@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

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