From patchwork Sun Dec 24 16:43:36 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: "ashish.is--- via Guix-patches\" via" X-Patchwork-Id: 58034 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 49EB627BBE9; Sun, 24 Dec 2023 16:52:18 +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,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 E78C927BBE2 for ; Sun, 24 Dec 2023 16:52:15 +0000 (GMT) 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 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 X-Patchwork-Original-From: ds-ac--- via Guix-patches via From: "ashish.is--- via Guix-patches\" via" 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 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,