search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
452 stars 138 forks source link

Library type-checking time #748

Open anuyts opened 2 years ago

anuyts commented 2 years ago

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 commented 2 years ago

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

anuyts commented 2 years ago

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 commented 2 years ago

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