GNU bug report logs - #64249
[PATCH ocaml-team 1/2] gnu: ocaml: Update to 4.14.1.

Previous Next

Full log

View this message in rfc822 format

From: pukkamustard <pukkamustard <at> posteo.net>
To: 64249 <at> debbugs.gnu.org
Cc: pukkamustard <pukkamustard <at> posteo.net>, Julien Lepiller <julien <at> lepiller.eu>, pukkamustard <pukkamustard <at> posteo.net>
Subject: [bug#64249] [PATCH ocaml-team v3 2/6] gnu: coq: Update to 8.17.1.
Date: Tue, 18 Jul 2023 12:23:59 +0000

* gnu/packages/coq.scm (coq-core, coq-stdlib, coq): Update to 8.17.1 and
remove test-target argument.
---
 gnu/packages/coq.scm | 24 +++++-------------------
 1 file changed, 5 insertions(+), 19 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 09ca4030ea..3332707a71 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -53,7 +53,7 @@ (define-module (gnu packages coq)
 (define-public coq-core
   (package
     (name "coq-core")
-    (version "8.16.1")
+    (version "8.17.1")
     (source
      (origin
        (method git-fetch)
@@ -63,7 +63,7 @@ (define-public coq-core
        (file-name (git-file-name name version))
        (sha256
         (base32
-         "0ljpqhh5lfsim29fcfp2xfcvm3j84pf1mb0gnpdr8vcqqw7mqwpf"))
+         "0gg6hizq0i08lk741b579cbswhy6qvkh6inc3d3i5a2af98psq63"))
        (patches (search-patches "coq-fix-envvars.patch"))))
     (native-search-paths
      (list (search-path-specification
@@ -83,8 +83,7 @@ (define-public coq-core
     (native-inputs
      (list ocaml-ounit2 which))
     (arguments
-     `(#:package "coq-core"
-       #:test-target "."))
+     `(#:package "coq-core"))
     (properties '((upstream-name . "coq"))) ; also for inherited packages
     (home-page "https://coq.inria.fr")
     (synopsis "Proof assistant for higher-order logic")
@@ -101,19 +100,7 @@ (define-public coq-stdlib
     (inherit coq-core)
     (name "coq-stdlib")
     (arguments
-     `(#:package "coq-stdlib"
-       #:test-target "."
-       #:phases
-       (modify-phases %standard-phases
-         (add-before 'build 'fix-dune
-           (lambda _
-             (substitute* "user-contrib/Ltac2/dune"
-               (("coq-core.plugins.ltac2")
-                (string-join
-                  (map (lambda (plugin) (string-append "coq-core.plugins." plugin))
-                       '("ltac2" "number_string_notation" "tauto" "cc"
-                         "firstorder"))
-                  " "))))))))
+     `(#:package "coq-stdlib"))
     (inputs
      (list coq-core gmp ocaml-zarith))
     (native-inputs '())))
@@ -123,8 +110,7 @@ (define-public coq
     (inherit coq-core)
     (name "coq")
     (arguments
-     `(#:package "coq"
-       #:test-target "."))
+     `(#:package "coq"))
     (propagated-inputs
      (list coq-core coq-stdlib))
     (native-inputs '())))
-- 
2.40.1

Previous Next

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