Files should not import Everything files unless necessary

[mortberg]

Some files import Everything files for no reason which can cause a headache when refactoring or renaming. It would be good to remove unnecessary imports of Everything and instead have more fine grained imports (for example if a file only uses 2-3 modules from Foundations there is no reason to import Foundations.Everything)

[mortberg]

This should also be added to the styleguide

[L-TChen]

Maybe off-topic, but I wonder why Cubical.Foundations.Everything renames a number of functions which are not reexported at all. What is the intended purpose of Everything after all?

[anuyts]

Currently, when I checkout the master branch and try to type-check Cubical.README, it fails because Cubical.Functions.Everything is missing. I see that there is a script Everythings.hs for generating them, but there is no guide about what I'm supposed to do at this point.

[felixwellen]

You can run make. I think this was mentioned as an installation step in the past, but got removed. So this is only mentioned in CONTRIBUTING.md now. I guess the idea is, that you only want to check the whole library as a contributer, but not as a user.

[anuyts]

Well, an end-user would expect to be able to typecheck a file called README.agda :-)

[felixwellen]

I agree, that is a reasonable expectation ;-)
There is a trade-off: make requires runhaskell, which is not available on any system that runs agda. So some people ran into problems, when they tried to run make. I guess the ideal solution would be to make that problem go away, so everyone can just run README.agda, after setting everything up.