I seem to be spending the evening trying to make Idris 2 run on a @Raspberry_Pi. I know how to have a good time.
(No, really, this is enormous fun. Getting there...)
-
Show this thread
-
It turns out it doesn't quite work yet because the Idris runtime thinks the current time is a negative number on a 32 bit machine. I say this just in case: a) Anyone thinks time errors like the Y2K bug are made up b) Anyone might think I'm a competent unix programmer :)
1 reply 0 retweets 14 likesShow this thread -
2 replies 7 retweets 58 likesShow this thread -
I have to go back to my proper job tomorrow, so polishing up the hacking I just did for others to play with will have to wait until next week when I'm back on strike again... (unless something good happens in the mean time)
1 reply 0 retweets 2 likesShow this thread -
Still, one side effect is that there is now an Idris 2 you can build and install even if you don't have Idris 1, at https://www.idris-lang.org/pages/download.html …
1 reply 1 retweet 15 likesShow this thread -
It took ~50s to build the libraries (not using -O2 to build the C, but I'll try that later) compared to about 12s on my laptop. That's much better than I expected. That means Idris 2 on a Pi is more usable than Idris 1 on my laptop. Yay/Oh dear (depending on your point of view)
3 replies 3 retweets 16 likesShow this thread
Incidentally, the ":set cg racket" is because it was the only back end I could persuade to work. If Idris is ever close to as portable and usable as Racket I will be delighted.
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.