* [bug#72755] [WIP][PATCH] guix: Add lean-build-system.
@ 2024-08-22 4:44 Antero Mejr
0 siblings, 0 replies; only message 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] only message in thread
only message in thread, other threads:[~2024-08-22 4:45 UTC | newest]
Thread overview: (only message) (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
Code repositories for project(s) associated with this external index
https://git.savannah.gnu.org/cgit/guix.git
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.