Subject: [bug#58310] Manifest for coq-mathcomp-analysis

From: Julien Lepiller <[email-masked]>
Date: Sun, 13 Nov 2022 10:17:07 +0100

Hi!

I tried building your file (it's technically not a manifest) and indeed it's failing in the chack-findlib-path.

Why do you want to run it? There's no way it could work at this point, right after the check phase, since the package is not even installed yet. Also, the OCAMLPATH that would allow findlib to find it is not set to the outputs, only to the inputs.

Le 13 novembre 2022 00:48:50 GMT+01:00, Garek Dyszel <[email-masked]> a écrit :
>Hi,
>
>CC: ocaml team
>
>I am including a manifest file instead of sending patches for now. It
>seems like a good idea to stick with that until these packages are ready
>to be put into the Guix source tree. I'm refactoring them too often.
>
>After opening an issue on Github [1] [2], it seems that coq-elpi is the
>package that is not building properly. It is clear that ocamlfind (from
>ocaml-findlib) can't find coq-elpi after coq-elpi's install phase.
>[1]: https://github.com/math-comp/hierarchy-builder/issues/320
>[2]: https://github.com/LPCIC/coq-elpi/issues/384
>
>It looks like the META file is not being installed by coq-elpi either.
>I'm not sure whether that's relevant, since ocamlfind couldn't find
>coq-elpi even when META was present (in a much older revision of this
>manifest; I can dig for it but just today don't have time).
>
>The problem seems to be something in the build process itself; if the
>extra phase 'check-findlib-path' is omitted then coq-elpi's build is
>reported as a success.
>
>The later package coq-mathcomp-hierarchy-builder runs ocamlfind to find
>coq-elpi, too.
>
>What would be a way to ensure that coq-elpi is found by ocamlfind? 
>
>Thanks!
>Garek
>
>(Manifest attached with an ocaml-elpi patch. You will need to change the path for
>the ocaml-elpi (patches) field to match your directory structure, but otherwise
>this manifest should work.)
>