install target is unusable when sudo doesn't have access to coqc

[JasonGross]

make install should not be invoking bytedump test, or at the very least the bytedump test should respect COQBIN

 COQFLAGS="-Q src/bedrock2 bedrock2 -Q src/bedrock2Examples bedrock2Examples -Q /github/workspace/rupicola/bedrock2/deps/coqutil/src/coqutil coqutil " ../etc/bytedump.py bedrock2.PrintListByte.allBytes > special/BytedumpTest.out.tmp
Traceback (most recent call last):
  File "/github/workspace/rupicola/bedrock2/bedrock2/../etc/bytedump.py", line 16, in <module>
    p = subprocess.run(["coqtop", "-q", "-quiet"] + COQFLAGS, stdout=subprocess.PIPE, stderr=subprocess.PIPE, input=os.fsencode(f"""
  File "/usr/lib/python3.9/subprocess.py", line 505, in run
    with Popen(*popenargs, **kwargs) as process:
  File "/usr/lib/python3.9/subprocess.py", line 951, in __init__
    self._execute_child(args, executable, preexec_fn, close_fds,
  File "/usr/lib/python3.9/subprocess.py", line 1823, in _execute_child
    raise child_exception_type(errno_num, err_msg, err_filename)
FileNotFoundError: [Errno 2] No such file or directory: 'coqtop'
Error: make[2]: *** [Makefile:64: special/BytedumpTest.out] Error 1

https://github.com/mit-plv/fiat-crypto/actions/runs/6921348406/job/18826839337?pr=1733#step:18:3326

[samuelgruetter]

I'm trying to understand why these 4 dependencies of the test target are always run:

https://github.com/mit-plv/bedrock2/blob/463e132a5b8b8e841ffbcca73b37619dd9505a9f/bedrock2/Makefile#L49

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:

https://github.com/mit-plv/bedrock2/blob/463e132a5b8b8e841ffbcca73b37619dd9505a9f/bedrock2/Makefile#L63-L71

Do you understand this @JasonGross ?

[JasonGross]

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

[samuelgruetter]

Aah thanks for explaining me order-only prerequisites :+1:

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?

[JasonGross]

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 of mytarget and only after completing these dependencies will it determine whether or not the rule for mytarget should be run.

That is, my mental model is:

1. 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
2. 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)