X-Loop: help-debbugs@HIDDEN
Subject: [bug#72755] [WIP][PATCH] guix: Add lean-build-system.
Resent-From: Antero Mejr <mail@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Thu, 22 Aug 2024 04:46:02 +0000
Resent-Message-ID: <handler.72755.B.172430192916159 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
X-GNU-PR-Message: report 72755
X-GNU-PR-Package: guix-patches
X-GNU-PR-Keywords: patch
To: 72755 <at> debbugs.gnu.org
X-Debbugs-Original-To: guix-patches@HIDDEN
Received: via spool by submit <at> debbugs.gnu.org id=B.172430192916159
(code B ref -1); Thu, 22 Aug 2024 04:46:02 +0000
Received: (at submit) by debbugs.gnu.org; 22 Aug 2024 04:45:29 +0000
Received: from localhost ([127.0.0.1]:36560 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1sgzhQ-0004CY-1t
for submit <at> debbugs.gnu.org; Thu, 22 Aug 2024 00:45:29 -0400
Received: from lists.gnu.org ([209.51.188.17]:42358)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <mail@HIDDEN>) id 1sgzhL-0004CM-UP
for submit <at> debbugs.gnu.org; Thu, 22 Aug 2024 00:45:26 -0400
Received: from eggs.gnu.org ([2001:470:142:3::10])
by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from <mail@HIDDEN>) id 1sgzgc-0008N8-At
for guix-patches@HIDDEN; Thu, 22 Aug 2024 00:44:38 -0400
Received: from mout-p-103.mailbox.org ([80.241.56.161])
by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_CHACHA20_POLY1305:256)
(Exim 4.90_1) (envelope-from <mail@HIDDEN>) id 1sgzgY-0004zd-16
for guix-patches@HIDDEN; Thu, 22 Aug 2024 00:44:38 -0400
Received: from smtp102.mailbox.org (smtp102.mailbox.org [10.196.197.102])
(using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)
key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256)
(No client certificate requested)
by mout-p-103.mailbox.org (Postfix) with ESMTPS id 4Wq9bB58Gpz9sV8
for <guix-patches@HIDDEN>; Thu, 22 Aug 2024 06:44:22 +0200 (CEST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=antr.me; s=MBO0001;
t=1724301862;
h=from:from:reply-to:subject:subject:date:date:message-id:message-id:
to:to:cc:mime-version:mime-version:content-type:content-type:
content-transfer-encoding:content-transfer-encoding;
bh=4sOQkNiBWqHveeO52h2+jkHpacB/SWXCRLwLEOk1z3Q=;
b=urx7ToLgmPmQy9D+I+EXtdEAxwg+yQYppZI2CKA20fJnEa2rbDOzLbU4rhuSn0mOu3LY26
kJnnMKaEjBf5ImC0vhHzbeY0i+EVd0dboJIHVMRtQpswuf/2PgTmuB9JlYtAM4ZxE2QY67
aLAQ+pT1YMRfG312QBpfDRT9+IjOWsF/11VXMr9Rnr1WHr55abzZQqMgi4y7luoWJ7rAcX
gfh771424JfQhSIGeb8fshTN4DIl2Y3XBsLhJYdj2KEOcGpsQ5TYIrNq97bLUfFsS+UqL9
3IzwU5rqOrbBcRNRILxcpQZLhwx2R9a2PO0nKYDdIQ5GJCdw0KIVWYLC3euNCA==
From: Antero Mejr <mail@HIDDEN>
Date: Thu, 22 Aug 2024 04:44:13 +0000
Message-ID: <8734mxnp42.fsf@HIDDEN>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable
Received-SPF: pass client-ip=80.241.56.161; envelope-from=mail@HIDDEN;
helo=mout-p-103.mailbox.org
X-Spam_score_int: -27
X-Spam_score: -2.8
X-Spam_bar: --
X-Spam_report: (-2.8 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1,
DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1,
RCVD_IN_DNSWL_LOW=-0.7, RCVD_IN_VALIDITY_RPBL_BLOCKED=0.001,
RCVD_IN_VALIDITY_SAFE_BLOCKED=0.001, SPF_HELO_NONE=0.001, SPF_PASS=-0.001,
T_SCC_BODY_TEXT_LINE=-0.01 autolearn=ham autolearn_force=no
X-Spam_action: no action
X-Spam-Score: -1.3 (-)
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -2.3 (--)
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
=20
+@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 impleme=
nts
a build procedure for @uref{https://maven.apache.org, Maven} packages. Ma=
ven
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 =C2=A9 2020 Tobias Geerinckx-Rice <me@HIDDEN>
;;; Copyright =C2=A9 2022 Pradana Aumars <paumars@HIDDEN>
;;; Copyright =C2=A9 2023 Zhu Zihao <all_but_last@HIDDEN>
+;;; Copyright =C2=A9 2024 Antero Mejr <mail@HIDDEN>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -21,60 +22,110 @@
;;; along with GNU Guix. If not, see <http://www.gnu.org/licenses/>.
=20
(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))
=20
(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 trust=
ed
core based on dependent typed theory, aiming to bridge the gap between
interactive and automated theorem proving.")
(license license:asl2.0)))
=20
+(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 L=
ean
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 versi=
on
+ (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 f=
or
+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.ht=
ml")
+ (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 =C2=A9 2024 Antero Mejr <mail@HIDDEN>
+;;;
+;;; 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->s=
exp
+ 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->se=
xp
+ 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->s=
exp
+ 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-syste=
m.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 =C2=A9 2024 Antero Mejr <mail@HIDDEN>
+;;;
+;;; 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
--=20
2.45.1
Content-Disposition: inline Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-Mailer: MIME-tools 5.505 (Entity 5.505) Content-Type: text/plain; charset=utf-8 X-Loop: help-debbugs@HIDDEN From: help-debbugs@HIDDEN (GNU bug Tracking System) To: Antero Mejr <mail@HIDDEN> Subject: bug#72755: Acknowledgement ([WIP][PATCH] guix: Add lean-build-system.) Message-ID: <handler.72755.B.172430192916159.ack <at> debbugs.gnu.org> References: <8734mxnp42.fsf@HIDDEN> X-Gnu-PR-Message: ack 72755 X-Gnu-PR-Package: guix-patches X-Gnu-PR-Keywords: patch Reply-To: 72755 <at> debbugs.gnu.org Date: Thu, 22 Aug 2024 04:46:02 +0000 Thank you for filing a new bug report with debbugs.gnu.org. This is an automatically generated reply to let you know your message has been received. Your message is being forwarded to the package maintainers and other interested parties for their attention; they will reply in due course. Your message has been sent to the package maintainer(s): guix-patches@HIDDEN If you wish to submit further information on this problem, please send it to 72755 <at> debbugs.gnu.org. Please do not send mail to help-debbugs@HIDDEN unless you wish to report a problem with the Bug-tracking system. --=20 72755: https://debbugs.gnu.org/cgi/bugreport.cgi?bug=3D72755 GNU Bug Tracking System Contact help-debbugs@HIDDEN with problems
X-Loop: help-debbugs@HIDDEN
Subject: [bug#72755] [WIP][PATCH] guix: Add lean-build-system.
Resent-From: Divya Ranjan <divya@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Sat, 07 Dec 2024 07:24:02 +0000
Resent-Message-ID: <handler.72755.B72755.173355621014154 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
X-GNU-PR-Message: followup 72755
X-GNU-PR-Package: guix-patches
X-GNU-PR-Keywords: patch
To: Antero Mejr <mail@HIDDEN>
Cc: 72755 <at> debbugs.gnu.org
Received: via spool by 72755-submit <at> debbugs.gnu.org id=B72755.173355621014154
(code B ref 72755); Sat, 07 Dec 2024 07:24:02 +0000
Received: (at 72755) by debbugs.gnu.org; 7 Dec 2024 07:23:30 +0000
Received: from localhost ([127.0.0.1]:45205 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1tJpA0-0003g9-A4
for submit <at> debbugs.gnu.org; Sat, 07 Dec 2024 02:23:30 -0500
Received: from latitanza.investici.org ([82.94.249.234]:39365)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <divya@HIDDEN>) id 1tJp9v-0003fw-6L
for 72755 <at> debbugs.gnu.org; Sat, 07 Dec 2024 02:23:26 -0500
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=subvertising.org;
s=stigmate; t=1733556201;
bh=HhLd0Iz9Qbsx6+DzPYSJZLL6vBu5Cl0+8H2SL1FzZLQ=;
h=From:To:Cc:Subject:In-Reply-To:References:Date:From;
b=geo8PT+OpiLkXQnCliQ+O+xp0kwLzS0QSNmyChU0DiNM2TG7+/GNFYJm44BWU9T/9
3QDIG+rsMx7hdfNlL3ZbFHNDt7IkPicCIAgd5u+ltRMtRNWjo90pyXc2pH+dDhCFqz
VKRDzeNuG7hbN8zWFEbGugiKdG0OcDUwQJABSNKo=
Received: from mx3.investici.org (unknown [127.0.0.1])
by latitanza.investici.org (Postfix) with ESMTP id 4Y503F4pQ2zGp48;
Sat, 7 Dec 2024 07:23:21 +0000 (UTC)
Received: from [82.94.249.234] (mx3.investici.org [82.94.249.234])
(Authenticated sender: divya@HIDDEN) by localhost (Postfix) with
ESMTPSA id 4Y503D6BkwzGp3M; Sat, 7 Dec 2024 07:23:20 +0000 (UTC)
From: Divya Ranjan <divya@HIDDEN>
In-Reply-To: <8734mxnp42.fsf@HIDDEN> (Antero Mejr's message of "Thu, 22 Aug
2024 04:44:13 +0000")
References: <8734mxnp42.fsf@HIDDEN>
Date: Sat, 07 Dec 2024 07:23:18 +0000
Message-ID: <87o71ovtw9.fsf@HIDDEN>
User-Agent: Gnus/5.13 (Gnus v5.13)
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable
X-Spam-Score: 0.0 (/)
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.0 (-)
Antero Mejr <mail@HIDDEN> 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
>=20=20
> +@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 imple=
ments
> 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 =C2=A9 2020 Tobias Geerinckx-Rice <me@HIDDEN>
> ;;; Copyright =C2=A9 2022 Pradana Aumars <paumars@HIDDEN>
> ;;; Copyright =C2=A9 2023 Zhu Zihao <all_but_last@HIDDEN>
> +;;; Copyright =C2=A9 2024 Antero Mejr <mail@HIDDEN>
> ;;;
> ;;; This file is part of GNU Guix.
> ;;;
> @@ -21,60 +22,110 @@
> ;;; along with GNU Guix. If not, see <http://www.gnu.org/licenses/>.
>=20=20
> (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))
>=20=20
> (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 tru=
sted
> core based on dependent typed theory, aiming to bridge the gap between
> interactive and automated theorem proving.")
> (license license:asl2.0)))
>=20=20
> +(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 wit=
h 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.htm=
l")
> + (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 ver=
sion
> + (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 L=
ean
> +4. It supports:
> +@itemize
> +@item{symbolic visualizations of mathematical objects and data structure=
s}
> +@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 versi=
on
> + (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 =C2=A9 2024 Antero Mejr <mail@HIDDEN>
> +;;;
> +;;; 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-gui=
le))
> + 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-specificatio=
n->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-gui=
le))
> + 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-sys=
tem.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 =C2=A9 2024 Antero Mejr <mail@HIDDEN>
> +;;;
> +;;; 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-ke=
ys)
> + "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-pa=
th)
> + (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=E2=80=99ve also been involved in packaging Lean4, have you had any more p=
rogress 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 f=
or ~7 hours. I believe it gets stuck at compiling gash. Any clue?
Regards,
Divya Ranjan
X-Loop: help-debbugs@HIDDEN
Subject: [bug#72755] [WIP][PATCH] guix: Add lean-build-system.
Resent-From: Antero Mejr <mail@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Sat, 07 Dec 2024 18:04:01 +0000
Resent-Message-ID: <handler.72755.B72755.17335946009957 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
X-GNU-PR-Message: followup 72755
X-GNU-PR-Package: guix-patches
X-GNU-PR-Keywords: patch
To: Divya Ranjan <divya@HIDDEN>
Cc: 72755 <at> debbugs.gnu.org
Received: via spool by 72755-submit <at> debbugs.gnu.org id=B72755.17335946009957
(code B ref 72755); Sat, 07 Dec 2024 18:04:01 +0000
Received: (at 72755) by debbugs.gnu.org; 7 Dec 2024 18:03:20 +0000
Received: from localhost ([127.0.0.1]:48443 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1tJz9D-0002aX-VJ
for submit <at> debbugs.gnu.org; Sat, 07 Dec 2024 13:03:20 -0500
Received: from sender4-op-o15.zoho.com ([136.143.188.15]:17504)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <mail@HIDDEN>) id 1tJz9B-0002aO-IK
for 72755 <at> debbugs.gnu.org; Sat, 07 Dec 2024 13:03:18 -0500
ARC-Seal: i=1; a=rsa-sha256; t=1733594585; cv=none;
d=zohomail.com; s=zohoarc;
b=gfoBzgcLIliXVweCo9Xvkbxkmd2A3haqfayBzIEZW03RgztbAjhjBONTLV9bCi/OaKdTLg+1xRietbfB3HMojHy3kSO8dcWMA5aXtIT6HWdW4eFwdfO2vPirdVU03ZFjlVsvYmuJhMEYbqycm+KRImKzu7ziLeHb+cNLYPlHHA0=
ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=zohomail.com;
s=zohoarc; t=1733594585;
h=Content-Type:Content-Transfer-Encoding:Cc:Cc:Date:Date:From:From:In-Reply-To:MIME-Version:Message-ID:References:Subject:Subject:To:To:Message-Id:Reply-To;
bh=nPjcnG/s0Es8yHiCcmq34mS+ojsssLfMz4VCGHEv1yM=;
b=jBWsGEPPKCdgZideOhlBsBhU6h+O18AWg+rCtG8RLt493QEWAbkCAJyG59fzy57Ctqmb2ggxeW6c3Til9J7wt/CDGaB6WpJ7aQ3eMIeNhGQFtEs6JLoFxoXfTSy/8FlLZNt1CVrRAUR4NbMWqd/mVAbKTFbdzW6vn8/yaGzSjrw=
ARC-Authentication-Results: i=1; mx.zohomail.com; dkim=pass header.i=antr.me;
spf=pass smtp.mailfrom=mail@HIDDEN;
dmarc=pass header.from=<mail@HIDDEN>
DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; t=1733594585;
s=zmail; d=antr.me; i=mail@HIDDEN;
h=From:From:To:To:Cc:Cc:Subject:Subject:In-Reply-To:References:Date:Date:Message-ID:MIME-Version:Content-Type:Content-Transfer-Encoding:Message-Id:Reply-To;
bh=nPjcnG/s0Es8yHiCcmq34mS+ojsssLfMz4VCGHEv1yM=;
b=Eqtl/m5A7CkvsuDwSzOXqXbnIxls5hw6wLy7iQcveL3dfuU2VXhw1y2ycdhELe2l
LK/LftWzZ/2MxfJnu0rjggFZSM9eLLUo1aZh/MkYs4+JQ3yT4mvzWp7b5bGHJOkvCs9
H4XjNdwl1bUmWTLM6Y/gihK6qHOp4M3/XsGzwPSY=
Received: by mx.zohomail.com with SMTPS id 1733594583473287.0442225761236;
Sat, 7 Dec 2024 10:03:03 -0800 (PST)
From: Antero Mejr <mail@HIDDEN>
In-Reply-To: <87o71ovtw9.fsf@HIDDEN> (Divya Ranjan's message of
"Sat, 07 Dec 2024 07:23:18 +0000")
References: <8734mxnp42.fsf@HIDDEN> <87o71ovtw9.fsf@HIDDEN>
Date: Sat, 07 Dec 2024 13:03:00 -0500
Message-ID: <87v7vv74mj.fsf@HIDDEN>
User-Agent: Gnus/5.13 (Gnus v5.13)
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable
X-ZohoMailClient: External
X-Spam-Score: 0.7 (/)
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -0.3 (/)
Divya Ranjan <divya@HIDDEN> writes:
> I=E2=80=99ve 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 bui=
ld
> lean` gets stuck at some point after trying to compile things for ~7 hour=
s. I
> believe it gets stuck at compiling gash. Any clue?
You shouldn't have to rebuild the entire dependency chain (and things
like gash) to use the above patch - maybe someone on IRC or a maintainer
can help with fixing that?
The above patches should work for building Lean4, but packaging any Lean
library with dependencies (like mathlib) won't work until the lean
developers resolve this issue:
https://github.com/leanprover/lean4/issues/5122
Unfortunately the devs marked it as low priority and seem to be pushing
back against reproducible packaging, which is disappointing. I am
unlikely to continue work on this patch series, as I have switched over
to Coq.
X-Loop: help-debbugs@HIDDEN
Subject: [bug#72755] [WIP][PATCH] guix: Add lean-build-system.
Resent-From: Divya Ranjan <divya@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Sat, 07 Dec 2024 22:15:02 +0000
Resent-Message-ID: <handler.72755.B72755.173360964925466 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
X-GNU-PR-Message: followup 72755
X-GNU-PR-Package: guix-patches
X-GNU-PR-Keywords: patch
To: Antero Mejr <mail@HIDDEN>
Cc: 72755 <at> debbugs.gnu.org
Received: via spool by 72755-submit <at> debbugs.gnu.org id=B72755.173360964925466
(code B ref 72755); Sat, 07 Dec 2024 22:15:02 +0000
Received: (at 72755) by debbugs.gnu.org; 7 Dec 2024 22:14:09 +0000
Received: from localhost ([127.0.0.1]:48846 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1tK33x-0006cf-4o
for submit <at> debbugs.gnu.org; Sat, 07 Dec 2024 17:14:09 -0500
Received: from devianza.investici.org ([198.167.222.108]:28701)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <divya@HIDDEN>) id 1tK33u-0006cS-Fw
for 72755 <at> debbugs.gnu.org; Sat, 07 Dec 2024 17:14:08 -0500
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=subvertising.org;
s=stigmate; t=1733609637;
bh=O3k4kX00+yxImxj+1dBOj5YvPai0ZZkebE/IYgj36pQ=;
h=From:To:Cc:Subject:In-Reply-To:References:Date:From;
b=Zh2gsAxvCZU46M07/FuWFu0ynreGvRRH6zi9dxTHucxKlP4IHQpem4FVUjTR/D6Wd
x4+ITrPrymmtqHCu41qZyw+eyCgSXPh85tr6WBZ2wI39v0qWk+iL28ckjB3UpcHWc/
ncIXqRK4ct/pXfWWINNj1o3tJ/4zMcMQP5vCqnAs=
Received: from mx2.investici.org (unknown [127.0.0.1])
by devianza.investici.org (Postfix) with ESMTP id 4Y5Mps4q0Cz70XX;
Sat, 7 Dec 2024 22:13:57 +0000 (UTC)
Received: from [198.167.222.108] (mx2.investici.org [198.167.222.108])
(Authenticated sender: divya@HIDDEN) by localhost (Postfix) with
ESMTPSA id 4Y5Mpr5W2Wz70XT; Sat, 7 Dec 2024 22:13:56 +0000 (UTC)
From: Divya Ranjan <divya@HIDDEN>
In-Reply-To: <87v7vv74mj.fsf@HIDDEN> (Antero Mejr's message of "Sat, 07 Dec
2024 13:03:00 -0500")
References: <8734mxnp42.fsf@HIDDEN> <87o71ovtw9.fsf@HIDDEN>
<87v7vv74mj.fsf@HIDDEN>
Date: Sat, 07 Dec 2024 22:13:45 +0000
Message-ID: <87msh73zvq.fsf@HIDDEN>
User-Agent: Gnus/5.13 (Gnus v5.13)
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable
X-Spam-Score: 0.0 (/)
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.0 (-)
Antero Mejr <mail@HIDDEN> writes:
> Divya Ranjan <divya@HIDDEN> writes:
>> I=E2=80=99ve also been involved in packaging Lean4, have you had any mor=
e progress on
>> this? I tried to build guix from your patch, but `./pre-inst-env guix bu=
ild
>> lean` gets stuck at some point after trying to compile things for ~7 hou=
rs. I
>> believe it gets stuck at compiling gash. Any clue?
>
> You shouldn't have to rebuild the entire dependency chain (and things
> like gash) to use the above patch - maybe someone on IRC or a maintainer
> can help with fixing that?
Okay, I=E2=80=99ll ask them about it.
> The above patches should work for building Lean4, but packaging any Lean
> library with dependencies (like mathlib) won't work until the lean
> developers resolve this issue:
> https://github.com/leanprover/lean4/issues/5122
>
> Unfortunately the devs marked it as low priority and seem to be pushing
> back against reproducible packaging, which is disappointing. I am
> unlikely to continue work on this patch series, as I have switched over
> to Coq.
Indeed, I saw that. Is there any way around it? How is Nix packaging mathli=
b et.al?
Regards,
Divya Ranjan
GNU bug tracking system
Copyright (C) 1999 Darren O. Benham,
1997 nCipher Corporation Ltd,
1994-97 Ian Jackson.