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

fix: remove non-conforming size-0 arrays #5564

Merged
merged 1 commit into from
Oct 1, 2024

Conversation

eric-wieser
Copy link
Contributor

@eric-wieser eric-wieser commented Oct 1, 2024

In C, these are supported only as a vendor extension; they should instead use proper C99 flexible array members.

In C++, both [] and [0] are vendor extensions.

These are supported only as a vendor extension; they should instead use proper C99 flexible array members.

Co-authored-by: Thomas Köppe <[email protected]>
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Oct 1, 2024
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d0ee9d012774d4343ca2078b19adb11b10940fe0 --onto 5e8718dff9d7906e1d4ca7020256dae7c05e49c2. (2024-10-01 14:08:55)

@tkoeppe
Copy link
Contributor

tkoeppe commented Oct 1, 2024

We wanted to note separately that the header lean.h, despite best efforts, is not actually conforming as a C and C++ interop header, since neither zero-sized nor flexible array members are conforming C++.

This change is still useful to make non-conforming C into conforming C, but as an interop header, the header should not contain these type definitions at all, and only declare opaque functions that can be used from both languages. The struct types with flexible array members should only exist in the C code.

@eric-wieser eric-wieser marked this pull request as ready for review October 1, 2024 14:43
@nomeata nomeata added this pull request to the merge queue Oct 1, 2024
Merged via the queue into leanprover:master with commit e90c3cf Oct 1, 2024
14 checks passed
@eric-wieser eric-wieser deleted the patch-21 branch October 1, 2024 15:48
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants