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: Julien Lepiller <julien <at> lepiller.eu>
To: pukkamustard <pukkamustard <at> posteo.net>
Cc: 64249 <at> debbugs.gnu.org
Subject: [bug#64249] [PATCH ocaml-team v3 2/6] gnu: coq: Update to 8.17.1.
Date: Wed, 19 Jul 2023 20:18:43 +0200

Hi,

I'm not sure why, but this is breaking all coq dependents, with
messages similar to:

cannot guess a path for Coq libraries; please use -coqlib option or
ensure you have installed the package containing Coq's stdlib
(coq-stdlib in OPAM) If you intend to use Coq without a standard
library, the -boot -noinit options must be used.

I think this is because coq-stdlib is mostly empty for some reason.


Le Tue, 18 Jul 2023 12:23:59 +0000,
pukkamustard <pukkamustard <at> posteo.net> a écrit :

> * 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 '())))

Previous Next

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