[CI] enable cache for Unix jobs

[Alizter]

No description provided.

[emillon]

I tried to set DUNE_CACHE=disabled for the rest of the run but it was still causing problems. I think there's an issue with dune's test suite itself when the cache is enabled.

[emillon]

@Alizter disabling the dune cache for tests through (env) seems to work (I'll submit that in a separate PR)` but coq is still not cached. The opam file for coq 8.16.0 still overrides COQ_USE_DUNE and so it continues to use the make-based build. Do you know why that's the case?

[Alizter]

@emillon The 8.16 makefile just calls dune under the hood so it shouldn't be an issue. We are generating the build rules ourselves since Dune is unable to generate and execute at the same time. AFAIK if DUNE_CACHE=enabled then it should work. Have a look at Makefile.dune.

[emillon]

@emillon The 8.16 makefile just calls dune under the hood so it shouldn't be an issue. We are generating the build rules ourselves since Dune is unable to generate and execute at the same time. AFAIK if DUNE_CACHE=enabled then it should work. Have a look at Makefile.dune.

I understand that it's the intent, but this does not correspond to what is in the tarball that's being used by opam:

• here's the opam file as present in opam-repository - it calls make "COQ_USE_DUNE=" "-j%{jobs}%"
• this is executed after unpacking the tarball at this url. we can browse the contents of that tarball here (it's the V8.16.0 tag)
• the Makefile has the branching logic. because COQ_USE_DUNE is set to the empty string, this calls out the make-based build

What confuses me is that in master, the Makefile just calls out to dune. But the version in the 8.16.0 release tarball does not have this so we're never going into Makefile.dune through opam.

Do you see what I mean? I don't know how the coq release process works in terms of branches and tags but the changes in the Makefile have not been propagated to the release tag.

[Alizter]

@emillon Sorry you are correct! It has been some time since I thought about it. I guess we have to wait one more version to take advantage of the Dune caching via opam.

The changes Emilio and I made switching everything to Dune is in rocq-prover/rocq#15560 and that was tagged 8.17 rather than 8.16. The reason 8.16 released now is because the Summer got in the way.

[emillon]

Makes sense! so 8.17 should use the dune cache out of the box.