Skip to content

chore: limit JSON number exponent more - #15574

Open
Vtec234 wants to merge 1 commit into
masterfrom
json-exp
Open

Vtec234 wants to merge 1 commit into
masterfrom
json-exp

Conversation

@Vtec234

@Vtec234 Vtec234 commented Oct 9, 2026

Copy link
Copy Markdown
Member

This PR limits exponents accepted by Json.parse to 100_000. Beyond that, the JsonNumber representation either becomes prohibitively slow or panics.

@Vtec234 Vtec234 added the changelog-no Do not include this PR in the release changelog label Oct 9, 2026
@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 9, 2026
@Vtec234
Vtec234 requested a review from mhuisi October 9, 2026 10:17

@mhuisi mhuisi left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

This is a reasonable quick-fix. Do you know if there would be any significant breakage from adjusting JsonNumber to support positive exponents?

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-no Do not include this PR in the release changelog 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.

2 participants