From patchwork Mon Jan 6 08:25:52 2020 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Brett Gilio X-Patchwork-Id: 19609 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id 3C117179FE; Mon, 6 Jan 2020 08:26:10 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.0 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTP id E57141798D for ; Mon, 6 Jan 2020 08:26:09 +0000 (GMT) Received: from localhost ([::1]:49318 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioNiD-0000vh-FU for patchwork@mira.cbaines.net; Mon, 06 Jan 2020 03:26:09 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:41653) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioNi7-0000uA-Dh for guix-patches@gnu.org; Mon, 06 Jan 2020 03:26:04 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1ioNi6-00029i-B9 for guix-patches@gnu.org; Mon, 06 Jan 2020 03:26:03 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:38965) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1ioNi6-00029Y-8G for guix-patches@gnu.org; Mon, 06 Jan 2020 03:26:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1ioNi6-0002xv-2F for guix-patches@gnu.org; Mon, 06 Jan 2020 03:26:02 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#38965] [PATCH 01/12] gnu: Add ocaml-cairo2. References: <874kx9xa9u.fsf@gnu.org> In-Reply-To: <874kx9xa9u.fsf@gnu.org> Resent-From: Brett Gilio Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Mon, 06 Jan 2020 08:26:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 38965 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 38965@debbugs.gnu.org Received: via spool by 38965-submit@debbugs.gnu.org id=B38965.157829915211384 (code B ref 38965); Mon, 06 Jan 2020 08:26:02 +0000 Received: (at 38965) by debbugs.gnu.org; 6 Jan 2020 08:25:52 +0000 Received: from localhost ([127.0.0.1]:44938 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioNhw-0002xX-G2 for submit@debbugs.gnu.org; Mon, 06 Jan 2020 03:25:52 -0500 Received: from eggs.gnu.org ([209.51.188.92]:60769) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioNhu-0002xL-QJ for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:25:51 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]:50835) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1ioNhp-0001xn-Mh for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:25:45 -0500 Received: from [2605:6000:1a0d:4c95::3d] (port=48294 helo=oryx) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1ioNho-0005A4-Rj for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:25:45 -0500 From: Brett Gilio Date: Mon, 06 Jan 2020 02:25:52 -0600 Message-ID: <871rsdxa7j.fsf@gnu.org> MIME-Version: 1.0 Content-Disposition: inline; filename=0001-gnu-Add-ocaml-cairo2.patch Content-Description: [PATCH 01/12] gnu: Add ocaml-cairo2. X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 209.51.188.43 X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches From ce11c3d54c42f55a906a1457436f9486764f443e Mon Sep 17 00:00:00 2001 From: Brett Gilio 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(+) 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 From patchwork Mon Jan 6 08:26:41 2020 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Brett Gilio X-Patchwork-Id: 19610 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id 3F2D4179FE; Mon, 6 Jan 2020 08:27:15 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.0 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTP id EA5641798D for ; Mon, 6 Jan 2020 08:27:14 +0000 (GMT) Received: from localhost ([::1]:49320 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioNjG-0001Jx-D2 for patchwork@mira.cbaines.net; Mon, 06 Jan 2020 03:27:14 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:41881) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioNj9-0001Jl-Rk for guix-patches@gnu.org; Mon, 06 Jan 2020 03:27:08 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1ioNj5-0002yk-Gp for guix-patches@gnu.org; Mon, 06 Jan 2020 03:27:07 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:38972) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1ioNj3-0002xU-Rg for guix-patches@gnu.org; Mon, 06 Jan 2020 03:27:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1ioNj3-0002zv-Op for guix-patches@gnu.org; Mon, 06 Jan 2020 03:27:01 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#38965] [PATCH 02/12] gnu: Add ocaml-lablgtk3. References: <874kx9xa9u.fsf@gnu.org> In-Reply-To: <874kx9xa9u.fsf@gnu.org> Resent-From: Brett Gilio Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Mon, 06 Jan 2020 08:27:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 38965 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 38965@debbugs.gnu.org Received: via spool by 38965-submit@debbugs.gnu.org id=B38965.157829920311480 (code B ref 38965); Mon, 06 Jan 2020 08:27:01 +0000 Received: (at 38965) by debbugs.gnu.org; 6 Jan 2020 08:26:43 +0000 Received: from localhost ([127.0.0.1]:44942 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioNik-0002z6-Pm for submit@debbugs.gnu.org; Mon, 06 Jan 2020 03:26:43 -0500 Received: from eggs.gnu.org ([209.51.188.92]:60916) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioNij-0002yt-ID for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:26:41 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]:50841) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1ioNib-0002dD-52 for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:26:36 -0500 Received: from [2605:6000:1a0d:4c95::3d] (port=48298 helo=oryx) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1ioNia-0005HU-GC for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:26:32 -0500 From: Brett Gilio Date: Mon, 06 Jan 2020 02:26:41 -0600 Message-ID: <87y2ulvvlq.fsf@gnu.org> MIME-Version: 1.0 Content-Disposition: inline; filename=0002-gnu-Add-ocaml-lablgtk3.patch Content-Description: [PATCH 02/12] gnu: Add ocaml-lablgtk3. X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 209.51.188.43 X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches From 33425dcb8f66b7d7669c08a3f37f276087459717 Mon Sep 17 00:00:00 2001 From: Brett Gilio 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(+) 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 From patchwork Mon Jan 6 08:26:51 2020 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Brett Gilio X-Patchwork-Id: 19611 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id 97B3A179FE; Mon, 6 Jan 2020 08:27:15 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.0 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTP id 54FEF1798D for ; Mon, 6 Jan 2020 08:27:15 +0000 (GMT) Received: from localhost ([::1]:49322 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioNjG-0001KK-QC for patchwork@mira.cbaines.net; Mon, 06 Jan 2020 03:27:14 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:41879) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioNj9-0001Jk-RX for guix-patches@gnu.org; Mon, 06 Jan 2020 03:27:08 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1ioNj5-0002yp-Gy for guix-patches@gnu.org; Mon, 06 Jan 2020 03:27:07 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:38973) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1ioNj4-0002xk-7f for guix-patches@gnu.org; Mon, 06 Jan 2020 03:27:03 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1ioNj4-000302-4p for guix-patches@gnu.org; Mon, 06 Jan 2020 03:27:02 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#38965] [PATCH 03/12] gnu: coq: Update to 8.10.2. References: <874kx9xa9u.fsf@gnu.org> In-Reply-To: <874kx9xa9u.fsf@gnu.org> Resent-From: Brett Gilio Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Mon, 06 Jan 2020 08:27:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 38965 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 38965@debbugs.gnu.org Received: via spool by 38965-submit@debbugs.gnu.org id=B38965.157829921511507 (code B ref 38965); Mon, 06 Jan 2020 08:27:02 +0000 Received: (at 38965) by debbugs.gnu.org; 6 Jan 2020 08:26:55 +0000 Received: from localhost ([127.0.0.1]:44945 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioNix-0002zX-2M for submit@debbugs.gnu.org; Mon, 06 Jan 2020 03:26:55 -0500 Received: from eggs.gnu.org ([209.51.188.92]:60980) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioNit-0002zG-7y for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:26:53 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]:50843) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1ioNik-0002la-Sr for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:26:46 -0500 Received: from [2605:6000:1a0d:4c95::3d] (port=48302 helo=oryx) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1ioNik-0005JS-82 for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:26:42 -0500 From: Brett Gilio Date: Mon, 06 Jan 2020 02:26:51 -0600 Message-ID: <87v9ppvvlg.fsf@gnu.org> MIME-Version: 1.0 Content-Disposition: inline; filename=0003-gnu-coq-Update-to-8.10.2.patch Content-Description: [PATCH 03/12] gnu: coq: Update to 8.10.2. X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 209.51.188.43 X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches From 23e916aebde29a97a00d1813d007fb6475449548 Mon Sep 17 00:00:00 2001 From: Brett Gilio 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(-) 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 From patchwork Mon Jan 6 08:27:00 2020 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Brett Gilio X-Patchwork-Id: 19612 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id 2B42B179FE; Mon, 6 Jan 2020 08:28:12 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.0 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTP id D774D1798D for ; Mon, 6 Jan 2020 08:28:11 +0000 (GMT) Received: from localhost ([::1]:49334 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioNkA-0001Xe-RF for patchwork@mira.cbaines.net; Mon, 06 Jan 2020 03:28:10 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:42155) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioNk3-0001Vp-0H for guix-patches@gnu.org; Mon, 06 Jan 2020 03:28:04 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1ioNk1-0003dj-P7 for guix-patches@gnu.org; Mon, 06 Jan 2020 03:28:02 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:38992) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1ioNk1-0003df-MK for guix-patches@gnu.org; Mon, 06 Jan 2020 03:28:01 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1ioNk1-00032k-Jx for guix-patches@gnu.org; Mon, 06 Jan 2020 03:28:01 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#38965] [PATCH 04/12] gnu: coq: Reword several comments. References: <874kx9xa9u.fsf@gnu.org> In-Reply-To: <874kx9xa9u.fsf@gnu.org> Resent-From: Brett Gilio Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Mon, 06 Jan 2020 08:28:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 38965 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 38965@debbugs.gnu.org Received: via spool by 38965-submit@debbugs.gnu.org id=B38965.157829922511564 (code B ref 38965); Mon, 06 Jan 2020 08:28:01 +0000 Received: (at 38965) by debbugs.gnu.org; 6 Jan 2020 08:27:05 +0000 Received: from localhost ([127.0.0.1]:44950 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioNj7-00030S-BU for submit@debbugs.gnu.org; Mon, 06 Jan 2020 03:27:05 -0500 Received: from eggs.gnu.org ([209.51.188.92]:32790) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioNj5-0002zh-VT for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:27:04 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]:50845) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1ioNiz-0002vT-5e for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:26:58 -0500 Received: from [2605:6000:1a0d:4c95::3d] (port=48306 helo=oryx) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1ioNiu-0005dU-3u for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:26:52 -0500 From: Brett Gilio Date: Mon, 06 Jan 2020 02:27:00 -0600 Message-ID: <87sgktvvl7.fsf@gnu.org> MIME-Version: 1.0 Content-Disposition: inline; filename=0004-gnu-coq-Reword-several-comments.patch Content-Description: [PATCH 04/12] gnu: coq: Reword several comments. X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 209.51.188.43 X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches From 0a7b050f58b9f9a014e6512e0b12a0ed1e0f813b Mon Sep 17 00:00:00 2001 From: Brett Gilio 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(-) 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 From patchwork Mon Jan 6 08:27:15 2020 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Patchwork-Submitter: Brett Gilio X-Patchwork-Id: 19613 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id D523A179FE; Mon, 6 Jan 2020 08:28:14 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.0 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTP id 80F4E1798D for ; Mon, 6 Jan 2020 08:28:14 +0000 (GMT) Received: from localhost ([::1]:49338 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioNkD-0001ZL-I7 for patchwork@mira.cbaines.net; Mon, 06 Jan 2020 03:28:13 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:42163) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioNk3-0001Vr-EY for guix-patches@gnu.org; Mon, 06 Jan 2020 03:28:04 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1ioNk2-0003e6-5G for guix-patches@gnu.org; Mon, 06 Jan 2020 03:28:03 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:38993) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1ioNk2-0003dv-2U for guix-patches@gnu.org; Mon, 06 Jan 2020 03:28:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1ioNk2-00032r-0L for guix-patches@gnu.org; Mon, 06 Jan 2020 03:28:02 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#38965] [PATCH 05/12] gnu: coq-flocq: Update to 3.2.0. References: <874kx9xa9u.fsf@gnu.org> In-Reply-To: <874kx9xa9u.fsf@gnu.org> Resent-From: Brett Gilio Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Mon, 06 Jan 2020 08:28:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 38965 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 38965@debbugs.gnu.org Received: via spool by 38965-submit@debbugs.gnu.org id=B38965.157829923611589 (code B ref 38965); Mon, 06 Jan 2020 08:28:01 +0000 Received: (at 38965) by debbugs.gnu.org; 6 Jan 2020 08:27:16 +0000 Received: from localhost ([127.0.0.1]:44953 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioNjH-00030q-Ke for submit@debbugs.gnu.org; Mon, 06 Jan 2020 03:27:15 -0500 Received: from eggs.gnu.org ([209.51.188.92]:32842) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioNjG-00030f-Dm for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:27:15 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]:50847) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1ioNjB-00033F-9g for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:27:09 -0500 Received: from [2605:6000:1a0d:4c95::3d] (port=48310 helo=oryx) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1ioNj9-00069R-3I for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:27:08 -0500 From: Brett Gilio Date: Mon, 06 Jan 2020 02:27:15 -0600 Message-ID: <87pnfxvvks.fsf@gnu.org> MIME-Version: 1.0 Content-Disposition: inline; filename=0005-gnu-coq-flocq-Update-to-3.2.0.patch Content-Description: [PATCH 05/12] gnu: coq-flocq: Update to 3.2.0. X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 209.51.188.43 X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches From 241cfab94794ed4edcaaa338ba48b8292e5c6a0a Mon Sep 17 00:00:00 2001 From: Brett Gilio 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(-) 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 From patchwork Mon Jan 6 08:27:27 2020 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Brett Gilio X-Patchwork-Id: 19614 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id E3CD3179FE; Mon, 6 Jan 2020 08:28:15 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.0 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTP id A4C461798D for ; Mon, 6 Jan 2020 08:28:15 +0000 (GMT) Received: from localhost ([::1]:49342 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioNkE-0001bF-Ki for patchwork@mira.cbaines.net; Mon, 06 Jan 2020 03:28:14 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:42168) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioNk3-0001Vs-KQ for guix-patches@gnu.org; Mon, 06 Jan 2020 03:28:04 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1ioNk2-0003eK-HM for guix-patches@gnu.org; Mon, 06 Jan 2020 03:28:03 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:38994) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1ioNk2-0003eE-Eh for guix-patches@gnu.org; Mon, 06 Jan 2020 03:28:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1ioNk2-00032y-CT for guix-patches@gnu.org; Mon, 06 Jan 2020 03:28:02 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#38965] [PATCH 06/12] gnu: coq-flocq: Use HTTPS home page URI. References: <874kx9xa9u.fsf@gnu.org> In-Reply-To: <874kx9xa9u.fsf@gnu.org> Resent-From: Brett Gilio Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Mon, 06 Jan 2020 08:28:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 38965 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 38965@debbugs.gnu.org Received: via spool by 38965-submit@debbugs.gnu.org id=B38965.157829924911617 (code B ref 38965); Mon, 06 Jan 2020 08:28:02 +0000 Received: (at 38965) by debbugs.gnu.org; 6 Jan 2020 08:27:29 +0000 Received: from localhost ([127.0.0.1]:44956 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioNjU-00031I-Uq for submit@debbugs.gnu.org; Mon, 06 Jan 2020 03:27:29 -0500 Received: from eggs.gnu.org ([209.51.188.92]:32939) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioNjT-000314-0y for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:27:27 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]:50858) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1ioNjN-0003Dm-2j for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:27:21 -0500 Received: from [2605:6000:1a0d:4c95::3d] (port=48314 helo=oryx) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1ioNjK-0006Hs-Rr for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:27:19 -0500 From: Brett Gilio Date: Mon, 06 Jan 2020 02:27:27 -0600 Message-ID: <87mub1vvkg.fsf@gnu.org> MIME-Version: 1.0 Content-Disposition: inline; filename=0006-gnu-coq-flocq-Use-HTTPS-home-page-URI.patch Content-Description: [PATCH 06/12] gnu: coq-flocq: Use HTTPS home page URI. X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 209.51.188.43 X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches From a725c0c6f8889105354c26f8dc1125bb90467d55 Mon Sep 17 00:00:00 2001 From: Brett Gilio 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(-) 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 From patchwork Mon Jan 6 08:27:39 2020 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Brett Gilio X-Patchwork-Id: 19617 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id 72C07179FE; Mon, 6 Jan 2020 08:28:36 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.0 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTP id 2BE8C1798D for ; Mon, 6 Jan 2020 08:28:36 +0000 (GMT) Received: from localhost ([::1]:49354 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioNkZ-0002C5-La for patchwork@mira.cbaines.net; Mon, 06 Jan 2020 03:28:35 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:42193) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioNk4-0001WL-7l for guix-patches@gnu.org; Mon, 06 Jan 2020 03:28:05 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1ioNk2-0003ee-US for guix-patches@gnu.org; Mon, 06 Jan 2020 03:28:04 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:38995) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1ioNk2-0003eW-RQ for guix-patches@gnu.org; Mon, 06 Jan 2020 03:28:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1ioNk2-000336-P3 for guix-patches@gnu.org; Mon, 06 Jan 2020 03:28:02 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#38965] [PATCH 07/12] gnu: coq-gappa: Update to 1.4.2. References: <874kx9xa9u.fsf@gnu.org> In-Reply-To: <874kx9xa9u.fsf@gnu.org> Resent-From: Brett Gilio Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Mon, 06 Jan 2020 08:28:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 38965 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 38965@debbugs.gnu.org Received: via spool by 38965-submit@debbugs.gnu.org id=B38965.157829926111643 (code B ref 38965); Mon, 06 Jan 2020 08:28:02 +0000 Received: (at 38965) by debbugs.gnu.org; 6 Jan 2020 08:27:41 +0000 Received: from localhost ([127.0.0.1]:44959 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioNjh-00031h-74 for submit@debbugs.gnu.org; Mon, 06 Jan 2020 03:27:41 -0500 Received: from eggs.gnu.org ([209.51.188.92]:32990) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioNjf-00031V-OR for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:27:40 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]:50865) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1ioNja-0003N4-KI for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:27:34 -0500 Received: from [2605:6000:1a0d:4c95::3d] (port=48318 helo=oryx) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1ioNjW-0006VM-Kk for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:27:33 -0500 From: Brett Gilio Date: Mon, 06 Jan 2020 02:27:39 -0600 Message-ID: <87k165vvk4.fsf@gnu.org> MIME-Version: 1.0 Content-Disposition: inline; filename=0007-gnu-coq-gappa-Update-to-1.4.2.patch Content-Description: [PATCH 07/12] gnu: coq-gappa: Update to 1.4.2. X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 209.51.188.43 X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches From 49a03cd326f8cdb26fdb07b7d931d8b9560d69ab Mon Sep 17 00:00:00 2001 From: Brett Gilio 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(-) 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 From patchwork Mon Jan 6 08:27:52 2020 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Brett Gilio X-Patchwork-Id: 19615 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id E3881179FE; Mon, 6 Jan 2020 08:28:21 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.0 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTP id A70941798D for ; Mon, 6 Jan 2020 08:28:21 +0000 (GMT) Received: from localhost ([::1]:49344 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioNkK-0001ne-SR for patchwork@mira.cbaines.net; Mon, 06 Jan 2020 03:28:20 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:42200) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioNk4-0001XV-LD for guix-patches@gnu.org; Mon, 06 Jan 2020 03:28:05 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1ioNk3-0003fE-E4 for guix-patches@gnu.org; Mon, 06 Jan 2020 03:28:04 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:38996) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1ioNk3-0003ew-8x for guix-patches@gnu.org; Mon, 06 Jan 2020 03:28:03 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1ioNk3-00033D-5n for guix-patches@gnu.org; Mon, 06 Jan 2020 03:28:03 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#38965] [PATCH 08/12] gnu: coq-gappa: Use HTTPS home page URI. References: <874kx9xa9u.fsf@gnu.org> In-Reply-To: <874kx9xa9u.fsf@gnu.org> Resent-From: Brett Gilio Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Mon, 06 Jan 2020 08:28:03 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 38965 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 38965@debbugs.gnu.org Received: via spool by 38965-submit@debbugs.gnu.org id=B38965.157829927111669 (code B ref 38965); Mon, 06 Jan 2020 08:28:03 +0000 Received: (at 38965) by debbugs.gnu.org; 6 Jan 2020 08:27:51 +0000 Received: from localhost ([127.0.0.1]:44962 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioNjr-000329-GQ for submit@debbugs.gnu.org; Mon, 06 Jan 2020 03:27:51 -0500 Received: from eggs.gnu.org ([209.51.188.92]:33014) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioNjp-00031s-Jo for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:27:49 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]:50866) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1ioNjk-0003VD-GY for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:27:44 -0500 Received: from [2605:6000:1a0d:4c95::3d] (port=48322 helo=oryx) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1ioNjj-0006m5-D8 for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:27:44 -0500 From: Brett Gilio Date: Mon, 06 Jan 2020 02:27:52 -0600 Message-ID: <87h819vvjr.fsf@gnu.org> MIME-Version: 1.0 Content-Disposition: inline; filename=0008-gnu-coq-gappa-Use-HTTPS-home-page-URI.patch Content-Description: [PATCH 08/12] gnu: coq-gappa: Use HTTPS home page URI. X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 209.51.188.43 X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches From 0cb2f1f9f5a15cdebf3c5c69a8970a14b86e7d1f Mon Sep 17 00:00:00 2001 From: Brett Gilio 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(-) 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 From patchwork Mon Jan 6 08:28:02 2020 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Brett Gilio X-Patchwork-Id: 19616 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id F3D85179FE; Mon, 6 Jan 2020 08:28:24 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.0 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTP id AEAC41798D for ; Mon, 6 Jan 2020 08:28:24 +0000 (GMT) Received: from localhost ([::1]:49348 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioNkO-0001tP-5D for patchwork@mira.cbaines.net; Mon, 06 Jan 2020 03:28:24 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:42204) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioNk4-0001Xq-W8 for guix-patches@gnu.org; Mon, 06 Jan 2020 03:28:06 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1ioNk3-0003fb-Pk for guix-patches@gnu.org; Mon, 06 Jan 2020 03:28:04 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:38997) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1ioNk3-0003fR-Mx for guix-patches@gnu.org; Mon, 06 Jan 2020 03:28:03 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1ioNk3-00033K-KO for guix-patches@gnu.org; Mon, 06 Jan 2020 03:28:03 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#38965] [PATCH 09/12] gnu: coq-coquelicot: Update to 3.0.3. References: <874kx9xa9u.fsf@gnu.org> In-Reply-To: <874kx9xa9u.fsf@gnu.org> Resent-From: Brett Gilio Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Mon, 06 Jan 2020 08:28:03 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 38965 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 38965@debbugs.gnu.org Received: via spool by 38965-submit@debbugs.gnu.org id=B38965.157829928111694 (code B ref 38965); Mon, 06 Jan 2020 08:28:03 +0000 Received: (at 38965) by debbugs.gnu.org; 6 Jan 2020 08:28:01 +0000 Received: from localhost ([127.0.0.1]:44965 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioNk0-00032V-Pi for submit@debbugs.gnu.org; Mon, 06 Jan 2020 03:28:01 -0500 Received: from eggs.gnu.org ([209.51.188.92]:33045) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioNjz-00032J-Hz for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:27:59 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]:50867) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1ioNju-0003Zr-EB for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:27:54 -0500 Received: from [2605:6000:1a0d:4c95::3d] (port=48326 helo=oryx) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1ioNjt-0006vm-BD for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:27:53 -0500 From: Brett Gilio Date: Mon, 06 Jan 2020 02:28:02 -0600 Message-ID: <87eewdvvjh.fsf@gnu.org> MIME-Version: 1.0 Content-Disposition: inline; filename=0009-gnu-coq-coquelicot-Update-to-3.0.3.patch Content-Description: [PATCH 09/12] gnu: coq-coquelicot: Update to 3.0.3. X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 209.51.188.43 X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches From 766d25903c01cece3e88eaec2f1cbe28b322cdae Mon Sep 17 00:00:00 2001 From: Brett Gilio 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(-) 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 From patchwork Mon Jan 6 08:28:12 2020 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Brett Gilio X-Patchwork-Id: 19618 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id CCD97179FE; Mon, 6 Jan 2020 08:29:11 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.0 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTP id 8C93F1798D for ; Mon, 6 Jan 2020 08:29:11 +0000 (GMT) Received: from localhost ([::1]:49356 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioNl8-0002Jo-NS for patchwork@mira.cbaines.net; Mon, 06 Jan 2020 03:29:10 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:42409) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioNl2-0002IR-4n for guix-patches@gnu.org; Mon, 06 Jan 2020 03:29:05 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1ioNl0-0004Oi-64 for guix-patches@gnu.org; Mon, 06 Jan 2020 03:29:04 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:39007) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1ioNl0-0004Od-3R for guix-patches@gnu.org; Mon, 06 Jan 2020 03:29:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1ioNl0-00035K-0n for guix-patches@gnu.org; Mon, 06 Jan 2020 03:29:02 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#38965] [PATCH 10/12] gnu: coq-coquelicot: Truncate home-page. References: <874kx9xa9u.fsf@gnu.org> In-Reply-To: <874kx9xa9u.fsf@gnu.org> Resent-From: Brett Gilio Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Mon, 06 Jan 2020 08:29:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 38965 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 38965@debbugs.gnu.org Received: via spool by 38965-submit@debbugs.gnu.org id=B38965.157829929311775 (code B ref 38965); Mon, 06 Jan 2020 08:29:01 +0000 Received: (at 38965) by debbugs.gnu.org; 6 Jan 2020 08:28:13 +0000 Received: from localhost ([127.0.0.1]:44974 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioNkD-00033r-26 for submit@debbugs.gnu.org; Mon, 06 Jan 2020 03:28:13 -0500 Received: from eggs.gnu.org ([209.51.188.92]:33158) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioNkB-00033f-7m for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:28:11 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]:50868) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1ioNk6-0003iS-43 for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:28:06 -0500 Received: from [2605:6000:1a0d:4c95::3d] (port=48330 helo=oryx) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1ioNk4-0007DD-7P for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:28:05 -0500 From: Brett Gilio Date: Mon, 06 Jan 2020 02:28:12 -0600 Message-ID: <87blrhvvj7.fsf@gnu.org> MIME-Version: 1.0 Content-Disposition: inline; filename=0010-gnu-coq-coquelicot-Truncate-home-page.patch Content-Description: [PATCH 10/12] gnu: coq-coquelicot: Truncate home-page. X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 209.51.188.43 X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches From e292512deb9c9c30bb2dffa9bf405c8a9aea66f7 Mon Sep 17 00:00:00 2001 From: Brett Gilio 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(-) 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 From patchwork Mon Jan 6 08:28:23 2020 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Brett Gilio X-Patchwork-Id: 19620 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id 3641E179FE; Mon, 6 Jan 2020 08:29:18 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.0 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTP id E06871798D for ; Mon, 6 Jan 2020 08:29:17 +0000 (GMT) Received: from localhost ([::1]:49362 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioNlF-0002Mw-El for patchwork@mira.cbaines.net; Mon, 06 Jan 2020 03:29:17 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:42419) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioNl2-0002Jh-NF for guix-patches@gnu.org; Mon, 06 Jan 2020 03:29:05 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1ioNl0-0004Pg-Ks for guix-patches@gnu.org; Mon, 06 Jan 2020 03:29:04 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:39008) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1ioNl0-0004P9-Hz for guix-patches@gnu.org; Mon, 06 Jan 2020 03:29:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1ioNl0-00035S-Eh for guix-patches@gnu.org; Mon, 06 Jan 2020 03:29:02 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#38965] [PATCH 11/12] gnu: coq-interval: Update to 3.4.1. References: <874kx9xa9u.fsf@gnu.org> In-Reply-To: <874kx9xa9u.fsf@gnu.org> Resent-From: Brett Gilio Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Mon, 06 Jan 2020 08:29:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 38965 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 38965@debbugs.gnu.org Received: via spool by 38965-submit@debbugs.gnu.org id=B38965.157829930511802 (code B ref 38965); Mon, 06 Jan 2020 08:29:02 +0000 Received: (at 38965) by debbugs.gnu.org; 6 Jan 2020 08:28:25 +0000 Received: from localhost ([127.0.0.1]:44977 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioNkP-00034I-Ai for submit@debbugs.gnu.org; Mon, 06 Jan 2020 03:28:25 -0500 Received: from eggs.gnu.org ([209.51.188.92]:33212) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioNkN-000344-Vf for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:28:24 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]:50877) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1ioNkI-0003s9-RP for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:28:18 -0500 Received: from [2605:6000:1a0d:4c95::3d] (port=48334 helo=oryx) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1ioNkF-0007Pr-31 for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:28:15 -0500 From: Brett Gilio Date: Mon, 06 Jan 2020 02:28:23 -0600 Message-ID: <878smlvviw.fsf@gnu.org> MIME-Version: 1.0 Content-Disposition: inline; filename=0011-gnu-coq-interval-Update-to-3.4.1.patch Content-Description: [PATCH 11/12] gnu: coq-interval: Update to 3.4.1. X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 209.51.188.43 X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches From a846a0ecb584c8f76e366db33a720ab68f6df0d7 Mon Sep 17 00:00:00 2001 From: Brett Gilio 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(-) 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 From patchwork Mon Jan 6 08:28:35 2020 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Brett Gilio X-Patchwork-Id: 19619 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id B215C179FE; Mon, 6 Jan 2020 08:29:17 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.0 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTP id 5636F179FC for ; Mon, 6 Jan 2020 08:29:17 +0000 (GMT) Received: from localhost ([::1]:49358 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioNlE-0002MA-Rv for patchwork@mira.cbaines.net; Mon, 06 Jan 2020 03:29:16 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:42428) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioNl3-0002Jk-84 for guix-patches@gnu.org; Mon, 06 Jan 2020 03:29:06 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1ioNl2-0004RU-2k for guix-patches@gnu.org; Mon, 06 Jan 2020 03:29:05 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:39009) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1ioNl1-0004Ql-Vq for guix-patches@gnu.org; Mon, 06 Jan 2020 03:29:04 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1ioNl0-00035a-TO for guix-patches@gnu.org; Mon, 06 Jan 2020 03:29:02 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#38965] [PATCH 12/12] gnu: coq-equations: Update to 1.2.1. References: <874kx9xa9u.fsf@gnu.org> In-Reply-To: <874kx9xa9u.fsf@gnu.org> Resent-From: Brett Gilio Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Mon, 06 Jan 2020 08:29:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 38965 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 38965@debbugs.gnu.org Received: via spool by 38965-submit@debbugs.gnu.org id=B38965.157829931711827 (code B ref 38965); Mon, 06 Jan 2020 08:29:02 +0000 Received: (at 38965) by debbugs.gnu.org; 6 Jan 2020 08:28:37 +0000 Received: from localhost ([127.0.0.1]:44980 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioNkb-00034h-L2 for submit@debbugs.gnu.org; Mon, 06 Jan 2020 03:28:37 -0500 Received: from eggs.gnu.org ([209.51.188.92]:33258) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioNkZ-00034V-Hs for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:28:35 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]:50885) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1ioNkU-0003y9-Dz for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:28:30 -0500 Received: from [2605:6000:1a0d:4c95::3d] (port=48338 helo=oryx) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1ioNkR-0007VL-97 for 38965@debbugs.gnu.org; Mon, 06 Jan 2020 03:28:28 -0500 From: Brett Gilio Date: Mon, 06 Jan 2020 02:28:35 -0600 Message-ID: <875zhpvvik.fsf@gnu.org> MIME-Version: 1.0 Content-Disposition: inline; filename=0012-gnu-coq-equations-Update-to-1.2.1.patch Content-Description: [PATCH 12/12] gnu: coq-equations: Update to 1.2.1. X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 209.51.188.43 X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches From 89b5acd77c520c2cf72c0dda28bd1a1c0ea97e55 Mon Sep 17 00:00:00 2001 From: Brett Gilio 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(-) 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