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

From: Divya Ranjan <[email-masked]>
Date: Sat, 07 Dec 2024 07:23:18 +0000

Antero Mejr <[email-masked]> 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 <[email-masked]>
>  ;;; Copyright © 2022 Pradana Aumars <[email-masked]>
>  ;;; Copyright © 2023 Zhu Zihao <[email-masked]>
> +;;; Copyright © 2024 Antero Mejr <[email-masked]>
>  ;;;
>  ;;; 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 <[email-masked]>
> +;;;
> +;;; 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 <[email-masked]>
> +;;;
> +;;; 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