Subject: [bug#64249] [PATCH 1/9] gnu: why3: Update to 1.6.0.

From: [email-masked]
Date: Sun, 24 Dec 2023 17:43:36 +0100

From: Arnaud DABY-SEESARAM <[email-masked]>

* 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