Comments (2)
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.
Related Issues (20)
- Invalid term with get-value on array constant. HOT 2
- Assertion failure at solvers/simplex/simplex.c:10349
- The Source Code link is broken HOT 2
- Makefile.build:56: [...]/configs/make.include.amd64-portbld-freebsd13.0: No such file or directory HOT 2
- debian apt instruction fail HOT 4
- Segment fault in mcsat_process_registeration_queue HOT 2
- "FATAL ERROR: unexpected context status" when using (get-model) on an 'unknown' result HOT 2
- `get-value` on array does not inline function HOT 2
- Segmentation Fault when calling get-value
- Internal Yices Bug
- Context cloning HOT 2
- (get-value (0.0)) gives ((0.0 0)) , missing decimal point
- Is there any C API for me to extract value of a function? HOT 2
- E: Unable to locate package yices2 HOT 3
- QF_LIA performance issue with mod/div
- yices_new_uninterpreted_term does not produce an uninterpreted term HOT 1
- Doesn't always exit immediately on error
- Double quotes omitted in echo command response
- "" escape sequence not supported in strings
- Cannot build per-thread-state branch with mingw64 HOT 2
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from yices2.