From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 ) for ; 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 ) for ; 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 ; 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 ) 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 ) 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 ) 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 ) 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 Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 13 Nov 2022 18:55:02 +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: Julien Lepiller , zimoun , 58310@debbugs.gnu.org Cc: pukkamustard 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 ) 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 ) 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> <87v8njspi5.fsf@disroot.org> <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: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Reply-to: Garek Dyszel X-ACL-Warn: , Garek Dyszel via Guix-patches From: Garek Dyszel via Guix-patches via 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".