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.

Sign up for GitHub

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

Jump to bottom

drop -rectypes from coq_makefile OCaml compilation flags #17038

Merged
merged 1 commit into from Jan 3, 2023
Merged

drop -rectypes from coq_makefile OCaml compilation flags #17038

merged 1 commit into from Jan 3, 2023

Conversation

palmskog
Copy link
Contributor

@palmskog palmskog commented Dec 30, 2022 •
edited by SkySkimmer

After #16007 was merged, there is no need to use -rectypes anymore when compiling OCaml code that uses coq-core, in particular plugins. However, coq_makefile still passes -rectypes when it compiles OCaml code, so we remove it.

@SkySkimmer does this need a changelog?

Overlays:

@palmskog palmskog requested a review from a team as a code owner December 30, 2022 13:26
@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 Dec 30, 2022
@palmskog palmskog added the part: coq_makefile The coq_makefile binary for generating makefiles. label Dec 30, 2022
@Alizter
Copy link
Contributor

Alizter commented Dec 30, 2022

I would say yes for changelog so people don't get surprised.

@SkySkimmer
Copy link
Contributor

Yes changelog
It should say how to use rectypes for plugins which actually need it: in the local makefile (https://coq.github.io/doc/master/refman/practical-tools/utilities.html#coqmakefilelocal) put CAMLFLAGS+=-rectypes

@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 Dec 30, 2022
@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 Dec 30, 2022
@palmskog
Copy link
Contributor Author

@SkySkimmer I added the changelog, but could I get help with the overlays (that are seemingly required in some failing projects like Elpi, Itauto)? At least they would be backwards-compatible.

@Zimmi48 Zimmi48 added this to the 8.18+rc1 milestone Dec 30, 2022
@SkySkimmer
Copy link
Contributor

What help do you need? Is the local makefile not working?

palmskog added a commit to palmskog/coq-elpi that referenced this pull request Dec 30, 2022
@palmskog
Adapt to coq/coq#17038 (drop -rectypes flag as coq_makefile default)
9d2c0de
palmskog added a commit to palmskog/Coq-Equations that referenced this pull request Dec 30, 2022
@palmskog
Adapt to coq/coq#17038 (drop -rectypes flag as coq_makefile default)
9e030a2
@palmskog
Copy link
Contributor Author

@SkySkimmer I created LPCIC/coq-elpi#416 mattam82/Coq-Equations#523 - but for itauto, I don't have rights to create a fork+PR in Inria's GitLab. Could you maybe help out with that?

gares added a commit to LPCIC/coq-elpi that referenced this pull request Dec 30, 2022
@gares
Merge pull request #416 from palmskog/coq-master+rectypes
b58fe5b 
Adapt to coq/coq#17038 (drop -rectypes flag as coq_makefile default)
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Dec 31, 2022
@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 Dec 31, 2022
@SkySkimmer SkySkimmer self-assigned this Jan 3, 2023
@SkySkimmer SkySkimmer added the kind: infrastructure CI, build tools, development tools. label Jan 3, 2023
ppedrot added a commit to mattam82/Coq-Equations that referenced this pull request Jan 3, 2023
@ppedrot
Merge pull request #523 from palmskog/master+rectypes
e18d9e8 
Adapt to coq/coq#17038 (drop -rectypes flag as coq_makefile default)
@SkySkimmer
Copy link
Contributor

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 76010ef into coq:master Jan 3, 2023
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Jan 3, 2023

@SkySkimmer: Please take care of the following overlays:

  • 17038-palmskog-drop-rectypes-coq_makefile.sh

@palmskog palmskog deleted the drop-rectypes-coq_makefile branch January 3, 2023 14:10
rlepigre pushed a commit to rlepigre/itauto that referenced this pull request Sep 15, 2023
@SkySkimmer
Don't rely on rectypes
0bf9b60 
cf coq/coq#17038
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@SkySkimmer SkySkimmer SkySkimmer approved these changes

Assignees

@SkySkimmer SkySkimmer

Labels
kind: infrastructure CI, build tools, development tools. part: coq_makefile The coq_makefile binary for generating makefiles.
Projects
None yet
Milestone
8.18+rc1
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@palmskog @Alizter @SkySkimmer @Zimmi48