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

Adapt w.r.t. coq/coq#18652. #722

Merged
merged 6 commits into from
Feb 19, 2024
Merged

Conversation

ppedrot
Copy link
Member

@ppedrot ppedrot commented Feb 9, 2024

No description provided.

Copy link
Member

@gares gares left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This change breaks 8.19 and 8.18.
We use ppx_optcomp that gives you ifdefs at the top level. There are a few examples around already, please follow that style

@ppedrot ppedrot force-pushed the prettyp-explicit-env branch from bcfd2bd to 83e4a89 Compare February 10, 2024 13:40
@ppedrot ppedrot requested a review from gares February 10, 2024 13:40
@ppedrot
Copy link
Member Author

ppedrot commented Feb 10, 2024

Fixed.

@gares
Copy link
Member

gares commented Feb 11, 2024

@rtetley we should not fail fast in the matrix. Here coq master does not include the change yet, but we still want to test 8.18 and 8.19

@gares
Copy link
Member

gares commented Feb 11, 2024

Also the opamfile ditches .dev, so we test coq 8.19 twice (the dev job downgrades it)

@gares
Copy link
Member

gares commented Feb 11, 2024

We should add a ... | = "dev" in the expression

@gares
Copy link
Member

gares commented Feb 11, 2024

Sorry for pushing here ci changes, but this is the first PR after the ppx_optcomp change, hence we need to streamline the process

@gares
Copy link
Member

gares commented Feb 11, 2024

Opam ci still broken. We need to pin coq to the version, otherwise the next command upgrades it to .dev

.github/workflows/ci.yml Outdated Show resolved Hide resolved
@gares gares marked this pull request as ready for review February 11, 2024 15:48
@gares
Copy link
Member

gares commented Feb 11, 2024

looks finally ok, the only jobs failing are the ones about coq master, since these are tested by Coq ci (against the PR requiring this change). The jobs about stable versions are green.

@rtetley the CI changes can be pushed to master, IMO. Dunno if we want the dev jobs to be in allowed-failure, or not. It could make the reading of this CI much clearer for the coq dev submitting PRs.

@ppedrot
Copy link
Member Author

ppedrot commented Feb 11, 2024

There are unrelated changes in this PR, maybe it should still be marked as a draft while the upstream Coq PR is not merged...

@gares gares marked this pull request as draft February 11, 2024 21:54
@gares gares mentioned this pull request Feb 12, 2024
@SkySkimmer SkySkimmer marked this pull request as ready for review February 19, 2024 11:30
@SkySkimmer SkySkimmer merged commit 50231cb into coq:main Feb 19, 2024
11 of 15 checks passed
@ppedrot ppedrot deleted the prettyp-explicit-env branch February 19, 2024 12:13
@rtetley rtetley mentioned this pull request Feb 19, 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

Successfully merging this pull request may close these issues.

3 participants