[bug#64249,ocaml-team,v3,2/6] gnu: coq: Update to 8.17.1.

* gnu/packages/coq.scm (coq-core, coq-stdlib, coq): Update to 8.17.1 and
remove test-target argument.
---
 gnu/packages/coq.scm | 24 +++++-------------------
 1 file changed, 5 insertions(+), 19 deletions(-)

Hi,

I'm not sure why, but this is breaking all coq dependents, with
messages similar to:

cannot guess a path for Coq libraries; please use -coqlib option or
ensure you have installed the package containing Coq's stdlib
(coq-stdlib in OPAM) If you intend to use Coq without a standard
library, the -boot -noinit options must be used.

I think this is because coq-stdlib is mostly empty for some reason.


Le Tue, 18 Jul 2023 12:23:59 +0000,
pukkamustard <pukkamustard@posteo.net> a écrit :

> * gnu/packages/coq.scm (coq-core, coq-stdlib, coq): Update to 8.17.1
> and remove test-target argument.
> ---
>  gnu/packages/coq.scm | 24 +++++-------------------
>  1 file changed, 5 insertions(+), 19 deletions(-)
> 
> diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
> index 09ca4030ea..3332707a71 100644
> --- a/gnu/packages/coq.scm
> +++ b/gnu/packages/coq.scm
> @@ -53,7 +53,7 @@ (define-module (gnu packages coq)
>  (define-public coq-core
>    (package
>      (name "coq-core")
> -    (version "8.16.1")
> +    (version "8.17.1")
>      (source
>       (origin
>         (method git-fetch)
> @@ -63,7 +63,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
> @@ -83,8 +83,7 @@ (define-public coq-core
>      (native-inputs
>       (list ocaml-ounit2 which))
>      (arguments
> -     `(#:package "coq-core"
> -       #:test-target "."))
> +     `(#:package "coq-core"))
>      (properties '((upstream-name . "coq"))) ; also for inherited
> packages (home-page "https://coq.inria.fr")
>      (synopsis "Proof assistant for higher-order logic")
> @@ -101,19 +100,7 @@ (define-public coq-stdlib
>      (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"))
> -                  " "))))))))
> +     `(#:package "coq-stdlib"))
>      (inputs
>       (list coq-core gmp ocaml-zarith))
>      (native-inputs '())))
> @@ -123,8 +110,7 @@ (define-public coq
>      (inherit coq-core)
>      (name "coq")
>      (arguments
> -     `(#:package "coq"
> -       #:test-target "."))
> +     `(#:package "coq"))
>      (propagated-inputs
>       (list coq-core coq-stdlib))
>      (native-inputs '())))

Hi,

Julien Lepiller <julien@lepiller.eu> writes:

> I'm not sure why, but this is breaking all coq dependents, with
> messages similar to:
>
> cannot guess a path for Coq libraries; please use -coqlib option or
> ensure you have installed the package containing Coq's stdlib
> (coq-stdlib in OPAM) If you intend to use Coq without a standard
> library, the -boot -noinit options must be used.
>
> I think this is because coq-stdlib is mostly empty for some reason.

A couple of build failures later this is where I'm at:

- Coq 8.17.1 includes considerable changes to the build system.

- Some `dune` files are autogenerated with `make dunestrap` (which runs
  the OCaml program `tools/dune_rule_gen/gen_rules.ml`.

- In the v3 patches I submitted `make dunestrap` was not being run,
  resulting in missing dune files and a quite empty `coq-stdlib`
  package.

- The 8.17.1 generated dune files for `coq-stdlib` reference things in
  `coq-core` directly with relative paths instead of letting
  dune/findlib find them (with entries in the `libraries` stanza in dune
  files). This makes building `coq-core` and `coq-stdlib` seperately
  more tricky.

I've asked in #coq for ideas on how `coq-stdlib` and `coq-core` can be
built seperately/kept in separate packages. Nothing yet.

What do you think about merging `coq-core`, `coq-stdlib` and `coq` into
a single package? Not as nice as the current situation, but maybe a way
to go without too many custom patches/hacks?

CC: Arnaud and Josselin who might be interested in Coq stuff.

Thanks,
pukkamustard


>> * gnu/packages/coq.scm (coq-core, coq-stdlib, coq): Update to 8.17.1
>> and remove test-target argument.
>> ---
>>  gnu/packages/coq.scm | 24 +++++-------------------
>>  1 file changed, 5 insertions(+), 19 deletions(-)
>> 
>> diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
>> index 09ca4030ea..3332707a71 100644
>> --- a/gnu/packages/coq.scm
>> +++ b/gnu/packages/coq.scm
>> @@ -53,7 +53,7 @@ (define-module (gnu packages coq)
>>  (define-public coq-core
>>    (package
>>      (name "coq-core")
>> -    (version "8.16.1")
>> +    (version "8.17.1")
>>      (source
>>       (origin
>>         (method git-fetch)
>> @@ -63,7 +63,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
>> @@ -83,8 +83,7 @@ (define-public coq-core
>>      (native-inputs
>>       (list ocaml-ounit2 which))
>>      (arguments
>> -     `(#:package "coq-core"
>> -       #:test-target "."))
>> +     `(#:package "coq-core"))
>>      (properties '((upstream-name . "coq"))) ; also for inherited
>> packages (home-page "https://coq.inria.fr")
>>      (synopsis "Proof assistant for higher-order logic")
>> @@ -101,19 +100,7 @@ (define-public coq-stdlib
>>      (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"))
>> -                  " "))))))))
>> +     `(#:package "coq-stdlib"))
>>      (inputs
>>       (list coq-core gmp ocaml-zarith))
>>      (native-inputs '())))
>> @@ -123,8 +110,7 @@ (define-public coq
>>      (inherit coq-core)
>>      (name "coq")
>>      (arguments
>> -     `(#:package "coq"
>> -       #:test-target "."))
>> +     `(#:package "coq"))
>>      (propagated-inputs
>>       (list coq-core coq-stdlib))
>>      (native-inputs '())))

I don't see how one would use coq-core without coq-stdlib and coq-stdlib depends on coq-core, so I think it's fine to merge these packages. It might make the package definition a bit harder, since there isn't a single dune target, but I'm fine with it.

Le 24 juillet 2023 16:54:05 GMT+02:00, pukkamustard <pukkamustard@posteo.net> a écrit :
>
>Hi,
>
>Julien Lepiller <julien@lepiller.eu> writes:
>
>> I'm not sure why, but this is breaking all coq dependents, with
>> messages similar to:
>>
>> cannot guess a path for Coq libraries; please use -coqlib option or
>> ensure you have installed the package containing Coq's stdlib
>> (coq-stdlib in OPAM) If you intend to use Coq without a standard
>> library, the -boot -noinit options must be used.
>>
>> I think this is because coq-stdlib is mostly empty for some reason.
>
>A couple of build failures later this is where I'm at:
>
>- Coq 8.17.1 includes considerable changes to the build system.
>
>- Some `dune` files are autogenerated with `make dunestrap` (which runs
>  the OCaml program `tools/dune_rule_gen/gen_rules.ml`.
>
>- In the v3 patches I submitted `make dunestrap` was not being run,
>  resulting in missing dune files and a quite empty `coq-stdlib`
>  package.
>
>- The 8.17.1 generated dune files for `coq-stdlib` reference things in
>  `coq-core` directly with relative paths instead of letting
>  dune/findlib find them (with entries in the `libraries` stanza in dune
>  files). This makes building `coq-core` and `coq-stdlib` seperately
>  more tricky.
>
>I've asked in #coq for ideas on how `coq-stdlib` and `coq-core` can be
>built seperately/kept in separate packages. Nothing yet.
>
>What do you think about merging `coq-core`, `coq-stdlib` and `coq` into
>a single package? Not as nice as the current situation, but maybe a way
>to go without too many custom patches/hacks?
>
>CC: Arnaud and Josselin who might be interested in Coq stuff.
>
>Thanks,
>pukkamustard
>
>
>>> * gnu/packages/coq.scm (coq-core, coq-stdlib, coq): Update to 8.17.1
>>> and remove test-target argument.
>>> ---
>>>  gnu/packages/coq.scm | 24 +++++-------------------
>>>  1 file changed, 5 insertions(+), 19 deletions(-)
>>> 
>>> diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
>>> index 09ca4030ea..3332707a71 100644
>>> --- a/gnu/packages/coq.scm
>>> +++ b/gnu/packages/coq.scm
>>> @@ -53,7 +53,7 @@ (define-module (gnu packages coq)
>>>  (define-public coq-core
>>>    (package
>>>      (name "coq-core")
>>> -    (version "8.16.1")
>>> +    (version "8.17.1")
>>>      (source
>>>       (origin
>>>         (method git-fetch)
>>> @@ -63,7 +63,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
>>> @@ -83,8 +83,7 @@ (define-public coq-core
>>>      (native-inputs
>>>       (list ocaml-ounit2 which))
>>>      (arguments
>>> -     `(#:package "coq-core"
>>> -       #:test-target "."))
>>> +     `(#:package "coq-core"))
>>>      (properties '((upstream-name . "coq"))) ; also for inherited
>>> packages (home-page "https://coq.inria.fr")
>>>      (synopsis "Proof assistant for higher-order logic")
>>> @@ -101,19 +100,7 @@ (define-public coq-stdlib
>>>      (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"))
>>> -                  " "))))))))
>>> +     `(#:package "coq-stdlib"))
>>>      (inputs
>>>       (list coq-core gmp ocaml-zarith))
>>>      (native-inputs '())))
>>> @@ -123,8 +110,7 @@ (define-public coq
>>>      (inherit coq-core)
>>>      (name "coq")
>>>      (arguments
>>> -     `(#:package "coq"
>>> -       #:test-target "."))
>>> +     `(#:package "coq"))
>>>      (propagated-inputs
>>>       (list coq-core coq-stdlib))
>>>      (native-inputs '())))
>