Should 'make -C deps clean-*' wipe all versions of a dependency?

[jiahao]

Most of the time, having old versions of dependencies in deps/ is mostly harmless. Occasionally, however, they do interact in unexpected ways. Today @andreasnoack encountered a build error in gmp owing to having both gmp 5.1.3 and gmp 6.0.0 around, and the build tried to use the header file from the former and the library from the latter, resulting in a build failure. make -C deps clean-gmp only deleted the version explicitly stated in deps/Versions.make and did not solve the problem.

Given that we have special clean targets for dependencies in make -C deps clean-* which are meant to wipe out specific dependencies, would it make sense for them for them to nuke all versions of the dependency that are sitting around in deps? Or possibly have a different clean target that aggressively deleted all downloaded versions?

[staticfloat]

I think this is more of a problem of not clearing usr/ completely, since likely what's going on is that the header file from 5.1.3 is not getting overwritten by 6.0.0, or some such similar thing.

[tkelman]

Agree with @staticfloat. You almost definitely have to either make cleanall or rm -rf usr before switching versions of a dependency. I can't think of an easy universal way to check whether the pre-existing installed version of a dependency sitting in usr actually matches the version given in deps/Versions.make

[jiahao]

Closing with better documentation in #8426