Skip to content

Port to Rocq 9.1#135

Open
4ever2 wants to merge 24 commits intoCertiCoq:masterfrom
4ever2:coq-9.1
Open

Port to Rocq 9.1#135
4ever2 wants to merge 24 commits intoCertiCoq:masterfrom
4ever2:coq-9.1

Conversation

@4ever2
Copy link

@4ever2 4ever2 commented Feb 22, 2026

Port CertiCoq to be compatible with Rocq 9.1, MetaRocq 1.4, and CompCert 3.17, based on @yforster's 9.1 branch.
It still depends on the Coq compatibility wrapper as I haven't ported the makefiles.

CI needs to be updated with a new Docker image with Rocq 9.1 before merging.

@4ever2 4ever2 marked this pull request as draft February 22, 2026 20:45
@4ever2 4ever2 force-pushed the coq-9.1 branch 2 times, most recently from 962ec1c to a806cc5 Compare February 23, 2026 16:44
@4ever2 4ever2 marked this pull request as ready for review February 23, 2026 16:45
@mattam82
Copy link
Collaborator

mattam82 commented Mar 4, 2026

Thanks a bunch @4ever2 !

@4ever2
Copy link
Author

4ever2 commented Mar 4, 2026

@mattam82 Can we get a new Docker image for CI with Rocq 9.1, CompCert 3.17, MetaRocq 1.4.1+9.1, coq-wasm 2.2.0.

@mattam82
Copy link
Collaborator

mattam82 commented Mar 4, 2026

I'm on it

@mattam82
Copy link
Collaborator

mattam82 commented Mar 4, 2026

@4ever2 the pipeline producing it runs here https://gitlab.inria.fr/sozeau/docker-keeper/-/pipelines/1365158 and the image should appear here https://hub.docker.com/r/mattam82/metacoq/tags

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.

3 participants