diff mbox series

[bug#70567,v2,4/7] gnu: why3: Use new style.

Message ID 8d9581a5f8063da2f40c4d9d35529219d3a0ee6b.1714058471.git.jean@foundation.xyz
State New
Headers show
Series [bug#70567,v2,1/7] gnu: ocaml-lablgtk3-sourceview3: Fix inputs. | expand

Commit Message

Jean-Pierre De Jesus Diaz April 25, 2024, 3:21 p.m. UTC 
* gnu/packages/maths.scm (why3): Use new style and move arguments
above input fields.

Change-Id: Ia9cb04cafe426d7f20c5efb10ca540572dbd3be9
---
 gnu/packages/maths.scm | 63 +++++++++++++++++++++++-------------------
 1 file changed, 34 insertions(+), 29 deletions(-)
diff mbox series

Patch

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 5c7f3102f3..57f750accc 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9400,36 +9400,41 @@  (define-public why3
                (base32
                 "0fq8wg8ji2v2ssz1d681glmk8glps1irnmdlhqfklaggx01hlf4p"))))
     (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))
     (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)))))
+     (list #: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"))))
+               (add-after 'configure 'fix-makefile
+                 (lambda _
+                   (substitute* "Makefile"
+                     ;; find ocaml-num in the correct directory
+                     (("site-lib/num") "site-lib"))))
+            (add-after 'install 'install-lib
+              (lambda _
+                (invoke "make" "byte")
+                (invoke "make" "install-lib"))))))
+    (native-inputs (list autoconf
+                         automake
+                         coq
+                         ocaml
+                         ocaml-findlib
+                         which))
+    (propagated-inputs (list camlzip
+                             ocaml-graph
+                             ocaml-menhir
+                             ocaml-num
+                             ocaml-zarith))
+    (inputs (list coq-flocq
+                  emacs-minimal
+                  zlib))
     (home-page "https://why3.lri.fr")
     (synopsis "Deductive program verification")
     (description "Why3 provides a language for specification and programming,