strings

Stream: general

[Rob Lewis]

This works:

def s : string := /- 4084 '0's -/

But not if you make it 4085.

deep recursion was detected at 'replace' (potential solution: increase stack space in your system)

[Rob Lewis]

Do we really have an effective 4084 character limit on strings?

[Rob Lewis]

We seem to be able to process and trace longer strings. But not to use them expanded in definitions.

[Simon Hudon]

I don't think it's specific about strings. There's a bound on the stack size. By looking at that message, it's probably 4 kb

[Gabriel Ebner]

Rob Lewis said:

Do we really have an effective 4084 character limit on strings?

Yes, for various reasons. If you write the string literal literally, then it is a deeply nested term, lots of stuff will break on that. If you're clever and write "3000chars" ++ "3000chars" then the VM compiler will fail because there are 6000 branches in the bytecode. (Each character is checked to be a valid Unicode codepoint.) EDIT: wrong theory, but the stack usage of the optimization pass is still proportional to the function size.

[Sebastian Ullrich]

Fixed in Lean 4