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 CIoaCJfJAmNirwAAbAwnHQ (envelope-from ) for ; Mon, 22 Aug 2022 02:11:03 +0200 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 EModCJfJAmP6hAAA9RJhRA (envelope-from ) for ; Mon, 22 Aug 2022 02:11:03 +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 706792EC02 for ; Mon, 22 Aug 2022 02:11:02 +0200 (CEST) Received: from localhost ([::1]:44058 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1oPuYz-0006Fy-K9 for larch@yhetil.org; Sun, 21 Aug 2022 19:41:05 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:45330) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1oPuYf-0006Ej-S0 for help-guix@gnu.org; Sun, 21 Aug 2022 19:40:46 -0400 Received: from out2-smtp.messagingengine.com ([66.111.4.26]:38597) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1oPuYd-0002y7-JG for help-guix@gnu.org; Sun, 21 Aug 2022 19:40:45 -0400 Received: from compute4.internal (compute4.nyi.internal [10.202.2.44]) by mailout.nyi.internal (Postfix) with ESMTP id 3DA5C5C00CB; Sun, 21 Aug 2022 19:40:41 -0400 (EDT) Received: from imap52 ([10.202.2.102]) by compute4.internal (MEProxy); Sun, 21 Aug 2022 19:40:41 -0400 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d= philipmcgrath.com; h=cc:content-transfer-encoding:content-type :date:date:from:from:in-reply-to:in-reply-to:message-id :mime-version:references:reply-to:sender:subject:subject:to:to; s=fm1; t=1661125241; x=1661211641; bh=ERDXvgHGAyZ0dmmVejCsrtick M/9D6AJ0Gax8i2/Tt0=; b=j6Z7yCfGtvPCHGDvWSJa63MTiYlgswhZyt89ujtnT zW9OhNjjPDQuk5faKtxSK8GLYH7rAUGWySDj8dqaU29DTfmaT2C+7qEH0tQHOgZZ pg7UksR3oUkt+infVvT2kYeWNcSyMeEg/5vF8tSfYsrOQUW0dD9fd7Mj5gsWfXOr FX89Ul+xrmm7sQfZvIEhDivHzw3fONPHIOXwKB/L8niEfLGU6SOkWsIJ1Ga6kEQ0 jLZIcJI2A1/8jk9gqBNUYaTWnoe1fVKCWD1pF3fEEwGt/UBWd+BOw2VJ9NdKs3I7 IizsDpGuX1rJsZmLnL+4a+jJp1DWnXWMKBmdfHPrUQSQw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d= messagingengine.com; h=cc:content-transfer-encoding:content-type :date:date:feedback-id:feedback-id:from:from:in-reply-to :in-reply-to:message-id:mime-version:references:reply-to:sender :subject:subject:to:to:x-me-proxy:x-me-proxy:x-me-sender :x-me-sender:x-sasl-enc; s=fm1; t=1661125241; x=1661211641; bh=E RDXvgHGAyZ0dmmVejCsrtickM/9D6AJ0Gax8i2/Tt0=; b=f11GFeeMeKaUZ1gQp UTByR6eUSIz0P4hcQbqmkTuEfjd1ohwCpoVygJ3b/cvnYMjDCFBeo4svxAeXtOYe 6Jyc3bmeFlVG+gx43/Plmt31m68ShcedcPbblh0FUDi32WkPpCS4fy0oeX8oVWVl ZubfWJrct7k+Klq0LEAyTjTKoQqtGKeCD02v5S08CuCE7KpXKbA6fCVbcURzPCqe Kh4OhchxZRJ2CZpBS+UDV19IPdmkx1HuU11l70cYWyioR1JFrwlHdpdOFHYuKAc6 gu9NfYJ5tnza/v4hqvo3VXNWugNFedGa9EiUNroopzrhrzSTi1kA+YBtg2NiJu0i TgRKQ== X-ME-Sender: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgedvfedrvdeiiedgvdeiucetufdoteggodetrfdotf fvucfrrhhofhhilhgvmecuhfgrshhtofgrihhlpdfqfgfvpdfurfetoffkrfgpnffqhgen uceurghilhhouhhtmecufedttdenucenucfjughrpefofgggkfgjfhffhffvufgtgfesth hqredtreerjeenucfhrhhomhepfdfrhhhilhhiphcuofgtifhrrghthhdfuceophhhihhl ihhpsehphhhilhhiphhmtghgrhgrthhhrdgtohhmqeenucggtffrrghtthgvrhhnpeehle dvhffgudffvdeujefhudetueeiveffgfdttefhtdfhueegudevhfevgfdvteenucffohhm rghinhepghhnuhdrohhrghdpghhithhhuhgsrdgtohhmpdguihhstghouhhrshgvrdhgrh houhhppdhuthgrhhdrvgguuhdpphhnphhmrdhiohenucevlhhushhtvghrufhiiigvpedt necurfgrrhgrmhepmhgrihhlfhhrohhmpehphhhilhhiphesphhhihhlihhpmhgtghhrrg hthhdrtghomh X-ME-Proxy: Feedback-ID: i2b1146f3:Fastmail Received: by mailuser.nyi.internal (Postfix, from userid 501) id C9066C6008B; Sun, 21 Aug 2022 19:40:40 -0400 (EDT) X-Mailer: MessagingEngine.com Webmail Interface User-Agent: Cyrus-JMAP/3.7.0-alpha0-841-g7899e99a45-fm-20220811.002-g7899e99a Mime-Version: 1.0 Message-Id: <9075371f-40a9-4a6b-a5f8-f4656f8007eb@www.fastmail.com> In-Reply-To: <86v8qlvku9.fsf@gmail.com> References: <138fc06ac78045c4a7117566484ebb936caff178.camel@phfrohring.com> <87r11aeot8.fsf@riseup.net> <871qta8tgp.fsf@softland> <87zgfxrj6f.fsf@softland> <86v8qlvku9.fsf@gmail.com> Date: Sun, 21 Aug 2022 19:40:20 -0400 From: "Philip McGrath" To: zimoun , "(" , "Andreas Reuleaux" , "Felix Lechner via" Subject: Re: Packaging Idris2 Content-Type: text/plain;charset=utf-8 Content-Transfer-Encoding: quoted-printable Received-SPF: pass client-ip=66.111.4.26; envelope-from=philip@philipmcgrath.com; helo=out2-smtp.messagingengine.com X-Spam_score_int: -27 X-Spam_score: -2.8 X-Spam_bar: -- X-Spam_report: (-2.8 / 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, RCVD_IN_DNSWL_LOW=-0.7, RCVD_IN_MSPIKE_H3=-0.01, RCVD_IN_MSPIKE_WL=-0.01, SPF_HELO_PASS=-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=1661127062; 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=ERDXvgHGAyZ0dmmVejCsrtickM/9D6AJ0Gax8i2/Tt0=; b=c/X+m1cdTuUX3jOs37BCWx9Z5/V0OjbYhB2P38l8dQPuoDTPdkCnnjdyaTui0dVV3NUkHY RTDHjQOXCfk4lZwtW2iPN1veFVOsCtCvU3184+cwEHl+3PxZP0jIn17QSXsRyAiL17sh27 a6EyGL9ELo4+V8tFMWczZsko+8FQv3rygWoQxGih2BgXfZYkgPku07BWXL5k8r2GA6Zcvs YLvge4t706ksUDNqYzskrHdrE2AKdQE/77gWyi6WcmrT1MC4gs4QiOv1lDx0dY/4HqzPoL 8qMHuFJjaWc5DmRDBagxa8/39UW1ST7EEl/3PWqLqllM+pxwXpzJRQIsCFoYtw== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1661127062; a=rsa-sha256; cv=none; b=A1gHCjddeqRz2Smx6/HH1/S0aFswnJWs6yN3x+qIL9NerKNNo3VeJ4JqhsuxCC4l09Xgvq ft8uewot790WCVFpWYAet9Y1Irnock1vylE8+9FkePy8LqCXnAkAj+KnrJiyshViG9N+vl TIS/ElnWaGsFKaeI63fFNsAQHXt4Z4OF669a3V2vw8q1fCcsNmtWwI2x2HYfTUG/NowRt1 8GPGqhq4roMYgF0cAxpSQ14A9Q+1HIdT2xQoEXi5M0Yc0CbVxNZE/YtTpIRYqgWmTXgmVl 7PZnexLOfpkDMcs7wO2BZTBPUJBk/GikdnAKPhbJfcgLLdiGaUV2lSXCGFeD1w== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=philipmcgrath.com header.s=fm1 header.b=j6Z7yCfG; dkim=fail ("headers rsa verify failed") header.d=messagingengine.com header.s=fm1 header.b=f11GFeeM; dmarc=none; 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: 4.39 Authentication-Results: aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=philipmcgrath.com header.s=fm1 header.b=j6Z7yCfG; dkim=fail ("headers rsa verify failed") header.d=messagingengine.com header.s=fm1 header.b=f11GFeeM; dmarc=none; 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: 706792EC02 X-Spam-Score: 4.39 X-Migadu-Scanner: scn0.migadu.com X-TUID: mjXdr3qW1v2S Hi, On Sun, Aug 21, 2022, at 8:31 AM, zimoun wrote: > Hi, > > Some quick comments. :-) > > On Sun, 21 Aug 2022 at 11:39, "(" wrote: > >> Yes, that's true -- however, it's still not the complete, readable >> source code. (It presumably doesn't have comments either, which great= ly >> aid understanding, of course.) We do make exceptions when bootstrappi= ng >> is simply impossible with currently existing tools (see Haskell, Pasc= al, >> and Nim) but here, where it does seem to be possile,=20 > > [...] > > b) =C2=ABit does seem to be possible=C2=BB but it had not been done si= nce 1.5 > years. Maybe it would be better to have something now instead than > never; then it would be still possible to improve the situation. IMHO. > I strongly agree with this. The emphasis Guix places on bootstrapping and the incredible work the co= mmunity has put into finding or creating bootstrapping tools are extreme= ly valuable. Even so, I think it would be counterproductive for Guix to = make a barrier to entry out of bootstrapping things that no one actually= knows how to bootstrap. I think that applies also in this case, where i= t seems like there's a possible path to bootstrapping, but it isn't work= ing yet despite reasonable effort: indeed, more than reasonable effort. = (I can only imagine the frustration of having patches in limbo for 1.5 y= ears.) I've seen this come up with other compilers (e.g. https://lists.gnu.org/= archive/html/help-guix/2021-11/msg00037.html), so maybe it's worth speci= fying and documenting Guix's policy. In particular, because this issue primarily affects compilers (there are= also related issues with e.g. build tools), there is a vicious cycle: i= f some language is not supported in Guix, people who specialize in that = language probably won't use Guix, and those are precisely the people who= se expertise might help improve the bootstrap situation. AIUI, many of the impressive bootstrapping stories in Guix have come abo= ut this way, with incremental improvement over time. I think it's better for Guix to package Idris2 in the best way we actual= ly know how to do today than to leave the whole Idris2 universe bereft o= f all of the benefits of Guix. Another factor that weighs in favor of accepting Idris2 for me is that t= he upstream community has mitigated at least some of the worst problems = of bootstrapping. While the generated Racket or Scheme code is not espec= ially readable, neither is it an opaque binary blob, and it is not "mini= fied" or obfuscated: it would be quite hard to hide a "trusting trust" a= ttack here. And of course there are many dimensions to reliability: I ca= n understand why a community that's developed a language with the advanc= ed correctness guarantees of Idris2 would want to take advantage of thos= e guarantees in their compiler. It's a bit of a tangent, but I also wanted to highlight the discrepancy = between the bootstrapping limitation blocking Idris2 and the current sta= te of some of its backends: 1) Upstream Chez Scheme (i.e. our 'chez-scheme', as opposed to 'chez-sch= eme-for-racket') is not bootstrappable. It relies on pre-generated machi= ne code "bootfiles" that can only be built by essentially the same versi= on of Chez Scheme. The first release of Chez as free software in 2016 re= lied on bootfiles generated by its non-free ancestors dating back to 198= 5 (before GCC!). The only reasonable path to bootstrapping Chez is to ad= apt the bootstrapping code from the Racket variant (which simulates enou= gh of Chez in Racket to slowly compile the Chez Scheme compiler): it may= be as simple as finding a version in the Git history before Racket's Ch= ez diverged too much from upstream, but I haven't found one yet, and it'= s not my top priority. 2) Compiled Chez Scheme code is not bit-for-bit reproducible due to the = use of type 4 UUIDs for gensyms. (It is reproducible with respect to the= Scheme function '#%$fasl-file-equal?'.) See https://github.com/cisco/Ch= ezScheme/issues/585#issuecomment-955408143 for details and my thoughts o= n a possible solution. 3) Racket is mostly bootstrappable, but it relies on generated code (R6R= S Scheme or primitive "linklets") for the expander (which implements the= reader and module system in addition to macro expansion per se). See th= e comments at the top of '(gnu packages racket)' or https://racket.disco= urse.group/t/951/4 for more discussion. I think it might be possible to = write a bootstrap shim in Guile analogous to the way Racket bootstraps C= hez. Sam Tobin-Hochstadt has suggested that it might be easier to adapt = the C expander implementation from before Racket 7.0. (The C implementat= ion was completely replaced with a Racket implementation based on the "s= ets of scopes" model from https://www.cs.utah.edu/plt/scope-sets/ rather= than "marks" and "renamings".) Extreme care has been taken to make the = generated code readable and editable, including indentation and preservi= ng variable names: anecdotally, I have sometimes read even tens of lines= of diff before realizing I was looking at the generated file rather tha= n the source. 4) I'm less involved in Node.js, but there are some limitations there, t= oo. Our 'node' package bundles NPM and its dependencies, some of which i= nclude generated code (for Unicode, at least) or cyclic dependencies. On= e thing I think would help would be to avoid NPM in 'node-build-system' = (somewhat like the antioxidant effort for Rust/Cargo) and instead implem= ent some of the ideas from https://pnpm.io in Guile or another language = with a good bootstrapping story. For Idris2, I hope that puts the bootstrapping situation in perspective:= Guix tries hard to avoid generated code, and we try to remove limitatio= ns over time, but the generated code in Idris2 is well within the bounds= of what Guix has accepted in existing packages. -Philip