Comments (4)
I'm trying to understand why these 4 dependencies of the test
target are always run:
Line 49 in 463e132
For typecheckExprToCString
, testStackLoop
, testStackNondet
, I think one reason is that they don't create a file with that name, so running these tests does not leave any trace of when it has been run last, so make
has to rerun it each time. An easy fix for these would probably be to have the tests create a .ok
file.
So I tried the following patch in bedrock2/Makefile
:
$(BYTEDUMP) bedrock2.ToCStringStackallocLoopTest.main_cbytes > special/stackloop.c
special/stackloop: special/stackloop.c
$(CC) -O0 special/stackloop.c -o special/stackloop
-testStackLoop: special/stackloop
- special/stackloop
+special/stackloop.ok: special/stackloop
+ special/stackloop > $@
+testStackLoop: special/stackloop.ok
special/stacknondet.c: ex
$(BYTEDUMP) bedrock2Examples.stackalloc.stacknondet_c > special/stacknondet.c
But it seems that stackloop is still rerun each time.
And I also don't understand why this code, creating special/BytedumpTest.out
, is rerun each time:
Lines 63 to 71 in 463e132
Do you understand this @JasonGross ?
from bedrock2.
ex and noex are declared PHONY, so they are considered out of date on every run. Since they are remade, all targets that list them as prerequisites are also considered out of date (much like how force is used). The solution is to make them order-only dependencies, as in special/BytedumpTest.out: special/BytedumpTest.golden.bin | noex
and special/stacknondet.c: | ex
, etc. An order only dependency is a prerequisite that does not cause a recipe to be re-run if it is out of date.
(I guess you want something like
special/stacknondet.c: bedrock2Examples.stackalloc.stacknondet_c $(BYTEDUMP) | ex
$(BYTEDUMP): | ex
to ensure that special/stacknondet.c
is remade when BYTEDUMP changes? Or you make it depend (not order-only) on whatever files it actually uses
from bedrock2.
Aah thanks for explaining me order-only prerequisites 👍
But I'm still a bit confused, and can't resolve it using google. Let's say I have
mytarget: fileProducedBy_ex | ex
myrecipe
and running ex
might modify fileProducedBy_ex
. Now, when does make
determine whether mytarget
is out of date? I guess before running ex
? That would be unfortunate, because if ex
updates fileProducedBy_ex
, I would like mytarget
to be rebuilt -- is there a way to achieve that?
from bedrock2.
You can make ex
an order-only dependency of fileProducedBy_ex
without a recipe.
Details:
I'm not sure, but I think:
- if
fileProducedBy_ex
does not exist and there's no explicit mention of it, make will error before trying ex - if
fileProducedBy_ex
either already exists or has a(n order-only) dependency on some other target,make mytarget
will first invoke all dependencies and order-only dependencies ofmytarget
and only after completing these dependencies will it determine whether or not the rule formytarget
should be run.
That is, my mental model is:
- First
make
walks the entire dependency chain of targets that need to be refreshed to build the dependency tree. In this step there is no difference between normal dependency and order-only dependency - Then make does a (possibly parallel) traversal of the dag from the leaves to the roots. Once make has traversed all the children of a node, it will rebuild the current node only if there are any non-order-only dependencies which are newer than the current target. (PHONY targets are always considered newer; not sure how non-file non-PHONY targets are handled)
from bedrock2.
Related Issues (20)
- Using multiple return values HOT 2
- Why does bedrock2 use `Load`? HOT 2
- Please create a tag for Coq 8.16 in Coq Platform 2022.09 HOT 6
- bedrock2 fails with a syntax error on Windows HOT 9
- bedrock2 lightbulb example is incompatible with native_compute HOT 5
- Less Memory-Hungry, More Principled Solution for Decidable Side-Conditions HOT 2
- Failing in coq CI HOT 1
- `make` should not run `coq` and `cc` when there's nothing to be done
- Update tested is failing with rate limits HOT 2
- Bedrock2 is broken on Coq's CI HOT 1
- Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.03 HOT 2
- Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.03 HOT 2
- design: outputting bitwidth-generic code? HOT 7
- design: core functionality of RecordPredicates? HOT 4
- Unbound value Int.land HOT 2
- Please pick the version you prefer for Coq 8.18 in Coq Platform 2023.10 [coq-bedrock2] HOT 2
- Please pick the version you prefer for Coq 8.18 in Coq Platform 2023.10 [coq-bedrock2-compiler] HOT 2
- [coq-bedrock2] Please create a tag for Coq 8.19 in Coq Platform 2024.01
- [coq-bedrock2-compiler] Please create a tag for Coq 8.19 in Coq Platform 2024.01
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 bedrock2.