Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

CI broken will break with update to 8.20 #64

Open
Zimmi48 opened this issue Oct 18, 2024 · 5 comments
Open

CI broken will break with update to 8.20 #64

Zimmi48 opened this issue Oct 18, 2024 · 5 comments

Comments

@Zimmi48
Copy link
Member

Zimmi48 commented Oct 18, 2024

Our current CI setup always uses the latest version of Coq.

A recent (auto-)upgrade from Coq 8.19 to Coq 8.20 has broken the CI (some tutorials are not compatible).

In practice, it seems not so reasonable to only test the latest Coq version given that the deployment still uses Coq 8.17 through jsCoq.

A natural solution would be to fix the Coq version used for the deployment to the one available in jsCoq and at the same time have other test jobs for different Coq versions.

@thomas-lamiaux
Copy link
Collaborator

@Zimmi48 duplicate of #64 ?

Anyway, if we switch to JsCoq2 soon, we will just be using 8.20 ?
We have not discussed the timeline yet, but I think it is fine to target compatibility with Rocq1 for the 1st "release" / index version, and hence to use the latest Coq version.

I'll try later with Coq 8.20 but I found the error weird.

@thomas-lamiaux
Copy link
Collaborator

Actually, I would prefer to use the current version of the coq platform because it is less work

@Zimmi48
Copy link
Member Author

Zimmi48 commented Oct 19, 2024

@Zimmi48 duplicate of #64 ?

Duplicate of what? This is #64.

compatibility with Rocq1

FTR, the first release of Rocq will be Rocq 9.0.

@thomas-lamiaux
Copy link
Collaborator

ha I meant #48.

@thomas-lamiaux
Copy link
Collaborator

I am renaming it

@thomas-lamiaux thomas-lamiaux changed the title CI broken since update to 8.20 CI broken will break with update to 8.20 Oct 21, 2024
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

No branches or pull requests

2 participants