From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <guix-patches-bounces+larch=yhetil.org@gnu.org>
Received: from mp11.migadu.com ([2001:41d0:8:6d80::])
	(using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits))
	by ms5.migadu.com with LMTPS
	id wEzcBps9cWPo1QAAbAwnHQ
	(envelope-from <guix-patches-bounces+larch=yhetil.org@gnu.org>)
	for <larch@yhetil.org>; Sun, 13 Nov 2022 19:55:23 +0100
Received: from aspmx1.migadu.com ([2001:41d0:8:6d80::])
	(using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits))
	by mp11.migadu.com with LMTPS
	id mEoDBps9cWNQZgEA9RJhRA
	(envelope-from <guix-patches-bounces+larch=yhetil.org@gnu.org>)
	for <larch@yhetil.org>; Sun, 13 Nov 2022 19:55:23 +0100
Received: from lists.gnu.org (lists.gnu.org [209.51.188.17])
	(using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits))
	(No client certificate requested)
	by aspmx1.migadu.com (Postfix) with ESMTPS id CC81A245FA
	for <larch@yhetil.org>; Sun, 13 Nov 2022 19:55:22 +0100 (CET)
Received: from localhost ([::1] helo=lists1p.gnu.org)
	by lists.gnu.org with esmtp (Exim 4.90_1)
	(envelope-from <guix-patches-bounces@gnu.org>)
	id 1ouI8H-0001aq-Nc; Sun, 13 Nov 2022 13:55:05 -0500
Received: from eggs.gnu.org ([2001:470:142:3::10])
 by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
 (Exim 4.90_1) (envelope-from <Debian-debbugs@debbugs.gnu.org>)
 id 1ouI8F-0001aM-57
 for guix-patches@gnu.org; Sun, 13 Nov 2022 13:55:03 -0500
Received: from debbugs.gnu.org ([209.51.188.43])
 by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
 (Exim 4.90_1) (envelope-from <Debian-debbugs@debbugs.gnu.org>)
 id 1ouI8E-0002aI-T8
 for guix-patches@gnu.org; Sun, 13 Nov 2022 13:55:02 -0500
Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2)
 (envelope-from <Debian-debbugs@debbugs.gnu.org>) id 1ouI8E-0002tj-Ka
 for guix-patches@gnu.org; Sun, 13 Nov 2022 13:55:02 -0500
X-Loop: help-debbugs@gnu.org
Subject: [bug#58310] Manifest for coq-mathcomp-analysis
Resent-From: Garek Dyszel <garekdyszel@disroot.org>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces@debbugs.gnu.org>
Resent-CC: guix-patches@gnu.org
Resent-Date: Sun, 13 Nov 2022 18:55:02 +0000
Resent-Message-ID: <handler.58310.B58310.166836566111085@debbugs.gnu.org>
Resent-Sender: help-debbugs@gnu.org
X-GNU-PR-Message: followup 58310
X-GNU-PR-Package: guix-patches
X-GNU-PR-Keywords: patch
To: Julien Lepiller <julien@lepiller.eu>, zimoun <zimon.toutoune@gmail.com>,
 58310@debbugs.gnu.org
Cc: pukkamustard <pukkamustard@posteo.net>
Received: via spool by 58310-submit@debbugs.gnu.org id=B58310.166836566111085
 (code B ref 58310); Sun, 13 Nov 2022 18:55:02 +0000
Received: (at 58310) by debbugs.gnu.org; 13 Nov 2022 18:54:21 +0000
Received: from localhost ([127.0.0.1]:48356 helo=debbugs.gnu.org)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <debbugs-submit-bounces@debbugs.gnu.org>)
 id 1ouI7Z-0002si-FP
 for submit@debbugs.gnu.org; Sun, 13 Nov 2022 13:54:21 -0500
Received: from knopi.disroot.org ([178.21.23.139]:36664)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <garekdyszel@disroot.org>) id 1ouI7X-0002sZ-8W
 for 58310@debbugs.gnu.org; Sun, 13 Nov 2022 13:54:20 -0500
Received: from localhost (localhost [127.0.0.1])
 by disroot.org (Postfix) with ESMTP id 5DA464109F;
 Sun, 13 Nov 2022 19:54:17 +0100 (CET)
X-Virus-Scanned: SPAM Filter at disroot.org
Received: from knopi.disroot.org ([127.0.0.1])
 by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024)
 with ESMTP id tsR6Dc4vqlPE; Sun, 13 Nov 2022 19:54:16 +0100 (CET)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail;
 t=1668365656; bh=7owb286lg1W+KRlDux9HwDBAsNVSSlcMbNEXDPRA1SA=;
 h=From:To:Cc:Subject:In-Reply-To:References:Date:From;
 b=TmC1ecQ4pjpLKHg2hGkOCIFQDO6auhAs9nGI39CBgUWaVE6IHzPV03vXbwMnFmtu2
 9Uc/01AV7xNH2cIuLos1ujvmL5tSABdr9rwONFy7L1uRNmLwRNx+1enRYUNiJJBqGe
 5w7R3+QW5gfWd2OfpceaefjR3V/fTiSkG0/9VcoVXsDxDmtAPPQJwTa00lHUWN1XdN
 AbgWPdJA9em0XBC0ZEYSMF+t9DpglxX97g9K5iZvhd2LWCIMud10TxxRhx96j/S1q2
 KPMaXMEvZb7SdXGChHbv3PLviRrgApaa9Eyt4gXASSq3xiLeTZw56FCbAC69glYr9E
 VnVQr6c6Rs66A==
In-Reply-To: <20221113115303.66ccb071@sybil.lepiller.eu>
References: <87h70iqji2.fsf@disroot.org>
 <handler.58310.B.166499048624567.ack@debbugs.gnu.org>
 <87v8njspi5.fsf@disroot.org>
 <A2D9782B-4542-4403-B078-51C3A2BD7640@lepiller.eu>
 <20221113115303.66ccb071@sybil.lepiller.eu>
Date: Sun, 13 Nov 2022 13:54:03 -0500
Message-ID: <87tu32eldg.fsf@disroot.org>
MIME-Version: 1.0
Content-Type: text/plain
X-BeenThere: debbugs-submit@debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
X-BeenThere: guix-patches@gnu.org
List-Id: <guix-patches.gnu.org>
List-Unsubscribe: <https://lists.gnu.org/mailman/options/guix-patches>,
 <mailto:guix-patches-request@gnu.org?subject=unsubscribe>
List-Archive: <https://lists.gnu.org/archive/html/guix-patches>
List-Post: <mailto:guix-patches@gnu.org>
List-Help: <mailto:guix-patches-request@gnu.org?subject=help>
List-Subscribe: <https://lists.gnu.org/mailman/listinfo/guix-patches>,
 <mailto:guix-patches-request@gnu.org?subject=subscribe>
Reply-to:  Garek Dyszel <garekdyszel@disroot.org>
X-ACL-Warn: ,  Garek Dyszel via Guix-patches <guix-patches@gnu.org>
From:  Garek Dyszel via Guix-patches via <guix-patches@gnu.org>
Errors-To: guix-patches-bounces+larch=yhetil.org@gnu.org
Sender: guix-patches-bounces+larch=yhetil.org@gnu.org
X-Migadu-Flow: FLOW_IN
X-Migadu-Country: US
ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org;
	s=key1; t=1668365722;
	h=from:from:sender:sender:reply-to:reply-to:subject:subject:date:date:
	 message-id:message-id:to:to:cc:cc:mime-version:mime-version:
	 content-type:content-type:resent-cc:resent-from:resent-sender:
	 resent-message-id:in-reply-to:in-reply-to:references:references:
	 list-id:list-help:list-unsubscribe:list-subscribe:list-post:
	 dkim-signature; bh=mm61Is4pINEWovsIX91dNouWir9Pstd1gj5wujHWiyA=;
	b=mhH1JYA5GEKX9eyaFp2oA5G3taDG7f8bqt04bk5C6CAr8BzKR0RnKcXLKt1E5K7kvH6i0a
	h2OIk+xz5Kcm2TbPF7EfHjxIDhl2DLTslAWfaz7zzssfSBL9MHnhjK+lBhlD0Czd+A56/h
	mUphnGbOZqBQCp4cRPM61vYDThv3eGqPyWpZTEhRQgs0wa9o/JwrIRLQB4kK6GlvWctd4P
	VG4poI/53920TtIoHX7lyBb6/D6rC9GlMXQ37T8R48NDYW4wBT0VaC9CJh18LPOx7bKaiA
	VBnk9Q3FC5SSr0IZJ/zAtTnNAmFwq0zfAy1gfpOQKwvT0oduNIhGwVkr2rJ8Ig==
ARC-Seal: i=1; s=key1; d=yhetil.org; t=1668365722; a=rsa-sha256; cv=none;
	b=R6F41lQuQtbnS7NfAz4DD2RahE7HqOCT83qqucmgZ0kz6bnVETiH9x4bKCJsv+pKGy6ph0
	1q6+kC/UTYr3lHp2BOqGNbU1G6Jt+LVXgw9AMF4DY9sIS+5I0I99YzaW0DAA3uepEGTrFw
	iuIVl9VKCge8xryTmEQXNjeiOl5/33vek/5zm5S8B4ckaSNp/U0molUelhQIRZVtImOvcr
	YCUDxLasAKnPxJ4OT1GKxq429ua+PPeUz+eDHJ7qrWYh1xPf3c244Kim+1a47F/lmfH6kP
	fIJp8etK+JOXVHyQobefknK+5Z8CsbdCdl6ErGvmmmfYh1FZycMuzQ8nDZCLMA==
ARC-Authentication-Results: i=1;
	aspmx1.migadu.com;
	dkim=fail ("headers rsa verify failed") header.d=disroot.org header.s=mail header.b=TmC1ecQ4;
	dmarc=pass (policy=none) header.from=gnu.org;
	spf=pass (aspmx1.migadu.com: domain of "guix-patches-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="guix-patches-bounces+larch=yhetil.org@gnu.org"
X-Migadu-Spam-Score: -0.55
Authentication-Results: aspmx1.migadu.com;
	dkim=fail ("headers rsa verify failed") header.d=disroot.org header.s=mail header.b=TmC1ecQ4;
	dmarc=pass (policy=none) header.from=gnu.org;
	spf=pass (aspmx1.migadu.com: domain of "guix-patches-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="guix-patches-bounces+larch=yhetil.org@gnu.org"
X-Migadu-Queue-Id: CC81A245FA
X-Spam-Score: -0.55
X-Migadu-Scanner: scn1.migadu.com
X-TUID: zHhlzskzTD2V

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