GNU bug report logs - #38965
[PATCH 00/12] gnu: coq: Update to 8.10.2.

Previous Next

Full log

View this message in rfc822 format

From: Brett Gilio <brettg <at> gnu.org>
To: 38965 <at> debbugs.gnu.org
Subject: [bug#38965] [PATCH 05/12] gnu: coq-flocq: Update to 3.2.0.
Date: Mon, 06 Jan 2020 02:27:15 -0600

[0005-gnu-coq-flocq-Update-to-3.2.0.patch (text/x-patch, inline)]

From 241cfab94794ed4edcaaa338ba48b8292e5c6a0a Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg <at> gnu.org>
Date: Mon, 6 Jan 2020 01:35:55 -0600
Subject: [PATCH 05/12] gnu: coq-flocq: Update to 3.2.0.
To: guix-patches <at> gnu.org

* gnu/packages/coq.scm (coq-flocq): Update to 3.2.0.
[source]: Use GIT-FETCH and GIT-FILE-NAME.
[native-inputs]: Add autoconf and automake for remake.
[arguments]: Add remove-failing-examples phase to work around union error.
---
 gnu/packages/coq.scm | 30 ++++++++++++++++++++----------
 1 file changed, 20 insertions(+), 10 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index f0869b0d90..e7baae908c 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -207,18 +207,22 @@ provers.")
 (define-public coq-flocq
   (package
     (name "coq-flocq")
-    (version "3.1.0")
-    (source (origin
-              (method url-fetch)
-              ;; Use the ‘Latest version’ link for a stable URI across releases.
-              (uri (string-append "https://gforge.inria.fr/frs/download.php/"
-                                  "file/37901/flocq-" version ".tar.gz"))
-              (sha256
-               (base32
-                "02szrgz9m0ac51la1lqpiv6i2g0zbgx9gz5rp0q1g00ajldyna5c"))))
+    (version "3.2.0")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+             (url "https://gitlab.inria.fr/flocq/flocq.git")
+             (commit (string-append "flocq-" version))))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32
+         "15bi36x7zj0glsb3s2gwqd4wswhfzh36rbp7imbyff53a7nna95l"))))
     (build-system gnu-build-system)
     (native-inputs
-     `(("ocaml" ,ocaml)
+     `(("autoconf" ,autoconf)
+       ("automake" ,automake)
+       ("ocaml" ,ocaml)
        ("which" ,which)
        ("coq" ,coq)))
     (arguments
@@ -227,6 +231,12 @@ provers.")
                             "/lib/coq/user-contrib/Flocq"))
        #:phases
        (modify-phases %standard-phases
+         (add-after 'unpack 'remove-failing-examples
+           (lambda _
+             (substitute* "Remakefile.in"
+               ;; Fails on a union error.
+               (("Double_rounding_odd_radix.v") ""))
+             #t))
          (add-before 'configure 'fix-remake
            (lambda _
              (substitute* "remake.cpp"
-- 
2.24.1

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.