port-status#data/buffer/parser

Stream: mathlib4

[Eric Wieser]

What's the plan for this file and the downstream port-status#data/buffer/parser/numeral? cc @Yakov Pechersky

[Eric Wieser]

IIRC, start_port.sh doesn't work for lean core files, so you have to copy the file manually from mathport output

[Eric Wieser]

port-status#data/buffer/basic is marked "not needed" with no explanation; without this the numeral file is unportable.

[Ruben Van de Velde]

Do we need/want to port parser/numeral?

[Ruben Van de Velde]

I understood that lean 3 buffer was replaced by something else

[Scott Morrison]

I don't think we want data.buffer.parser.numeral either.

[Mario Carneiro]

lean 3 buffer is basically Array, although for character buffers you probably want to use String in lean 4

[Mario Carneiro]

I don't think it is unportable, but it might require a substantial rewrite, much like data.rbmap

[Eric Wieser]

:ping_pong: @Yakov Pechersky; are you happy if this doesn't end up in the "100% ported" mathlib4?

[Eric Wieser]

I would guess that we can (painfully) port data/buffer from lean3port (replacing buffer X with Array X), and then everything downstream will work without issue

[Yakov Pechersky]

I'm okay if it doesn't get ported as it is. I'd still want us to have a moral equivalent, like Mario said in a meeting the other week, that we can have proofs about how lean parsing works now.