From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp10.migadu.com ([2001:41d0:2:bcc0::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms5.migadu.com with LMTPS id oHd3DGi2cGMiYQAAbAwnHQ (envelope-from ) for ; Sun, 13 Nov 2022 10:18:32 +0100 Received: from aspmx1.migadu.com ([2001:41d0:2:bcc0::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp10.migadu.com with LMTPS id 4PuBC2i2cGOAPAEAG6o9tA (envelope-from ) for ; Sun, 13 Nov 2022 10:18:32 +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 A38353C9CF for ; Sun, 13 Nov 2022 10:18:31 +0100 (CET) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ou980-0008QU-Jf; Sun, 13 Nov 2022 04:18:12 -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 ) id 1ou97q-0008Ps-Ok for guix-patches@gnu.org; Sun, 13 Nov 2022 04:18:02 -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 ) id 1ou97q-0005oR-Gw for guix-patches@gnu.org; Sun, 13 Nov 2022 04:18:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1ou97p-0003pC-Vu for guix-patches@gnu.org; Sun, 13 Nov 2022 04:18:01 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#58310] Manifest for coq-mathcomp-analysis Resent-From: Julien Lepiller Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 13 Nov 2022 09:18:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 58310 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Garek Dyszel , zimoun , 58310@debbugs.gnu.org Cc: pukkamustard Received: via spool by 58310-submit@debbugs.gnu.org id=B58310.166833103614643 (code B ref 58310); Sun, 13 Nov 2022 09:18:01 +0000 Received: (at 58310) by debbugs.gnu.org; 13 Nov 2022 09:17:16 +0000 Received: from localhost ([127.0.0.1]:50065 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ou975-0003o7-Or for submit@debbugs.gnu.org; Sun, 13 Nov 2022 04:17:16 -0500 Received: from lepiller.eu ([89.234.186.109]:36142) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ou973-0003nv-19 for 58310@debbugs.gnu.org; Sun, 13 Nov 2022 04:17:14 -0500 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id 1f3cc262; Sun, 13 Nov 2022 09:17:10 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=date:from :to:cc:subject:in-reply-to:references:message-id:mime-version :content-type:content-transfer-encoding; s=dkim; bh=J8pvBhghCTBa 24YuOcA2hwXeCjP29Rpy25j19HpNMoY=; b=K2GvhwuDI/xW7v1H05cAWH2dWAkk XVHYUIac4oIu2Csj5g1Pi5Ha9Qk0ijR4+FzhsVaEvDTVeQOx7H+F2HV96EP7nb0Q nCQXt5jFGY7QSuLfKmtdKZAO80uzaET7UcX/rg4w4ubrRagPwzYSeIwgwtieGN6v y6BtYDOsNeQdQtLAkb/rrtkwvvXZQAb+fU7TZYyGc3KDMXh1LwAgxJjan16nl+4K cDxnSjHylH7JWryXNqsLZSe5TvXv7tnpRtXuDvB26I7ze2N0nxCHlWfCOVjEW8gc ERjfB1Krx26LVGmW2908ubML7Th0D9Bk90BVon7rxBUcJ8G/1BAYCz2p/g== Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id 5db1b513 (TLSv1.3:AEAD-AES256-GCM-SHA384:256:NO); Sun, 13 Nov 2022 09:17:10 +0000 (UTC) Date: Sun, 13 Nov 2022 10:17:07 +0100 From: Julien Lepiller User-Agent: K-9 Mail for Android In-Reply-To: <87v8njspi5.fsf@disroot.org> References: <87h70iqji2.fsf@disroot.org> <87v8njspi5.fsf@disroot.org> Message-ID: MIME-Version: 1.0 Content-Type: multipart/alternative; boundary=----VEXPOYMVGO9M0GJPBXQXP1DBARXM2G Content-Transfer-Encoding: 7bit X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , 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=1668331112; h=from:from:sender:sender:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:cc:mime-version:mime-version: content-type:content-type: content-transfer-encoding:content-transfer-encoding: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=J8pvBhghCTBa24YuOcA2hwXeCjP29Rpy25j19HpNMoY=; b=nyeljvDC8Kn+2Q7q8HTIZhYGjlbi+AZX2oSSRL5aFkuA0whQULv1NueVCiTCs/9zQD2X31 UcxXvUTHB+gTg+OqBbIkLvOejfPV0feLAyJCUKkiLeAPCKUNmARCx+UtV6e8iF6fOC/ZwR UAtrTnZMWPmAVI0Bm1NrEll2vXZ/8NpAkMU79mh+g5Q0V015moBVUg7jArPnKmkH7zIIHY B0jsGaYB3o+lxVVdQW+Z6ottHYGqSQhmYgVkY9kHM4Fg2gySw6/uYmsXdUqR7FByNsQ9HQ +fKN6KUmfJgwEe0ajzuI9/oRACQiuGvYtk4UG6VSv0cHvWun1/AiBruEP4fONA== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1668331112; a=rsa-sha256; cv=none; b=ZiTfuSwJ6HN3f4m5l0YBBFoY6DxXkwccdl5Hy3oAaReA5+PD6D2Tm4ecl85fQQ9f6shs0r g87MI9RS/osxGAHIcYFcw60Mox0p3XliwdZItmMHXE8ix3goYXwcMAN/Srmml7+8XothBu 1E52oygfSLgtyaVpWC3LWyQ9dlYy/ckZrteDvd2LctqWnhaa0JCbVre9eyy4T6LWv9m9CG kDliYUqv5V4Hjeh+W4wecjBgxWKIrT4DzI2eyvGNMvNCSuibYmEEcAYCRrvqF2fkKnAq/T z2AT12k+n72OjcYS75+w0yvuJV5+BMT8B1Msk0TNvVhDMCLL29eMJ6Onh2ulAQ== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=lepiller.eu header.s=dkim header.b=K2GvhwuD; dmarc=fail reason="SPF not aligned (relaxed)" header.from=lepiller.eu (policy=none); 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: 7.85 Authentication-Results: aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=lepiller.eu header.s=dkim header.b=K2GvhwuD; dmarc=fail reason="SPF not aligned (relaxed)" header.from=lepiller.eu (policy=none); 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: A38353C9CF X-Spam-Score: 7.85 X-Migadu-Scanner: scn0.migadu.com X-TUID: gvC8YOvBdTpM ------VEXPOYMVGO9M0GJPBXQXP1DBARXM2G Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Hi! I tried building your file (it's technically not a manifest) and indeed it= 's failing in the chack-findlib-path=2E Why do you want to run it? There's no way it could work at this point, rig= ht after the check phase, since the package is not even installed yet=2E Al= so, the OCAMLPATH that would allow findlib to find it is not set to the out= puts, only to the inputs=2E Le 13 novembre 2022 00:48:50 GMT+01:00, Garek Dyszel a =C3=A9crit=C2=A0: >Hi, > >CC: ocaml team > >I am including a manifest file instead of sending patches for now=2E It >seems like a good idea to stick with that until these packages are ready >to be put into the Guix source tree=2E I'm refactoring them too often=2E > >After opening an issue on Github [1] [2], it seems that coq-elpi is the >package that is not building properly=2E It is clear that ocamlfind (from >ocaml-findlib) can't find coq-elpi after coq-elpi's install phase=2E >[1]: https://github=2Ecom/math-comp/hierarchy-builder/issues/320 >[2]: https://github=2Ecom/LPCIC/coq-elpi/issues/384 > >It looks like the META file is not being installed by coq-elpi either=2E >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)=2E > >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=2E > >The later package coq-mathcomp-hierarchy-builder runs ocamlfind to find >coq-elpi, too=2E > >What would be a way to ensure that coq-elpi is found by ocamlfind?=20 > >Thanks! >Garek > >(Manifest attached with an ocaml-elpi patch=2E You will need to change th= e path for >the ocaml-elpi (patches) field to match your directory structure, but oth= erwise >this manifest should work=2E) > ------VEXPOYMVGO9M0GJPBXQXP1DBARXM2G Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable Hi!

I tried building your file (it's techni= cally not a manifest) and indeed it's failing in the chack-findlib-path=2E<= br>
Why do you want to run it? There's no way it could work at this poin= t, right after the check phase, since the package is not even installed yet= =2E Also, the OCAMLPATH that would allow findlib to find it is not set to t= he outputs, only to the inputs=2E

Le 13 n= ovembre 2022 00:48:50 GMT+01:00, Garek Dyszel <garekdyszel@disroot=2Eorg= > a =C3=A9crit=C2=A0:
Hi,

CC: ocaml team

I am i=
ncluding a manifest file instead of sending patches for now=2E It
seems =
like a good idea to stick with that until these packages are ready
to be=
 put into the Guix source tree=2E I'm refactoring them too often=2E

=
After opening an issue on Github [1] [2], it seems that coq-elpi is the
=
package that is not building properly=2E It is clear that ocamlfind (fromocaml-findlib) can't find coq-elpi after coq-elpi's install phase=2E
[=
1]: https://github=2Ecom/math-comp/hierarchy-builder/issues/320
[2]: https://github=2Ec=
om/LPCIC/coq-elpi/issues/384

It looks like the META file is not =
being installed by coq-elpi either=2E
I'm not sure whether that's releva=
nt, since ocamlfind couldn't find
coq-elpi even when META was present (i=
n a much older revision of this
manifest; I can dig for it but just toda=
y don't have time)=2E

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=2E

The later package c=
oq-mathcomp-hierarchy-builder runs ocamlfind to find
coq-elpi, too=2E
What would be a way to ensure that coq-elpi is found by ocamlfind? 
Thanks!
Garek

(Manifest attached with an ocaml-elpi patch=2E=
 You will need to change the path for
the ocaml-elpi (patches) field to =
match your directory structure, but otherwise
this manifest should work=
=2E)

------VEXPOYMVGO9M0GJPBXQXP1DBARXM2G--