I just got this down to 54s by fixing a silly mistake. I hope I've made more silly mistakes.https://twitter.com/edwinbrady/status/1265223132396367873 …
-
Show this thread
-
Down to 48.5s through the magic of inlining. This is really quite addictive... I am at least a little bit motivated by
@Augustsson telling me how fast Mu Haskell is (or was...)2 replies 1 retweet 44 likesShow this thread -
Replying to @edwinbrady @Augustsson
Unless you make it negative latency via writing a compiler that predicts future binaries ahead of the time you write the corresponding source code: /r/programming will not be satisfied.
1 reply 0 retweets 9 likes -
Question: Does the Idris 2 compiler already parallelize independent module subgraph compilation?
1 reply 0 retweets 0 likes -
Replying to @_m_b_j_ @Augustsson
No, that's less fun than optimising the single thread. But it is at least now possible - the Idris 1 run time wasn't good enough.
2 replies 0 retweets 3 likes -
Replying to @edwinbrady @_m_b_j_
Is the Scheme profiling hooked back into Idris so you can find where time is spent?
1 reply 0 retweets 0 likes -
Replying to @Augustsson @_m_b_j_
It's possible but fiddly. It's given me a few clues though.
1 reply 0 retweets 0 likes -
Replying to @edwinbrady @_m_b_j_
Are you preserving source locations through compilation? (It's annoying, but worth the effort.)
1 reply 0 retweets 1 like
Yes, so in theory they could go into the scheme. I learned to do that one the hard way... I can tell by the generated name what's what in the output though.
-
-
Replying to @edwinbrady @_m_b_j_
I think we all learned that one the hard way.
0 replies 0 retweets 3 likesThanks. Twitter will use this to make your timeline better. UndoUndo
-
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.