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 -
Replying to @edwinbrady
If you have easy to understand directions, and want a test done on a pi4. Gimme a shout
1 reply 0 retweets 0 likes -
Replying to @quixoticgeek
Once I've patched the run time system to not have my comedy time bug, I'll let you know! I think it'll need the 4gb version (it takes a touch over 50% RAM on mine)
1 reply 0 retweets 0 likes -
Challenge accepted, as long as the strike goes on long enough :)
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.