From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp1.migadu.com ([2001:41d0:1008:1e59::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms8.migadu.com with LMTPS id KB2VEcFhiGWNDwEAkFu2QA (envelope-from ) for ; Sun, 24 Dec 2023 17:52:17 +0100 Received: from aspmx1.migadu.com ([2001:41d0:303:e16b::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp1.migadu.com with LMTPS id eOpSDsFhiGWxTQEA62LTzQ (envelope-from ) for ; Sun, 24 Dec 2023 17:52:17 +0100 X-Envelope-To: larch@yhetil.org Authentication-Results: aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=nanein.fr header.s=mail header.b=iicazK9z; 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=1703436737; 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-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=NJbkXRJBkztfE4gZOMjWKEAx8Uf+im504OYhUHlrq7w=; b=G/BihB/2g0IAfoKkdkq+XzWW9EZUZwOqpTfihk5MkawQmcNQI5FofM0Y6S13QNFDv2+vPz Mb/lWmzcDK24Y5JilPufjEfv3zj1absd9XDOdAsMjIqhGK7bGhGxlA/g5fsIa/w1n9p3Vb YtiSK4Huo8oVxqWXaE1q/az4rYAdnhG9FadmP4JKbAqjzq/MbJ1htIRASrlQCRXo8Yq7SG 9VbVge27UtMFDFxPDH3T/tV8MMU/pyO0CCQF0qMdw8CurXi89KlRYH0W8PxQcCjoQyMmOD L0K/mzXVdVNNA7HkdOMrj+qBK9leRZDujfvqJ+ylFB8TiFqHsAbx7keiSw1Oqg== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=nanein.fr header.s=mail header.b=iicazK9z; 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=1703436737; a=rsa-sha256; cv=none; b=sF6u9kZ7Opznv0ewT31diB+GQkmuAW7dCDvsNkqDxvoVv9FNXdOmrZWVZIPUTW6E3PWlUM BzQaWTRTKytijm9A2li3FO1elYzCKjJ7OHXj9L22f/7bNwYxCHJKPpc6CkniIC5aAmof7w TfVvc+/k+FqtWUrP+Hi3zbylvGt/WUS+RhXMy13JYozVBEl8ow+kSazqhj9rQh8iqtDAZl +VfwI/0+gwlLYtGvgp8+aodIRm6vscMFuWNHHFqJlbRrCVWG1l6NZW6gChsEcusuzVyTF+ HlPYqVbEM5HxKULhUoFPP9T5i0QBC7nWV+Ohxmx215ivOAc7xU90P78dye2ayw== 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 E892E420F8 for ; Sun, 24 Dec 2023 17:52:16 +0100 (CET) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1rHRhp-0004xt-MY; Sun, 24 Dec 2023 11:52:01 -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 1rHRhm-0004xb-0R for guix-patches@gnu.org; Sun, 24 Dec 2023 11:51:58 -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 1rHRhk-0007kE-IB for guix-patches@gnu.org; Sun, 24 Dec 2023 11:51:56 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1rHRhq-0001YM-GH for guix-patches@gnu.org; Sun, 24 Dec 2023 11:52:02 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#64249] [PATCH 1/9] gnu: why3: Update to 1.6.0. Resent-From: ds-ac@nanein.fr Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 24 Dec 2023 16:52:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 64249 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 64249@debbugs.gnu.org Cc: pukkamustard@posteo.net, Arnaud DABY-SEESARAM , Josselin Poiret , Julien Lepiller Received: via spool by 64249-submit@debbugs.gnu.org id=B64249.17034366955934 (code B ref 64249); Sun, 24 Dec 2023 16:52:02 +0000 Received: (at 64249) by debbugs.gnu.org; 24 Dec 2023 16:51:35 +0000 Received: from localhost ([127.0.0.1]:53457 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rHRhP-0001Xd-29 for submit@debbugs.gnu.org; Sun, 24 Dec 2023 11:51:35 -0500 Received: from nanein.fr ([185.230.78.41]:40124) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rHRhL-0001XO-6j for 64249@debbugs.gnu.org; Sun, 24 Dec 2023 11:51:33 -0500 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=nanein.fr; s=mail; t=1703436379; bh=LQkarKPtNTty/5Ta7T3Rm6ABqv4fqp0B/S3AM9Hj+Qg=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=iicazK9zBLMAO9bh0y7E0m+6awoU2e7BhAoIPCGdZ3ILBEHPwWvYxS5BONYQSY+i2 J52yXKKQ7j9qTXpedukCX6hR0aj3U0mwl83itBUy3W8uN1pYzJ5aZwaoMISYHvCJJP H/OY+dO2mUhw6QxqLH0rBRwpwK7imTcoDloQr2E8iuoNfAuhMyj9UbPwynGlrBHTkW C8V+CZken3aQEAut/oacVVHvNDPznj1vQUdGQ9UuHtT4XN3kevJdFOhZEcE7dxN5WK NvpjE+lnEohVG8BlkyPVymsNWyGGPxGisRQGXZtpFRJuvm00t0rTjQbaY/iRfaqn6O n76+0s+PWr0eoUvT8xTLON//y2pp+scAp2cU73hEQg79c0RPSuxYOXEVuF+In6icFb 6QOPp4cXdykEZTYOcdTFOrVwrqylBc0xWRmv1II4Z3pE1fmSuZvsMbruDY1b9tK6V2 SZUW5Ba99snQH0LSlDgfTmn/5d5b+jt8kUllosZMnsutmSe7Ata9fG0exmp/HTlfmP P3HQdv7MhKpujeThxxItylp8m3J8oCfAv4tr5x1IVuz76ZNL/NB7sD5tGVsmqFu3X4 pLUFJ+IgsppCnTllmwnE9GHQ0wInw3PIyni1Hih80XNuf+WmUiOUDHmt/pJcE8jZJA AP4vpb12Xmki0cOV5BHr9vcQ= Received: from localhost.localdomain (unknown [IPv6:2a01:e0a:a9e:a4c0:9d01:2b7b:5834:e51]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature ECDSA (prime256v1) server-digest SHA256) (No client certificate requested) by nanein.fr (Postfix) with ESMTPSA id 7F6621401F2; Sun, 24 Dec 2023 17:46:19 +0100 (CET) Date: Sun, 24 Dec 2023 17:43:36 +0100 Message-ID: <3bb1fdf1696f86080333f71d8b41aaa4b242a154.1703436224.git.ds-ac@nanein.fr> X-Mailer: git-send-email 2.41.0 In-Reply-To: <20231224140732.4467c1fa@tachikoma.lepiller.eu> References: <20231224140732.4467c1fa@tachikoma.lepiller.eu> MIME-Version: 1.0 Content-Transfer-Encoding: 8bit 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: ds-ac@nanein.fr X-ACL-Warn: , ds-ac--- via Guix-patches From: ds-ac--- 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: mx13.migadu.com X-Migadu-Spam-Score: -4.71 X-Spam-Score: -4.71 X-Migadu-Queue-Id: E892E420F8 X-TUID: zgxQwCgC1Cjj From: Arnaud DABY-SEESARAM * gnu/packages/maths.scm (why3): Update to 1.6.0. Change-Id: I4d6e0e2224f1ffe85b84493f1834114bc8687d1b --- gnu/packages/maths.scm | 81 +++++++++++++++++++++--------------------- 1 file changed, 41 insertions(+), 40 deletions(-) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index ed1708c77b1..7d17ee58ae6 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -9201,50 +9201,51 @@ (define-public numdiff (define-public why3 (package (name "why3") - (version "1.4.1") - (source (origin - (method git-fetch) - (uri (git-reference - (url "https://gitlab.inria.fr/why3/why3") - (commit version))) - (file-name (git-file-name name version)) - (sha256 - (base32 - "1yca6mx8bjm8x0i594ivh31aw45s6fbimmwfj8g2v9zwrgmr1i4s")))) + (version "1.6.0") + (source + (origin + (method git-fetch) + (uri (git-reference + (url "https://gitlab.inria.fr/why3/why3") + (commit version))) + (file-name (git-file-name name version)) + (sha256 + (base32 "0k3y98xzhrl44vwzq2m6k4nrllrwp3ll69lc2gfl8d77w0wg7gkp")))) (build-system ocaml-build-system) - (native-inputs - (list autoconf automake coq ocaml which)) - (propagated-inputs - (list camlzip ocaml-graph ocaml-menhir ocaml-num ocaml-zarith)) - (inputs - (list coq-flocq emacs-minimal zlib)) + (native-inputs (list autoconf automake coq ocaml which)) + (propagated-inputs (list camlzip ocaml-graph ocaml-menhir ocaml-num + ocaml-zarith)) + (inputs (list coq-flocq emacs-minimal zlib)) (arguments - `(#:phases - (modify-phases %standard-phases - (add-before 'configure 'bootstrap - (lambda _ - (invoke "./autogen.sh") - (setenv "CONFIG_SHELL" (which "sh")) - (substitute* "configure" - (("#! /bin/sh") (string-append "#!" (which "sh"))) - ;; find ocaml-num in the correct directory - (("\\$DIR/nums.cma") "$DIR/num.cma") - (("\\$DIR/num.cmi") "$DIR/core/num.cmi")) - #t)) - (add-after 'configure 'fix-makefile - (lambda _ - (substitute* "Makefile" - ;; find ocaml-num in the correct directory - (("site-lib/num") "site-lib")) - #t)) - (add-after 'install 'install-lib - (lambda _ - (invoke "make" "byte") - (invoke "make" "install-lib") - #t))))) + `(#:phases (modify-phases %standard-phases + (add-before 'configure 'bootstrap + (lambda _ + (invoke "./autogen.sh") + (setenv "CONFIG_SHELL" + (which "sh")) + (substitute* "configure" + (("#! /bin/sh") + (string-append "#!" + (which "sh"))) + ;; find ocaml-num in the correct directory + (("\\$DIR/nums.cma") + "$DIR/num.cma") + (("\\$DIR/num.cmi") + "$DIR/core/num.cmi")) #t)) + (add-after 'configure 'fix-makefile + (lambda _ + (substitute* "Makefile" + ;; find ocaml-num in the correct directory + (("site-lib/num") + "site-lib")) #t)) + (add-after 'install 'install-lib + (lambda _ + (invoke "make" "byte") + (invoke "make" "install-lib") #t))))) (home-page "https://why3.lri.fr") (synopsis "Deductive program verification") - (description "Why3 provides a language for specification and programming, + (description + "Why3 provides a language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, -- 2.41.0