Skip to content

Put trakt back in CI#22137

Merged
coqbot-app[bot] merged 3 commits into
rocq-prover:masterfrom
ckeller:master
Jun 19, 2026
Merged

Put trakt back in CI#22137
coqbot-app[bot] merged 3 commits into
rocq-prover:masterfrom
ckeller:master

Conversation

@ckeller

@ckeller ckeller commented Jun 17, 2026

Copy link
Copy Markdown
Contributor

Trakt was about to be added to Rocq CI but for some health problems I was not able to finish it. Now it compiles again on Rocq master, and also got nice software engineering improvements on its own.

Note: smtcoq_trakt is not required to be in the CI anymore.

Note: @lafeychine is now a maintainer of trakt.

Fixes rocq-trakt/trakt#19

Trakt was about to be added to Rocq CI but for some health problems I was not able to finish it. Now it compiles again on Rocq master, and also got nice software engineering improvements on its own.
Note: smtcoq_trakt is not required to be in the CI anymore.
Note: @lafeychine is now a maintainer of trakt.
Fixes rocq-trakt/trakt#19
@ckeller ckeller requested a review from a team as a code owner June 17, 2026 13:03
@coqbot-app

coqbot-app Bot commented Jun 17, 2026

Copy link
Copy Markdown
Contributor

Hello, thanks for your pull request!
In the future, we strongly recommend that you do not use master as the name of your branch when submitting a pull request.
By the way, you may be interested in reading our contributing guide.

@coqbot-app

coqbot-app Bot commented Jun 17, 2026

Copy link
Copy Markdown
Contributor

I am not triggering a CI run on this PR because the CI configuration has been modified. CI can be triggered manually by an authorized contributor.

@coqbot-app coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jun 17, 2026
Comment thread dev/ci/scripts/ci-smtcoq_trakt.sh Outdated
@coqbot-app

coqbot-app Bot commented Jun 17, 2026

Copy link
Copy Markdown
Contributor

I am not triggering a CI run on this PR because the CI configuration has been modified. CI can be triggered manually by an authorized contributor.

@SkySkimmer

Copy link
Copy Markdown
Contributor

@coqbot run full ci

@coqbot-app coqbot-app Bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jun 17, 2026
@proux01

proux01 commented Jun 17, 2026

Copy link
Copy Markdown
Contributor

Apparently trakt depends on Stdlib and elpi, we should thus ensure it is tested in both CI before merging this (otherwise a change in Stdlib or elpi could break Rocq CI). elpi's CI seems to be good, we still have to update the CI of the Stdlib library.

@ckeller

ckeller commented Jun 17, 2026

Copy link
Copy Markdown
Contributor Author

we still have to update the CI of the Stdlib library

Should I do it on my side?

@proux01

proux01 commented Jun 17, 2026

Copy link
Copy Markdown
Contributor

I can do it if you can wait by the end of the week.

@ckeller

ckeller commented Jun 17, 2026

Copy link
Copy Markdown
Contributor Author

Sure, we are not in a hurry :-)

@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Jun 17, 2026
@coqbot-app

coqbot-app Bot commented Jun 17, 2026

Copy link
Copy Markdown
Contributor

I am not triggering a CI run on this PR because the CI configuration has been modified. CI can be triggered manually by an authorized contributor.

@coqbot-app coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jun 17, 2026
@SkySkimmer

Copy link
Copy Markdown
Contributor

@coqbot run full ci

@coqbot-app coqbot-app Bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Jun 17, 2026
proux01 added a commit to proux01/stdlib that referenced this pull request Jun 19, 2026
proux01 added a commit to proux01/stdlib that referenced this pull request Jun 19, 2026
@SkySkimmer SkySkimmer added the kind: infrastructure CI, build tools, development tools. label Jun 19, 2026
@SkySkimmer SkySkimmer added this to the 9.3+rc1 milestone Jun 19, 2026
@SkySkimmer

Copy link
Copy Markdown
Contributor

@proux01 can you self assign this PR? then when the stdlib side is ready you can merge both at the same time

@proux01 proux01 self-assigned this Jun 19, 2026
@proux01

proux01 commented Jun 19, 2026

Copy link
Copy Markdown
Contributor

Stdlib done rocq-prover/stdlib#280 , let's merge here

@coqbot merge now

@coqbot-app coqbot-app Bot merged commit 6555712 into rocq-prover:master Jun 19, 2026
8 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

kind: infrastructure CI, build tools, development tools.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Broken in Rocq CI

3 participants