Face aux mouvements de contestation de la Gen Z de Madagascar qui, à la base manifeste pour un réel accès à l'eau potable et à électricité sans coupure, le président malgache a nommé comme premier ministre un général de l'armée de terre.

22 personnes sont mortes selon les chiffres de l'ONU qui datent d'il y a déjà une semaine. Une grève générale est prévue si le gouvernement ne répond pas aux exigences du mouvement Gen Z et la répression des forces de l'ordre va sûrement être de nouveau violente. Il est important de regarder et de partager ce qu'il se passe là-bas.

Bluesky et Mastodon dans tout ça ? La portée de ces évènements est assez faible sur le fedivers, les rares publications sur le sujet que j'ai vues passer sont à peine partagées.

Bluesky c'est à peine mieux mais uniquement parce qu'il y a plus de monde qu'ici, une recherche du terme "Madagascar" sur Bluesky me donne un peu trop de résultats sur les films d'animation.

Et honnêtement je m'en fous, si on doit combattre l'algorithme sur les réseaux sociaux détenus par des milliardaires pour avoir de la portée médiatique, on fera ce qu'il faudra.

Two years ago today was the vicious Hamas October 7th attack. So much suffering of innocents on that day, so much suffering since. That was of course what Hamas wanted; their plan was to provoke a response from the Israeli government that would eventually weaken international support for Israel.

I pray that the residents of the Holy Land may live in peace someday. May it be soon.

#Israel #Palestine #Gaza

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.

#AI #a11y #coding