I was nodding along until I hit that point too. 25 seconds for a simple program??!? That would be a complete dealbreaker.

It’s not as bad as it sounds because you don’t have to compile your program while you write it. Rather, you send the program to a repl and the type checker tells you about problems. You can even run the total parts pretty quickly in the repl.

The only issue is that the language server seems to have a memory leak or something that leads to it taking a huge amount of memory and getting sluggish over the course of an extended development session.

>The only issue is that the language server seems to have a memory leak or something that leads to it taking a huge amount of memory and getting sluggish over the course of an extended development session.

that is not good advertising!

I'm sort of hoping someone here will tell me that I'm doing it wrong. Because, this has always been the showstopper for me.

The language sounds very interesting otherwise, so I’d like to hear of any fixes or workarounds too.

There are various reasons why Idris is slow, but it generally comes down to it being because the current system is the result of lots of experimentation about how to even implement a dependently typed language in the first place, and what it should look like. It needs quite a bit of re-engineering - I prioritised ease of playing with features over efficiency.

The good news is that I'm working on a new version, taking into account the many things I know now that I didn't when starting on version 1. Don't hold your breath though, it might take a while...

In the end, it's a research project, and our job isn't so much to make a good product as to get people excited about the ideas. Mostly we do this by trying to be obviously having lots of fun. But I'd still like a better implementation, because then we can have even more fun.

Does Haskell do this?

Do what? The memory leaks? No, GHC is an extremely solid system. There are various editor integrations for Haskell that make it easy to bounce between coding and experimenting in the REPL, though.

yes, memory leaks. thanks for answering my question my dude.

2015 MacBook Pro, compiling his 'first cut at it' example:

    # time idris -o Foo Foo.idr
    
    real	0m31.683s
    user	0m30.646s
    sys	0m0.876s