Library type-checking time

[anuyts]

When I run make or typecheck README.agda, this also typechecks modules such as Cubical.Experiments.ZCohomology.Benchmarks, a module which seems almost intended to take a long time to load. Is it strictly necessary for these files to be part of the library and kept permanently up to date by anyone contributing to any of the dependencies?

[mortberg]

Would it be possible to set things up so that one can use make to typecheck only the package one is working on?

[anuyts]

Well in this case I probably did change a file that Cubical.Experiments.ZCohomology.Benchmarks depended on.
My point is more that maybe performance benchmarks (is that what they are?) need not be part of a library.

[mortberg]

It's some benchmarks for a paper that we don't want to ever break. How about having the general make target not build anything in Experiments but have the CI do? Nothing in the library should depend on something in Experiments anyway