collie
collie copied to clipboard
Poor type checking performance with many subcommands
Using a large number of subcommands seems to give the type checker trouble, and results in very long + high memory usage compile times. For example, consider the program below with 6 subcommands. On my machine, this uses 10G+ of memory, and I haven't managed to get it to finish type checking yet. It seems that compilation time is exponential wrt. the number of subcommands. I'm using the latest Idris2 pull.
module Slow
import Collie
mainCommand : Command "main"
mainCommand = MkCommand
{ description = ""
, subcommands = [ "x1" ::= basic "" none
, "x2" ::= basic "" none
, "x3" ::= basic "" none
, "x4" ::= basic "" none
, "x5" ::= basic "" none
, "x6" ::= basic "" none ]
, modifiers = []
, arguments = none }
main' : Slow.mainCommand ~~> IO ()
main' = [
\_ => putStrLn "Invalid command",
"x1" ::= [ ?x1 ],
"x2" ::= [ ?x2 ],
"x3" ::= [ ?x3 ],
"x4" ::= [ ?x4 ],
"x5" ::= [ ?x5 ],
"x6" ::= [ ?x6 ] ]
main : IO ()
main = Slow.mainCommand .handleWith main'
This may be an upstream problem if we're breaking sharing and recomputing a lot of the same checks.