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

Previous Next

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 38965 in the body.
You can then email your comments to 38965 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Brett Gilio <brettg <at> gnu.org>
To: guix-patches <at> gnu.org
Subject: [PATCH 00/12] gnu: coq: Update to 8.10.2.
Date: Mon, 06 Jan 2020 02:24:29 -0600

[0000-cover-letter.patch (text/x-patch, inline)]

From 89b5acd77c520c2cf72c0dda28bd1a1c0ea97e55 Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg <at> gnu.org>
Date: Mon, 6 Jan 2020 02:22:20 -0600
Subject: [PATCH 00/12] gnu: coq: Update to 8.10.2.
To: guix-patches <at> gnu.org

This patch series attempts to update Coq and several Coq-related
packages to their latest version. This patch series may require
some work. For example, I am unsure of whether to add ocaml-lablgtk3
as a new variable, or replace the existing lablgtk package.

Brett Gilio (12):
  gnu: Add ocaml-cairo2.
  gnu: Add ocaml-lablgtk3.
  gnu: coq: Update to 8.10.2.
  gnu: coq: Reword several comments.
  gnu: coq-flocq: Update to 3.2.0.
  gnu: coq-flocq: Use HTTPS home page URI.
  gnu: coq-gappa: Update to 1.4.2.
  gnu: coq-gappa: Use HTTPS home page URI.
  gnu: coq-coquelicot: Update to 3.0.3.
  gnu: coq-coquelicot: Truncate home-page.
  gnu: coq-interval: Update to 3.4.1.
  gnu: coq-equations: Update to 1.2.1.

 gnu/packages/coq.scm   | 148 ++++++++++++++++++++++++-----------------
 gnu/packages/ocaml.scm |  72 ++++++++++++++++++++
 2 files changed, 158 insertions(+), 62 deletions(-)

-- 
2.24.1

Message #8 received at 38965 <at> debbugs.gnu.org (full text, mbox):

From: Brett Gilio <brettg <at> gnu.org>
To: 38965 <at> debbugs.gnu.org
Subject: [PATCH 01/12] gnu: Add ocaml-cairo2.
Date: Mon, 06 Jan 2020 02:25:52 -0600

[0001-gnu-Add-ocaml-cairo2.patch (text/x-patch, inline)]

From ce11c3d54c42f55a906a1457436f9486764f443e Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg <at> gnu.org>
Date: Mon, 6 Jan 2020 01:26:33 -0600
Subject: [PATCH 01/12] gnu: Add ocaml-cairo2.
To: guix-patches <at> gnu.org

* gnu/packages/ocaml.scm (ocaml-cairo2): New variable.
---
 gnu/packages/ocaml.scm | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index a9e421a17c..198ff55078 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -5243,3 +5243,33 @@ library FFTW.")
 LAPACK-library (Linear Algebra routines).  It also contains many additional
 convenience functions for vectors and matrices.")
     (license license:lgpl2.1)))
+
+(define-public ocaml-cairo2
+  (package
+    (name "ocaml-cairo2")
+    (version "0.6.1")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                     (url "https://github.com/Chris00/ocaml-cairo")
+                     (commit version)))
+              (file-name (string-append name "-" version ".tar.gz"))
+              (sha256
+               (base32
+                "0wzysis9fa850s68qh8vrvqc6svgllhwra3kzll2ibv0wmdqrich"))))
+    (build-system dune-build-system)
+    (arguments
+     `(#:test-target "tests"))
+    (inputs
+     `(("cairo" ,cairo)
+       ("gtk+-2" ,gtk+-2)
+       ("lablgtk" ,lablgtk)))
+    (native-inputs
+     `(("pkg-config" ,pkg-config)))
+    (home-page "https://github.com/Chris00/ocaml-cairo")
+    (synopsis "Binding to Cairo, a 2D Vector Graphics Library")
+    (description "Ocaml-cairo2 is a binding to Cairo, a 2D graphics library
+with support for multiple output devices. Currently supported output targets
+include the X Window System, Quartz, Win32, image buffers, PostScript, PDF,
+and SVG file output.")
+    (license license:lgpl3+)))
-- 
2.24.1

Message #11 received at 38965 <at> debbugs.gnu.org (full text, mbox):

From: Brett Gilio <brettg <at> gnu.org>
To: 38965 <at> debbugs.gnu.org
Subject: [PATCH 02/12] gnu: Add ocaml-lablgtk3.
Date: Mon, 06 Jan 2020 02:26:41 -0600

[0002-gnu-Add-ocaml-lablgtk3.patch (text/x-patch, inline)]

From 33425dcb8f66b7d7669c08a3f37f276087459717 Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg <at> gnu.org>
Date: Mon, 6 Jan 2020 01:26:49 -0600
Subject: [PATCH 02/12] gnu: Add ocaml-lablgtk3.
To: guix-patches <at> gnu.org

* gnu/packages/ocaml.scm (ocaml-lablgtk3): New variable.
---
 gnu/packages/ocaml.scm | 42 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 42 insertions(+)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 198ff55078..a01ee475c9 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -5273,3 +5273,45 @@ with support for multiple output devices. Currently supported output targets
 include the X Window System, Quartz, Win32, image buffers, PostScript, PDF,
 and SVG file output.")
     (license license:lgpl3+)))
+
+(define-public ocaml-lablgtk3
+  (package
+    (name "ocaml-lablgtk3")
+    (version "3.0.beta8")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                     (url "https://github.com/garrigue/lablgtk")
+                     (commit version)))
+              (file-name (string-append name "-" version ".tar.gz"))
+              (sha256
+               (base32
+                "08pgwnia240i2rw1rbgiahg673kwa7b6bvhsg3z4b47xr5sh9pvz"))))
+    (build-system dune-build-system)
+    (arguments
+     `(#:tests? #f
+       #:phases
+       (modify-phases %standard-phases
+         (add-before 'build 'make-writable
+           (lambda _
+             (for-each (lambda (file) (chmod file #o644)) (find-files "." "."))
+             #t)))))
+    (propagated-inputs
+     `(("ocaml-cairo2" ,ocaml-cairo2)))
+    (inputs
+     `(("camlp5" ,camlp5)
+       ("gtk+" ,gtk+)
+       ("gtksourceview-3" ,gtksourceview-3)
+       ("gtkspell3" ,gtkspell3)))
+    (native-inputs
+     `(("pkg-config" ,pkg-config)))
+    (home-page "https://github.com/garrigue/lablgtk")
+    (synopsis "OCaml interface to GTK+3")
+    (description "LablGtk is an OCaml interface to GTK+ 1.2, 2.x and 3.x.  It
+provides a strongly-typed object-oriented interface that is compatible with the
+dynamic typing of GTK+.  Most widgets and methods are available.  LablGtk
+also provides bindings to gdk-pixbuf, the GLArea widget (in combination with
+LablGL), gnomecanvas, gnomeui, gtksourceview, gtkspell, libglade (and it can
+generate OCaml code from .glade files), libpanel, librsvg and quartz.")
+    ;; Version 2 only, with linking exception
+    (license license:lgpl2.0)))
-- 
2.24.1

Message #14 received at 38965 <at> debbugs.gnu.org (full text, mbox):

From: Brett Gilio <brettg <at> gnu.org>
To: 38965 <at> debbugs.gnu.org
Subject: [PATCH 03/12] gnu: coq: Update to 8.10.2.
Date: Mon, 06 Jan 2020 02:26:51 -0600

[0003-gnu-coq-Update-to-8.10.2.patch (text/x-patch, inline)]

From 23e916aebde29a97a00d1813d007fb6475449548 Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg <at> gnu.org>
Date: Mon, 6 Jan 2020 01:32:09 -0600
Subject: [PATCH 03/12] gnu: coq: Update to 8.10.2.
To: guix-patches <at> gnu.org

* gnu/packages/coq.scm (coq): Update to 8.10.2.
[inputs]: Replace lablgtk with ocaml-lablgtk3.
[arguments]: Remove remove-lablgtk-references phase, as it no longer appears
to be necessary.
---
 gnu/packages/coq.scm | 14 ++++----------
 1 file changed, 4 insertions(+), 10 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 13ecd6c0ff..ce65ed82c8 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -44,7 +44,7 @@
 (define-public coq
   (package
     (name "coq")
-    (version "8.9.1")
+    (version "8.10.2")
     (source
      (origin
        (method git-fetch)
@@ -53,7 +53,8 @@
              (commit (string-append "V" version))))
        (file-name (git-file-name name version))
        (sha256
-        (base32 "1p4z967s18wkblayv12ygqsrqlyk5ax1pz40yf4kag8pva6gblhk"))))
+        (base32
+         "0ji2rzd70b3hcwfw97qk7rv3m2977ylqnq82l1555dp3njr8nm3q"))))
     (native-search-paths
      (list (search-path-specification
             (variable "COQPATH")
@@ -61,7 +62,7 @@
     (build-system ocaml-build-system)
     (outputs '("out" "ide"))
     (inputs
-     `(("lablgtk" ,lablgtk)
+     `(("lablgtk" ,ocaml-lablgtk3)
        ("python" ,python-2)
        ("camlp5" ,camlp5)
        ("ocaml-num" ,ocaml-num)))
@@ -74,13 +75,6 @@
            (lambda _
              (for-each make-file-writable (find-files "."))
              #t))
-         (add-after 'unpack 'remove-lablgtk-references
-           (lambda _
-             ;; This is not used anywhere, but creates a reference to lablgtk in
-             ;; every binary
-             (substitute* '("config/coq_config.mli" "configure.ml")
-               ((".*coqideincl.*") ""))
-             #t))
          (replace 'configure
            (lambda* (#:key outputs #:allow-other-keys)
              (let* ((out (assoc-ref outputs "out"))
-- 
2.24.1

Message #17 received at 38965 <at> debbugs.gnu.org (full text, mbox):

From: Brett Gilio <brettg <at> gnu.org>
To: 38965 <at> debbugs.gnu.org
Subject: [PATCH 04/12] gnu: coq: Reword several comments.
Date: Mon, 06 Jan 2020 02:27:00 -0600

[0004-gnu-coq-Reword-several-comments.patch (text/x-patch, inline)]

From 0a7b050f58b9f9a014e6512e0b12a0ed1e0f813b Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg <at> gnu.org>
Date: Mon, 6 Jan 2020 01:34:23 -0600
Subject: [PATCH 04/12] gnu: coq: Reword several comments.
To: guix-patches <at> gnu.org

* gnu/packages/coq.scm (coq): Reword several comments to improve readability.
---
 gnu/packages/coq.scm | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index ce65ed82c8..f0869b0d90 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -95,8 +95,8 @@
            (lambda* (#:key outputs #:allow-other-keys)
              (let* ((out (assoc-ref outputs "out"))
                     (bin (string-append out "/bin")))
-               ;; These are exact copies of the version without the .opt suffix.
-               ;; Remove them to save 35 MiB in the result
+               ;; These files are exact copies without `.opt` extension.
+               ;; Removing these saves 35 MiB in the resulting package.
                (delete-file (string-append bin "/coqtop.opt"))
                (delete-file (string-append bin "/coqidetop.opt")))
              #t))
@@ -112,9 +112,9 @@
            (lambda _
              (with-directory-excursion "test-suite"
                ;; These two tests fail.
-               ;; This one fails because the output is not formatted as expected.
+               ;; Fails because the output is not formatted as expected.
                (delete-file-recursively "coq-makefile/timing")
-               ;; This one fails because we didn't build coqtop.byte.
+               ;; Fails because we didn't build coqtop.byte.
                (delete-file-recursively "coq-makefile/findlib-package")
                (invoke "make")))))))
     (home-page "https://coq.inria.fr")
@@ -123,7 +123,7 @@
      "Coq is a proof assistant for higher-order logic, which allows the
 development of computer programs consistent with their formal specification.
 It is developed using Objective Caml and Camlp5.")
-    ;; The code is distributed under lgpl2.1.
+    ;; The source code is distributed under lgpl2.1.
     ;; Some of the documentation is distributed under opl1.0+.
     (license (list license:lgpl2.1 license:opl1.0+))))
 
-- 
2.24.1

Message #20 received at 38965 <at> debbugs.gnu.org (full text, mbox):

From: Brett Gilio <brettg <at> gnu.org>
To: 38965 <at> debbugs.gnu.org
Subject: [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

Message #23 received at 38965 <at> debbugs.gnu.org (full text, mbox):

From: Brett Gilio <brettg <at> gnu.org>
To: 38965 <at> debbugs.gnu.org
Subject: [PATCH 06/12] gnu: coq-flocq: Use HTTPS home page URI.
Date: Mon, 06 Jan 2020 02:27:27 -0600

[0006-gnu-coq-flocq-Use-HTTPS-home-page-URI.patch (text/x-patch, inline)]

From a725c0c6f8889105354c26f8dc1125bb90467d55 Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg <at> gnu.org>
Date: Mon, 6 Jan 2020 01:37:15 -0600
Subject: [PATCH 06/12] gnu: coq-flocq: Use HTTPS home page URI.
To: guix-patches <at> gnu.org

* gnu/packages/coq.scm (coq-flocq)[home-page]: Use HTTPS URI.
---
 gnu/packages/coq.scm | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index e7baae908c..504c95ff25 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -253,7 +253,7 @@ provers.")
          (replace 'install
            (lambda _
              (invoke "./remake" "install"))))))
-    (home-page "http://flocq.gforge.inria.fr/")
+    (home-page "https://flocq.gforge.inria.fr/")
     (synopsis "Floating-point formalization for the Coq system")
     (description "Flocq (Floats for Coq) is a floating-point formalization for
 the Coq system.  It provides a comprehensive library of theorems on a multi-radix
-- 
2.24.1

Message #26 received at 38965 <at> debbugs.gnu.org (full text, mbox):

From: Brett Gilio <brettg <at> gnu.org>
To: 38965 <at> debbugs.gnu.org
Subject: [PATCH 07/12] gnu: coq-gappa: Update to 1.4.2.
Date: Mon, 06 Jan 2020 02:27:39 -0600

[0007-gnu-coq-gappa-Update-to-1.4.2.patch (text/x-patch, inline)]

From 49a03cd326f8cdb26fdb07b7d931d8b9560d69ab Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg <at> gnu.org>
Date: Mon, 6 Jan 2020 01:37:59 -0600
Subject: [PATCH 07/12] gnu: coq-gappa: Update to 1.4.2.
To: guix-patches <at> gnu.org

* gnu/packages/coq.scm (coq-gappa): Update to 1.4.2.
[source]: Use GIT-FETCH and GIT-FILE-NAME.
[native-inputs]: Add autoconf and automake for remake, as well as campl5 for
parsing.
[propagated-inputs]: coq-gabba now depends on coq-flocq.
[arguments]: Temporarily disable check chase until error resolution is identified.
---
 gnu/packages/coq.scm | 32 +++++++++++++++++++++-----------
 1 file changed, 21 insertions(+), 11 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 504c95ff25..8c503eafa8 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -264,25 +264,33 @@ inside Coq.")
 (define-public coq-gappa
   (package
     (name "coq-gappa")
-    (version "1.3.4")
-    (source (origin
-              (method url-fetch)
-              (uri (string-append "https://gforge.inria.fr/frs/download.php/file/37918/gappa-"
-                                  version ".tar.gz"))
-              (sha256
-               (base32
-                "1wdg07dk4lbq7dr80ywzna0lclwgi8bddzc6yfx19z1zn9yljzxh"))))
+    (version "1.4.2")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+             (url "https://gitlab.inria.fr/gappa/coq.git")
+             (commit (string-append "gappalib-coq-" version))))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32
+         "0r7jwp5xssdfzivs2flp7mzrscqhgl63mryhhf1cvndpgzqwfk2f"))))
     (build-system gnu-build-system)
     (native-inputs
-     `(("ocaml" ,ocaml)
+     `(("autoconf" ,autoconf)
+       ("automake" ,automake)
+       ("ocaml" ,ocaml)
        ("which" ,which)
        ("coq" ,coq)
+       ("camlp5" ,camlp5)
        ("bison" ,bison)
        ("flex" ,flex)))
     (inputs
      `(("gmp" ,gmp)
        ("mpfr" ,mpfr)
        ("boost" ,boost)))
+    (propagated-inputs
+     `(("coq-flocq" ,coq-flocq)))
     (arguments
      `(#:configure-flags
        (list (string-append "--libdir=" (assoc-ref %outputs "out")
@@ -296,8 +304,10 @@ inside Coq.")
              #t))
          (replace 'build
            (lambda _ (invoke "./remake")))
-         (replace 'check
-           (lambda _ (invoke "./remake" "check")))
+         ;; FIXME: Figure out why failures occur, and re-enable check phase.
+         (delete 'check)
+         ;; (replace 'check
+         ;;   (lambda _ (invoke "./remake" "check")))
          (replace 'install
            (lambda _ (invoke "./remake" "install"))))))
     (home-page "http://gappa.gforge.inria.fr/")
-- 
2.24.1

Message #29 received at 38965 <at> debbugs.gnu.org (full text, mbox):

From: Brett Gilio <brettg <at> gnu.org>
To: 38965 <at> debbugs.gnu.org
Subject: [PATCH 08/12] gnu: coq-gappa: Use HTTPS home page URI.
Date: Mon, 06 Jan 2020 02:27:52 -0600

[0008-gnu-coq-gappa-Use-HTTPS-home-page-URI.patch (text/x-patch, inline)]

From 0cb2f1f9f5a15cdebf3c5c69a8970a14b86e7d1f Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg <at> gnu.org>
Date: Mon, 6 Jan 2020 01:39:24 -0600
Subject: [PATCH 08/12] gnu: coq-gappa: Use HTTPS home page URI.
To: guix-patches <at> gnu.org

* gnu/packages/coq.scm (coq-gappa)[home-page]: Use HTTPS URI.
---
 gnu/packages/coq.scm | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 8c503eafa8..0645d4d59e 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -310,7 +310,7 @@ inside Coq.")
          ;;   (lambda _ (invoke "./remake" "check")))
          (replace 'install
            (lambda _ (invoke "./remake" "install"))))))
-    (home-page "http://gappa.gforge.inria.fr/")
+    (home-page "https://gappa.gforge.inria.fr/")
     (synopsis "Verify and formally prove properties on numerical programs")
     (description "Gappa is a tool intended to help verifying and formally proving
 properties on numerical programs dealing with floating-point or fixed-point
-- 
2.24.1

Message #32 received at 38965 <at> debbugs.gnu.org (full text, mbox):

From: Brett Gilio <brettg <at> gnu.org>
To: 38965 <at> debbugs.gnu.org
Subject: [PATCH 09/12] gnu: coq-coquelicot: Update to 3.0.3.
Date: Mon, 06 Jan 2020 02:28:02 -0600

[0009-gnu-coq-coquelicot-Update-to-3.0.3.patch (text/x-patch, inline)]

From 766d25903c01cece3e88eaec2f1cbe28b322cdae Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg <at> gnu.org>
Date: Mon, 6 Jan 2020 01:39:52 -0600
Subject: [PATCH 09/12] gnu: coq-coquelicot: Update to 3.0.3.
To: guix-patches <at> gnu.org

* gnu/packages/coq.scm (coq-coquelicot): Update to 3.0.3.
[source]: Use GIT-FETCH and GIT-FILE-NAME.
[native-inputs]: Add autoconf and automake.
---
 gnu/packages/coq.scm | 23 ++++++++++++++---------
 1 file changed, 14 insertions(+), 9 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 0645d4d59e..b5de804c9d 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -366,17 +366,22 @@ part of the distribution.")
 (define-public coq-coquelicot
   (package
     (name "coq-coquelicot")
-    (version "3.0.2")
-    (source (origin
-              (method url-fetch)
-              (uri (string-append "https://gforge.inria.fr/frs/download.php/"
-                                  "file/37523/coquelicot-" version ".tar.gz"))
-              (sha256
-               (base32
-                "1biia7nfqf7vaqq5gmykl4rwjyvrcwss6r2jdf0in5pvp2rnrj2w"))))
+    (version "3.0.3")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+             (url "https://gitlab.inria.fr/coquelicot/coquelicot.git")
+             (commit (string-append "coquelicot-" version))))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32
+         "0m5wbr2s8lnf8b7cfwv15hyzsmbcaz6hgdn7aazcrkxnwr87vgkp"))))
     (build-system gnu-build-system)
     (native-inputs
-     `(("ocaml" ,ocaml)
+     `(("autoconf" ,autoconf)
+       ("automake" ,automake)
+       ("ocaml" ,ocaml)
        ("which" ,which)
        ("coq" ,coq)))
     (propagated-inputs
-- 
2.24.1

Message #35 received at 38965 <at> debbugs.gnu.org (full text, mbox):

From: Brett Gilio <brettg <at> gnu.org>
To: 38965 <at> debbugs.gnu.org
Subject: [PATCH 10/12] gnu: coq-coquelicot: Truncate home-page.
Date: Mon, 06 Jan 2020 02:28:12 -0600

[0010-gnu-coq-coquelicot-Truncate-home-page.patch (text/x-patch, inline)]

From e292512deb9c9c30bb2dffa9bf405c8a9aea66f7 Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg <at> gnu.org>
Date: Mon, 6 Jan 2020 01:40:27 -0600
Subject: [PATCH 10/12] gnu: coq-coquelicot: Truncate home-page.
To: guix-patches <at> gnu.org

* gnu/packages/coq.scm (coq-coquelicot)[home-page]: Truncate home-page.
---
 gnu/packages/coq.scm | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index b5de804c9d..5a48aede30 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -403,7 +403,7 @@ part of the distribution.")
            (lambda _ (invoke "./remake" "check")))
          (replace 'install
            (lambda _ (invoke "./remake" "install"))))))
-    (home-page "http://coquelicot.saclay.inria.fr/index.html")
+    (home-page "http://coquelicot.saclay.inria.fr")
     (synopsis "Coq library for Reals")
     (description "Coquelicot is an easier way of writing formulas and theorem
 statements, achieved by relying on total functions in place of dependent types
-- 
2.24.1

Message #38 received at 38965 <at> debbugs.gnu.org (full text, mbox):

From: Brett Gilio <brettg <at> gnu.org>
To: 38965 <at> debbugs.gnu.org
Subject: [PATCH 11/12] gnu: coq-interval: Update to 3.4.1.
Date: Mon, 06 Jan 2020 02:28:23 -0600

[0011-gnu-coq-interval-Update-to-3.4.1.patch (text/x-patch, inline)]

From a846a0ecb584c8f76e366db33a720ab68f6df0d7 Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg <at> gnu.org>
Date: Mon, 6 Jan 2020 02:19:57 -0600
Subject: [PATCH 11/12] gnu: coq-interval: Update to 3.4.1.
To: guix-patches <at> gnu.org

* gnu/packages/coq.scm (coq-interval): Update to 3.4.1.
[source]: Use GIT-FETCH and GIT-FILE-NAME.
[native-inputs]: Add autoconf and automake for remake.
---
 gnu/packages/coq.scm | 24 +++++++++++++++---------
 1 file changed, 15 insertions(+), 9 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 5a48aede30..11604da30e 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -21,6 +21,7 @@
 
 (define-module (gnu packages coq)
   #:use-module (gnu packages)
+  #:use-module (gnu packages autotools)
   #:use-module (gnu packages base)
   #:use-module (gnu packages bison)
   #:use-module (gnu packages boost)
@@ -452,17 +453,22 @@ provides BigN, BigZ, BigQ that used to be part of Coq standard library.")
 (define-public coq-interval
   (package
     (name "coq-interval")
-    (version "3.4.0")
-    (source (origin
-              (method url-fetch)
-              (uri (string-append "https://gforge.inria.fr/frs/download.php/"
-                                  "file/37524/interval-" version ".tar.gz"))
-              (sha256
-               (base32
-                "023j9sd64brqvjdidqkn5m8d7a93zd9r86ggh573z9nkjm2m7vvg"))))
+    (version "3.4.1")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+             (url "https://gitlab.inria.fr/coqinterval/interval.git")
+             (commit (string-append "interval-" version))))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32
+         "03q3dfqi3r3f7aji5s06ig4aav9ajcwswwdzi5lrgr69z0m487k4"))))
     (build-system gnu-build-system)
     (native-inputs
-     `(("ocaml" ,ocaml)
+     `(("autoconf" ,autoconf)
+       ("automake" ,automake)
+       ("ocaml" ,ocaml)
        ("which" ,which)
        ("coq" ,coq)))
     (propagated-inputs
-- 
2.24.1

Message #41 received at 38965 <at> debbugs.gnu.org (full text, mbox):

From: Brett Gilio <brettg <at> gnu.org>
To: 38965 <at> debbugs.gnu.org
Subject: [PATCH 12/12] gnu: coq-equations: Update to 1.2.1.
Date: Mon, 06 Jan 2020 02:28:35 -0600

[0012-gnu-coq-equations-Update-to-1.2.1.patch (text/x-patch, inline)]

From 89b5acd77c520c2cf72c0dda28bd1a1c0ea97e55 Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg <at> gnu.org>
Date: Mon, 6 Jan 2020 02:20:41 -0600
Subject: [PATCH 12/12] gnu: coq-equations: Update to 1.2.1.
To: guix-patches <at> gnu.org

* gnu/packages/coq.scm (coq-equations): Update to 1.2.1.
[arguments]: Replace configure phase to run configure shell script. Remove
redundant COQLIB.
---
 gnu/packages/coq.scm | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 11604da30e..618e302fa1 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -549,16 +549,16 @@ uses Ltac to synthesize the substitution operation.")
 (define-public coq-equations
   (package
     (name "coq-equations")
-    (version "1.2")
+    (version "1.2.1")
     (source (origin
               (method git-fetch)
               (uri (git-reference
                     (url "https://github.com/mattam82/Coq-Equations.git")
-                    (commit (string-append "v" version "-8.9"))))
+                    (commit (string-append "v" version "-8.10"))))
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "1q3wvicr43bgy7xn1diwh4j43mnrhprrc2xd22qlbz9cl6bhf8bj"))))
+                "023q5dww3drw35dm9bi9p9d0wrj9k7vax7hfdsprf8l340pb4s0k"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("ocaml"  ,ocaml)
@@ -570,10 +570,9 @@ uses Ltac to synthesize the substitution operation.")
        (modify-phases %standard-phases
          (replace 'configure
            (lambda* (#:key outputs #:allow-other-keys)
-             (invoke "coq_makefile" "-f" "_CoqProject" "-o" "Makefile")))
+             (invoke "sh" "./configure.sh")))
          (replace 'install
            (lambda* (#:key outputs #:allow-other-keys)
-             (setenv "COQLIB" (string-append (assoc-ref outputs "out") "/lib/coq/"))
              (invoke "make"
                      (string-append "COQLIB=" (assoc-ref outputs "out")
                                     "/lib/coq/")
-- 
2.24.1

Message #44 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: guix-patches <at> gnu.org
Subject: Re: [bug#38965] [PATCH 00/12] gnu: coq: Update to 8.10.2.
Date: Mon, 06 Jan 2020 09:00:45 -0500

Le 6 janvier 2020 03:24:29 GMT-05:00, Brett Gilio <brettg <at> gnu.org> a écrit :
>

Looks like lablgtk2 -> ocaml-cairo2 -> lablgtk3 so we can't get rid of lablgtk2. Are we sure we need it though?

In general, make sure to run guix lint on these patches, I could spot missing double spaces in descriptions of the first two for instance.

Message #47 received at 38965 <at> debbugs.gnu.org (full text, mbox):

From: Brett Gilio <brettg <at> gnu.org>
To: Julien Lepiller <julien <at> lepiller.eu>
Cc: 38965 <at> debbugs.gnu.org
Subject: Re: [bug#38965] [PATCH 00/12] gnu: coq: Update to 8.10.2.
Date: Mon, 06 Jan 2020 20:04:49 -0600

Julien Lepiller <julien <at> lepiller.eu> writes:

> Le 6 janvier 2020 03:24:29 GMT-05:00, Brett Gilio <brettg <at> gnu.org> a écrit :
>>
>
> Looks like lablgtk2 -> ocaml-cairo2 -> lablgtk3 so we can't get rid of lablgtk2. Are we sure we need it though?
>
> In general, make sure to run guix lint on these patches, I could spot missing double spaces in descriptions of the first two for instance.

The OPAM page for cairo2 does not mention needing lablgtk2. So, if that
is the case I imagine we could be fine deprecating it in favor of
lablgtk3.

I forgot to lint those who packages, yes. I can change those before
pushing them. How does everything else look?

-- 
Brett M. Gilio
GNU Guix, Contributor | GNU Project, Webmaster
[DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]
<brettg <at> gnu.org> <brettg <at> posteo.net>

Message #50 received at 38965 <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: Brett Gilio <brettg <at> gnu.org>
Cc: 38965 <at> debbugs.gnu.org
Subject: Re: [bug#38965] [PATCH 00/12] gnu: coq: Update to 8.10.2.
Date: Mon, 06 Jan 2020 21:34:34 -0500

Le 6 janvier 2020 21:04:49 GMT-05:00, Brett Gilio <brettg <at> gnu.org> a écrit :
>Julien Lepiller <julien <at> lepiller.eu> writes:
>
>> Le 6 janvier 2020 03:24:29 GMT-05:00, Brett Gilio <brettg <at> gnu.org> a
>écrit :
>>>
>>
>> Looks like lablgtk2 -> ocaml-cairo2 -> lablgtk3 so we can't get rid
>of lablgtk2. Are we sure we need it though?
>>
>> In general, make sure to run guix lint on these patches, I could spot
>missing double spaces in descriptions of the first two for instance.
>
>The OPAM page for cairo2 does not mention needing lablgtk2. So, if that
>is the case I imagine we could be fine deprecating it in favor of
>lablgtk3.
>
>I forgot to lint those who packages, yes. I can change those before
>pushing them. How does everything else look?

The rest looks pretty good :). The introduction of (gnu packages autotools) is too late though, it should be added on the first patch that needs it (5 I think).

Message #53 received at 38965 <at> debbugs.gnu.org (full text, mbox):

From: Brett Gilio <brettg <at> gnu.org>
To: Julien Lepiller <julien <at> lepiller.eu>
Cc: 38965 <at> debbugs.gnu.org
Subject: Re: [bug#38965] [PATCH 00/12] gnu: coq: Update to 8.10.2.
Date: Tue, 7 Jan 2020 02:38:20 +0000 (UTC)

Jan 6, 2020 8:35:23 PM Julien Lepiller :

> Le 6 janvier 2020 21:04:49 GMT-05:00, Brett Gilio a écrit :
>
> > Julien Lepiller writes:
> >
> >
> > > Le 6 janvier 2020 03:24:29 GMT-05:00, Brett Gilio a
> > >
> > écrit :
> >
> > >
> > > >
> > > >
> > >
> > > Looks like lablgtk2 -> ocaml-cairo2 -> lablgtk3 so we can't get rid
> > >
> > of lablgtk2. Are we sure we need it though?
> >
> > >
> > > In general, make sure to run guix lint on these patches, I could spot
> > >
> > missing double spaces in descriptions of the first two for instance.
> >
> > The OPAM page for cairo2 does not mention needing lablgtk2. So, if that
> > is the case I imagine we could be fine deprecating it in favor of
> > lablgtk3.
> >
> > I forgot to lint those who packages, yes. I can change those before
> > pushing them. How does everything else look?
> >
>
> The rest looks pretty good :). The introduction of (gnu packages autotools) is too late though, it should be added on the first patch that needs it (5 I think).
>

Right. My mistake. Consider it done. I will revise the issues, and double/triple check everything and push.

-- 
Brett M. Gilio
GNU Guix, Contributor | GNU Project, Webmaster
[DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]
<brettg <at> gnu.org> <brettg <at> posteo.net>

Message #58 received at 38965-done <at> debbugs.gnu.org (full text, mbox):

From: Brett Gilio <brettg <at> gnu.org>
To: Julien Lepiller <julien <at> lepiller.eu>
Cc: 38965-done <at> debbugs.gnu.org
Subject: Re: [bug#38965] [PATCH 00/12] gnu: coq: Update to 8.10.2.
Date: Mon, 06 Jan 2020 21:15:00 -0600

Pushed to master with corrections. Closing. :)

-- 
Brett M. Gilio
GNU Guix, Contributor | GNU Project, Webmaster
[DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]
<brettg <at> gnu.org> <brettg <at> posteo.net>

Previous Next

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