From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp2.migadu.com ([2001:41d0:303:e16b::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms13.migadu.com with LMTPS id OEFnOBqOVGd9PwAAe85BDQ:P1 (envelope-from ) for ; Sat, 07 Dec 2024 18:04:26 +0000 Received: from aspmx1.migadu.com ([2001:41d0:303:e16b::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp2.migadu.com with LMTPS id OEFnOBqOVGd9PwAAe85BDQ (envelope-from ) for ; Sat, 07 Dec 2024 19:04:11 +0100 X-Envelope-To: larch@yhetil.org Authentication-Results: aspmx1.migadu.com; dkim=pass header.d=debbugs.gnu.org header.s=debbugs-gnu-org header.b=JuV+X2gJ; dkim=fail ("headers rsa verify failed") header.d=antr.me header.s=zmail header.b="Eqtl/m5A"; arc=reject ("signature check failed: fail, {[1] = sig:zohomail.com:reject}"); dmarc=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" ARC-Seal: i=2; s=key1; d=yhetil.org; t=1733594650; a=rsa-sha256; cv=fail; b=c5lKWwxvZ4zNY6HsMXPAxC6tdSq0kiTAjN1BVX04rCrIyuRBX67+WBXZvvKJCDh0ICIHce 0Z9sY2wa/MGqLjdfAuomm4Bfa1tKJuOdKgdeMYAfEEBlgQW2AzpCjPJyDxLs27oUpjcAQq AWDXegFy7s7KuNgta1e7E5Sviq4nWnx4vz23OZPitKYPRZyFIne1ZmX1UqOA1RqbXa2JQV A6b2Ye4mkpDOP7fXC/d4aqmuHH0vyzN6eRQXSHykNTLDwdANiE9xXbv2Zsabp8+ldRjMVK Mfx3PYiOBMD5UqTt/fB3lw67DkJnWZ/lOTljBTR1C5xDi1d9RW0lHmuHXxZu0w== ARC-Authentication-Results: i=2; aspmx1.migadu.com; dkim=pass header.d=debbugs.gnu.org header.s=debbugs-gnu-org header.b=JuV+X2gJ; dkim=fail ("headers rsa verify failed") header.d=antr.me header.s=zmail header.b="Eqtl/m5A"; arc=reject ("signature check failed: fail, {[1] = sig:zohomail.com:reject}"); dmarc=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" ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1733594650; 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=nPjcnG/s0Es8yHiCcmq34mS+ojsssLfMz4VCGHEv1yM=; b=ni923ETEkaKn768t9Y11IdPX8VzA0tCTmtXhyGw+hh3GOxjBZQZV0LqPr/N4YWvLBYi1Ym 4SXxyk11+TGxjxb1aVXTFk3oa2Oh97BLkCJcYkzxRWIuqBQ4k5QNgo5U/t3+ELzK/hTptK hfPkUTjEnjusawQCrUxVu+eJOhZNQ+CBsN62iLQS0ub+pH0bsuD+Prx2zpWxFnGpr/zlY6 JFy2AZNtWVsY+gKKwpZ/PBQbXNYMOdFGbY+E9mb3H5jFU4p9dWAu+c+f+N4YFzueKxYmQN BlmmsGmgrMB4M8RenZXyc4QPuIYjPKClJEa+FKC78jt4QlK5wnJ9NdUmDC2g2g== 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 72C068011F for ; Sat, 07 Dec 2024 19:04:10 +0100 (CET) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1tJz9x-00007p-0t; Sat, 07 Dec 2024 13:04: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 1tJz9u-00006T-Dz for guix-patches@gnu.org; Sat, 07 Dec 2024 13:04:02 -0500 Received: from debbugs.gnu.org ([2001:470:142:5::43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1tJz9u-0008RK-1j for guix-patches@gnu.org; Sat, 07 Dec 2024 13:04:02 -0500 DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=debbugs.gnu.org; s=debbugs-gnu-org; h=MIME-Version:Date:References:In-Reply-To:From:To:Subject; bh=nPjcnG/s0Es8yHiCcmq34mS+ojsssLfMz4VCGHEv1yM=; b=JuV+X2gJ8og+gKhpDFi1MOeKnG5uus6ZqDyA62vvdZbQLQpVdoDibjO0xPdXW7m6ann3Iax3r7yZNSjqD1gDHrLLXiUi98tWNSZ8u8sSAZIyPhJKPntv23ExKXJegZI3uRhiHY5kc3nipAWcqCBEh471eutzpCGjTM6DAKzsuLOTbN8SqYBJgmOwSv3XDL3zNNEApSkTSH+PzPg5J1X5DVEMg4Thw0LAqu9jkL3ZAiiwdwtNQhFM1xI+HHVOfS3ZrdQlRNHbfmpMbmj9xG2t0Qpc7zrrDIzxIK3S2sKg6tP4tUmrHU5BkMQd6F7ttEfXev4ERWce04HbpyMht5h74g==; Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1tJz9t-0002bu-SG for guix-patches@gnu.org; Sat, 07 Dec 2024 13:04:01 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#72755] [WIP][PATCH] guix: Add lean-build-system. Resent-From: Antero Mejr Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sat, 07 Dec 2024 18:04:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 72755 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Divya Ranjan Cc: 72755@debbugs.gnu.org Received: via spool by 72755-submit@debbugs.gnu.org id=B72755.17335946009957 (code B ref 72755); Sat, 07 Dec 2024 18:04:01 +0000 Received: (at 72755) by debbugs.gnu.org; 7 Dec 2024 18:03:20 +0000 Received: from localhost ([127.0.0.1]:48443 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1tJz9D-0002aX-VJ for submit@debbugs.gnu.org; Sat, 07 Dec 2024 13:03:20 -0500 Received: from sender4-op-o15.zoho.com ([136.143.188.15]:17504) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1tJz9B-0002aO-IK for 72755@debbugs.gnu.org; Sat, 07 Dec 2024 13:03:18 -0500 ARC-Seal: i=1; a=rsa-sha256; t=1733594585; cv=none; d=zohomail.com; s=zohoarc; b=gfoBzgcLIliXVweCo9Xvkbxkmd2A3haqfayBzIEZW03RgztbAjhjBONTLV9bCi/OaKdTLg+1xRietbfB3HMojHy3kSO8dcWMA5aXtIT6HWdW4eFwdfO2vPirdVU03ZFjlVsvYmuJhMEYbqycm+KRImKzu7ziLeHb+cNLYPlHHA0= ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=zohomail.com; s=zohoarc; t=1733594585; h=Content-Type:Content-Transfer-Encoding:Cc:Cc:Date:Date:From:From:In-Reply-To:MIME-Version:Message-ID:References:Subject:Subject:To:To:Message-Id:Reply-To; bh=nPjcnG/s0Es8yHiCcmq34mS+ojsssLfMz4VCGHEv1yM=; b=jBWsGEPPKCdgZideOhlBsBhU6h+O18AWg+rCtG8RLt493QEWAbkCAJyG59fzy57Ctqmb2ggxeW6c3Til9J7wt/CDGaB6WpJ7aQ3eMIeNhGQFtEs6JLoFxoXfTSy/8FlLZNt1CVrRAUR4NbMWqd/mVAbKTFbdzW6vn8/yaGzSjrw= ARC-Authentication-Results: i=1; mx.zohomail.com; dkim=pass header.i=antr.me; spf=pass smtp.mailfrom=mail@antr.me; dmarc=pass header.from= DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; t=1733594585; s=zmail; d=antr.me; i=mail@antr.me; h=From:From:To:To:Cc:Cc:Subject:Subject:In-Reply-To:References:Date:Date:Message-ID:MIME-Version:Content-Type:Content-Transfer-Encoding:Message-Id:Reply-To; bh=nPjcnG/s0Es8yHiCcmq34mS+ojsssLfMz4VCGHEv1yM=; b=Eqtl/m5A7CkvsuDwSzOXqXbnIxls5hw6wLy7iQcveL3dfuU2VXhw1y2ycdhELe2l LK/LftWzZ/2MxfJnu0rjggFZSM9eLLUo1aZh/MkYs4+JQ3yT4mvzWp7b5bGHJOkvCs9 H4XjNdwl1bUmWTLM6Y/gihK6qHOp4M3/XsGzwPSY= Received: by mx.zohomail.com with SMTPS id 1733594583473287.0442225761236; Sat, 7 Dec 2024 10:03:03 -0800 (PST) From: Antero Mejr In-Reply-To: <87o71ovtw9.fsf@subvertising.org> (Divya Ranjan's message of "Sat, 07 Dec 2024 07:23:18 +0000") References: <8734mxnp42.fsf@antr.me> <87o71ovtw9.fsf@subvertising.org> Date: Sat, 07 Dec 2024 13:03:00 -0500 Message-ID: <87v7vv74mj.fsf@antr.me> User-Agent: Gnus/5.13 (Gnus v5.13) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-ZohoMailClient: External 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 X-Migadu-Queue-Id: 72C068011F X-Migadu-Scanner: mx13.migadu.com X-Migadu-Spam-Score: -5.55 X-Spam-Score: -5.55 X-TUID: YEFY4VRNQGBq Divya Ranjan writes: > I=E2=80=99ve also been involved in packaging Lean4, have you had any more= progress on > this? I tried to build guix from your patch, but `./pre-inst-env guix bui= ld > lean` gets stuck at some point after trying to compile things for ~7 hour= s. I > believe it gets stuck at compiling gash. Any clue? You shouldn't have to rebuild the entire dependency chain (and things like gash) to use the above patch - maybe someone on IRC or a maintainer can help with fixing that? The above patches should work for building Lean4, but packaging any Lean library with dependencies (like mathlib) won't work until the lean developers resolve this issue: https://github.com/leanprover/lean4/issues/5122 Unfortunately the devs marked it as low priority and seem to be pushing back against reproducible packaging, which is disappointing. I am unlikely to continue work on this patch series, as I have switched over to Coq.