Strange case of infinite loop in the build system about yices2 HOT 2 CLOSED

Yes. there's a rule in src/Makefile that prints 'filename.h' not found. It causes
this infinite loop. I've seen this behavior many times, but I haven't found a
good fix. Here's a long explanation. Maybe somebody will have an idea.

All this has to to with the way GNU Make automatically rebuilds
all makefiles that may have changed. In Yices's case, the Makefiles
that are rebuilt are dependency files like 'source-file.d' that are generated
automatically from 'source-file.c'. The 'source-file.d' contains a rule that
specifies the dependencies for 'source-file.o'. The rule also specifies that
'source-file.d' has the same dependencies as 'source-file.o'.

When you call make, it will read/include all the 'source-file.d' Makefiles. If they
are missing or if their dependents have changed, they get built or rebuilt.

The problem happens when you have an out-of-date 'source-file.d' that has 'old-stuff.h' as
a prerequisite but 'old-stuff.h' has been deleted. In this case, I want 'source-file.d'
to be regenerated. This would normally fail because 'source-file.d' depends on 'old-stuff.h' and
Make doesn't know how to build 'old-stuff.h'. To fix this issue, I have added a default
rule that's triggered when 'xxx.h' is missing. It just prints 'xxx.h not found' and
doesn't fail.

This works fine as long as 'source-file.c' doesn't include 'old-stuff.h' anymore.
Then 'source-file.d' is rebuilt; the dependency on 'old-stuff.h' is removed and all is well.
But this loops if 'source-file.c' still refers to 'old-stuff.h', because then the regenerated
'source-file.d' still has 'old-stuff.h' as a prerequisite. Your missing gmp.h loop is similar.

from yices2.

@BrunoDutertre you could create a file to prevent the loop while giving a nice user error:
echo '#error "This file is a stub created by make to fill dependency..."' > old-stuff.h

Worst case, the file was created for nothing and a git clean will clean it?

from yices2.