Message ID | 7c82263ece8fff6106930babd4afe2c7a107f3d8.1691335142.git.pukkamustard@posteo.net |
---|---|
State | New |
Headers | show |
Series | [bug#64249,ocaml-team,v5,01/12] gnu: ocaml: Update to 4.14.1. | expand |
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
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