From patchwork Tue Nov 21 03:54:38 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Patchwork-Submitter: Zhu Zihao X-Patchwork-Id: 56675 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id C31DB27BBEA; Tue, 21 Nov 2023 03:56:29 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-2.7 required=5.0 tests=BAYES_00,DKIM_INVALID, DKIM_SIGNED,FREEMAIL_FROM,MAILING_LIST_MULTI,SPF_HELO_PASS autolearn=ham autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id 760B527BBE2 for ; Tue, 21 Nov 2023 03:56:28 +0000 (GMT) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1r5Hro-00033Y-Gn; Mon, 20 Nov 2023 22:56:04 -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 1r5Hrl-000335-7E for guix-patches@gnu.org; Mon, 20 Nov 2023 22:56:01 -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 1r5Hrk-0001Q7-UA for guix-patches@gnu.org; Mon, 20 Nov 2023 22:56:00 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1r5Hrl-00018l-Ta for guix-patches@gnu.org; Mon, 20 Nov 2023 22:56:01 -0500 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 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-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+patchwork=mira.cbaines.net@gnu.org Sender: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org X-getmail-retrieved-from-mailbox: Patches * gnu/packages/lean.scm (lean)[arguments]: Use G-expressions. --- gnu/packages/lean.scm | 49 +++++++++++++++++++++++-------------------- 1 file changed, 26 insertions(+), 23 deletions(-) base-commit: d20ece07dbb09382f361c8bbf0bcab9e83d8b73e 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 From patchwork Tue Nov 21 04:48:29 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Zhu Zihao X-Patchwork-Id: 56676 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id 90D9627BBE2; Tue, 21 Nov 2023 04:50:20 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-2.7 required=5.0 tests=BAYES_00,DKIM_INVALID, DKIM_SIGNED,FREEMAIL_FROM,MAILING_LIST_MULTI,SPF_HELO_PASS, URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id DBBA527BBE9 for ; Tue, 21 Nov 2023 04:50:16 +0000 (GMT) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1r5Ii2-000893-F4; Mon, 20 Nov 2023 23:50:02 -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 1r5Ii0-00088g-4t for guix-patches@gnu.org; Mon, 20 Nov 2023 23:50:00 -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 1r5Ihz-00086k-IV for guix-patches@gnu.org; Mon, 20 Nov 2023 23:49:59 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1r5Ii1-0002bJ-Un for guix-patches@gnu.org; Mon, 20 Nov 2023 23:50:01 -0500 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 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-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+patchwork=mira.cbaines.net@gnu.org Sender: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org X-getmail-retrieved-from-mailbox: Patches * 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")