[bug#52164] [PATCH] gnu: coq: Update to 8.14.0.

[zimoun <zimon.toutoune@gmail.com>]

Hi,

On dim., 28 nov. 2021 at 18:27, Julien Lepiller <julien@lepiller.eu> wrote:
> * gnu/packages/coq.scm (coq): Update to 8.14.0.
> (coq-bignums): Update to 8.14.0.
> (coq-equations): Update to 1.3.
> * gnu/packages/patches/coq-fix-envvars.patch: New file.
> * gnu/local.mk (dist_patch_DATA): Add it.
> ---
>  gnu/local.mk                               |   1 +
>  gnu/packages/coq.scm                       |  65 +++++++---
>  gnu/packages/patches/coq-fix-envvars.patch | 139 +++++++++++++++++++++
>  3 files changed, 188 insertions(+), 17 deletions(-)
>  create mode 100644 gnu/packages/patches/coq-fix-envvars.patch

[...]

> -(define-public coq
> +(define-public coq-core

[...]

> -     `(("which" ,which)))
> +     `(("ocaml-ounit2" ,ocaml-ounit2)
> +       ("which" ,which)))

This ’which’ could be removed. :-)


> +(define-public coq-stdlib
> +  (package
> +    (inherit coq-core)
> +    (name "coq-stdlib")
> +    (arguments
> +     `(#:package "coq-stdlib"
> +       #:test-target "."))
> +    (inputs
> +     `(("coq-core" ,coq-core)
> +       ("gmp" ,gmp)
> +       ("ocaml-zarith" ,ocaml-zarith)))
> +    (native-inputs '())))
> +
> +(define-public coq
> +  (package
> +    (inherit coq-core)
> +    (name "coq")
> +    (arguments
> +     `(#:package "coq"
> +       #:test-target "."))
> +    (propagated-inputs
> +     `(("coq-core" ,coq-core)
> +       ("coq-stdlib" ,coq-stdlib)))
> +    (native-inputs '())))

With this approach, 3 builds.  Is it required by kind-of Coq bootstrap?


>  (define-public coq-bignums
>    (package
>      (name "coq-bignums")
> -    (version "8.13.0")
> +    (version "8.14.0")

This…

>  (define-public coq-equations
>    (package
>      (name "coq-equations")
> -    (version "1.2.4")
> +    (version "1.3")

and this… Cannot they be upgraded by a separated commit?

They will probably be broken with Coq 8.13 but if their upgrade is right
after and pushed with the same batch, it is transparent and the
atomicity appears to me better.


> diff --git a/gnu/packages/patches/coq-fix-envvars.patch b/gnu/packages/patches/coq-fix-envvars.patch
> new file mode 100644
> index 0000000000..deecf5ce74
> --- /dev/null
> +++ b/gnu/packages/patches/coq-fix-envvars.patch
> @@ -0,0 +1,139 @@
> +From ebe09fcac72b21d17c4e8fe6edc1b6076a4ae97c Mon Sep 17 00:00:00 2001
> +From: Julien Lepiller <julien@lepiller.eu>
> +Date: Sun, 21 Nov 2021 00:38:03 +0100
> +Subject: [PATCH] Fix environment variable usage.
> +
> +---
> + checker/checker.ml      |  2 ++
> + lib/envars.ml           | 26 ++++++++++++++++----------
> + sysinit/coqargs.ml      |  3 ++-
> + sysinit/coqloadpath.ml  |  3 ++-
> + sysinit/coqloadpath.mli |  2 +-
> + tools/coqdep.ml         |  2 +-
> + 6 files changed, 24 insertions(+), 14 deletions(-)

This fix LGTM.


Otherwise, LTGM.


Cheers,
simon