From unknown Mon Jun 23 16:46:11 2025 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-Mailer: MIME-tools 5.509 (Entity 5.509) Content-Type: text/plain; charset=utf-8 From: bug#28925 <28925@debbugs.gnu.org> To: bug#28925 <28925@debbugs.gnu.org> Subject: Status: [PATCH] Update coq and coq libraries. Reply-To: bug#28925 <28925@debbugs.gnu.org> Date: Mon, 23 Jun 2025 23:46:11 +0000 retitle 28925 [PATCH] Update coq and coq libraries. reassign 28925 guix-patches submitter 28925 Julien Lepiller severity 28925 normal tag 28925 patch thanks From debbugs-submit-bounces@debbugs.gnu.org Sat Oct 21 12:18:43 2017 Received: (at submit) by debbugs.gnu.org; 21 Oct 2017 16:18:43 +0000 Received: from localhost ([127.0.0.1]:54471 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1e5wTz-0002tU-B9 for submit@debbugs.gnu.org; Sat, 21 Oct 2017 12:18:43 -0400 Received: from eggs.gnu.org ([208.118.235.92]:35860) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1e5wTx-0002tH-SG for submit@debbugs.gnu.org; Sat, 21 Oct 2017 12:18:42 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1e5wTs-00013f-7g for submit@debbugs.gnu.org; Sat, 21 Oct 2017 12:18:36 -0400 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=disabled version=3.3.2 Received: from lists.gnu.org ([2001:4830:134:3::11]:37832) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1e5wTs-00013Z-4e for submit@debbugs.gnu.org; Sat, 21 Oct 2017 12:18:36 -0400 Received: from eggs.gnu.org ([2001:4830:134:3::10]:55056) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1e5wTr-0007NZ-6c for guix-patches@gnu.org; Sat, 21 Oct 2017 12:18:35 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1e5wTm-00010P-A6 for guix-patches@gnu.org; Sat, 21 Oct 2017 12:18:35 -0400 Received: from lepiller.eu ([2a00:5884:8208::1]:60040) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1e5wTl-0000zj-Ve for guix-patches@gnu.org; Sat, 21 Oct 2017 12:18:30 -0400 Received: from localhost (static-176-182-42-79.ncc.abo.bbox.fr [176.182.42.79]) by lepiller.eu (OpenSMTPD) with ESMTPSA id 78626fe9 (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO) for ; Sat, 21 Oct 2017 16:19:43 +0000 (UTC) Date: Sat, 21 Oct 2017 18:16:38 +0200 From: Julien Lepiller To: guix-patches@gnu.org Subject: [PATCH] Update coq and coq libraries. Message-ID: <20171021181638.27d0d0d8@lepiller.eu> X-Mailer: Claws Mail 3.15.1-dirty (GTK+ 2.24.31; x86_64-unknown-linux-gnu) MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit X-detected-operating-system: by eggs.gnu.org: Genre and OS details not recognized. X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.6.x X-Received-From: 2001:4830:134:3::11 X-Spam-Score: -4.0 (----) X-Debbugs-Envelope-To: submit X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -4.0 (----) Hi, this patch series updates coq and its libraries. From debbugs-submit-bounces@debbugs.gnu.org Sat Oct 21 12:22:51 2017 Received: (at 28925) by debbugs.gnu.org; 21 Oct 2017 16:22:51 +0000 Received: from localhost ([127.0.0.1]:54477 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1e5wXy-00030L-US for submit@debbugs.gnu.org; Sat, 21 Oct 2017 12:22:51 -0400 Received: from lepiller.eu ([89.234.186.109]:55360) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1e5wXx-000308-8l for 28925@debbugs.gnu.org; Sat, 21 Oct 2017 12:22:49 -0400 Received: from localhost.localdomain (static-176-182-42-79.ncc.abo.bbox.fr [176.182.42.79]) by lepiller.eu (OpenSMTPD) with ESMTPSA id b39d5075 (TLSv1.2:ECDHE-RSA-AES128-GCM-SHA256:128:NO); Sat, 21 Oct 2017 16:24:04 +0000 (UTC) From: julien@lepiller.eu To: 28925@debbugs.gnu.org Subject: [PATCH 1/7] gnu: camlp5: install META file. Date: Sat, 21 Oct 2017 18:20:51 +0200 Message-Id: <20171021162058.27938-1-julien@lepiller.eu> X-Mailer: git-send-email 2.14.2 In-Reply-To: <20171021181638.27d0d0d8@lepiller.eu> References: <20171021181638.27d0d0d8@lepiller.eu> X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 28925 Cc: Julien Lepiller X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.0 (/) From: Julien Lepiller * gnu/packages/ocaml.scm (camlp5) [phases]: New install-meta phase. --- gnu/packages/ocaml.scm | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index aa2f00667..40d42a5d4 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -401,7 +401,12 @@ syntax of OCaml.") (lambda _ (zero? (system* "make" "-j" (number->string (parallel-job-count)) - "world.opt"))))))) + "world.opt")))) + ;; Required for findlib to find camlp5's libraries + (add-after 'install 'install-meta + (lambda* (#:key outputs #:allow-other-keys) + (install-file "etc/META" (string-append (assoc-ref outputs "out") + "/lib/ocaml/camlp5/"))))))) (home-page "http://camlp5.gforge.inria.fr/") (synopsis "Pre-processor Pretty Printer for OCaml") (description -- 2.14.2 From debbugs-submit-bounces@debbugs.gnu.org Sat Oct 21 12:22:54 2017 Received: (at 28925) by debbugs.gnu.org; 21 Oct 2017 16:22:54 +0000 Received: from localhost ([127.0.0.1]:54483 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1e5wY2-00030q-5t for submit@debbugs.gnu.org; Sat, 21 Oct 2017 12:22:54 -0400 Received: from lepiller.eu ([89.234.186.109]:55360) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1e5wXy-000308-8l for 28925@debbugs.gnu.org; Sat, 21 Oct 2017 12:22:50 -0400 Received: from localhost.localdomain (static-176-182-42-79.ncc.abo.bbox.fr [176.182.42.79]) by lepiller.eu (OpenSMTPD) with ESMTPSA id 819ae9c7 (TLSv1.2:ECDHE-RSA-AES128-GCM-SHA256:128:NO); Sat, 21 Oct 2017 16:24:04 +0000 (UTC) From: julien@lepiller.eu To: 28925@debbugs.gnu.org Subject: [PATCH] gnu: youtube-dl: Update to 2017.10.20. Date: Sat, 21 Oct 2017 18:20:52 +0200 Message-Id: <20171021162058.27938-2-julien@lepiller.eu> X-Mailer: git-send-email 2.14.2 In-Reply-To: <20171021162058.27938-1-julien@lepiller.eu> References: <20171021181638.27d0d0d8@lepiller.eu> <20171021162058.27938-1-julien@lepiller.eu> X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 28925 Cc: Tobias Geerinckx-Rice X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.0 (/) From: Tobias Geerinckx-Rice * gnu/packages/video.scm (youtube-dl): Update to 2017.10.20. --- gnu/packages/ocaml.scm | 22 +++++++++++++++------- gnu/packages/video.scm | 4 ++-- 2 files changed, 17 insertions(+), 9 deletions(-) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index aa2f00667..8292ece2e 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -401,7 +401,11 @@ syntax of OCaml.") (lambda _ (zero? (system* "make" "-j" (number->string (parallel-job-count)) - "world.opt"))))))) + "world.opt")))) + (add-after 'install 'install-meta + (lambda* (#:key outputs #:allow-other-keys) + (install-file "etc/META" (string-append (assoc-ref outputs "out") + "/lib/ocaml/camlp5/"))))))) (home-page "http://camlp5.gforge.inria.fr/") (synopsis "Pre-processor Pretty Printer for OCaml") (description @@ -445,26 +449,25 @@ written in Objective Caml.") (define-public coq (package (name "coq") - (version "8.5pl2") + (version "8.7.0") (source (origin (method url-fetch) (uri (string-append "https://coq.inria.fr/distrib/V" version "/files/" name "-" version ".tar.gz")) (sha256 (base32 - "0wyywia0darak2zmc5v0ra9rn0b9whwdfiahralm8v5za499s8w3")))) + "15wjngjd5pyfqdl5yw92rvdxvy15xcjlpx0rqlkzvcsis1z20xpk")))) (native-search-paths (list (search-path-specification (variable "COQPATH") (files (list "lib/coq/user-contrib"))))) - (build-system gnu-build-system) + (build-system ocaml-build-system) (native-inputs `(("texlive" ,texlive) - ("findlib" ,ocaml-findlib) ("hevea" ,hevea))) (inputs - `(("ocaml" ,ocaml) - ("lablgtk" ,lablgtk) + `(("lablgtk" ,lablgtk) + ("python" ,python-2) ("camlp5" ,camlp5))) (arguments `(#:phases @@ -488,6 +491,11 @@ written in Objective Caml.") (add-after 'install 'check (lambda _ (with-directory-excursion "test-suite" + ;; These two tests fail. + ;; This one 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. + (delete-file-recursively "coq-makefile/findlib-package") (zero? (system* "make")))))))) (home-page "https://coq.inria.fr") (synopsis "Proof assistant for higher-order logic") diff --git a/gnu/packages/video.scm b/gnu/packages/video.scm index 43e4fc2eb..63824f6c5 100644 --- a/gnu/packages/video.scm +++ b/gnu/packages/video.scm @@ -1116,7 +1116,7 @@ access to mpv's powerful playback capabilities.") (define-public youtube-dl (package (name "youtube-dl") - (version "2017.10.15.1") + (version "2017.10.20") (source (origin (method url-fetch) (uri (string-append "https://yt-dl.org/downloads/" @@ -1124,7 +1124,7 @@ access to mpv's powerful playback capabilities.") version ".tar.gz")) (sha256 (base32 - "0zr9sx0nxk36si8xbvhlnazb69xzlygrhsxcyiydm0dy5y5ycsns")))) + "0npr8b1xg1dylz717kfllw433h1y16251npzch48lchq69bhm4iy")))) (build-system python-build-system) (arguments ;; The problem here is that the directory for the man page and completion -- 2.14.2 From debbugs-submit-bounces@debbugs.gnu.org Sat Oct 21 12:22:55 2017 Received: (at 28925) by debbugs.gnu.org; 21 Oct 2017 16:22:55 +0000 Received: from localhost ([127.0.0.1]:54487 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1e5wY2-00030t-HA for submit@debbugs.gnu.org; Sat, 21 Oct 2017 12:22:55 -0400 Received: from lepiller.eu ([89.234.186.109]:55360) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1e5wXz-000308-4o for 28925@debbugs.gnu.org; Sat, 21 Oct 2017 12:22:51 -0400 Received: from localhost.localdomain (static-176-182-42-79.ncc.abo.bbox.fr [176.182.42.79]) by lepiller.eu (OpenSMTPD) with ESMTPSA id ca56a25d (TLSv1.2:ECDHE-RSA-AES128-GCM-SHA256:128:NO); Sat, 21 Oct 2017 16:24:04 +0000 (UTC) From: julien@lepiller.eu To: 28925@debbugs.gnu.org Subject: [PATCH 2/7] gnu: Update coq to 8.7.0. Date: Sat, 21 Oct 2017 18:20:53 +0200 Message-Id: <20171021162058.27938-3-julien@lepiller.eu> X-Mailer: git-send-email 2.14.2 In-Reply-To: <20171021162058.27938-1-julien@lepiller.eu> References: <20171021181638.27d0d0d8@lepiller.eu> <20171021162058.27938-1-julien@lepiller.eu> X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 28925 Cc: Julien Lepiller X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.0 (/) From: Julien Lepiller * gnu/packages/ocaml.scm (coq): Update to 8.7.0. --- gnu/packages/ocaml.scm | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index 40d42a5d4..bbdde2801 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -450,26 +450,25 @@ written in Objective Caml.") (define-public coq (package (name "coq") - (version "8.5pl2") + (version "8.7.0") (source (origin (method url-fetch) (uri (string-append "https://coq.inria.fr/distrib/V" version "/files/" name "-" version ".tar.gz")) (sha256 (base32 - "0wyywia0darak2zmc5v0ra9rn0b9whwdfiahralm8v5za499s8w3")))) + "15wjngjd5pyfqdl5yw92rvdxvy15xcjlpx0rqlkzvcsis1z20xpk")))) (native-search-paths (list (search-path-specification (variable "COQPATH") (files (list "lib/coq/user-contrib"))))) - (build-system gnu-build-system) + (build-system ocaml-build-system) (native-inputs `(("texlive" ,texlive) - ("findlib" ,ocaml-findlib) ("hevea" ,hevea))) (inputs - `(("ocaml" ,ocaml) - ("lablgtk" ,lablgtk) + `(("lablgtk" ,lablgtk) + ("python" ,python-2) ("camlp5" ,camlp5))) (arguments `(#:phases @@ -493,6 +492,11 @@ written in Objective Caml.") (add-after 'install 'check (lambda _ (with-directory-excursion "test-suite" + ;; These two tests fail. + ;; This one 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. + (delete-file-recursively "coq-makefile/findlib-package") (zero? (system* "make")))))))) (home-page "https://coq.inria.fr") (synopsis "Proof assistant for higher-order logic") -- 2.14.2 From debbugs-submit-bounces@debbugs.gnu.org Sat Oct 21 12:22:55 2017 Received: (at 28925) by debbugs.gnu.org; 21 Oct 2017 16:22:55 +0000 Received: from localhost ([127.0.0.1]:54489 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1e5wY3-00031C-4m for submit@debbugs.gnu.org; Sat, 21 Oct 2017 12:22:55 -0400 Received: from lepiller.eu ([89.234.186.109]:55360) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1e5wXz-000308-RI for 28925@debbugs.gnu.org; Sat, 21 Oct 2017 12:22:52 -0400 Received: from localhost.localdomain (static-176-182-42-79.ncc.abo.bbox.fr [176.182.42.79]) by lepiller.eu (OpenSMTPD) with ESMTPSA id 39d423ef (TLSv1.2:ECDHE-RSA-AES128-GCM-SHA256:128:NO); Sat, 21 Oct 2017 16:24:04 +0000 (UTC) From: julien@lepiller.eu To: 28925@debbugs.gnu.org Subject: [PATCH 3/7] gnu: Update coq-flocq to 2.6.0. Date: Sat, 21 Oct 2017 18:20:54 +0200 Message-Id: <20171021162058.27938-4-julien@lepiller.eu> X-Mailer: git-send-email 2.14.2 In-Reply-To: <20171021162058.27938-1-julien@lepiller.eu> References: <20171021181638.27d0d0d8@lepiller.eu> <20171021162058.27938-1-julien@lepiller.eu> X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 28925 Cc: Julien Lepiller X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.0 (/) From: Julien Lepiller * gnu/packages/ocaml.scm (coq-flocq): Update to 2.6.0. --- gnu/packages/ocaml.scm | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index bbdde2801..f2b06d065 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -3560,14 +3560,14 @@ library is currently designed for Unicode Standard 3.2.") (define-public coq-flocq (package (name "coq-flocq") - (version "2.5.2") + (version "2.6.0") (source (origin (method url-fetch) (uri (string-append "https://gforge.inria.fr/frs/download.php/file" - "/36199/flocq-" version ".tar.gz")) + "/37054/flocq-" version ".tar.gz")) (sha256 (base32 - "0h5mlasirfzc0wwn2isg4kahk384n73145akkpinrxq5jsn5d22h")))) + "13fv150dcwnjrk00d7zj2c5x9jwmxgrq0ay440gkr730l8mvk3l3")))) (build-system gnu-build-system) (native-inputs `(("ocaml" ,ocaml) -- 2.14.2 From debbugs-submit-bounces@debbugs.gnu.org Sat Oct 21 12:22:55 2017 Received: (at 28925) by debbugs.gnu.org; 21 Oct 2017 16:22:55 +0000 Received: from localhost ([127.0.0.1]:54491 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1e5wY3-00031J-EK for submit@debbugs.gnu.org; Sat, 21 Oct 2017 12:22:55 -0400 Received: from lepiller.eu ([89.234.186.109]:55360) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1e5wY0-000308-K2 for 28925@debbugs.gnu.org; Sat, 21 Oct 2017 12:22:53 -0400 Received: from localhost.localdomain (static-176-182-42-79.ncc.abo.bbox.fr [176.182.42.79]) by lepiller.eu (OpenSMTPD) with ESMTPSA id ecfef18c (TLSv1.2:ECDHE-RSA-AES128-GCM-SHA256:128:NO); Sat, 21 Oct 2017 16:24:04 +0000 (UTC) From: julien@lepiller.eu To: 28925@debbugs.gnu.org Subject: [PATCH 4/7] gnu: Update coq-mathcomp to 1.6.2. Date: Sat, 21 Oct 2017 18:20:55 +0200 Message-Id: <20171021162058.27938-5-julien@lepiller.eu> X-Mailer: git-send-email 2.14.2 In-Reply-To: <20171021162058.27938-1-julien@lepiller.eu> References: <20171021181638.27d0d0d8@lepiller.eu> <20171021162058.27938-1-julien@lepiller.eu> X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 28925 Cc: Julien Lepiller X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.0 (/) From: Julien Lepiller * gnu/packages/ocaml.scm (coq-mathcomp): Update to 1..6.2. --- gnu/packages/ocaml.scm | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index f2b06d065..beb73a2d0 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -3657,14 +3657,14 @@ assistant.") (define-public coq-mathcomp (package (name "coq-mathcomp") - (version "1.6.1") + (version "1.6.2") (source (origin (method url-fetch) (uri (string-append "https://github.com/math-comp/math-comp/archive/mathcomp-" version ".tar.gz")) (sha256 (base32 - "1j9ylggjzrxz1i2hdl2yhsvmvy5z6l4rprwx7604401080p5sgjw")))) + "0lg5ncr7p4y8qqq6pfw6brqc6a9xzlfa0drprwfdn0rnyaq5nca6")))) (build-system gnu-build-system) (native-inputs `(("ocaml" ,ocaml) -- 2.14.2 From debbugs-submit-bounces@debbugs.gnu.org Sat Oct 21 12:23:02 2017 Received: (at 28925) by debbugs.gnu.org; 21 Oct 2017 16:23:02 +0000 Received: from localhost ([127.0.0.1]:54493 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1e5wY9-00031h-OQ for submit@debbugs.gnu.org; Sat, 21 Oct 2017 12:23:02 -0400 Received: from lepiller.eu ([89.234.186.109]:55360) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1e5wY1-000308-FW for 28925@debbugs.gnu.org; Sat, 21 Oct 2017 12:22:53 -0400 Received: from localhost.localdomain (static-176-182-42-79.ncc.abo.bbox.fr [176.182.42.79]) by lepiller.eu (OpenSMTPD) with ESMTPSA id 86574db1 (TLSv1.2:ECDHE-RSA-AES128-GCM-SHA256:128:NO); Sat, 21 Oct 2017 16:24:05 +0000 (UTC) From: julien@lepiller.eu To: 28925@debbugs.gnu.org Subject: [PATCH 5/7] gnu: Update coq-coquelicot to 3.0.1. Date: Sat, 21 Oct 2017 18:20:56 +0200 Message-Id: <20171021162058.27938-6-julien@lepiller.eu> X-Mailer: git-send-email 2.14.2 In-Reply-To: <20171021162058.27938-1-julien@lepiller.eu> References: <20171021181638.27d0d0d8@lepiller.eu> <20171021162058.27938-1-julien@lepiller.eu> X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 28925 Cc: Julien Lepiller X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.0 (/) From: Julien Lepiller * gnu/packages/ocaml.scm (coq-coquelicot): Update to 3.0.1. --- gnu/packages/ocaml.scm | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index beb73a2d0..6cf92689a 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -3699,14 +3699,14 @@ part of the distribution.") (define-public coq-coquelicot (package (name "coq-coquelicot") - (version "3.0.0") + (version "3.0.1") (source (origin (method url-fetch) (uri (string-append "https://gforge.inria.fr/frs/download.php/" - "file/36537/coquelicot-" version ".tar.gz")) + "file/37045/coquelicot-" version ".tar.gz")) (sha256 (base32 - "0fx99bvsbdizj00gx2im8939y4wwl05f4qhw184j90kcx5vjxxv9")))) + "0hsyhsy2lwqxxx2r8xgi5csmirss42lp9bkb9yy35mnya0w78c8r")))) (build-system gnu-build-system) (native-inputs `(("ocaml" ,ocaml) -- 2.14.2 From debbugs-submit-bounces@debbugs.gnu.org Sat Oct 21 12:23:02 2017 Received: (at 28925) by debbugs.gnu.org; 21 Oct 2017 16:23:02 +0000 Received: from localhost ([127.0.0.1]:54495 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1e5wYA-00031k-42 for submit@debbugs.gnu.org; Sat, 21 Oct 2017 12:23:02 -0400 Received: from lepiller.eu ([89.234.186.109]:55368) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1e5wY2-00030k-99 for 28925@debbugs.gnu.org; Sat, 21 Oct 2017 12:22:54 -0400 Received: from localhost.localdomain (static-176-182-42-79.ncc.abo.bbox.fr [176.182.42.79]) by lepiller.eu (OpenSMTPD) with ESMTPSA id 2da3fbf2 (TLSv1.2:ECDHE-RSA-AES128-GCM-SHA256:128:NO); Sat, 21 Oct 2017 16:24:05 +0000 (UTC) From: julien@lepiller.eu To: 28925@debbugs.gnu.org Subject: [PATCH 7/7] gnu: Update coq-interval to 3.3.0. Date: Sat, 21 Oct 2017 18:20:58 +0200 Message-Id: <20171021162058.27938-8-julien@lepiller.eu> X-Mailer: git-send-email 2.14.2 In-Reply-To: <20171021162058.27938-1-julien@lepiller.eu> References: <20171021181638.27d0d0d8@lepiller.eu> <20171021162058.27938-1-julien@lepiller.eu> X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 28925 Cc: Julien Lepiller X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.0 (/) From: Julien Lepiller * gnu/packages/ocaml.scm (coq-interval): Update to 3.3.0. --- gnu/packages/ocaml.scm | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index addcdba5a..b13168c7d 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -3781,14 +3781,14 @@ provides BigN, BigZ, BigQ that used to be part of Coq standard library.") (define-public coq-interval (package (name "coq-interval") - (version "3.2.0") + (version "3.3.0") (source (origin (method url-fetch) (uri (string-append "https://gforge.inria.fr/frs/download.php/" "file/36538/interval-" version ".tar.gz")) (sha256 (base32 - "16ir7mizl18kwa1ls8fwjih6r87894bvc1r6lh85cd43la7nriq3")))) + "08fdcf3hbwqphglvwprvqzgkg0qbimpyhnqsgv3gac4y1ap0f903")))) (build-system gnu-build-system) (native-inputs `(("ocaml" ,ocaml) @@ -3796,6 +3796,7 @@ provides BigN, BigZ, BigQ that used to be part of Coq standard library.") ("coq" ,coq))) (propagated-inputs `(("flocq" ,coq-flocq) + ("bignums" ,coq-bignums) ("coquelicot" ,coq-coquelicot) ("mathcomp" ,coq-mathcomp))) (arguments -- 2.14.2 From debbugs-submit-bounces@debbugs.gnu.org Sat Oct 21 12:23:04 2017 Received: (at 28925) by debbugs.gnu.org; 21 Oct 2017 16:23:04 +0000 Received: from localhost ([127.0.0.1]:54498 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1e5wYA-000328-Ih for submit@debbugs.gnu.org; Sat, 21 Oct 2017 12:23:04 -0400 Received: from lepiller.eu ([89.234.186.109]:55360) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1e5wY2-000308-4d for 28925@debbugs.gnu.org; Sat, 21 Oct 2017 12:22:55 -0400 Received: from localhost.localdomain (static-176-182-42-79.ncc.abo.bbox.fr [176.182.42.79]) by lepiller.eu (OpenSMTPD) with ESMTPSA id 5f3c82cc (TLSv1.2:ECDHE-RSA-AES128-GCM-SHA256:128:NO); Sat, 21 Oct 2017 16:24:05 +0000 (UTC) From: julien@lepiller.eu To: 28925@debbugs.gnu.org Subject: [PATCH 6/7] gnu: Add coq-bignums. Date: Sat, 21 Oct 2017 18:20:57 +0200 Message-Id: <20171021162058.27938-7-julien@lepiller.eu> X-Mailer: git-send-email 2.14.2 In-Reply-To: <20171021162058.27938-1-julien@lepiller.eu> References: <20171021181638.27d0d0d8@lepiller.eu> <20171021162058.27938-1-julien@lepiller.eu> X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 28925 Cc: Julien Lepiller X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.0 (/) From: Julien Lepiller * gnu/packages/ocaml.scm (coq-bignums): New variable. --- gnu/packages/ocaml.scm | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index 6cf92689a..addcdba5a 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -3746,6 +3746,38 @@ conservative extension of Coq's standard library and provides correspondence theorems between the two libraries.") (license license:lgpl3+))) +(define-public coq-bignums + (package + (name "coq-bignums") + (version "8.7.0") + (source (origin + (method url-fetch) + (uri (string-append "https://github.com/coq/bignums/archive/V" + version ".tar.gz")) + (file-name (string-append name "-" version ".tar.gz")) + (sha256 + (base32 + "03iw9jiwq9jx45gsvp315y3lxr8m9ksppmcjvxs5c23qnky6zqjx")))) + (build-system gnu-build-system) + (native-inputs + `(("ocaml" ,ocaml) + ("coq" ,coq))) + (inputs + `(("camlp5" ,camlp5))) + (arguments + `(#:tests? #f; No test target + #:make-flags + (list (string-append "COQLIBINSTALL=" (assoc-ref %outputs "out") + "/lib/coq/user-contrib")) + #:phases + (modify-phases %standard-phases + (delete 'configure)))) + (home-page "https://github.com/coq/bignums") + (synopsis "Coq library for arbitrary large numbers") + (description "Bignums is a coq library of arbitrary large numbers. It +provides BigN, BigZ, BigQ that used to be part of Coq standard library.") + (license license:lgpl2.1+))) + (define-public coq-interval (package (name "coq-interval") -- 2.14.2 From debbugs-submit-bounces@debbugs.gnu.org Sat Oct 21 13:09:46 2017 Received: (at 28925) by debbugs.gnu.org; 21 Oct 2017 17:09:46 +0000 Received: from localhost ([127.0.0.1]:54519 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1e5xHO-0004BF-1q for submit@debbugs.gnu.org; Sat, 21 Oct 2017 13:09:46 -0400 Received: from lepiller.eu ([89.234.186.109]:55370) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1e5xHL-0004B5-4n for 28925@debbugs.gnu.org; Sat, 21 Oct 2017 13:09:44 -0400 Received: from localhost (static-176-182-42-79.ncc.abo.bbox.fr [176.182.42.79]) by lepiller.eu (OpenSMTPD) with ESMTPSA id aebd738d (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO) for <28925@debbugs.gnu.org>; Sat, 21 Oct 2017 17:10:58 +0000 (UTC) Date: Sat, 21 Oct 2017 19:07:55 +0200 From: Julien Lepiller To: 28925@debbugs.gnu.org Subject: Re: [bug#28925] [PATCH] gnu: youtube-dl: Update to 2017.10.20. Message-ID: <20171021190755.053b95fa@lepiller.eu> In-Reply-To: <20171021162058.27938-2-julien@lepiller.eu> References: <20171021181638.27d0d0d8@lepiller.eu> <20171021162058.27938-1-julien@lepiller.eu> <20171021162058.27938-2-julien@lepiller.eu> X-Mailer: Claws Mail 3.15.1-dirty (GTK+ 2.24.31; x86_64-unknown-linux-gnu) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 28925 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.0 (/) Le Sat, 21 Oct 2017 18:20:52 +0200, julien@lepiller.eu a =C3=A9crit : > From: Tobias Geerinckx-Rice >=20 > [...] Whoops, this is not in the patch series, it's a mistake. The rest is correct. From debbugs-submit-bounces@debbugs.gnu.org Sat Oct 21 18:18:48 2017 Received: (at 28925) by debbugs.gnu.org; 21 Oct 2017 22:18:48 +0000 Received: from localhost ([127.0.0.1]:54705 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1e626S-0000RX-BW for submit@debbugs.gnu.org; Sat, 21 Oct 2017 18:18:48 -0400 Received: from out4-smtp.messagingengine.com ([66.111.4.28]:38831) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1e626Q-0000RP-1x for 28925@debbugs.gnu.org; Sat, 21 Oct 2017 18:18:47 -0400 Received: from compute5.internal (compute5.nyi.internal [10.202.2.45]) by mailout.nyi.internal (Postfix) with ESMTP id AD92F20C18; Sat, 21 Oct 2017 18:18:45 -0400 (EDT) Received: from frontend2 ([10.202.2.161]) by compute5.internal (MEProxy); Sat, 21 Oct 2017 18:18:45 -0400 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=fastmail.com; h= content-type:date:from:in-reply-to:message-id:mime-version :references:subject:to:x-me-sender:x-me-sender:x-sasl-enc; s= fm1; bh=0skIV3XGpRKswPpPsXMmGLt86oL3YaedC/RfJoh83MU=; b=mtczGbzY K/Wt3qhrhj3/X+kY5wkhxHvlig2pAKgyAG4G9T+Sq6y/CpxEY6TQXCM3UpAWpYCh mRNo2B6VxboDxf823iviIVqzNS2jHNq5gO0ObdNlnEgMu1mpGC9danr9HOlkrWfp fvaZTkhCeEYRHtRocj9vGGD2YDnQqJ0l0bfZAwoLwif2nkVKvhZcplvFTHssVX9C ZVprhTMYpo9EgceYW+ECup/6A4MjygXvqx8hqQYB4M0WzWlQbK0yU73F5kTCUfE3 5Lx3+QJQDqExDq7ShJAFFIE3GePGVWnEah4RWjZIA3wTkn1/oR4ud9Si34jCr+Kr drTDlXkBPsvp4Q== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d= messagingengine.com; h=content-type:date:from:in-reply-to :message-id:mime-version:references:subject:to:x-me-sender :x-me-sender:x-sasl-enc; s=fm1; bh=0skIV3XGpRKswPpPsXMmGLt86oL3Y aedC/RfJoh83MU=; b=p71mPVRfmtOopdkRPnbWrmt5SHw7oIB8UJkInnx+MhIYj Ti07eRH6FR53u1sfxGLGd6I+qmQxwyUoZgP0WC7L68mPyoMJcwjIKKDbamvDA63T u5SI4s3qZnd5Lq9vJzQNex+GYUnL7RNOiOkRKWxazPputZQkOy41Gf4cI7MGkYv6 BECSGFobl7U6xVPCmfCspi51f5ie1qB5rqEU8Zs7i77OKRuL0Kdy0kJjv01kh0WE I908QPduSieJ4jkjFpk7q6wzZbnTLfEIXVkddTrxL3D9U72yuAh2v5TxM72SvvFL 7ivseQqS0g+XNTgwG48JtBb3QDePctMr7sTFFhXWw== X-ME-Sender: Received: from localhost (cm-84.214.173.174.getinternet.no [84.214.173.174]) by mail.messagingengine.com (Postfix) with ESMTPA id 3E3B124A70; Sat, 21 Oct 2017 18:18:45 -0400 (EDT) From: Marius Bakke To: julien@lepiller.eu, 28925@debbugs.gnu.org Subject: Re: [bug#28925] [PATCH 2/7] gnu: Update coq to 8.7.0. In-Reply-To: <20171021162058.27938-3-julien@lepiller.eu> References: <20171021181638.27d0d0d8@lepiller.eu> <20171021162058.27938-1-julien@lepiller.eu> <20171021162058.27938-3-julien@lepiller.eu> User-Agent: Notmuch/0.25.1 (https://notmuchmail.org) Emacs/25.3.1 (x86_64-pc-linux-gnu) Date: Sun, 22 Oct 2017 00:18:43 +0200 Message-ID: <878tg45em4.fsf@fastmail.com> MIME-Version: 1.0 Content-Type: multipart/signed; boundary="=-=-="; micalg=pgp-sha512; protocol="application/pgp-signature" X-Spam-Score: -0.7 (/) X-Debbugs-Envelope-To: 28925 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.7 (/) --=-=-= Content-Type: text/plain julien@lepiller.eu writes: > From: Julien Lepiller > > * gnu/packages/ocaml.scm (coq): Update to 8.7.0. Please also mention the changes to inputs and build-system here. The same goes for the other patches. This series LGTM apart from that. --=-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQEzBAEBCgAdFiEEu7At3yzq9qgNHeZDoqBt8qM6VPoFAlnrx8MACgkQoqBt8qM6 VPogZAf/fFoOH6nLmldEjXfbw234dc5wByr2br9NimC8HJLwTXVcQILi2fYW4wwP EbTjmZ1P1J5v28dcv8QWT5IXgYBOMpOc8+aR44DV2vpJjf2IIYe/JayG8qAjla/8 c0BN1+xJtm4wzkjw0Qn2UusIg2C8RLr0lhuXf/k+1m4elVSSkZkIR1picxR+Brqu xXLjnzx7Ul8q6SRJwNY9OKhGRzbTENx/U6Zc8+aIWWFpuJU+IQvIysAl8srzPb+f Zgunu4hL/FS+BEzahNl5N+K5W2jXLEsf+fNJSjzLjdiVo8x0DrkLqxz1KqKJIuER d5sD80UdsowfS5yFUbfCMwDJKYEmhw== =b+jn -----END PGP SIGNATURE----- --=-=-=-- From debbugs-submit-bounces@debbugs.gnu.org Sun Oct 22 04:24:37 2017 Received: (at 28925-done) by debbugs.gnu.org; 22 Oct 2017 08:24:37 +0000 Received: from localhost ([127.0.0.1]:54907 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1e6BYj-0004EE-AP for submit@debbugs.gnu.org; Sun, 22 Oct 2017 04:24:37 -0400 Received: from lepiller.eu ([89.234.186.109]:59052) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1e6BYh-0004E4-1m for 28925-done@debbugs.gnu.org; Sun, 22 Oct 2017 04:24:35 -0400 Received: from localhost (static-176-182-42-79.ncc.abo.bbox.fr [176.182.42.79]) by lepiller.eu (OpenSMTPD) with ESMTPSA id 0f528029 (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO) for <28925-done@debbugs.gnu.org>; Sun, 22 Oct 2017 08:25:51 +0000 (UTC) Date: Sun, 22 Oct 2017 10:22:44 +0200 From: Julien Lepiller To: 28925-done@debbugs.gnu.org Subject: Re: [bug#28925] [PATCH 2/7] gnu: Update coq to 8.7.0. Message-ID: <20171022102244.3d25ba24@lepiller.eu> In-Reply-To: <878tg45em4.fsf@fastmail.com> References: <20171021181638.27d0d0d8@lepiller.eu> <20171021162058.27938-1-julien@lepiller.eu> <20171021162058.27938-3-julien@lepiller.eu> <878tg45em4.fsf@fastmail.com> X-Mailer: Claws Mail 3.15.1-dirty (GTK+ 2.24.31; x86_64-unknown-linux-gnu) MIME-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha256; boundary="Sig_/jQ7_GcVyNqQs3=Wi_dK8JLu"; protocol="application/pgp-signature" X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 28925-done X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.0 (/) --Sig_/jQ7_GcVyNqQs3=Wi_dK8JLu Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Le Sun, 22 Oct 2017 00:18:43 +0200, Marius Bakke a =C3=A9crit : > julien@lepiller.eu writes: >=20 > > From: Julien Lepiller > > > > * gnu/packages/ocaml.scm (coq): Update to 8.7.0. =20 >=20 > Please also mention the changes to inputs and build-system here. The > same goes for the other patches. This series LGTM apart from that. Thank you for the review, pushed as 07b4cd3a48022a472c90ec46f2e8b08d9cc8fc3e - 6efc99967800183daa74ba2ebff6185dfcf1b33d. --Sig_/jQ7_GcVyNqQs3=Wi_dK8JLu Content-Type: application/pgp-signature Content-Description: Signature digitale OpenPGP -----BEGIN PGP SIGNATURE----- iQIzBAEBCAAdFiEEtfrmKFtBNyiyoPrtQxEfRSAIagwFAlnsVVUACgkQQxEfRSAI agzhBxAAtZad8B51dzVBqpA6U78mtBfnZIFCX/5MymoCvSUHyUdCjQHYtxwbmSNe Hm18jcPyRtrvezqRGZ3p8WXEqhv+ITULCiit8BP3JoiYLMz2RtYlfoaU1qbhsweM EM0WGjH1JGiuGOBA0QVHZno9D2FUCpFPdDTRcBAsc1/6KPdDd55DE4RgdXFjz+bB 1aAs/JicKE2yW+vnaTbvRnU1gm3R7DhFxXbeb9XDFxbIYtNzeWytngibqmnBmBif BjqLdPnQLoeXihJJpxwL/k/8zLGAHXroaDu0jtlJRpkH1q/DzZsY5ag6D1g2Lytk IhHTtxbPabt2wJQadL/A1G4hLnVoNI0VSBZvXm6JK7psBLyoc7bGsiQ/RqFpVQby RGHaYu5NVLWAJnBQKzgeEzWYmuKTlGDndm7aIvME9Uic3cThkciOzreCRM3dkDrz Jv+QwVhPtqD+KQhIFHZSmY7tLEmG8FEPpMhl5ltWahK0kF1J0/PTaSPz0FDgtwvw 7rScZ3mJUKEFftVUzoEyNvaVrrTtL9Pl/fS/mVG8xh4cLbaHJy+ISBCmuiQDj0VS eI7CpHgVHxeQlSRWfbv8V0Bhazjkerq4qFh7Al0CkNkWQZyeR2XCWwUWzRTkJgRA VdPsTbqBivv+M3XQia5Rfxj8ZhfaUmDIEjqhnrp5ZulkCocCA/w= =5+wn -----END PGP SIGNATURE----- --Sig_/jQ7_GcVyNqQs3=Wi_dK8JLu-- From debbugs-submit-bounces@debbugs.gnu.org Tue Oct 24 00:50:39 2017 Received: (at 28925) by debbugs.gnu.org; 24 Oct 2017 04:50:39 +0000 Received: from localhost ([127.0.0.1]:58202 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1e6rAl-0002gl-C7 for submit@debbugs.gnu.org; Tue, 24 Oct 2017 00:50:39 -0400 Received: from hera.aquilenet.fr ([141.255.128.1]:47815) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1e6rAj-0002gb-6R for 28925@debbugs.gnu.org; Tue, 24 Oct 2017 00:50:37 -0400 Received: from localhost (localhost [127.0.0.1]) by hera.aquilenet.fr (Postfix) with ESMTP id 1A20EEF67; Tue, 24 Oct 2017 06:50:37 +0200 (CEST) X-Virus-Scanned: Debian amavisd-new at aquilenet.fr Received: from hera.aquilenet.fr ([127.0.0.1]) by localhost (hera.aquilenet.fr [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id g-LM_VyWXPge; Tue, 24 Oct 2017 06:50:35 +0200 (CEST) Received: from ribbon (node-1w7jr9qot7winqrne9k8b99d1.ipv6.telus.net [IPv6:2001:569:7803:2c00:728:f466:18ad:22a5]) by hera.aquilenet.fr (Postfix) with ESMTPSA id 80BF0BAA; Tue, 24 Oct 2017 06:50:34 +0200 (CEST) From: ludo@gnu.org (Ludovic =?utf-8?Q?Court=C3=A8s?=) To: julien@lepiller.eu Subject: Re: [bug#28925] [PATCH 1/7] gnu: camlp5: install META file. References: <20171021181638.27d0d0d8@lepiller.eu> <20171021162058.27938-1-julien@lepiller.eu> X-URL: http://www.fdn.fr/~lcourtes/ X-Revolutionary-Date: 2 Brumaire an 226 de la =?utf-8?Q?R=C3=A9volution?= X-PGP-Key-ID: 0x090B11993D9AEBB5 X-PGP-Key: http://www.fdn.fr/~lcourtes/ludovic.asc X-PGP-Fingerprint: 3CE4 6455 8A84 FDC6 9DB4 0CFB 090B 1199 3D9A EBB5 X-OS: x86_64-pc-linux-gnu Date: Mon, 23 Oct 2017 21:50:23 -0700 In-Reply-To: <20171021162058.27938-1-julien@lepiller.eu> (julien@lepiller.eu's message of "Sat, 21 Oct 2017 18:20:51 +0200") Message-ID: <87o9oxqhdc.fsf@gnu.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.3 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain X-Spam-Score: 1.0 (+) X-Debbugs-Envelope-To: 28925 Cc: 28925@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: 1.0 (+) julien@lepiller.eu skribis: > From: Julien Lepiller > > * gnu/packages/ocaml.scm (camlp5) [phases]: New install-meta phase. > --- > gnu/packages/ocaml.scm | 7 ++++++- > 1 file changed, 6 insertions(+), 1 deletion(-) > > diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm > index aa2f00667..40d42a5d4 100644 > --- a/gnu/packages/ocaml.scm > +++ b/gnu/packages/ocaml.scm > @@ -401,7 +401,12 @@ syntax of OCaml.") > (lambda _ > (zero? (system* "make" "-j" (number->string > (parallel-job-count)) > - "world.opt"))))))) > + "world.opt")))) > + ;; Required for findlib to find camlp5's libraries > + (add-after 'install 'install-meta > + (lambda* (#:key outputs #:allow-other-keys) > + (install-file "etc/META" (string-append (assoc-ref outputs "out") > + "/lib/ocaml/camlp5/"))))))) Return #t, but otherwise LGTM! Ludo'. From unknown Mon Jun 23 16:46:11 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: Tue, 21 Nov 2017 12:24:04 +0000 User-Agent: Fakemail v42.6.9 # This is a fake control message. # # The action: # bug archived. thanks # This fakemail brought to you by your local debbugs # administrator