search

uds-psl / coq-library-undecidability

A library of mechanised undecidability proofs in the Coq proof assistant.
Mozilla Public License 2.0
111 stars 30 forks source link

CI cache does not update #98

Open mrhaandi opened 4 years ago

mrhaandi commented 4 years ago

Currently, after each PR the CI runs opam upgrade each time resulting in upgrade coq 8.12.0 to 8.12.1. This should be done by the cache (and run only once) which currently does not seem to update correctly.

fakusb commented 4 years ago

In the workflow file, the key in the opam-cache action denotes which cache should be loaded: If we find a cache with exactly that key, we use it and do not change it in any way.

If we do not find key, but a key with a prefix listed in restore-keys, we use rhat other cache as "base", but save changes afterwards onder the key.

So we need to explicitly change the key whenever we want to be sure that we test a specific coq version. For example, we could add a variable to the workspace file to explicitly pin the tested version, and add this to the key-string.

I initially thought of using the opam file hash as suffix of the key and add the largest tested coq version, but that would mean we must watch out to not accidentally releasing an opam-package that does not work with new minor versions by default.

yforster commented 4 years ago

I initially thought of using the opam file hash as suffix of the key and add the largest tested coq version, but that would mean we must watch out to not accidentally releasing an opam-package that does not work with new minor versions by default.

Can we counter this by always specifying the exact upper bound in the opam file. E.g. in our case coq {>= "8.12." & <= "8.12.1"}?

fakusb commented 4 years ago

Yes, but then we must make sure to either not include the upper bound in the coq-opam repo. Or live with the fact that for every new 8.12.(x+1) bump, opam for users who updated coq does not compile our library until we say it's allowed, although most likely, fixlevel-releases do not impact our library at all.

I think we should just mention and pin coq explicitly in the CI-file.

fakusb commented 4 years ago

We could include the hash of the commit inside the key at the end to disable the keep-found-caches-without-update feature, and use the current key as restore-key. EDIT: (We should then remember that and not confuse ourselves if CI breakes for a new PR not because of the PR, but because the PR was the first one where a new coq version was used)

fakusb commented 4 years ago

related: https://github.com/actions/cache/issues/171 and https://github.com/actions/cache/issues/109

yforster commented 4 years ago

Or live with the fact that for every new 8.12.(x+1) bump, opam for users who updated coq does not compile our library until we say it's allowed, although most likely, fixlevel-releases do not impact our library at all.

The fixlevel-release of Coq 8.12.1 did impact our library - in fact compilation broke. We just fixed the issue way before we bumped CI to 8.12.1.

I think it's good to include an upper bound explicitly, especially in a phase like now were development is very active. At the same point were we bump CI we can bump the official opam release.