From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp2.migadu.com ([2001:41d0:403:58f0::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms13.migadu.com with LMTPS id aDYjOSP4U2e9WQEAe85BDQ:P1 (envelope-from ) for ; Sat, 07 Dec 2024 07:24:20 +0000 Received: from aspmx1.migadu.com ([2001:41d0:403:58f0::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp2.migadu.com with LMTPS id aDYjOSP4U2e9WQEAe85BDQ (envelope-from ) for ; Sat, 07 Dec 2024 08:24:20 +0100 X-Envelope-To: larch@yhetil.org Authentication-Results: aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=debbugs.gnu.org header.s=debbugs-gnu-org header.b=XSFF69Nq; dkim=fail ("headers rsa verify failed") header.d=subvertising.org header.s=stigmate header.b=geo8PT+O; 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"; dmarc=pass (policy=none) header.from=gnu.org ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1733556259; h=from:from:sender:sender:reply-to:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:cc:mime-version:mime-version: content-type:content-type: content-transfer-encoding:content-transfer-encoding:resent-cc: resent-from:resent-sender:resent-message-id:in-reply-to:in-reply-to: references:references:list-id:list-help:list-unsubscribe: list-subscribe:list-post:dkim-signature; bh=HhLd0Iz9Qbsx6+DzPYSJZLL6vBu5Cl0+8H2SL1FzZLQ=; b=JH1NyeqjR90fmwc0XLRHMA3Ibn2cup9Vc1CmTa2jq45j2AebLGfqmfNCpGW+YWnnDBiPRX 81dlYCGDSg2ku/NUV1XfjomYKLnJUEZKCoVgEkbpcKZxm48ZDm0I87fxEsdbVFUVeJvVDo 8KLGqBW9Y/cfWReem0Kay3myy+vh8gT3ZTQzCfUER7Nt7HQ5sexAlppU2d0FZWT6I7IgCZ QDyd+xi1rtjIb7Zr9GCOzu84hEwEa+suxN4YYkxdcgklOMx8Xj5tnJ0VWJp5VsFZIxv7Mt vLFr0YkUKM6eJd07Wu+YLsduEK1O9DQRsm3sRQMLdKzI0vb7UeAANmGNFI29WA== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=debbugs.gnu.org header.s=debbugs-gnu-org header.b=XSFF69Nq; dkim=fail ("headers rsa verify failed") header.d=subvertising.org header.s=stigmate header.b=geo8PT+O; 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"; dmarc=pass (policy=none) header.from=gnu.org ARC-Seal: i=1; s=key1; d=yhetil.org; t=1733556259; a=rsa-sha256; cv=none; b=R4r5AgyxTX0/IaAbF62h1yli2MMwHU8XNwKzCLstbEDEqzP1w4IyOmgMsujj8U3oi7bvnB H5FLgGMTGeTJiyy92WLpmUX6yw6+G0MoHEwP+9VgF5/8sz7RgtPzofYwymClsyCPqhFA7z eLmqT8AYhtx95bIay74e2a902R4H4FQePRkxbrpuHJdpAuobymmqHVkMOO4jAdxxvvjnL8 yVp20iC+ZeAs934crEdenE7dBeLlijLdjZ6a4Yqv2JI1tUtRdbQFpZ0sUx4svH4girzDgr wMCQvaln/WavU6T9dtj7n3X86p+j8uzEfbpI7NriY5wXNQ950i5LlDDlzYrccw== 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 9DC44897EA for ; Sat, 07 Dec 2024 08:24:19 +0100 (CET) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1tJpAb-0000MT-VD; Sat, 07 Dec 2024 02:24:06 -0500 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 1tJpAZ-0000Lh-CP for guix-patches@gnu.org; Sat, 07 Dec 2024 02:24:04 -0500 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 1tJpAY-0006BA-Rb for guix-patches@gnu.org; Sat, 07 Dec 2024 02:24:03 -0500 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:References:In-Reply-To:From:To:Subject; bh=HhLd0Iz9Qbsx6+DzPYSJZLL6vBu5Cl0+8H2SL1FzZLQ=; b=XSFF69NqnC4yVqs9G64exTOFHi7h8h5sOyAgaNzFiq0W6HvD/TT6w1NPDxYKteJydKZlsIhObaGLrMJUP0Im7HbM3ITEwxQ3uwNewxriHJjrVoCsWDUAz8gMjtfrwcJc56Kvc4dOU/Z37LYCpbpJPY0WUpKu8cr4eTzMrngdTeMpwAr7rO84Se9DesZLsfnXF8VEJ62gXyddddc87YunXnKlhFBKCCyfwsvz7nVYVhsdXR4CSnNR4iDXY6zh76xdlrcYZ/Nl5aqsLY6f4x6ur8yP0YTN8+M0uEJ+N4cnW+s5yV2vPSfbCzgWjDvLX+K/eNbCscBrGmUkqpFlFyCKtQ==; Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1tJpAY-0003hC-9F for guix-patches@gnu.org; Sat, 07 Dec 2024 02:24:02 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#72755] [WIP][PATCH] guix: Add lean-build-system. Resent-From: Divya Ranjan Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sat, 07 Dec 2024 07:24:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 72755 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Antero Mejr Cc: 72755@debbugs.gnu.org Received: via spool by 72755-submit@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 ) id 1tJpA0-0003g9-A4 for submit@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 ) id 1tJp9v-0003fw-6L for 72755@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@subvertising.org) by localhost (Postfix) with ESMTPSA id 4Y503D6BkwzGp3M; Sat, 7 Dec 2024 07:23:20 +0000 (UTC) In-Reply-To: <8734mxnp42.fsf@antr.me> (Antero Mejr's message of "Thu, 22 Aug 2024 04:44:13 +0000") References: <8734mxnp42.fsf@antr.me> Date: Sat, 07 Dec 2024 07:23:18 +0000 Message-ID: <87o71ovtw9.fsf@subvertising.org> 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-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: , Reply-to: Divya Ranjan X-ACL-Warn: , Divya Ranjan via Guix-patches From: Divya Ranjan via Guix-patches via Errors-To: guix-patches-bounces+larch=yhetil.org@gnu.org Sender: guix-patches-bounces+larch=yhetil.org@gnu.org X-Migadu-Country: US X-Migadu-Flow: FLOW_IN X-Migadu-Scanner: mx11.migadu.com X-Migadu-Spam-Score: -2.66 X-Spam-Score: -2.66 X-Migadu-Queue-Id: 9DC44897EA X-TUID: xpw55W580mX5 Antero Mejr 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 > ;;; 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=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 > +;;; > +;;; 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-= >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 > +;;; > +;;; 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-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