I will make this public by the time I rant at @curry_on_conf at the latest, by the way... there's still a hole or two to plug
-
-
Show this threadThanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
Isn’t that timing the ‘echo’ command? Don’t you mean “echo ‘:q’ | time idris2”? Or am I being thick?
-
No, that times the whole thing (for Idris 1 it reports about 1.5s for the same thing). Maybe it depends on the shell?
- 4 more replies
New conversation -
-
-
Which action had the highest effect?
-
The biggest trick, which is easier said than done, is to defer loading function definitions until they're actually used. This is a huge benefit to performance everywhere else too...
End of conversation
New conversation -
-
-
Yes, yes! I always get annoyed how it seems to take years for ghci to quit. Even worse: erl.
-
I haven't done anything about quit time :). This was all about loading function definitions it was never going to use... Next step is to get it to parse import headers faster, but that hurts a lot less!
End of conversation
New conversation -
-
-
all you're measuring is the time it takes for bash to execute the builtin command's write to the pipe.
-
It's interesting that it takes 1.5s to do that for Idris 1 then...
- 4 more replies
New conversation -
-
-
27 milliseconds? But I want it now!
Thanks. 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.