From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp2 ([2001:41d0:2:bcc0::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms0.migadu.com with LMTPS id EKJ2HYu9j2AiJwEAgWs5BA (envelope-from ) for ; Mon, 03 May 2021 11:08:27 +0200 Received: from aspmx1.migadu.com ([2001:41d0:2:bcc0::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp2 with LMTPS id UFYOGYu9j2DwZAAAB5/wlQ (envelope-from ) for ; Mon, 03 May 2021 09:08:27 +0000 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 EBE31148FB for ; Mon, 3 May 2021 11:08:26 +0200 (CEST) Received: from localhost ([::1]:33806 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ldUZ0-0002o9-2w for larch@yhetil.org; Mon, 03 May 2021 05:08:26 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:59554) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1ldUYc-0002mo-77 for guix-patches@gnu.org; Mon, 03 May 2021 05:08:03 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:34668) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1ldUYb-0001Zu-R6 for guix-patches@gnu.org; Mon, 03 May 2021 05:08:01 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1ldUYb-0001X8-LE for guix-patches@gnu.org; Mon, 03 May 2021 05:08:01 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#46124] [PATCH] Idris 2 Resent-From: raingloom Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Mon, 03 May 2021 09:08:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 46124 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Xinglu Chen Cc: Maxime Devos , 46124@debbugs.gnu.org Received: via spool by 46124-submit@debbugs.gnu.org id=B46124.16200328235870 (code B ref 46124); Mon, 03 May 2021 09:08:01 +0000 Received: (at 46124) by debbugs.gnu.org; 3 May 2021 09:07:03 +0000 Received: from localhost ([127.0.0.1]:46209 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ldUXe-0001WT-3X for submit@debbugs.gnu.org; Mon, 03 May 2021 05:07:02 -0400 Received: from mx1.riseup.net ([198.252.153.129]:55938) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ldUXZ-0001Vx-K8 for 46124@debbugs.gnu.org; Mon, 03 May 2021 05:07:00 -0400 Received: from fews1.riseup.net (fews1-pn.riseup.net [10.0.1.83]) (using TLSv1 with cipher ECDHE-RSA-AES256-SHA (256/256 bits)) (Client CN "*.riseup.net", Issuer "Sectigo RSA Domain Validation Secure Server CA" (not verified)) by mx1.riseup.net (Postfix) with ESMTPS id 4FYcY80x9VzDqCq; Mon, 3 May 2021 02:06:52 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=riseup.net; s=squak; t=1620032812; bh=Xj0mXdlPCpBF/jE2mnzQ9pRHhGtssEH+L01pUTYHg+4=; h=Date:From:To:Cc:Subject:In-Reply-To:References:From; b=jmgMcmiXQvKlcW9gSZs6QrTMKqUAmWi2kRRP2AX/4CE4l/cwOWxJ/h/mhz0CycIOW 4SgQgdSyl9t1ulrABPM5H/Ysj407fSqYSkcRn03A/nNS3PcEO/iXJUEQnSQQQ+vVR8 xPKfLnvG3auo3YFGMokb0Zh0+RC4PivfvE5Wu1RM= X-Riseup-User-ID: 41ADFC538ACE53CC682C99CD2FCB2A9AD5CEBB8F6D0E115F355DD9B6E04CAD90 Received: from [127.0.0.1] (localhost [127.0.0.1]) by fews1.riseup.net (Postfix) with ESMTPSA id 4FYcY66Mxdz5vRy; Mon, 3 May 2021 02:06:50 -0700 (PDT) Date: Mon, 3 May 2021 04:10:44 +0200 From: raingloom Message-ID: <20210503041044.13358182@riseup.net> In-Reply-To: <87im44nprp.fsf@yoctocell.xyz> References: <20210127064337.6a226301@riseup.net> <87r1j267c6.fsf@yoctocell.xyz> <20210426172240.683c4c2b@riseup.net> <5003aa160dc82b35b06e60d425a09309199e1670.camel@telenet.be> <20210429204317.7e3a707c@riseup.net> <87im44nprp.fsf@yoctocell.xyz> MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable 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" X-Migadu-Flow: FLOW_IN ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1620032907; 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=7cA57NgCC1bV9GKqhQhwbuQwipDRM+e/4D3Jx0EA7DE=; b=Xui1zB6fWP6d97EkhgONe1Oa+IjRdZG1P8AEbPNtqyQsARcnATAkzxD1L+NrVYzlsvdqWI P0MRIvZXhD6pSHkY49F/uojxVQSTlIRysfd6ODtm06Yt89JGKfBz+j0toHpL65dXAQVPVN kXf5gGWgzgiaT6wYzPthB70/Mkmvm0HmDv9/WhsEU+PiPVYtlOIqW0E5cGkfhqi0RgRDa4 17qEwNKEZXhzoXO2/ycuKhOB3NP+qGNRW3HcyWTutbtnudTDOdiU31h/SFOG7LW6r7m5bI qeI2kGJAw8oSe3ND+lJAatTk187jYuUoZuDwiZOTXzor+oyPCpS8DIQHT45uZw== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1620032907; a=rsa-sha256; cv=none; b=Mv8SvuLaZ6W3MXM2U3VPKHcGLiMyq0uGRBiOHyAIBFLLsqSqOVoecM5Q0+FxxWXIC6tosB HKgNz58z8B0Nr1/z6ZLz4dc1SPX/2MHJ8YKdO1Drb3vKDAMOBiXipFivGUeTqt+ud4LT6e DETxCWdwJ5rJ6wMSM0Luoycv8fhdfjDSIxzgRPS89gvpsRsUUQ8JO4XreskGdAeLF9xpkM 7vIzCDcOwwlMUjYnx5hrDFt7oHxtPlxUGX1KEpUc7y8SPCLpFigbnDZyEhTzhHod+CYaOP oNioTVKqxdaDvRnVz9ChyIH881Mx47NVAMlchCB9VvZg5KzLVPLCwx6HR4Ls5w== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=riseup.net header.s=squak header.b=jmgMcmiX; dmarc=fail reason="SPF not aligned (relaxed)" header.from=riseup.net (policy=none); spf=pass (aspmx1.migadu.com: domain of guix-patches-bounces@gnu.org designates 209.51.188.17 as permitted sender) smtp.mailfrom=guix-patches-bounces@gnu.org X-Migadu-Spam-Score: -1.36 Authentication-Results: aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=riseup.net header.s=squak header.b=jmgMcmiX; dmarc=fail reason="SPF not aligned (relaxed)" header.from=riseup.net (policy=none); spf=pass (aspmx1.migadu.com: domain of guix-patches-bounces@gnu.org designates 209.51.188.17 as permitted sender) smtp.mailfrom=guix-patches-bounces@gnu.org X-Migadu-Queue-Id: EBE31148FB X-Spam-Score: -1.36 X-Migadu-Scanner: scn0.migadu.com X-TUID: poDPsOmFTS0Z On Fri, 30 Apr 2021 10:24:42 +0200 Xinglu Chen wrote: > On Thu, Apr 29 2021, raingloom wrote: >=20 > > Here is the updated patch. No idea if this actually works cross > > compiled, but I don't have much time to test it. My suspicion is > > that it's likely broken and requires changes to Idris 2's code > > generators, because they almost definitely call Chez, GCC, etc, > > with the wrong arguments. =20 >=20 > I noticed that there is an =E2=80=98idris2_app=E2=80=99 directory in the = =E2=80=98bin=E2=80=99 > directory >=20 > $ ls /gnu/store/va62hzp46c3dp2vlcnqc7fg109axj8rq-idris2-0.3.0/bin > idris2* idris2_app/ >=20 > What is this used for? >=20 If you take a look at $(guix build idris2)/bin/idris2, it's actually just a wrapper. It contains the supporting dynamically linked shared objects and the executable itself. I don't know the details of what each file does or why it's like this, the codegen seems to use a similar structure for all backends. The scheme files are probably all for the Chez backend, the shared objects are either C libraries (for socket support and stuff), or compiled Chez code. I just noticed the Racket script, that I have no idea about. Idris 2's build system makes some... uhm... interesting choices, so it's entirely possible that not all of those are necessary, or could be moved somewhere more sensible.