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

[Garek Dyszel via Guix-patches via <guix-patches@gnu.org>]

I'm in UTC-0400, so your first email arrived in my inbox at around
04:00. Sorry I didn't see these!

At 10:17 2022-11-13 UTC+0100, Julien Lepiller wrote:
>> I tried building your file (it's technically not a manifest) and
>> indeed it's failing in the chack-findlib-path.

You're right that it's not a manifest. I had put a (packages->manifest)
invocation at the end of the file to see why coq-elpi wasn't building.
Later I just threw a package at the end when testing it later, and
forgot that the file then became a package file.

>> Why do you want to run it?

I knew that ocamlfind wasn't able to find the file coq-elpi.elpi when
building coq-mathcomp-hierarchy-builder. I was trying to test for the
presence of that file...

>> There's no way it could work at this point, right after the check
>> phase, since the package is not even installed yet.

...and I thought that the phase 'check' came after the phase 'install'
for some reason :/

>> Also, the OCAMLPATH that would allow findlib to find it is not set to
>> the outputs, only to the inputs.

Looks like I'll need to take a closer look at ocaml-build-system!

At 11:53 2022-11-13 UTC+0100, Julien Lepiller wrote:
> 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.

Tweaking the make-flags is exactly what's been occupying my time for the
last few months off and on, yep :)

> Attached is the fixed version of your file that builds
> coq-mathcomp-analysis.

Wow! Thanks so much! I can finally move to using it instead of building
it, although trying to get it to build was still a lot of fun :)

> Note that the build of mathcomp-analysis is
> very quiet and takes a long time, but it works eventually.

For anybody else who might be reading this thread, it took about 12
minutes to build on my system. I ran 'guix gc' beforehand to get an
accurate number:
$ until guix gc && time guix build -Kf coq-mathcomp-analysis.scm;\
$ do sleep 0.1; done
...

real	11m18.769s
user	0m7.332s
sys	0m0.490s

Out of curiosity, where did you put the patch file so that (patches
(search-patches "ocaml-elpi-fix-yojson.patch")) worked? My system throws
this error, so I had to switch the patch's path back: "guix build:
error: ocaml-elpi-fix-yojson.patch: patch not found".