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

[Julien Lepiller <julien@lepiller.eu>]

Le 29 novembre 2021 04:42:25 GMT-05:00, zimoun <zimon.toutoune@gmail.com> a écrit :
>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?

Coq now uses dune, and it is split into core, stdlib anl coq. I prefer to build one dune package in each guix package, rather than everything, especially since we want to separate coq-ide.

>
>
>>  (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.

They're broken with coq 8.13, and the previous version is also broken with coq 8.14. This is why I was able to update coq semantics independently but not these two.

>
>
>> 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