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 to https://github.com/coq/coq/pull/19530 #688

Merged
merged 1 commit into from
Dec 7, 2024

Conversation

proux01
Copy link
Contributor

@proux01 proux01 commented Sep 17, 2024

Adapt to coq/coq#19530
To be merged in sync with the upstream PR.

@proux01 proux01 force-pushed the stdlib_repo branch 2 times, most recently from fe2bb89 to d60f59f Compare December 2, 2024 20:03
Co-authored-by: Enrico Tassi <[email protected]>
@if $$(coqc --version | grep -q "8.19\|8.20") ; then \
sed -e 's/@@STDLIB_THEORY@@//' $< >> $@ ; \
else \
sed -e 's/@@STDLIB_THEORY@@/(theories Stdlib)/' $< >> $@ ; \
Copy link
Contributor

Choose a reason for hiding this comment

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

@proux can't we provide a stdlib-shim package for coq < 9 ?
Unless elpi is the only package needing this

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Well, coq-elpi is the only thing in the whole Coq CI that need this, so not sure it would be worth it. In any case, we should get rid of that dependency here (or at least isolate it to apps that really need it and put them in a separate coq-elpi-extra-apps or so package).

@proux01 proux01 marked this pull request as ready for review December 6, 2024 09:25
@proux01
Copy link
Contributor Author

proux01 commented Dec 6, 2024

Upstream PR merged, please merge

@ppedrot
Copy link
Collaborator

ppedrot commented Dec 7, 2024

@gares sorry to be a bit pushy, but a lot of stuff in the Coq CI depends on elpi, could you try to merge this asap so that we stabilize the Coq CI quickly?

-- Your desperate Rocq RM, truly.

@gares gares merged commit c082aee into LPCIC:master Dec 7, 2024
70 of 75 checks passed
@gares
Copy link
Contributor

gares commented Dec 7, 2024

Screenshot_20241207_093859_Firefox
You should have the rights

@ppedrot
Copy link
Collaborator

ppedrot commented Dec 7, 2024

ACK, but this is a somewhat non-trivial PR and I didn't want to interfere too much.

@proux01 proux01 deleted the stdlib_repo branch December 13, 2024 15:25
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