collie icon indicating copy to clipboard operation
collie copied to clipboard

Poor type checking performance with many subcommands

Open eayus opened this issue 3 years ago • 1 comments

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'

eayus avatar Dec 14 '21 16:12 eayus

This may be an upstream problem if we're breaking sharing and recomputing a lot of the same checks.

gallais avatar Dec 16 '21 15:12 gallais