Cleaning up after make coverage

[ssbrewster]

make coverage has a number of side effects including downloading tools to generate the coverage and overwriting the lib/ directory; make coverage-clean allows the user to clean these up.

While working on #15190 I suggested passing an option to allow make coverage and make coverage-clean to be done in one run but leaving the coverage/ dir intact (and adding it to .gitignore. @TimothyGu agreed this could be good and welcomed a PR for it (and added the correct syntax for the command line option).

I think there are a couple of options for how this could be done (plus leave as is) that would be great to get feedback on. I think the options are:

1. Pass CLEAN=true to make coverage that runs coverage-clean after coverage-test
2. Run coverage-clean after coverage-test as default and allow the user to pass NOCLEAN=true or CLEAN=false if they do not want the side-effects of coverage removed.
3. Leave as-is and require the user to run coverage-clean after coverage

Both options 1 and 2 would leave the coverage/ dir intact (so not rm -r that directory during coverage-clean as is done currently), and add that dir to .gitignore. I'm happy for the coverage/ dir to remain intact because I might want to keep referencing those files (as long as they are ignored by git) but do not want all the other side-effects showing up each time I run git status.

Any feedback is really appreciated.

[apapirovski]

Either 1 or 3 would be nice, I think. And I wholeheartedly agree re: keeping coverage dir intact and adding it to .gitignore. Not sure if there are any reasons not to.

[ssbrewster]

Thanks @apapirovski. Yes I can understand the principle of coverage-clean cleaning up all coverage files but the coverage reports themselves are a useful reference.

[ssbrewster]

@TimothyGu any thoughts about this?

[apapirovski]

This was addressed.