Stack Overflow Error

[JeffreyChang12]

Imported.txt

run the following .v file

From LeanImport Require Import Lean.
Redirect "Imported.log" Lean Import "Imported.txt".

Error:
Error at line 7951 (for _private.Init.Prelude0.isValidChar_UInt32.match_1): #DEF 941 6701 6739
Stack overflow.

The Rocq Prover, version 9.1+alpha
compiled with OCaml 4.14.2

The lean file this originated from is in the following zipped folder, but I'm not sure which lean file:
https://drive.google.com/file/d/1khQgYVokS9bUFak3U3WVSXZsmQwCbz0C/view?usp=drive_link

[SkySkimmer]

the error message implies it's from https://github.com/leanprover/lean4/blob/b0e6db322421ce368999f08870fd747e45242f86/src/Init/Prelude.lean#L2789
Probably a problem with large nats
You can try to Set Debug "backtrace" before running Lean Import to see if the backtrace is useful.