stdlib wastes time being rebuilt on every minimizer run

[JasonGross]

The bug minimizer needs to wrap coqc in order to extract information about the build. This means that the hashes are different in

stdlib/dev/with-rocq-wrap.sh

Lines 5 to 18 in 39664f2

	rocq=$(command -v rocq)
	# NB on cygwin "$rocq" is a cygwin path (/foo/bar)
	# but reading files from hash.exe needs windows paths (C:/cygwin/foo/bar)
	# we avoid the problem by going through stdin
	rocqhash=$(dune exec --root "$(dirname "$0")"/.. -- dev/tools/hash.exe < "$rocq")
	rm -rf .wrappers
	mkdir .wrappers
	cat > .wrappers/coqc <<EOF
	#!/bin/sh
	# hash = $rocqhash
	exec rocq c "\$@"
	EOF

which I guess has dune rebuild all files. What's the justification for doing this?

[SkySkimmer]

It is correct to rebuild when coqc changes.

[JasonGross]

Perhaps that is true in general, but it should be possible (and relatively easy, without needing to know the details of the build system of any given development) to bypass the rebuild. I don't think it's reasonable to force a rebuild of a development and all its dependencies when testing out a fix. What workflow is this serving?

Perhaps actually the issue is that Coq's CI targets should not be using this wrapper?

[JasonGross]

I'm going to reopen for now this so it doesn't get lost, feel free to transfer it to coq/coq or ask me to do that

[SkySkimmer]

We can avoid the rebuild by not doing dune build, ie coq/coq#19925