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

Previous Next

Full log

View this message in rfc822 format

From: raingloom <raingloom <at> riseup.net>
To: Maxime Devos <maximedevos <at> telenet.be>
Cc: Xinglu Chen <public <at> yoctocell.xyz>, 46124 <at> debbugs.gnu.org
Subject: [bug#46124] [PATCH] Idris 2
Date: Thu, 29 Apr 2021 20:43:17 +0200

[Message part 1 (text/plain, inline)]

On Mon, 26 Apr 2021 23:27:39 +0200
Maxime Devos <maximedevos <at> telenet.be> wrote:

> raingloom schreef op ma 26-04-2021 om 17:22 [+0200]:
> > There hasn't been a tagged release since then, so I'm sending my
> > original patch, but I should note that in my channel I've been
> > tracking the latest commit, which does seem to work, although it's
> > been a while since I used Idris for anything complicated.
> > 
> > +                     ;; TODO detect toolchain
> > +                     "CC=gcc")))  
> 
> Unless idris has a compiler built in that uses gcc for compiling
> idris to machine code, this should likely be
> ,(string-append "CC=" (cc-for-target)) instead, such that the
> cross-compiler is used when cross-compiling.
> 
> Teaching (cc-for-target) to detect which toolchain should be used
> is a separate matter.  Maybe it could be a macro that looks at
> (package-native-inputs this-package) or something.
> 
> Greetings,
> Maxime.

Oh, that's a leftover, I was using clang for a while, since it's
said to use less RAM. I switched back to gcc and left that in.

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.

[0001-gnu-Added-Idris-2.patch (text/x-patch, attachment)]

Previous Next

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