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

[Julien Lepiller <julien@lepiller.eu>]

[-- Attachment #1: Type: text/plain, Size: 2821 bytes --]

There's a trick for patches: they are loaded from the search path, so you can add the file to any empty directory and add that directory to the load path.

For instance, if you have ~/guix-patches/my.patch, then you can build a package that looks for my.patch with:

guix build -L ~/guix-patches

Le 13 novembre 2022 19:54:03 GMT+01:00, Garek Dyszel <garekdyszel@disroot.org> a écrit :
>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".
>

[-- Attachment #2: Type: text/html, Size: 4568 bytes --]