Rocq 9.2 + auto compilation = spurious recompilations

[Matafou]

The CI on compilation currently fails with rocq 9.2 because it recompiles for vo files that are not outdated.

@hendriktews I noticed in the CHANGES for 9.2 that rocq compile DOES NOT GENERATE EMPTY VOS and VOK anymore. And indeed when I touch vos and vok then the dependencies are detected again. I suspect this is the cause. Can you have a look?

Minimum reproducing steps below. But going in the CI file ~/pg/rocq_no_implicit_show/ci/compile-tests/005-change-recompile/a.v is faster if you have PG sources somewhere.

Have two files a.v and b.v

b.v:

Definition foo:nat := 0.

a.v:

Require Import b.

Open a.v: M-x coq-compile-before-require-toggle to 't'.

Start Rocq 9.2 and go back and forth on the Require command: compilation is triggered each time (you can check it by looking at buffer *Messages* there are lines Compile b.v), even though b.v did not change.

[Matafou]

I guess we really need to have a PG test in Rocq's CI, so that we can anticipate this kind of problems.

[SkySkimmer]

rocq-prover/rocq#21929

[Matafou]

Thank you @SkySkimmer. I will have a look at it.

In this case I think we just need to add a touch command to build empty vos/vok when compilation succeeds.

[Matafou]

ping @hendriktews do you think you can have a look at this? I think the best think to do is to create the empty files by ourselves as suggested in in the CHANGES for 9.2.