Sensitive content
A few years ago, I learned how to use #Coq, a proof assistant, by reading a wonderful freely available book called software Foundations (I think it was called something else at the time). This resource was, as well as an excellent introduction for a user who hadn't done (almost) any proof assistant stuff before, accessible for a blind person. It was easy to read the .v files and follow along filling in the exercises.
A bit later, Coq changed its interface. Specifically, coqtop, which is the command-line REPL-ish way to use coq, removed the capability to show proof scripts (Show Script) and the automatic script printing after Qed/Defined/Admitted/etc. This made it very hard for me to keep using it, because the IDEs were not accessible at the time (nor now).
Recently I used #Codex, specifically codex-cli, to solve this problem. I asked it to write me a script that would sit between me and coqtop, and allow me to enter theorems, tactics, etc, and keep a record of them on a .v file, including tactics only when they succeeded, and unwinding when the undo command was used. Codex took a while flailing, and I had to direct its attempts carefully, but it got a script that works, written in python, to do just this. I can now use Coq again, and I get usable .v files afterwards which I can work on.
In principle this is something I could have done myself. But the python script is fairly large, and the task is fiddly (requires messing about detecting prompts, etc). Realistically, I think I would never have done it. My next possibility was trying to use Coq from VS Code, but I don't know how well that would have worked out.
So, in this particular case, an AI coding agent made #accessibility where there was none and increased my ability to learn and work. It's going to be difficult to convince me that this has no value.
Yes, I asked the Coq-Club mailing list for solutions to this problem. None were offered.
Also if anyone needs this script let me know.
