Screen Readers in VS Code

Stream: general

[Tyler Josephson ⚛️]

Are there any folks in the Lean community who are visually impaired and use a screen reader? Or has anyone taught Lean to a student who uses a screen reader? I noticed that VS Code has accessibility tools - I’m curious if anyone has experience or feedback using this?

[Wojciech Nawrocki]

I don't have the answer, but just wanted to highlight that some input from visually impaired users would be very helpful. Especially in the infoview, I think the accessibility story is pretty tragic at the moment (e.g. this issue).

[Gabriel Ebner]

If you actually have a student who uses a screen reader, please get into contact with us. We want to make Lean more accessible, and I can invest time into making this happen.

[Patrick Massot]

I think using VSCode is a very bad start for blind people. If we want to make Lean accessible to them then we should focus on the vim or emacs extensions.

[Patrick Massot]

And this would probably also involve upstream work to make sure unicode is better handled by braille display libraries (one should at least check the status in brltty for instance).

[Patrick Massot]

Last time I checked, my PhD advisor who uses vi+brltty still complained about people using unicode-math in their TeX files.

[Tyler Josephson ⚛️]

Gabriel Ebner said:

If you actually have a student who uses a screen reader, please get into contact with us. We want to make Lean more accessible, and I can invest time into making this happen.

Thank you for the offer! I don’t have a student at the moment, but I’ll definitely reach out if/when I do. I’ve previously collaborated with a blind computational chemist, and was recently talking with her about ways my group might make our publications more accessible. This led me to thinking more broadly about making Lean accessible, so I thought I’d drop a note here, since others may have encountered this. I think with all the interactivity and automation that’s buildable, there’d be a lot of neat possibilities. But I definitely agree we need feedback from users to make this practical and appropriate.

[Wojciech Nawrocki]

Patrick Massot said:

I think using VSCode is a very bad start for blind people. If we want to make Lean accessible to them then we should focus on the vim or emacs extensions.

I am not certain this is true: see for instance the latest release notes which make a whole bunch of improvements for screen readers.