search

codewars / codewars-runner-cli

Old CodeRunner project. See https://github.com/codewars/runner instead.
GNU Affero General Public License v3.0
402 stars 141 forks source link

Agda: Improve type-checking time #733

Closed Bubbler-4 closed 5 years ago

Bubbler-4 commented 5 years ago

I have a feeling that it takes too long to typecheck Agda on CW. When I work locally with emacs, commonly used library modules like Data.Nat get pre-typechecked (so the compiled type information is stored for reuse), and re-typechecking takes (pretty much) less than a second.

If it isn't done already, can we get the library modules pre-typechecked inside the Docker image? For standard library, I think you can run GenerateEverything.hs then call agda Everything.agda or the like. For Cubical library, it should be enough to call make.

I'm suggesting this because this kata imports several big nested modules including Data.Nat, Data.Integer and Data.List, which makes the code time out several times. (And even if a run finishes successfully, having to wait ~12 seconds every time just to typecheck is not very good.)

kazk commented 5 years ago

If it isn't done already, can we get the library modules pre-typechecked inside the Docker image?

This is already done. cabal install does for agda itself. For agda-stdlib, cabal install, dist/build/GenerateEverything/GenerateEverything, and then agda -i. -isrc Everything.agda. For cubical, make.

Bubbler-4 commented 5 years ago

I guess we can do nothing about it (just found that batch mode is slow as hell, even on my local PC). Then can you at least increase the time limit, to 15s or maybe 20s?

kazk commented 5 years ago

I'll make it 16s for now.

kazk commented 5 years ago

I'll close this when it's deployed.

kazk commented 5 years ago

The change is deployed