[bug#64249] [PATCH ocaml-team v5 09/12] gnu: coq: Update to 8.17.1.

[Julien Lepiller]

this looks good to me, but there's a new failure in
coq-mathcomp-bigenough after that. Replacing "coq-core" with "coq" in
the configure flags fix the issue.

Le Sun,  6 Aug 2023 15:20:28 +0000,
pukkamustard <pukkamustard@posteo.net> a écrit :

> * gnu/packages/coq.scm (coq): Update to 8.17.1 and merge with
> coq-core and coq-stdlib. [arguments] Merge with coq-core and
> coq-stdlib. Add pre-build phases and add a custom install phase.
> Remove unnecessary test-target. (coq-core): Remove variable.
>   (coq-stdlib): Remove variable.
>   (coq-ide)[propagated-inputs]: Add zlib.
>   (coq-mathcomp-bigenough)[propagated-inputs]: Remove coq-core.
>   (coq-mathcomp-finmap)[inputs]: Remove coq-stdlib.
>   (coq-equations): Update to 1.3-8.17.
> ---
>  gnu/packages/coq.scm | 76
> +++++++++++++++++--------------------------- 1 file changed, 30
> insertions(+), 46 deletions(-)
> 
> diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
> index 663265f5be..b63239b99e 100644
> --- a/gnu/packages/coq.scm
> +++ b/gnu/packages/coq.scm
> @@ -31,6 +31,7 @@ (define-module (gnu packages coq)
>    #:use-module (gnu packages base)
>    #:use-module (gnu packages bison)
>    #:use-module (gnu packages boost)
> +  #:use-module (gnu packages compression)
>    #:use-module (gnu packages emacs)
>    #:use-module (gnu packages flex)
>    #:use-module (gnu packages gawk)
> @@ -50,10 +51,10 @@ (define-module (gnu packages coq)
>    #:use-module (guix utils)
>    #:use-module ((srfi srfi-1) #:hide (zip)))
>  
> -(define-public coq-core
> +(define-public coq
>    (package
> -    (name "coq-core")
> -    (version "8.16.1")
> +    (name "coq")
> +    (version "8.17.1")
>      (source
>       (origin
>         (method git-fetch)
> @@ -63,7 +64,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
> @@ -78,13 +79,29 @@ (define-public coq-core
>              (files (list "lib/ocaml/site-lib/coq-core"))
>              (separator #f))))
>      (build-system dune-build-system)
> +    (arguments
> +     `(#:package "coq-core,coq-stdlib,coq"
> +       #:phases
> +       (modify-phases %standard-phases
> +         (add-before 'build 'configure
> +           (lambda* (#:key outputs #:allow-other-keys)
> +             (let* ((out (assoc-ref outputs "out"))
> +                    (libdir (string-append out
> "/lib/ocaml/site-lib")))
> +               (invoke "./configure" "-prefix" out
> +                       "-libdir" libdir))))
> +         (add-before 'build 'make-dunestrap
> +           (lambda _ (invoke "make" "dunestrap")))
> +         (replace 'install
> +           (lambda* (#:key outputs #:allow-other-keys)
> +             (let* ((out (assoc-ref outputs "out"))
> +                    (libdir (string-append out
> "/lib/ocaml/site-lib")))
> +               (invoke "dune" "install" "--prefix" out
> +                       "--libdir" libdir
> +                       "coq-core" "coq-stdlib" "coq")))))))
>      (inputs
>       (list gmp ocaml-zarith))
>      (native-inputs
>       (list ocaml-ounit2 which))
> -    (arguments
> -     `(#:package "coq-core"
> -       #:test-target "."))
>      (properties '((upstream-name . "coq"))) ; also for inherited
> packages (home-page "https://coq.inria.fr";)
>      (synopsis "Proof assistant for higher-order logic")
> @@ -96,39 +113,6 @@ (define-public coq-core
>      ;; Some of the documentation is distributed under opl1.0+.
>      (license (list license:lgpl2.1 license:opl1.0+))))
>  
> -(define-public coq-stdlib
> -  (package
> -    (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"))
> -                  " "))))))))
> -    (inputs
> -     (list coq-core gmp ocaml-zarith))
> -    (native-inputs '())))
> -
> -(define-public coq
> -  (package
> -    (inherit coq-core)
> -    (name "coq")
> -    (arguments
> -     `(#:package "coq"
> -       #:test-target "."))
> -    (propagated-inputs
> -     (list coq-core coq-stdlib))
> -    (native-inputs '())))
> -
>  (define-public coq-ide-server
>    (package
>      (inherit coq)
> @@ -147,7 +131,7 @@ (define-public coq-ide
>       `(#:tests? #f
>         #:package "coqide"))
>      (propagated-inputs
> -     (list coq coq-ide-server))
> +     (list coq coq-ide-server zlib))
>      (inputs
>       (list lablgtk3 ocaml-lablgtk3-sourceview3))))
>  
> @@ -555,16 +539,16 @@ (define-public coq-autosubst
>  (define-public coq-equations
>    (package
>      (name "coq-equations")
> -    (version "1.3")
> +    (version "1.3-8.17")
>      (source (origin
>                (method git-fetch)
>                (uri (git-reference
>                      (url "https://github.com/mattam82/Coq-Equations";)
> -                    (commit (string-append "v" version "-8.16"))))
> +                    (commit (string-append "v" version))))
>                (file-name (git-file-name name version))
>                (sha256
>                 (base32
> -
> "08f756vgdd1wklkarg0b93j4n5mhkqm5ixxrhyb23dcv2dwhc8yg"))))
> +
> "0g68h4c1ijpphixvl9wkd7sibds38v4236dpvvh194j5ii42vnn8"))))
> (build-system gnu-build-system) (native-inputs
>       (list ocaml coq camlp5))
> @@ -716,7 +700,7 @@ (define-public coq-mathcomp-finmap
>                                           "/lib/coq/user-contrib"))
>         #:phases (modify-phases %standard-phases
>                    (delete 'configure))))
> -    (inputs (list coq coq-stdlib coq-mathcomp which))
> +    (inputs (list coq coq coq-mathcomp which))
>      (synopsis "Finite sets and finite types for coq-mathcomp")
>      (description
>       "This library is an extension of coq-mathcomp which supports
> finite sets @@ -757,7 +741,7 @@ (define-public coq-mathcomp-bigenough
>                                              "/lib/coq/user-contrib"))
>         #:phases (modify-phases %standard-phases
>                    (delete 'configure))))
> -    (propagated-inputs (list coq coq-core coq-mathcomp which))
> +    (propagated-inputs (list coq coq-mathcomp which))
>      (home-page "https://math-comp.github.io/";)
>      (synopsis "Small library to do epsilon - N reasoning")
>      (description