make clean does not clean dependency information about bedrock2 HOT 7 CLOSED

I see two reasons why this could happen:

1. There's a certain kind of files that make clean should delete but doesn't delete. If that's the case, do you know what kind of file?
2. make -j4 schedules stuff before make depend has run and ignores dependencies. I sometimes got similar errors as you when building with -j on a clean repo and the fix was to run make depend && make -j4 instead.

from bedrock2.

I am pretty sure I tried without -j4 and saw the same behavior.

from bedrock2.

To get the list of files that make clean removes (minus .depend), I ran this command:

find . -type f \( -name '*.glob' -o -name '*.vo' -o -name '*.aux' \) | sed -e 's/^\.\///g' | sort > tmp_find.txt

To get the list of files that git clean -dxf removes, I ran this command:

git clean -dxf --dry-run | sed -e 's/Would remove //g' | sort > tmp_gitclean.txt

The diff between these two lists doesn't contain anything interesting on my machine.
Next time you clean and recompile, could you please test these and let me know if the diff contains something interesting?

from bedrock2.

Thanks, will do.

from bedrock2.

In another project, I have *.v.d files, maybe you have such files in your repo too? Did you use another coqdep than me? A difference between 8.7 and 8.8?

from bedrock2.

Reading the makefile, I don't see how this could possibly happen unless you had a merge conflict or other local change in src/ExprImp.v and did something like git reset --hard in addition to git clean.

from bedrock2.

I think I figured out what happened: I had a stale .depend from earlier and it was not getting updated.

from bedrock2.