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

From: Julien Lepiller <[email-masked]>
Date: Sun, 13 Nov 2022 11:53:03 +0100

So, I've had a further look at the sources for the failing packages and
figured that some variables were missing in the make-flags. Attached is
the fixed version of your file that builds coq-mathcomp-analysis. Note
that the build of mathcomp-analysis is very quiet and takes a long time,
but it works eventually.

Le Sun, 13 Nov 2022 10:17:07 +0100,
Julien Lepiller <[email-masked]> a écrit :

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