unofficial mirror of guix-patches@gnu.org 
 help / color / mirror / code / Atom feed
From: Jean-Pierre De Jesus DIAZ <jean@foundation.xyz>
To: 70567@debbugs.gnu.org
Cc: Jean-Pierre De Jesus DIAZ <jean@foundation.xyz>,
	Andreas Enge <andreas@enge.fr>, Eric Bavier <bavier@posteo.net>,
	Sharlatan Hellseher <sharlatanus@gmail.com>
Subject: [bug#70567] [PATCH v2 4/7] gnu: why3: Use new style.
Date: Thu, 25 Apr 2024 17:21:54 +0200	[thread overview]
Message-ID: <8d9581a5f8063da2f40c4d9d35529219d3a0ee6b.1714058471.git.jean@foundation.xyz> (raw)
In-Reply-To: <fed82eb94f9d8f797e8ff23f3f4d45657295c1de.1714058471.git.jean@foundation.xyz>

* 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 --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,
-- 
2.41.0





  parent reply	other threads:[~2024-04-25 15:24 UTC|newest]

Thread overview: 38+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2024-04-25 13:08 [bug#70567] [PATCH 0/7] frama-c: Update to 28.1 Jean-Pierre De Jesus DIAZ
2024-04-25 13:12 ` [bug#70567] [PATCH 1/7] gnu: ocaml-lablgtk3-sourceview3: Fix inputs Jean-Pierre De Jesus DIAZ
2024-04-25 13:12 ` [bug#70567] [PATCH 2/7] gnu: coq-flocq: Update to 4.1.4 Jean-Pierre De Jesus DIAZ
2024-04-25 13:12 ` [bug#70567] [PATCH 3/7] gnu: why3: Update to 1.7.2 Jean-Pierre De Jesus DIAZ
2024-04-25 13:12 ` [bug#70567] [PATCH 4/7] gnu: why3: Use new style Jean-Pierre De Jesus DIAZ
2024-04-25 13:12 ` [bug#70567] [PATCH 5/7] gnu: why3: Enable extra features Jean-Pierre De Jesus DIAZ
2024-04-25 13:12 ` [bug#70567] [PATCH 6/7] gnu: Add ocaml-unionfind Jean-Pierre De Jesus DIAZ
2024-04-25 13:12 ` [bug#70567] [PATCH 7/7] gnu: frama-c: Update to 28.1 Jean-Pierre De Jesus DIAZ
2024-04-25 14:30 ` [bug#70567] [PATCH 0/7] " Julien Lepiller
2024-04-25 14:54 ` Arnaud Daby-Seesaram via Guix-patches via
2024-04-25 15:08   ` Jean-Pierre De Jesus Diaz
2024-04-25 15:23     ` Arnaud Daby-Seesaram via Guix-patches via
2024-04-25 15:22   ` Julien Lepiller
2024-04-25 15:35     ` Jean-Pierre De Jesus Diaz
2024-04-25 15:35     ` Andreas Enge
2024-04-26 13:03       ` Jean-Pierre De Jesus Diaz
2024-04-28 14:01         ` Andreas Enge
2024-04-25 15:21 ` [bug#70567] [PATCH v2 1/7] gnu: ocaml-lablgtk3-sourceview3: Fix inputs Jean-Pierre De Jesus DIAZ
2024-04-25 15:21   ` [bug#70567] [PATCH v2 2/7] gnu: coq-flocq: Update to 4.1.4 Jean-Pierre De Jesus DIAZ
2024-04-25 15:21   ` [bug#70567] [PATCH v2 3/7] gnu: why3: Update to 1.7.2 Jean-Pierre De Jesus DIAZ
2024-04-25 15:21   ` Jean-Pierre De Jesus DIAZ [this message]
2024-04-25 15:21   ` [bug#70567] [PATCH v2 5/7] gnu: why3: Enable extra features Jean-Pierre De Jesus DIAZ
2024-04-25 15:21   ` [bug#70567] [PATCH v2 6/7] gnu: Add ocaml-unionfind Jean-Pierre De Jesus DIAZ
2024-05-01 16:13     ` Ludovic Courtès
2024-04-25 15:21   ` [bug#70567] [PATCH v2 7/7] gnu: frama-c: Update to 28.1 Jean-Pierre De Jesus DIAZ
2024-05-07 15:57 ` [bug#70567] [PATCH v2 1/7] gnu: ocaml-lablgtk3-sourceview3: Fix inputs Jean-Pierre De Jesus DIAZ
2024-05-07 15:57   ` [bug#70567] [PATCH v2 2/7] gnu: coq-flocq: Update to 4.1.4 Jean-Pierre De Jesus DIAZ
2024-05-07 15:57   ` [bug#70567] [PATCH v2 3/7] gnu: why3: Update to 1.7.2 Jean-Pierre De Jesus DIAZ
2024-05-07 15:57   ` [bug#70567] [PATCH v2 4/7] gnu: why3: Use new style Jean-Pierre De Jesus DIAZ
2024-05-07 15:57   ` [bug#70567] [PATCH v2 5/7] gnu: why3: Enable extra features Jean-Pierre De Jesus DIAZ
2024-05-07 15:57   ` [bug#70567] [PATCH v2 6/7] gnu: Add ocaml-unionfind Jean-Pierre De Jesus DIAZ
2024-05-07 15:57   ` [bug#70567] [PATCH v2 7/7] gnu: frama-c: Update to 28.1 Jean-Pierre De Jesus DIAZ
2024-05-15 14:52     ` Andreas Enge
2024-05-15 15:05       ` Jean-Pierre De Jesus Diaz
2024-05-15 15:23         ` bug#70567: " Andreas Enge
2024-05-15 15:01 ` [bug#70567] [PATCH v3 1/3] gnu: why3: Update to 1.7.2 Jean-Pierre De Jesus DIAZ
2024-05-15 15:01   ` [bug#70567] [PATCH v3 2/3] gnu: why3: Use new style Jean-Pierre De Jesus DIAZ
2024-05-15 15:01   ` [bug#70567] [PATCH v3 3/3] gnu: why3: Enable extra features Jean-Pierre De Jesus DIAZ

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

  List information: https://guix.gnu.org/

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=8d9581a5f8063da2f40c4d9d35529219d3a0ee6b.1714058471.git.jean@foundation.xyz \
    --to=jean@foundation.xyz \
    --cc=70567@debbugs.gnu.org \
    --cc=andreas@enge.fr \
    --cc=bavier@posteo.net \
    --cc=sharlatanus@gmail.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
Code repositories for project(s) associated with this public inbox

	https://git.savannah.gnu.org/cgit/guix.git

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).