Package: guix-patches;
Reported by: pukkamustard <pukkamustard <at> posteo.net>
Date: Fri, 23 Jun 2023 13:45:02 UTC
Severity: normal
Tags: patch
Done: Julien Lepiller <julien <at> lepiller.eu>
Bug is archived. No further changes may be made.
Message #146 received at 64249 <at> debbugs.gnu.org (full text, mbox):
From: Julien Lepiller <julien <at> lepiller.eu> To: pukkamustard <pukkamustard <at> posteo.net> Cc: 64249 <at> debbugs.gnu.org Subject: Re: [bug#64249] [PATCH ocaml-team v5 09/12] gnu: coq: Update to 8.17.1. Date: Thu, 17 Aug 2023 21:08:24 +0200
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 <at> 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
GNU bug tracking system
Copyright (C) 1999 Darren O. Benham,
1997,2003 nCipher Corporation Ltd,
1994-97 Ian Jackson.