ajoute le stock chaud, la correction automatique et les nouveaux essais de création de stack

Stock de stacks prêtes par lab dans Redis (prise atomique en Lua, ménage
par comparaison avec Heat, disjoncteur), files gérées par Horizon, séances
planifiables. Correcteur Go sur l'hyperviseur : socket Unix, commandes lues
dans le lab.yaml uniquement, exécution par l'agent invité QEMU. Une création
de stack ratée est supprimée et réessayée deux fois, puis la session passe
en échec, visible du prof.

Corrige aussi trois défauts des étapes précédentes : la console se coupait
à la première frappe d'un navigateur (trames texte), l'élève ne pouvait pas
rejoindre une séance, la déconnexion n'avait pas de jeton CSRF.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This commit is contained in:
Adam Belkacemi 2026-10-08 21:52:16 +02:00
parent ca2f6f3b7a
commit 80b6c0722d
71 changed files with 2959 additions and 170 deletions

View file

@ -0,0 +1,54 @@
# Post-mortem — la première touche frappée coupait la console de l'élève
- **Date** : 2026-10-08 (défaut introduit à l'étape 9, découvert à l'étape 11)
- **Durée** : défaut latent depuis l'étape 9 ; corrigé dans l'heure suivant sa découverte
- **Gravité** : élevée si elle avait atteint une classe — aucun élève n'aurait pu taper une seule commande dans un vrai navigateur. Impact réel nul : aucun utilisateur.
- **Impact** : avec xterm.js, la première frappe de l'élève faisait fermer la connexion à la VM ; la console restait affichée mais muette.
## Résumé
`nova-serialproxy` (sous-protocole WebSocket `binary`) ferme sa connexion
dès qu'il reçoit une trame **texte**. Or xterm.js, dans le navigateur, envoie
les frappes en trames texte (`ws.send(chaîne)`), et le proxy Go les relayait
vers l'amont avec leur type d'origine.
Le test de l'étape 9 (`proxy-console/test-manuel.py`) envoyait des trames
**binaires** (`send_binary`) : il passait, et le critère « une élève tape
`ip a` et voit le résultat » a été déclaré vérifié sans qu'aucun vrai
navigateur n'ait tapé une touche.
## Chronologie
1. Étape 9 : proxy écrit et testé avec un script qui envoie du binaire. Critère validé.
2. Étape 11 : le script de parcours (`portail/tests/Reels/parcours-lab.py`) imite xterm.js et envoie `"\r"` en trame texte pour réveiller la console : aucune invite `login:`.
3. Journaux : `proxy-console` → « connexion amont fermée » 2 s après l'ouverture, à l'instant de la trame texte ; `nova-serialproxy` ne dit rien de plus.
4. Diagnostic par comparaison directe (`/tmp/diag-trames.py`) : trame texte → rien puis connexion perdue.
5. Correctif : `proxy-console/hub.go`, les frappes partent toujours en `websocket.BinaryMessage` vers l'amont. Redéployé ; texte et binaire font apparaître `login:`.
## Cause racine
Le test de l'étape 9 ne reproduisait pas le vrai client : il prenait un
raccourci (binaire) que le navigateur ne prend pas. La différence entre
« le chemin fonctionne » et « le chemin fonctionne avec le vrai client »
n'était pas testée.
## Ce qui a bien fonctionné
- Écrire le test de l'étape 11 comme un vrai navigateur (connexion, CSRF, jeton de console, trames texte) a fait remonter le défaut avant tout pilote.
- Les journaux du proxy, horodatés à la seconde, ont permis de relier la fermeture à la trame en quelques minutes.
## Actions correctives
- [x] Le proxy normalise : toute frappe part en binaire vers `nova-serialproxy`, quel que soit le client.
- [x] `parcours-lab.py` envoie des trames texte, comme xterm.js : il protège désormais contre ce défaut.
- [ ] Étape 12 : vérifier une fois le parcours dans un vrai navigateur (Playwright), la vérification visuelle de l'étape 8 n'ayant pas pu être faite.
## Comprendre
Un test qui passe ne prouve que ce qu'il teste vraiment. Le script de
l'étape 9 parlait au proxy « comme un outil », pas « comme un navigateur » :
il envoyait des octets bruts, alors qu'un navigateur envoie du texte. Les deux
arrivent au même proxy, mais `nova-serialproxy` les traite différemment. La
leçon générale : pour valider un critère utilisateur, le test doit imiter le
vrai client jusque dans les détails qui paraissent anodins — ici, le type de
trame WebSocket.