Skip to content

fix: correct lean_kernel_diag_is_enabled declaration to match generated C - #14886

Open
FawadHa1der wants to merge 1 commit into
leanprover:masterfrom
FawadHa1der:bug-lean_kernel_diag_is_enabled
Open

fix: correct lean_kernel_diag_is_enabled declaration to match generated C#14886
FawadHa1der wants to merge 1 commit into
leanprover:masterfrom
FawadHa1der:bug-lean_kernel_diag_is_enabled

Conversation

@FawadHa1der

Copy link
Copy Markdown
Contributor

This PR fixes the lean_kernel_diag_is_enabled C++ declaration to match generated C. This issue is manifesting only for wasm64 output but it is an issue nonetheless. C++ compiled to wasm64 via emscripten incorrectly translates based on the C++ external declaration.

Closes issue 14865

@FawadHa1der

Copy link
Copy Markdown
Contributor Author

maintainers apply the appropriate labels please. may be changelog-no (no observable change on supported targets) since wasm64 is not supported at the moment.

@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 Aug 21, 2026
@mathlib-lean-pr-testing

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f6c7d68c7fc27e3b60585f30740c7d141d3c5b36 --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-21 16:49:58)

@leanprover-bot

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase f6c7d68c7fc27e3b60585f30740c7d141d3c5b36 --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force reference manual CI using the force-manual-ci label. (2026-08-21 16:50:00)

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.

lean_kernel_diag_is_enabled implementation has one stray *

2 participants