Skip to content

Conversation

@ppedrot
Copy link
Contributor

@ppedrot ppedrot commented Sep 28, 2025

No description provided.

@ppedrot ppedrot enabled auto-merge (squash) September 28, 2025 15:16
@ppedrot ppedrot disabled auto-merge September 28, 2025 15:21
@ppedrot
Copy link
Contributor Author

ppedrot commented Sep 28, 2025

I'm clearly no fullstack dev.

@ppedrot ppedrot closed this Sep 28, 2025
@ppedrot ppedrot reopened this Sep 28, 2025
@ppedrot ppedrot force-pushed the fix-rocq-docker-image branch from 2c7ee35 to 7a2c481 Compare September 28, 2025 15:25
@ppedrot ppedrot enabled auto-merge (squash) September 28, 2025 15:30
@ppedrot
Copy link
Contributor Author

ppedrot commented Sep 28, 2025

For some reason, 8.19 and 8.20 take more than one hour to succeed, but this does not seem related to this patch. Rather, we're just compiling a bunch of reverse deps that are not there in the other runs.

@ppedrot ppedrot disabled auto-merge September 28, 2025 16:53
@ppedrot ppedrot enabled auto-merge (squash) September 28, 2025 16:53
@SkySkimmer SkySkimmer disabled auto-merge September 28, 2025 17:39
@SkySkimmer SkySkimmer enabled auto-merge (squash) September 28, 2025 17:40
@Lysxia
Copy link
Contributor

Lysxia commented Sep 29, 2025

ping @liyishuai @gmalecha who has the permissions for this?

@ppedrot ppedrot disabled auto-merge September 29, 2025 12:54
@Zimmi48
Copy link
Member

Zimmi48 commented Sep 29, 2025

The reason why it is testing reverse deps is because of this line in the meta.yml file:

ci_test_dependants: true

No idea why this happens only for Coq 8.20.

@SkySkimmer
Copy link
Contributor

No idea why this happens only for Coq 8.20.

It's not that it doesn't happen for 9.0 and dev, it's that certicoq has no package compatible with them so only gets tested (and brings in its metacoq dep) on 8.19 and 8.20.

@SkySkimmer SkySkimmer closed this Sep 29, 2025
auto-merge was automatically disabled September 29, 2025 13:23

Pull request was closed

@SkySkimmer SkySkimmer reopened this Sep 29, 2025
@SkySkimmer SkySkimmer enabled auto-merge (squash) September 29, 2025 13:26
@SkySkimmer SkySkimmer disabled auto-merge September 29, 2025 13:26
@SkySkimmer SkySkimmer enabled auto-merge (rebase) September 29, 2025 13:27
@SkySkimmer SkySkimmer disabled auto-merge September 29, 2025 15:04
@SkySkimmer SkySkimmer enabled auto-merge (squash) September 29, 2025 15:04
@SkySkimmer SkySkimmer merged commit dead440 into rocq-community:master Sep 29, 2025
13 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants