Has anyone here played with Idris 2 recently? How does it compare in terms of “readiness” with Idris 1?
I’m biased here, since I’m writing the thing, but I would strongly recommend using Idris 2 over Idris 1 now.
The tools aren’t as polished, but that’s coming, and it’s more than made up for by the fact the the tools we do have (especially interactive editing) actually scale beyond small programs - I’m actively using the interactive tools for editing Idris 2 itself. The code it generates is much faster (targetting Chez Scheme, which is well suited to the job) and erasure is predictable, so you actually know what’s going to run at run-time rather than trusting inference to do what you want.
Also, it’s much more robust. Not that there aren’t lots of issues to deal with, of course - that is always the way - but given that the implementation takes advantage of Idris’ type system, the issues that do arise tend to be more about high language design questions and presentational things than anything fundamental.