Stream: Hydras & Co. universe

Topic: Package issue

view this post on Zulip Pierre Castéran (Dec 21 2022 at 16:44):

The Docker CI for 8.13 failed with the following message:

Error:  Package conflict!
    * Missing dependency:
      - coq >= 8.14~
      not available because the package is pinned to version 8.13.2

view this post on Zulip Karl Palmskog (Dec 21 2022 at 17:50):

@Pierre Castéran the problem is as follows and specific to the coq-goedel package. We can only use the coq-coqprime.dev package as a dep for coq-goedel, since the changes from pocklington we added are not in a release of coq-coqprime yet. And the coq-coqprime.dev package recently started to require Coq 8.14 or later (this package update)

view this post on Zulip Karl Palmskog (Dec 21 2022 at 17:53):

there are two solutions here:

  1. we officially drop compatibility with Coq 8.13. It's quite old now, so this is fine by me at least.
  2. we set up a separate CI workflow for testing with Coq 8.13 that doesn't include coq-goedel. This is quite easy to do, but would be a bit ad-hoc.

view this post on Zulip Karl Palmskog (Dec 21 2022 at 17:54):

let me know what you prefer

view this post on Zulip Pierre Castéran (Dec 21 2022 at 18:16):

I’m fine with dropping compatibility with 8.13.
Anyway, we have archives for old versions of Coq?

view this post on Zulip Karl Palmskog (Dec 21 2022 at 18:24):

sure, we did a release in May this year. Maybe we can follow the general approach of making one tag per major Coq release (Platform release)

view this post on Zulip Karl Palmskog (Dec 21 2022 at 18:34):

I guess we are doing PR reviews these days? https://github.com/coq-community/hydra-battles/pull/140

Last updated: Jun 11 2023 at 00:30 UTC