Package: guix-patches;
Reported by: Antero Mejr <mail <at> antr.me>
Date: Thu, 22 Aug 2024 04:46:02 UTC
Severity: normal
Tags: patch
Message #8 received at 72755 <at> debbugs.gnu.org (full text, mbox):
From: Divya Ranjan <divya <at> subvertising.org> To: Antero Mejr <mail <at> antr.me> Cc: 72755 <at> debbugs.gnu.org Subject: Re: [bug#72755] [WIP][PATCH] guix: Add lean-build-system. Date: Sat, 07 Dec 2024 07:23:18 +0000
Antero Mejr <mail <at> 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 <at> tobias.gr>
> ;;; Copyright © 2022 Pradana Aumars <paumars <at> courrier.dev>
> ;;; Copyright © 2023 Zhu Zihao <all_but_last <at> 163.com>
> +;;; Copyright © 2024 Antero Mejr <mail <at> 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 <at> 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 <at> 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
GNU bug tracking system
Copyright (C) 1999 Darren O. Benham,
1997,2003 nCipher Corporation Ltd,
1994-97 Ian Jackson.