GNU bug report logs - #46124
[PATCH] Idris 2

Previous Next

Full log

View this message in rfc822 format

From: Xinglu Chen <public <at> yoctocell.xyz>
To: raingloom <raingloom <at> riseup.net>, Maxime Devos <maximedevos <at> telenet.be>
Cc: 46124 <at> debbugs.gnu.org
Subject: [bug#46124] [PATCH] Idris 2
Date: Fri, 30 Apr 2021 10:24:42 +0200

On Thu, Apr 29 2021, raingloom wrote:

> 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.

I noticed that there is an ‘idris2_app’ directory in the ‘bin’ directory

  $ ls /gnu/store/va62hzp46c3dp2vlcnqc7fg109axj8rq-idris2-0.3.0/bin
  idris2*  idris2_app/

What is this used for?

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.