Zulip Chat Archive

Stream: lean4

Topic: reducing String.data


Wojciech Nawrocki (Nov 28 2022 at 17:27):

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 (Nov 28 2022 at 17:43):

Yes, this is expected.

Andrés Goens (Nov 28 2022 at 17:46):

why do you need to #reduce it?

Mario Carneiro (Nov 28 2022 at 17:49):

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

Mario Carneiro (Nov 28 2022 at 17:51):

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 (Nov 28 2022 at 17:52):

If you strip the proofs it is fast:

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

Wojciech Nawrocki (Nov 28 2022 at 17:59):

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

Mario Carneiro (Nov 28 2022 at 18:00):

yes

Mario Carneiro (Nov 28 2022 at 18:01):

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 (Nov 28 2022 at 18:04):

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 (Nov 28 2022 at 18:05):

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 (Nov 28 2022 at 18:06):

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


Last updated: Dec 20 2023 at 11:08 UTC