Command line arguments improvement

[eayus]

Currently we use a very primitive method of parsing command line arguments. There is no way for the user to find out what commands are available or their correct usage. Error messages on invalid arguments are very poor.

We could do with a more robust approach. Originally I used the collie library, however after adding many subcommands, compile times became way too long (I could no longer compile the program on my machine without running out of RAM).

[JonathanLorimer]

Why does collie produce such bad compile times? Would it be worthwhile to upstream changes to collie or right a simple command line option library in the same vein as optparse-applicative?

[eayus]

It's hard to pinpoint exactly what the reason is with collie's compilation times. I suspect it might come from the fact that it allows defining commands in a different order in the "specification" and "implementation" - this requires significantly more compile-time computation than if it restricted them to the same order. (Note that this is just speculation based on a small amount of testing, it's very possible this might not be the problem).

I'm not sure that removing this flexibility of command order would be in the "spirit" of collie, so the ideal solution is probably tackling the problem at its root, namely figuring out why the compiler finds this so difficult. I will open an issue describing the problem on the collie repo and see if that gets us anywhere. If we can't solve it, then yeah, it might be worth implementing an alternative library which is less intensive on the type checker.

[ohad]

Sometimes this is due to bugs/bottlenecks in idris's elaborator. @edwinb usually manages to pinpoint it, but he's often busy!

It could also be some issue with module import (see also Idris2 feature request #2091), where some definition is blocked on a public exported definition in an import but not import public module, and definitions get larger and larger.

[ohad]

@eayus It's useful to have access to a commit with the very slow type-checking times. Both so that collie @gallais and I could play with it (and try to find issues on the collie side), and also for nerd-sniping @edwinb .

[eayus]

@ohad Yeah I do suspect it is an Idris2 bug. I've opened an issue on the collie repo giving my best try at a minimal example of the problem, which should give you something to play with.

[eayus]

This is temporarily solved by using the sap library. On the next Idris release when the bug affecting collie is fixed, we can consider switching back.