Stream: Coq devs & plugin devs

Topic: ci-coq_library_undecidability and PR #17538


view this post on Zulip Andrej Dudenhefner (Apr 28 2023 at 07:17):

Adapting ci-coq_library_undecidability for https://github.com/coq/coq/pull/17538 unfortunately broke the current Coq CI.
If https://github.com/coq/coq/pull/17538 is merged soon, then there is no problem.
Otherwise, we need some intermediate solution.

view this post on Zulip Jason Gross (Apr 28 2023 at 07:23):

We should just merge #17538. But if you want a backwards compatible change, you can do a hack like replacing tmExistingInstance global (ConstRef name) with ltac:(eapply tmExistingInstance; try exact (ConstRef name); constructor <whichever number global is>)

view this post on Zulip Andrej Dudenhefner (Apr 28 2023 at 07:30):

Just merging #17538 is fine. The policy of coq_library_undecidability is to be compatible with a specific Coq version (and avoid legacy glue code).

view this post on Zulip Gaëtan Gilbert (Apr 28 2023 at 08:29):

merged


Last updated: Nov 29 2023 at 22:01 UTC