[bug#46124] [PATCH] Idris 2

[raingloom <raingloom@riseup.net>]

On Fri, 30 Apr 2021 10:24:42 +0200
Xinglu Chen <public@yoctocell.xyz> wrote:

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

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.