[PATCH 00/12] gnu: coq: Update to 8.10.2.

  • Done
  • quality assurance status badge
Details
2 participants
  • Brett Gilio
  • Julien Lepiller
Owner
unassigned
Submitted by
Brett Gilio
Severity
normal

Debbugs page

Brett Gilio wrote 5 years ago
(address . guix-patches@gnu.org)
874kx9xa9u.fsf@gnu.org
From 89b5acd77c520c2cf72c0dda28bd1a1c0ea97e55 Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg@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@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
Brett Gilio wrote 5 years ago
[PATCH 01/12] gnu: Add ocaml-cairo2.
(address . 38965@debbugs.gnu.org)
871rsdxa7j.fsf@gnu.org
From ce11c3d54c42f55a906a1457436f9486764f443e Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg@gnu.org>
Date: Mon, 6 Jan 2020 01:26:33 -0600
Subject: [PATCH 01/12] gnu: Add ocaml-cairo2.
To: guix-patches@gnu.org

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

Toggle diff (40 lines)
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
Brett Gilio wrote 5 years ago
[PATCH 02/12] gnu: Add ocaml-lablgtk3.
(address . 38965@debbugs.gnu.org)
87y2ulvvlq.fsf@gnu.org
From 33425dcb8f66b7d7669c08a3f37f276087459717 Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg@gnu.org>
Date: Mon, 6 Jan 2020 01:26:49 -0600
Subject: [PATCH 02/12] gnu: Add ocaml-lablgtk3.
To: guix-patches@gnu.org

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

Toggle diff (52 lines)
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
Brett Gilio wrote 5 years ago
[PATCH 03/12] gnu: coq: Update to 8.10.2.
(address . 38965@debbugs.gnu.org)
87v9ppvvlg.fsf@gnu.org
From 23e916aebde29a97a00d1813d007fb6475449548 Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg@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@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(-)

Toggle diff (48 lines)
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
Brett Gilio wrote 5 years ago
[PATCH 04/12] gnu: coq: Reword several comments.
(address . 38965@debbugs.gnu.org)
87sgktvvl7.fsf@gnu.org
From 0a7b050f58b9f9a014e6512e0b12a0ed1e0f813b Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg@gnu.org>
Date: Mon, 6 Jan 2020 01:34:23 -0600
Subject: [PATCH 04/12] gnu: coq: Reword several comments.
To: guix-patches@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(-)

Toggle diff (38 lines)
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
Brett Gilio wrote 5 years ago
[PATCH 05/12] gnu: coq-flocq: Update to 3.2.0.
(address . 38965@debbugs.gnu.org)
87pnfxvvks.fsf@gnu.org
From 241cfab94794ed4edcaaa338ba48b8292e5c6a0a Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg@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@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(-)

Toggle diff (52 lines)
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
Brett Gilio wrote 5 years ago
[PATCH 06/12] gnu: coq-flocq: Use HTTPS home page URI.
(address . 38965@debbugs.gnu.org)
87mub1vvkg.fsf@gnu.org
From a725c0c6f8889105354c26f8dc1125bb90467d55 Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg@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@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(-)

Toggle diff (15 lines)
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
Brett Gilio wrote 5 years ago
[PATCH 07/12] gnu: coq-gappa: Update to 1.4.2.
(address . 38965@debbugs.gnu.org)
87k165vvk4.fsf@gnu.org
From 49a03cd326f8cdb26fdb07b7d931d8b9560d69ab Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg@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@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(-)

Toggle diff (62 lines)
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
Brett Gilio wrote 5 years ago
[PATCH 08/12] gnu: coq-gappa: Use HTTPS home page URI.
(address . 38965@debbugs.gnu.org)
87h819vvjr.fsf@gnu.org
From 0cb2f1f9f5a15cdebf3c5c69a8970a14b86e7d1f Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg@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@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(-)

Toggle diff (15 lines)
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
Brett Gilio wrote 5 years ago
[PATCH 09/12] gnu: coq-coquelicot: Update to 3.0.3.
(address . 38965@debbugs.gnu.org)
87eewdvvjh.fsf@gnu.org
From 766d25903c01cece3e88eaec2f1cbe28b322cdae Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg@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@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(-)

Toggle diff (38 lines)
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
Brett Gilio wrote 5 years ago
[PATCH 10/12] gnu: coq-coquelicot: Truncate home-page.
(address . 38965@debbugs.gnu.org)
87blrhvvj7.fsf@gnu.org
From e292512deb9c9c30bb2dffa9bf405c8a9aea66f7 Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg@gnu.org>
Date: Mon, 6 Jan 2020 01:40:27 -0600
Subject: [PATCH 10/12] gnu: coq-coquelicot: Truncate home-page.
To: guix-patches@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(-)

Toggle diff (15 lines)
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
Brett Gilio wrote 5 years ago
[PATCH 11/12] gnu: coq-interval: Update to 3.4.1.
(address . 38965@debbugs.gnu.org)
878smlvviw.fsf@gnu.org
From a846a0ecb584c8f76e366db33a720ab68f6df0d7 Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg@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@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(-)

Toggle diff (46 lines)
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
Brett Gilio wrote 5 years ago
[PATCH 12/12] gnu: coq-equations: Update to 1.2.1.
(address . 38965@debbugs.gnu.org)
875zhpvvik.fsf@gnu.org
From 89b5acd77c520c2cf72c0dda28bd1a1c0ea97e55 Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg@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@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(-)

Toggle diff (38 lines)
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
Julien Lepiller wrote 5 years ago
Re: [bug#38965] [PATCH 00/12] gnu: coq: Update to 8.10.2.
(address . guix-patches@gnu.org)
53E54994-18D2-4D82-8E96-3D6E8A3A9D14@lepiller.eu
Le 6 janvier 2020 03:24:29 GMT-05:00, Brett Gilio <brettg@gnu.org> a écrit :
Toggle quote (2 lines)
>

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.
Brett Gilio wrote 5 years ago
(name . Julien Lepiller)(address . julien@lepiller.eu)(address . 38965@debbugs.gnu.org)
87o8vgm37i.fsf@gnu.org
Julien Lepiller <julien@lepiller.eu> writes:

Toggle quote (7 lines)
> Le 6 janvier 2020 03:24:29 GMT-05:00, Brett Gilio <brettg@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@gnu.org> <brettg@posteo.net>
Julien Lepiller wrote 5 years ago
(name . Brett Gilio)(address . brettg@gnu.org)(address . 38965@debbugs.gnu.org)
2E36EFCF-C7C0-442B-8F03-46CC3167DA92@lepiller.eu
Le 6 janvier 2020 21:04:49 GMT-05:00, Brett Gilio <brettg@gnu.org> a écrit :
Toggle quote (19 lines)
>Julien Lepiller <julien@lepiller.eu> writes:
>
>> Le 6 janvier 2020 03:24:29 GMT-05:00, Brett Gilio <brettg@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).
Brett Gilio wrote 5 years ago
(name . Julien Lepiller)(address . julien@lepiller.eu)(address . 38965@debbugs.gnu.org)
bfe895f8-7c9b-41ce-9f32-77fd3e7cce59@localhost
Jan 6, 2020 8:35:23 PM Julien Lepiller :

Toggle quote (33 lines)
> 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@gnu.org> <brettg@posteo.net>
Brett Gilio wrote 5 years ago
(name . Julien Lepiller)(address . julien@lepiller.eu)(address . 38965-done@debbugs.gnu.org)
8736csrm8b.fsf@gnu.org
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@gnu.org> <brettg@posteo.net>
Closed
?
Your comment

This issue is archived.

To comment on this conversation send an email to 38965@debbugs.gnu.org

To respond to this issue using the mumi CLI, first switch to it
mumi current 38965
Then, you may apply the latest patchset in this issue (with sign off)
mumi am -- -s
Or, compose a reply to this issue
mumi compose
Or, send patches to this issue
mumi send-email *.patch
You may also tag this issue. See list of standard tags. For example, to set the confirmed and easy tags
mumi command -t +confirmed -t +easy
Or, remove the moreinfo tag and set the help tag
mumi command -t -moreinfo -t +help