From unknown Tue Jun 17 22:27:30 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#67315] [PATCH 1/2] gnu: lean: Use G-expressions. Resent-From: Zhu Zihao Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Tue, 21 Nov 2023 03:56:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 67315 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 67315@debbugs.gnu.org Cc: Zhu Zihao X-Debbugs-Original-To: guix-patches@gnu.org Received: via spool by submit@debbugs.gnu.org id=B.17005389554365 (code B ref -1); Tue, 21 Nov 2023 03:56:01 +0000 Received: (at submit) by debbugs.gnu.org; 21 Nov 2023 03:55:55 +0000 Received: from localhost ([127.0.0.1]:54919 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1r5Hre-00018L-OM for submit@debbugs.gnu.org; Mon, 20 Nov 2023 22:55:55 -0500 Received: from lists.gnu.org ([2001:470:142::17]:48090) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1r5HrZ-000184-RC for submit@debbugs.gnu.org; Mon, 20 Nov 2023 22:55:53 -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 1r5HrQ-0002zD-VJ for guix-patches@gnu.org; Mon, 20 Nov 2023 22:55:40 -0500 Received: from m15.mail.163.com ([45.254.50.220]) by eggs.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1r5HrJ-0001DK-MD for guix-patches@gnu.org; Mon, 20 Nov 2023 22:55:40 -0500 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=163.com; s=s110527; h=From:Subject:Date:Message-ID:MIME-Version: Content-Type; bh=wd/weZqrC+NoI6UNEncgjQ6bUBnRcg0E5lLbY4WEgUw=; b=DNgZrKgWL8tyorHyjBoQj0Wsl/wc0EkwcVxT3VaB0rBImjaY2ggIaAQLsn6gMG 1/Dx2iJvj1UNhZ+VlWub849aa+0eooOL+b1CjKfk19xA8ELtlygXZ5yPW/lPsfA6 Bsx/Cfa+IlZsUID4Z9jA2HJRoqbmEHDqSnNvSK7ZDCPtQ= Received: from localhost.localdomain (unknown [119.123.64.52]) by zwqz-smtp-mta-g2-0 (Coremail) with SMTP id _____wDn124YKlxlzd1wDg--.42165S2; Tue, 21 Nov 2023 11:55:11 +0800 (CST) From: Zhu Zihao Date: Tue, 21 Nov 2023 11:54:38 +0800 Message-ID: <8b5ac18136b62d453b06c3b2b1db3d9bad5b2bac.1700536251.git.all_but_last@163.com> X-Mailer: git-send-email 2.41.0 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-CM-TRANSID: _____wDn124YKlxlzd1wDg--.42165S2 X-Coremail-Antispam: 1Uf129KBjvJXoWxCr4xAw18KF13Ww45Zr17GFg_yoW5CF4kpa ySkw1Yqa1rGFy3ta1fXa1jvry5WF9a9rWjv393Aa97t3yYvFWvqF4xtrs5Wr13AF1Syw47 WF40qr4fW34DWrJanT9S1TB71UUUUUUqnTZGkaVYY2UrUUUUjbIjqfuFe4nvWSU5nxnvy2 9KBjDUYxBIdaVFxhVjvjDU0xZFpf9x0JUcAwxUUUUU= X-Originating-IP: [119.123.64.52] X-CM-SenderInfo: pdoosuxxwbztlvw6il2tof0z/xtbBLwQvr2Hmp85RawAAs- Received-SPF: pass client-ip=45.254.50.220; envelope-from=all_but_last@163.com; helo=m15.mail.163.com X-Spam_score_int: -20 X-Spam_score: -2.1 X-Spam_bar: -- X-Spam_report: (-2.1 / 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, FREEMAIL_FROM=0.001, RCVD_IN_DNSWL_NONE=-0.0001, RCVD_IN_MSPIKE_H2=-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: 0.9 (/) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.1 (/) * gnu/packages/lean.scm (lean)[arguments]: Use G-expressions. --- gnu/packages/lean.scm | 49 +++++++++++++++++++++++-------------------- 1 file changed, 26 insertions(+), 23 deletions(-) diff --git a/gnu/packages/lean.scm b/gnu/packages/lean.scm index 12c1849cdb..a8ad085d7e 100644 --- a/gnu/packages/lean.scm +++ b/gnu/packages/lean.scm @@ -3,6 +3,7 @@ ;;; Copyright © 2020 Brett Gilio ;;; Copyright © 2020 Tobias Geerinckx-Rice ;;; Copyright © 2022 Pradana Aumars +;;; Copyright © 2023 Zhu Zihao ;;; ;;; This file is part of GNU Guix. ;;; @@ -25,6 +26,7 @@ (define-module (gnu packages lean) #:use-module (guix build-system cmake) #:use-module (guix build-system python) #:use-module ((guix licenses) #:prefix license:) + #:use-module (guix gexp) #:use-module (guix packages) #:use-module (guix git-download) #:use-module (guix download) @@ -52,29 +54,30 @@ (define-public lean (inputs (list bash-minimal gmp)) (arguments - `(#: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-after 'patch-source-shebangs 'patch-tests-shebangs - (lambda _ - (let ((sh (which "sh")) - (bash (which "bash"))) - (substitute* (find-files "tests/lean" "\\.sh$") - (("#![[:blank:]]?/bin/sh") - (string-append "#!" sh)) - (("#![[:blank:]]?/bin/bash") - (string-append "#!" bash)) - (("#![[:blank:]]?usr/bin/env bash") - (string-append "#!" bash)))))) - (add-before 'configure 'chdir-to-src - (lambda _ (chdir "src")))))) + (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-after 'patch-source-shebangs 'patch-tests-shebangs + (lambda _ + (let ((sh (which "sh")) + (bash (which "bash"))) + (substitute* (find-files "tests/lean" "\\.sh$") + (("#![[:blank:]]?/bin/sh") + (string-append "#!" sh)) + (("#![[:blank:]]?/bin/bash") + (string-append "#!" bash)) + (("#![[:blank:]]?usr/bin/env bash") + (string-append "#!" bash)))))) + (add-before 'configure 'chdir-to-src + (lambda _ (chdir "src")))))) (synopsis "Theorem prover and programming language") (description "Lean is a theorem prover and programming language with a small trusted base-commit: d20ece07dbb09382f361c8bbf0bcab9e83d8b73e -- 2.41.0 From unknown Tue Jun 17 22:27:30 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#67315] [PATCH 2/2] gnu: lean: Update to 3.51.1. Resent-From: Zhu Zihao Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Tue, 21 Nov 2023 04:50:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 67315 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 67315@debbugs.gnu.org Cc: Zhu Zihao Received: via spool by 67315-submit@debbugs.gnu.org id=B67315.17005421509922 (code B ref 67315); Tue, 21 Nov 2023 04:50:01 +0000 Received: (at 67315) by debbugs.gnu.org; 21 Nov 2023 04:49:10 +0000 Received: from localhost ([127.0.0.1]:54963 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1r5IhB-0002Zw-6K for submit@debbugs.gnu.org; Mon, 20 Nov 2023 23:49:09 -0500 Received: from m15.mail.163.com ([45.254.50.220]:59636) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1r5Ih3-0002Z3-PT for 67315@debbugs.gnu.org; Mon, 20 Nov 2023 23:49:06 -0500 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=163.com; s=s110527; h=From:Subject:Date:Message-ID:MIME-Version; bh=98sPf FNs1qhTVelTD6udA0ZLsOVuugSMQC09vh5AdJQ=; b=Te2oIZDZAzDwMeOr/1HOz MmH7yB44XlS/dgXbCN149kFFvGS7THDKs2NiU5iDv89mbaZctO8TQd3Yiy83VIgq 56xbAxccCSh/pubzzem3LU0Hsx4iPk2haxxwy8YKw9UgscI80cbe49KJH6iJbV9A DhMEHTCqORLgr861sfzOZ8= Received: from localhost.localdomain (unknown [119.123.64.52]) by zwqz-smtp-mta-g0-1 (Coremail) with SMTP id _____wB3l3ygNlxlg4I2Bg--.38801S2; Tue, 21 Nov 2023 12:48:48 +0800 (CST) From: Zhu Zihao Date: Tue, 21 Nov 2023 12:48:29 +0800 Message-ID: X-Mailer: git-send-email 2.41.0 In-Reply-To: <8b5ac18136b62d453b06c3b2b1db3d9bad5b2bac.1700536251.git.all_but_last@163.com> References: <8b5ac18136b62d453b06c3b2b1db3d9bad5b2bac.1700536251.git.all_but_last@163.com> MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-CM-TRANSID: _____wB3l3ygNlxlg4I2Bg--.38801S2 X-Coremail-Antispam: 1Uf129KBjvJXoW7KF4kCF43Jw17AFy8tFWfuFg_yoW8ur17pa 4S9343uF1rCry3Jw48Wa12yryYgF97GryxA393Aw4kG3y2vay0grWxtFZakry7JF1Iqw1U Wr4fJF48WFy5WFJanT9S1TB71UUUUUUqnTZGkaVYY2UrUUUUjbIjqfuFe4nvWSU5nxnvy2 9KBjDUYxBIdaVFxhVjvjDU0xZFpf9x0JUcmi_UUUUU= X-Originating-IP: [119.123.64.52] X-CM-SenderInfo: pdoosuxxwbztlvw6il2tof0z/xtbBLxUvr2Hmp88ikwAAsk X-Spam-Score: -0.0 (/) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) * gnu/packages/lean.scm (lean): Update to 3.51.1. [home-page]: Use new home page. [arguments]<#:phases>: Remove stale phase 'patch-tests-shebangs'. [inputs]: Remove bash-minimal. Change-Id: Ib90a124b4a6b06fb30223ad4b9254249e56dd086 --- gnu/packages/lean.scm | 24 +++++++----------------- 1 file changed, 7 insertions(+), 17 deletions(-) diff --git a/gnu/packages/lean.scm b/gnu/packages/lean.scm index a8ad085d7e..1533200426 100644 --- a/gnu/packages/lean.scm +++ b/gnu/packages/lean.scm @@ -40,19 +40,20 @@ (define-module (gnu packages lean) (define-public lean (package (name "lean") - (version "3.41.0") - (home-page "https://github.com/leanprover-community/lean") + (version "3.51.1") + (home-page "https://lean-lang.org" ) (source (origin (method git-fetch) - (uri (git-reference (url home-page) - (commit (string-append "v" version)))) + (uri (git-reference + (url "https://github.com/leanprover-community/lean") + (commit (string-append "v" version)))) (file-name (git-file-name name version)) (sha256 (base32 - "0mpxlfjq460x1vi3v6qzgjv74asg0qlhykd51pj347795x5b1hf1")))) + "17g4d3lqnbl1yfy2pjannf73v8qhc5003d2jkmrqiy05zkqs8d9n")))) (build-system cmake-build-system) (inputs - (list bash-minimal gmp)) + (list gmp)) (arguments (list #:build-type "Release" ; default upstream build type @@ -65,17 +66,6 @@ (define-public lean (string-prefix? "armhf" arch))))) #:phases #~(modify-phases %standard-phases - (add-after 'patch-source-shebangs 'patch-tests-shebangs - (lambda _ - (let ((sh (which "sh")) - (bash (which "bash"))) - (substitute* (find-files "tests/lean" "\\.sh$") - (("#![[:blank:]]?/bin/sh") - (string-append "#!" sh)) - (("#![[:blank:]]?/bin/bash") - (string-append "#!" bash)) - (("#![[:blank:]]?usr/bin/env bash") - (string-append "#!" bash)))))) (add-before 'configure 'chdir-to-src (lambda _ (chdir "src")))))) (synopsis "Theorem prover and programming language") -- 2.41.0 From unknown Tue Jun 17 22:27:30 2025 MIME-Version: 1.0 X-Mailer: MIME-tools 5.505 (Entity 5.505) X-Loop: help-debbugs@gnu.org From: help-debbugs@gnu.org (GNU bug Tracking System) To: Zhu Zihao Subject: bug#67315: closed (Re: [bug#67315] [PATCH 1/2] gnu: lean: Use G-expressions.) Message-ID: References: <87sf481hig.fsf@gnu.org> <8b5ac18136b62d453b06c3b2b1db3d9bad5b2bac.1700536251.git.all_but_last@163.com> X-Gnu-PR-Message: they-closed 67315 X-Gnu-PR-Package: guix-patches X-Gnu-PR-Keywords: patch Reply-To: 67315@debbugs.gnu.org Date: Mon, 11 Dec 2023 22:51:02 +0000 Content-Type: multipart/mixed; boundary="----------=_1702335062-31100-1" This is a multi-part message in MIME format... ------------=_1702335062-31100-1 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" Your bug report #67315: [PATCH 1/2] gnu: lean: Use G-expressions. which was filed against the guix-patches package, has been closed. The explanation is attached below, along with your original report. If you require more details, please reply to 67315@debbugs.gnu.org. --=20 67315: https://debbugs.gnu.org/cgi/bugreport.cgi?bug=3D67315 GNU Bug Tracking System Contact help-debbugs@gnu.org with problems ------------=_1702335062-31100-1 Content-Type: message/rfc822 Content-Disposition: inline Content-Transfer-Encoding: 7bit Received: (at 67315-done) by debbugs.gnu.org; 11 Dec 2023 22:50:28 +0000 Received: from localhost ([127.0.0.1]:54906 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rCp6Z-00084s-Ry for submit@debbugs.gnu.org; Mon, 11 Dec 2023 17:50:28 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:56358) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rCp6U-00084a-8X for 67315-done@debbugs.gnu.org; Mon, 11 Dec 2023 17:50:26 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1rCp69-0007wB-EH; Mon, 11 Dec 2023 17:50:01 -0500 DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=gnu.org; s=fencepost-gnu-org; h=MIME-Version:Date:References:In-Reply-To:Subject:To: From; bh=1iQqXeEC8OgJ7KeiFt05qYTdz8Lq1eEg5ovythYO0GA=; b=rWLH/kmjXf4wzTkdxASj +OgDeAz4Sg3MGUN7ouk4fMzXJaU2H1WQ6jEIZ1EHTtFnYXEfKUCBnmq6usba22jnkaDf6pEJnLao5 kXjjk/4NP6BLBji7gLhXiPUnYv7K8EiC37Na7atMMYfNgEtoe5p9ZWWizQbT6hwivCb/jHZMn8fOd gs54f98G3voMptvYnOqgMPi8xTvei/sFtuhWaZ21hLsEiJJPNSN9N/spLc66iRQCQiGzz5mMJ5sIj 5+lyZJvvIt55PFhLtOr/rFZG0sH5cvbm/HTMu8SU+c3f26fuevdQMv7jYxu7ABz/OBJc/YxYqNFGs /bkhgN89srMFCg==; From: =?utf-8?Q?Ludovic_Court=C3=A8s?= To: Zhu Zihao Subject: Re: [bug#67315] [PATCH 1/2] gnu: lean: Use G-expressions. In-Reply-To: <8b5ac18136b62d453b06c3b2b1db3d9bad5b2bac.1700536251.git.all_but_last@163.com> (Zhu Zihao's message of "Tue, 21 Nov 2023 11:54:38 +0800") References: <8b5ac18136b62d453b06c3b2b1db3d9bad5b2bac.1700536251.git.all_but_last@163.com> Date: Mon, 11 Dec 2023 23:49:59 +0100 Message-ID: <87sf481hig.fsf@gnu.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-Spam-Score: -2.3 (--) X-Debbugs-Envelope-To: 67315-done Cc: 67315-done@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -3.3 (---) Hi, Zhu Zihao skribis: > * gnu/packages/lean.scm (lean)[arguments]: Use G-expressions. [...] > * gnu/packages/lean.scm (lean): Update to 3.51.1. > [home-page]: Use new home page. > [arguments]<#:phases>: Remove stale phase 'patch-tests-shebangs'. > [inputs]: Remove bash-minimal. > > Change-Id: Ib90a124b4a6b06fb30223ad4b9254249e56dd086 Applied, thanks! Ludo=E2=80=99. ------------=_1702335062-31100-1 Content-Type: message/rfc822 Content-Disposition: inline Content-Transfer-Encoding: 7bit Received: (at submit) by debbugs.gnu.org; 21 Nov 2023 03:55:55 +0000 Received: from localhost ([127.0.0.1]:54919 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1r5Hre-00018L-OM for submit@debbugs.gnu.org; Mon, 20 Nov 2023 22:55:55 -0500 Received: from lists.gnu.org ([2001:470:142::17]:48090) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1r5HrZ-000184-RC for submit@debbugs.gnu.org; Mon, 20 Nov 2023 22:55:53 -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 1r5HrQ-0002zD-VJ for guix-patches@gnu.org; Mon, 20 Nov 2023 22:55:40 -0500 Received: from m15.mail.163.com ([45.254.50.220]) by eggs.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1r5HrJ-0001DK-MD for guix-patches@gnu.org; Mon, 20 Nov 2023 22:55:40 -0500 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=163.com; s=s110527; h=From:Subject:Date:Message-ID:MIME-Version: Content-Type; bh=wd/weZqrC+NoI6UNEncgjQ6bUBnRcg0E5lLbY4WEgUw=; b=DNgZrKgWL8tyorHyjBoQj0Wsl/wc0EkwcVxT3VaB0rBImjaY2ggIaAQLsn6gMG 1/Dx2iJvj1UNhZ+VlWub849aa+0eooOL+b1CjKfk19xA8ELtlygXZ5yPW/lPsfA6 Bsx/Cfa+IlZsUID4Z9jA2HJRoqbmEHDqSnNvSK7ZDCPtQ= Received: from localhost.localdomain (unknown [119.123.64.52]) by zwqz-smtp-mta-g2-0 (Coremail) with SMTP id _____wDn124YKlxlzd1wDg--.42165S2; Tue, 21 Nov 2023 11:55:11 +0800 (CST) From: Zhu Zihao To: guix-patches@gnu.org Subject: [PATCH 1/2] gnu: lean: Use G-expressions. Date: Tue, 21 Nov 2023 11:54:38 +0800 Message-ID: <8b5ac18136b62d453b06c3b2b1db3d9bad5b2bac.1700536251.git.all_but_last@163.com> X-Mailer: git-send-email 2.41.0 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-CM-TRANSID: _____wDn124YKlxlzd1wDg--.42165S2 X-Coremail-Antispam: 1Uf129KBjvJXoWxCr4xAw18KF13Ww45Zr17GFg_yoW5CF4kpa ySkw1Yqa1rGFy3ta1fXa1jvry5WF9a9rWjv393Aa97t3yYvFWvqF4xtrs5Wr13AF1Syw47 WF40qr4fW34DWrJanT9S1TB71UUUUUUqnTZGkaVYY2UrUUUUjbIjqfuFe4nvWSU5nxnvy2 9KBjDUYxBIdaVFxhVjvjDU0xZFpf9x0JUcAwxUUUUU= X-Originating-IP: [119.123.64.52] X-CM-SenderInfo: pdoosuxxwbztlvw6il2tof0z/xtbBLwQvr2Hmp85RawAAs- Received-SPF: pass client-ip=45.254.50.220; envelope-from=all_but_last@163.com; helo=m15.mail.163.com X-Spam_score_int: -20 X-Spam_score: -2.1 X-Spam_bar: -- X-Spam_report: (-2.1 / 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, FREEMAIL_FROM=0.001, RCVD_IN_DNSWL_NONE=-0.0001, RCVD_IN_MSPIKE_H2=-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: 0.9 (/) X-Debbugs-Envelope-To: submit Cc: Zhu Zihao X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.1 (/) * gnu/packages/lean.scm (lean)[arguments]: Use G-expressions. --- gnu/packages/lean.scm | 49 +++++++++++++++++++++++-------------------- 1 file changed, 26 insertions(+), 23 deletions(-) diff --git a/gnu/packages/lean.scm b/gnu/packages/lean.scm index 12c1849cdb..a8ad085d7e 100644 --- a/gnu/packages/lean.scm +++ b/gnu/packages/lean.scm @@ -3,6 +3,7 @@ ;;; Copyright © 2020 Brett Gilio ;;; Copyright © 2020 Tobias Geerinckx-Rice ;;; Copyright © 2022 Pradana Aumars +;;; Copyright © 2023 Zhu Zihao ;;; ;;; This file is part of GNU Guix. ;;; @@ -25,6 +26,7 @@ (define-module (gnu packages lean) #:use-module (guix build-system cmake) #:use-module (guix build-system python) #:use-module ((guix licenses) #:prefix license:) + #:use-module (guix gexp) #:use-module (guix packages) #:use-module (guix git-download) #:use-module (guix download) @@ -52,29 +54,30 @@ (define-public lean (inputs (list bash-minimal gmp)) (arguments - `(#: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-after 'patch-source-shebangs 'patch-tests-shebangs - (lambda _ - (let ((sh (which "sh")) - (bash (which "bash"))) - (substitute* (find-files "tests/lean" "\\.sh$") - (("#![[:blank:]]?/bin/sh") - (string-append "#!" sh)) - (("#![[:blank:]]?/bin/bash") - (string-append "#!" bash)) - (("#![[:blank:]]?usr/bin/env bash") - (string-append "#!" bash)))))) - (add-before 'configure 'chdir-to-src - (lambda _ (chdir "src")))))) + (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-after 'patch-source-shebangs 'patch-tests-shebangs + (lambda _ + (let ((sh (which "sh")) + (bash (which "bash"))) + (substitute* (find-files "tests/lean" "\\.sh$") + (("#![[:blank:]]?/bin/sh") + (string-append "#!" sh)) + (("#![[:blank:]]?/bin/bash") + (string-append "#!" bash)) + (("#![[:blank:]]?usr/bin/env bash") + (string-append "#!" bash)))))) + (add-before 'configure 'chdir-to-src + (lambda _ (chdir "src")))))) (synopsis "Theorem prover and programming language") (description "Lean is a theorem prover and programming language with a small trusted base-commit: d20ece07dbb09382f361c8bbf0bcab9e83d8b73e -- 2.41.0 ------------=_1702335062-31100-1--