Meanwhile, the experimental effort of self hosting Idris 2 now typechecks (the whole thing) in about 1m30. So that's promising. I "just" have to make Idris 2 generate good enough code to be able to use it...
-
-
Show this thread
-
Also worth adding: I'm fairly confident I haven't broken anything while doing this, because whatever I do has to get past a separate checker for the core language (~500 LOC) Your language with fancy types *does* have a separately checkable core, doesn't it? :)
Show this thread
End of conversation
New conversation -
-
-
Well I'm not sure it's a normal way to spend your evenings. But we live in strange times, I suppose.
End of conversation
New conversation -
-
-
What did you change?
-
It was mostly about being careful when to evaluate. It was evaluating types of pattern variables too much (by far the biggest problem), and inlining some small definitions not enough. Also there were some needless system calls in the garbage collector which hurt a lot.
- 1 more reply
New conversation -
-
-
it's not odd, making things faster is god's own work!!
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
Yes! I just optimised something that took ~9 seconds into ~68 milliseconds and it feels rewarding! :)
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.