Make clean to just remove generated directories #269
Labels
documentation
Involves touching documentation
enhancement
make
Involves touching GNU Makefiles
python
Involves touching python code
tests
Involves touching tests
Feature Request
Describe the new feature:
Right now, the generated
Makefile
will attempt to clean all object files and dependency files from the generatedobj
directory with themake clean
target. However, when there are a lot of source files (e.g., more than 1,000), then this takes quite a long time, certainly longer than if we just deleted the directory along with all of its contents (i.e.,rm -rf obj
).Suggested change:
Change the
make clean
target to remove theobj
directory entirely instead of each object file individually.We could potentially do the same for the
results
directory, butresults
directory is dependent on the compilation search space, not the size of the project. Therefore, it is unlikely to get unwieldyWe could, however, split out the executables into a separate directory, say
runbuild
and the results would still go intoresults
. While we're at it, I think it would be good to remove the intermediate results that exist before being compared with the ground-truth. Suppose we put therunbuild
executables in therunbuild/
directory, then when executed, they generate an output file in theresults/
directory with suffix-out
. Then when compared usinggtrun
, they would add the suffix_comparison.csv
(or something like that). The clean target would then remove therunbuild/
directory and also any files ending in-out
inresults/
.Similar changes could be made to the clean targets of the bisect makefile.
Alternative approaches:
For the
obj
dir, we could instead delete all object files and dependency files with afind
commandbut, this would add one more dependency on the system (not that
find
is uncommon). My guess is thatrm -rf obj
is much faster, and the user should probably not be putting anything in this directory anyway.The text was updated successfully, but these errors were encountered: