reducing String.data

Stream: lean4

[Wojciech Nawrocki]

Is this expected? It seems reducing String.data is somehow terribly expensive. Bumping maxRecDepth doesn't help, it runs out of stack space.

#reduce ("".data) -- []

/- maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit) -/
#reduce ("a".data)

[Leonardo de Moura]

Yes, this is expected.

[Andrés Goens]

why do you need to #reduce it?

[Mario Carneiro]

This is the same issue in lean 3 when you #reduce 'a'

[Mario Carneiro]

the problem is that a char is a unicode scalar value, which is a natural number less than 0x110000; even though you don't have to work out the numeral itself in lean 4 to unary anymore you still have to work out the proof that 97 is less than this value which is also ultimately encoded in unary

[Mario Carneiro]

If you strip the proofs it is fast:

#reduce ("a".data).map (·.toNat) -- [97]

[Wojciech Nawrocki]

Oh of course, I see. So this would reduce okay were the kernel not to reduce proofs, right?

[Mario Carneiro]

yes

[Mario Carneiro]

it wouldn't be hard to expose an option to do that either, #reduce isn't something the kernel does anyway, IIRC it's just a frontend command

[Sebastian Ullrich]

I guess we really should implement https://github.com/leanprover/lean4/blob/d780ed12b391baa3823afee9f79217becef684aa/src/Lean/Elab/BuiltinCommand.lean#L252. And probably default skipProofs to true.

[Mario Carneiro]

I think there is an argument for just removing #reduce entirely and moving it to std. It's more of a teaching tool than anything else

[Mario Carneiro]

and I think people semi-frequently get it confused with #eval