From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp0.migadu.com ([2001:41d0:303:e224::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms13.migadu.com with LMTPS id kIT3EXLCxmZlqgAAqHPOHw:P1 (envelope-from ) for ; Thu, 22 Aug 2024 04:45:38 +0000 Received: from aspmx1.migadu.com ([2001:41d0:303:e224::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp0.migadu.com with LMTPS id kIT3EXLCxmZlqgAAqHPOHw (envelope-from ) for ; Thu, 22 Aug 2024 06:45:38 +0200 X-Envelope-To: larch@yhetil.org Authentication-Results: aspmx1.migadu.com; dkim=pass header.d=debbugs.gnu.org header.s=debbugs-gnu-org header.b=vCTfB9wb; dkim=fail ("headers rsa verify failed") header.d=antr.me header.s=MBO0001 header.b=urx7ToLg; dmarc=fail reason="SPF not aligned (relaxed), DKIM not aligned (relaxed)" header.from=antr.me (policy=none); spf=pass (aspmx1.migadu.com: domain of "guix-patches-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="guix-patches-bounces+larch=yhetil.org@gnu.org" ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1724301937; h=from:from:sender:sender: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:resent-cc: resent-from:resent-sender:resent-message-id:list-id:list-help: list-unsubscribe:list-subscribe:list-post:dkim-signature; bh=4sOQkNiBWqHveeO52h2+jkHpacB/SWXCRLwLEOk1z3Q=; b=TS06URnFUpC+vFkZ4FBPEzGt85kDP1lXWh9YHunkxEwpid/754ZcxKrQGgCPgENdXUSRdK Cg6Dkm7FWJ61OhUh0DSwxgQJqUsQfZuJpmTj1mBhsp14MqVklu7zIOYl/Kk3ierDwNvZ2Q 40rSQpYDGM6UpGLWMJ60/udJgVRa1U2f4Xod995tCKXFn8XhhQIL00RC+DetSkcKNVLWxE bp2yUED5/ON+F9SW9B+hCP5D2IpXP4mfTKEBG+u1PP3I50x+K3CMSC3AP1RqXIZ6ffSAHO B8JB4H3adHP/AN+l2C6TsHsTPXNnQRi0COhm7SVaFCOQbCZroy7wlZb+PqdopQ== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1724301937; a=rsa-sha256; cv=none; b=Q453vIGNK4ELsH/8qUzwhR1sKcvT+lBHkABjzYrjfPZtmi5rLN5i6WzMyEVCSVhzvb5304 yhgy+rpzwFE0AJT3LuMpW0Lhrck37Gr2Ut8Er9KAl3BxqeY/Ryl0PtkJeFvOo0YmkYuJSD 5eENOlwmViyqova8XN4rK+L4BdstynkZ1hqL90u97SLofhJP1JCZolkeBc0jVsOWR8fvUH v0kFLI02ISR/9NoX3qJAKlylRfxu17r/6FFsFPaqzXu90xieGq8ClhNhNeCuDbZSvN9xhS K3HW04Zk5xFacVdRHn81zibexc2UKGjK/4QNa4UhEVDPg/h67dXBR1p7mq86EA== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=pass header.d=debbugs.gnu.org header.s=debbugs-gnu-org header.b=vCTfB9wb; dkim=fail ("headers rsa verify failed") header.d=antr.me header.s=MBO0001 header.b=urx7ToLg; dmarc=fail reason="SPF not aligned (relaxed), DKIM not aligned (relaxed)" header.from=antr.me (policy=none); spf=pass (aspmx1.migadu.com: domain of "guix-patches-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="guix-patches-bounces+larch=yhetil.org@gnu.org" Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by aspmx1.migadu.com (Postfix) with ESMTPS id 6508F1E9CA for ; Thu, 22 Aug 2024 06:45:37 +0200 (CEST) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1sgzhN-0008RT-3w; Thu, 22 Aug 2024 00:45:25 -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 ) id 1sgzhG-0008RB-Rk for guix-patches@gnu.org; Thu, 22 Aug 2024 00:45:19 -0400 Received: from debbugs.gnu.org ([2001:470:142:5::43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1sgzhF-0005DP-HJ for guix-patches@gnu.org; Thu, 22 Aug 2024 00:45:18 -0400 DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=debbugs.gnu.org; s=debbugs-gnu-org; h=MIME-Version:Date:From:To:Subject; bh=4sOQkNiBWqHveeO52h2+jkHpacB/SWXCRLwLEOk1z3Q=; b=vCTfB9wbqxt6t4lCymOWuA12QSE9vkFJdQXqyTEtPsquaXBi+vbKz8UPXVuR+aeYvz6iys9bTjG2dpQxX0OpmqlVEgTbZsgtUsCMnWlrZG8fETGUCA5JFKEv5tUu8U+WCYFQvc5/mfLx2HTu0+OQ+Yh1m3eSouSyxUlvSY7NiS7UWzXgN/pDeDU+iO1+EXG7QfIwEjlTB57Gfb20WBwcidRrR8AAE+L6PJbdhQRF/UfTA5vyEN2IFAiMqqYVqOHZ4qfGu5dNuuZAs+9EduVibo5I/AfXtW4rTFw/AmzKAKP2mpb1YBs5qVonDvFfVQgbBg7pmXhsvMHKGFUMg1KNrA==; Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1sgzhy-0004DY-Ps for guix-patches@gnu.org; Thu, 22 Aug 2024 00:46:02 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#72755] [WIP][PATCH] guix: Add lean-build-system. Resent-From: Antero Mejr Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Thu, 22 Aug 2024 04:46:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 72755 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 72755@debbugs.gnu.org X-Debbugs-Original-To: guix-patches@gnu.org Received: via spool by submit@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 ) id 1sgzhQ-0004CY-1t for submit@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 ) id 1sgzhL-0004CM-UP for submit@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 ) id 1sgzgc-0008N8-At for guix-patches@gnu.org; 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 ) id 1sgzgY-0004zd-16 for guix-patches@gnu.org; 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 ; 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 Date: Thu, 22 Aug 2024 04:44:13 +0000 Message-ID: <8734mxnp42.fsf@antr.me> 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@antr.me; 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-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+larch=yhetil.org@gnu.org Sender: guix-patches-bounces+larch=yhetil.org@gnu.org X-Migadu-Flow: FLOW_IN X-Migadu-Country: US X-Migadu-Queue-Id: 6508F1E9CA X-Migadu-Scanner: mx12.migadu.com X-Migadu-Spam-Score: -10.71 X-Spam-Score: -10.71 X-TUID: kkLuG721rfof 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 ;;; Copyright =C2=A9 2022 Pradana Aumars ;;; Copyright =C2=A9 2023 Zhu Zihao +;;; Copyright =C2=A9 2024 Antero Mejr ;;; ;;; This file is part of GNU Guix. ;;; @@ -21,60 +22,110 @@ ;;; along with GNU Guix. If not, see . =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 +;;; +;;; 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 . + +(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 +;;; +;;; 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 . + +(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