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 oOAfN+nxAWNq/gAAbAwnHQ (envelope-from ) for ; Sun, 21 Aug 2022 10:50:49 +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 QDcpN+nxAWN9aQEA9RJhRA (envelope-from ) for ; Sun, 21 Aug 2022 10:50:49 +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 E9F56AC16 for ; Sun, 21 Aug 2022 10:50:48 +0200 (CEST) Received: from localhost ([::1]:36660 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1oPgfP-0002YD-KZ for larch@yhetil.org; Sun, 21 Aug 2022 04:50:47 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:50574) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1oPgfD-0002Y4-Hh for help-guix@gnu.org; Sun, 21 Aug 2022 04:50:35 -0400 Received: from mx1.riseup.net ([198.252.153.129]:38344) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1oPgfB-0000CH-8z for help-guix@gnu.org; Sun, 21 Aug 2022 04:50:34 -0400 Received: from fews1.riseup.net (fews1-pn.riseup.net [10.0.1.83]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256 client-signature RSA-PSS (2048 bits) client-digest SHA256) (Client CN "mail.riseup.net", Issuer "R3" (not verified)) by mx1.riseup.net (Postfix) with ESMTPS id 4M9Tj35lydzDqQl; Sun, 21 Aug 2022 08:50:31 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=riseup.net; s=squak; t=1661071831; bh=9MKAkovaTRbELakXQGafXGzRCxjJk8eTXAIngklAr2A=; h=References:From:To:Cc:Subject:Date:In-reply-to:From; b=H+8cHnnc8kGHFBI58DqUQJ1vw/EwNvt1DhBWFMdbVb7mhl4iqAx0vpG5PKTz93K3z K9PmPD2uZ9YJ9nwS8eX+M/o5yFtu682/tYqeeRc5PgDj5rXXLFGuo6e5gbYD4A5Sgg lwq06uNFgAgOiSJBF8H28WOYTfEft6Qh60YeNwrE= X-Riseup-User-ID: FD6EA21E8872CC09B7254A6EE7B33DE345871C30AC169B99D8FA0D9FCD91679D Received: from [127.0.0.1] (localhost [127.0.0.1]) by fews1.riseup.net (Postfix) with ESMTPSA id 4M9Tj30TH8z5vcM; Sun, 21 Aug 2022 08:50:30 +0000 (UTC) References: <138fc06ac78045c4a7117566484ebb936caff178.camel@phfrohring.com> <87r11aeot8.fsf@riseup.net> <871qta8tgp.fsf@softland> From: Csepp To: "(" Cc: Andreas Reuleaux , help-guix@gnu.org Subject: Re: Packaging Idris2 Date: Sun, 21 Aug 2022 10:42:21 +0200 In-reply-to: Message-ID: <874jy63rqk.fsf@riseup.net> MIME-Version: 1.0 Content-Type: text/plain Received-SPF: pass client-ip=198.252.153.129; envelope-from=raingloom@riseup.net; helo=mx1.riseup.net 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.001, RCVD_IN_MSPIKE_WL=0.001, 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=1661071849; 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:in-reply-to:in-reply-to: references:references:list-id:list-help:list-unsubscribe: list-subscribe:list-post:dkim-signature; bh=zPgB9Jf/PMdbKN+TBmNTsod2vu0uHj19l+VFlMAS83w=; b=P4MQZWw9wpImAZnF83+AUs6pwqyjdNQNixI92nChbBhrA/nfsyBehnWnAfy1boucmUdp6r EFMf7J4EM3rDCdNXDPmnpZ1Y+4vHY15F12IxFcoOvPZSQEYoB0efK5qarPjhJxnjy7Ijze B8PTKZ8iN6D/nqhLl4KVs14gt/HujVi4z2Zh7T+I/okF4aRnmviUWU01KBr4B4VK5cIhPw GsF/1UsdSGUIrIbc7iPpHozwjVonwnkmy5mlF9Z0iBUZmp+jmkDVCoQe1DbEbVdch986Om JHuRpCPf+z/zvGPBl/oBMY5sI/7vnb79D9gc5xG/tehz/VXOPq77YLm/ctsSDQ== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1661071849; a=rsa-sha256; cv=none; b=rYk5GQPJUn0jOA08Kgu41oxDpiPeyJukq58jiy6WmHsns3vr/dRohG9kCRCrKWLSBzW961 AWRfe4XSKHx2108eqNHBxMZC2IvZ2fmGt+8h9HKaS6NMi43vsS/kHxRPv/6P9hDl2gW2Bs 1Oc/Pi2c6waYcFUnGfIz+JgRxSWxA1dqMlbYb4Xhzed6aGqeUE3jcPqQRDtURBSV07v5oJ mPczb4jocfyszLy33152APyWiHc8kyEMx1d4IzKw3EKGPhSqnsn6n9NXwzZi+EyN0tQs7a 552agKABrsjkcZo0a8bTJrJQUA3Hz7KtCgmqnr+QLTn3c/79U1VpcsAhSu5nkA== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=pass header.d=riseup.net header.s=squak header.b=H+8cHnnc; dmarc=pass (policy=none) header.from=riseup.net; 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: -2.43 Authentication-Results: aspmx1.migadu.com; dkim=pass header.d=riseup.net header.s=squak header.b=H+8cHnnc; dmarc=pass (policy=none) header.from=riseup.net; 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: E9F56AC16 X-Spam-Score: -2.43 X-Migadu-Scanner: scn1.migadu.com X-TUID: 3KbpZP+vG97v "(" writes: > Hi Andreas, > > On Sat Aug 20, 2022 at 11:01 PM BST, Andreas Reuleaux wrote: >> You bootstrap it from scheme (chez or racket), as comes within the Idris2 tarball >> (and built with Idris 2 itself: Idris2 -> Chez Scheme / Racket). > > Since this Scheme is pregenerated, it cannot really count as source code. So > we need to find a version of Idris2 that can still be built with Idris1, then > try to build a later version with that Idris2, and keep going until we get to > the latest version, like our rustc bootstrap process. > > -- ( Yup. And there are already patches and channels floating around that do that. Anyways, if you want to work on Idris 2, I highly recommend looking at them. Otherwise you are doing work that has already been done. Which is fine if you are only doing this as an exercise, but if you are serious about packaging Idris 2, you should know about the issues that have come up with it. ps.: pls no benchmarks without hardware info. :) I know what I'm talking about when I say it takes too many resources on my machine and I'm aware that more powerful computers exist and that Idris 2 compiles itself faster than Idris 1 does.