From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp11.migadu.com ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms5.migadu.com with LMTPS id yHcHMX0LAmMt/gAAbAwnHQ (envelope-from ) for ; Sun, 21 Aug 2022 12:39:57 +0200 Received: from aspmx1.migadu.com ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp11.migadu.com with LMTPS id 2HQOMX0LAmM/rgAA9RJhRA (envelope-from ) for ; Sun, 21 Aug 2022 12:39:57 +0200 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 709F9C27F for ; Sun, 21 Aug 2022 12:39:57 +0200 (CEST) Received: from localhost ([::1]:55478 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1oPiN2-00071A-Id for larch@yhetil.org; Sun, 21 Aug 2022 06:39:56 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:54174) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1oPiMQ-0006rN-2k for help-guix@gnu.org; Sun, 21 Aug 2022 06:39:18 -0400 Received: from knopi.disroot.org ([178.21.23.139]:39816) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1oPiML-0005hW-Vg for help-guix@gnu.org; Sun, 21 Aug 2022 06:39:17 -0400 Received: from localhost (localhost [127.0.0.1]) by disroot.org (Postfix) with ESMTP id E4BEB400C7; Sun, 21 Aug 2022 12:39:09 +0200 (CEST) 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 Oa-qmaSTlQdB; Sun, 21 Aug 2022 12:39:08 +0200 (CEST) Mime-Version: 1.0 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail; t=1661078348; bh=TvUPBPEoRmL0CZiExKYa5c+rsy9HbGWPIAUApgSQcZM=; h=Date:Subject:From:To:References:In-Reply-To; b=f8lHSXxoGbjRmx8ku2v0NgFWSOVhgC5Nw68NXr1sjN/ZUxFkXmZAkc9Rrh3oCBdOw RKiOx052wd5IgQgycRQzQWCI/iP+zpKViIrRp6LXyBz3WrSx1XHvpgSc0iSirIxw20 Ra/Lkh4LRo6RdqJaCuZjuEzRubJm19+gCBkTtC8UWWQeSsDFMujnWex/H78ka9uwJ/ KgrzNbZpDi2g+/qQKULnwQ/q/x74cOa88TUt5JChCkTPD8cC0B6QXtqCGwW/4t4LM2 a40hBYXGLPLoTKgMwikwrIH2eWqTMgMwO5vTh9l3KDMTs9P8RBqCWH85BD84zJ5/2x Q4z3qNgPj+BBw== Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=UTF-8 Date: Sun, 21 Aug 2022 11:39:08 +0100 Message-Id: Subject: Re: Packaging Idris2 From: "(" To: "Andreas Reuleaux" , "help-guix" References: <138fc06ac78045c4a7117566484ebb936caff178.camel@phfrohring.com> <87r11aeot8.fsf@riseup.net> <871qta8tgp.fsf@softland> <87zgfxrj6f.fsf@softland> In-Reply-To: <87zgfxrj6f.fsf@softland> Received-SPF: pass client-ip=178.21.23.139; envelope-from=paren@disroot.org; helo=knopi.disroot.org X-Spam_score_int: -20 X-Spam_score: -2.1 X-Spam_bar: -- X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, SPF_HELO_NONE=0.001, SPF_PASS=-0.001, T_SCC_BODY_TEXT_LINE=-0.01 autolearn=ham autolearn_force=no X-Spam_action: no action X-BeenThere: help-guix@gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: help-guix-bounces+larch=yhetil.org@gnu.org Sender: "Help-Guix" X-Migadu-Flow: FLOW_IN X-Migadu-To: larch@yhetil.org X-Migadu-Country: US ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1661078397; h=from:from:sender:sender:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:mime-version:mime-version: content-type:content-type: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references:list-id:list-help: list-unsubscribe:list-subscribe:list-post:dkim-signature; bh=AgFl7EUU7466Hhkt+lo+Bj+jir9ruqg8G8tYKRAck3Q=; b=NSQ6jEfsRYqQiQ9ZlZ0s3T11EpPNv5M6sw3ZLB/oetBtabruIYYr9AQBXcQAD/Wu/dC11B byIfNZkpMrr/wpSlc1P66I5i9CBnsCyDGPTQsNr3W9thWynIMyfFBlMvAnHxIBSaFQAXyW TFRVXZH3hOMh5TuZ+l2Rfpev5OPvEmtwJgF/d1oR4LTk0CVHvNj08Ywh/pymwNGWdrCZPf fxWmLADAxR9uIVxBgBDclhgR6UcZrP08zV3L/QqhxGw3U1HVwX4jMKb9QAkwVtgCq7tIFp ci8E7HmB62fivEWKacO6zxplyMXM5+4bJltY5iBcLY4HxejjW4LPmLQYII+EGw== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1661078397; a=rsa-sha256; cv=none; b=MCQ3ihI92YiH2OWstB1uheRNtVRDeWEQPG+m2hGeZtXe9Cl0QNDav1a+syGqaQdCdOoRWD 5VPxnFx77c/LQi+i53A13JzQgPMB8QDr2yd8kEMQT21b4DcMbOviMBYw7TDLGKCCFBBdPZ pT8i+MEOUUbAoorc0LFAc9gBd13cWE6/3xOWnMa+lvtFREw8vkYOgJOVTFPNDjLvsacaF8 PG0qbk0Rt2NHaFPIhcuiAFac83bVpelLAidb2s7kbiEHu4UPmsw5M+eUNFHOrUulcYzdqs Gdr/QCiIZc7OTLYe9CthvjzbDrLKTvYLsoEJv6j96uMJc3LF8XDf+e5vTa+nSQ== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=pass header.d=disroot.org header.s=mail header.b=f8lHSXxo; dmarc=pass (policy=quarantine) header.from=disroot.org; spf=pass (aspmx1.migadu.com: domain of "help-guix-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="help-guix-bounces+larch=yhetil.org@gnu.org" X-Migadu-Spam-Score: -1.33 Authentication-Results: aspmx1.migadu.com; dkim=pass header.d=disroot.org header.s=mail header.b=f8lHSXxo; dmarc=pass (policy=quarantine) header.from=disroot.org; spf=pass (aspmx1.migadu.com: domain of "help-guix-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="help-guix-bounces+larch=yhetil.org@gnu.org" X-Migadu-Queue-Id: 709F9C27F X-Spam-Score: -1.33 X-Migadu-Scanner: scn1.migadu.com X-TUID: 46fQ9rygniha On Sun Aug 21, 2022 at 11:21 AM BST, Andreas Reuleaux wrote: > (And by the way: the pregenerated scheme in there is not a binary, > it is readable scheme code after all - well not terribly readable, > but nevertheless). Yes, that's true -- however, it's still not the complete, readable source code. (It presumably doesn't have comments either, which greatly aid understanding, of course.) We do make exceptions when bootstrapping is simply impossible with currently existing tools (see Haskell, Pascal, and Nim) but here, where it does seem to be possile,=20 > What is won with the extra step of having an older Idris2 installed > first, that still compiles with Idris 1 - And then do what with that: > compile a newer Idris2 from that (that may still not be sufficiant > to compile the latest Idris2), ... Reproducibility ? - Certainly > not simplicity! You can't trust pregenerated source, as it's usually far more difficult to read (especially in the case where it's a binary), so Guix tries to build everything from source as much as possible, even when the generated files are textual. See . -- (