GNU bug report logs -
#58310
[PATCH] Add coq-mathcomp-analysis
Previous Next
Full log
Message #95 received at 58310 <at> debbugs.gnu.org (full text, mbox):
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".
This bug report was last modified 2 years and 218 days ago.
Previous Next
GNU bug tracking system
Copyright (C) 1999 Darren O. Benham,
1997,2003 nCipher Corporation Ltd,
1994-97 Ian Jackson.