it should be possible to `sudo make install` even when the `sudo` account doesn't have `coq_makefile` in `PATH`

[JasonGross]

We have https://github.com/mit-plv/coqutil/blob/421630237d546678afa836a083cf678d631572a6/Makefile#L45 https://github.com/mit-plv/coqutil/blob/421630237d546678afa836a083cf678d631572a6/Makefile#L30-L32 https://github.com/mit-plv/coqutil/blob/421630237d546678afa836a083cf678d631572a6/Makefile#L28 https://github.com/mit-plv/coqutil/blob/421630237d546678afa836a083cf678d631572a6/Makefile#L3 which means make install invariably regenerates Makefile.coq.notest. I'd like this to not be the case.

This breaks testing fiat-crypto's make install target on docker: https://github.com/mit-plv/fiat-crypto/actions/runs/6909719309/job/18801575975?pr=1733#step:18:3269

[samuelgruetter]

I like regenerating the coq makefile each time so that I don't need to run an extra command each time I add a new Coq file. Are you happy with the workaround you found in https://github.com/JasonGross/fiat-crypto/commit/6d64ca66473d0c47990cd7ec833a8c0ab67aaa17 ? Or do you have a lightweight solution that fixes this issue without requiring the user to run an extra command whenever adding a new file?

[JasonGross]

If you make Makefile.coq.notest depend on $(SRC_VS), this will almost get you what you want. It'll work for the common case of "the user created a new file", but won't work as well when the user deletes a file. Or you could do something like

ifneq ($(strip $(sort $(SRC_VS))),$(strip $(sort $(shell cat .src_vs 2>/dev/null))))
.PHONY: .src_vs
.src_vs:
    printf '%s' '$(SRC_VS)' > $@
endif

and then make Makefile.coq depend on .src_vs. Or switch to dune, I hear they correctly have each build target automatically depend on its invocation recipe.

[JasonGross]

And I'm not really happy with the workaround, but I can tolerate it.

[samuelgruetter]

ifneq ($(strip $(sort $(SRC_VS))),$(strip $(sort $(shell cat .src_vs 2>/dev/null))))
.PHONY: .src_vs
.src_vs:
  printf '%s' '$(SRC_VS)' > $@
endif

That looks interesting, but what's the .PHONY: .src_vs good for here? And do you think an auto-generated _CoqProject could take the role of this .src_vs?

[JasonGross]

PHONY targets are considered always out of date / are always remade. A target with no prerequisites is considered up to date if the file exists at all, unless its PHONY. If you want, you could make it depend on a PHONY force target instead, and that would serve the same purpose of forcing it to be remade here. (Ultimately, the problem is that we want a contents-based check but make only does timestamp-based checks, so we hack it by hand.)

And do you think an auto-generated _CoqProject could take the role of this .src_vs?

Yeah, we do that in fiat-crypto at https://github.com/mit-plv/fiat-crypto/blob/00a4b8ea16d0764b72a27adfb5d1e8821494c666/Makefile#L509-L523 It's a bit more complicated because we have to deal with the flags in the file (using shell to generate the expected contents). I had also assumed there was a reason you weren't listing .v files in _CoqProject, but if not, it's probably better to do _CoqProject.

[JasonGross]

You could do something like

COQPROJECT_CMD := { printf -- '-R %s/coqutil/ coqutil\n-arg -w -arg unsupported-attributes\n' '$(SRC_DIR)'; printf '%s\n' $(sort $(SRC_VS)); }

and then compare $(strip $(shell cat _CoqProject 2>/dev/null)) with $(strip $(shell $(COQPROJECT_CMD) 2>/dev/null)

[samuelgruetter]

If you want, you could make it depend on a PHONY force target instead, and that would serve the same purpose of forcing it to be remade here.

Aah I see, I read PHONY as "this is not a file" and would prefer a force target.

Yeah, we do that in fiat-crypto at https://github.com/mit-plv/fiat-crypto/blob/00a4b8ea16d0764b72a27adfb5d1e8821494c666/Makefile#L509-L523 It's a bit more complicated because we have to deal with the flags in the file (using shell to generate the expected contents).

I wasn't aware of that, last time I read that part of the fiat-crypto Makefile, there was an update-_CoqProject target that had to be manually run, which I didn't like.

I had also assumed there was a reason you weren't listing .v files in _CoqProject, but if not, it's probably better to do _CoqProject.

The only reason why I didn't want to list .v files in _CoqProject was because I didn't want to run a command each time a file is added or deleted.

I think I can now make some changes to the Makefile that we both will like :wink: