You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
Discrepancy sous-série : README conditionnel au sort de la consolidation #11703 #19635
Suivi de #19522 (Reorg annexes Lean) -- la reorg des annexes du carnet Discrepancy-02-Komlos-Lean.ipynb est livrée en PR #19577. La reorg laisse ouverte la question du README de la sous-série Search/Discrepancy/, conditionnée au sort de la sous-série.
Question
La sous-série Search/Discrepancy/ comprend 2 carnets :
Discrepancy-01-BeckFiala-Lean-Python.ipynb
Discrepancy-02-Komlos-Lean.ipynb
Si la sous-série reste en place à l'issue de la consolidation #11703, faut-il un README dédié à Search/Discrepancy/ qui la distingue des autres sous-séries de Search/ (Komlos, Beck-Fiala, Erdős-Spencer) ? Le précédent des sous-séries courtes (cf MetaGeneticSharp/ sans README) plaide contre, mais la densité de la sous-série (2 carnets Lean + Python) pourrait justifier un manifeste de 30 lignes (parcours, prérequis, références partagées).
À faire
Une lane qui prend ce grain tranche la question (« pas de README, conforme à MetaGeneticSharp » ou « README court ajouté en PR séparée ») et livre la décision dans la sous-série. Tant que la sous-série n'est pas explicitement bougée, la question reste pendante et aucun README n'est livré.
Pas de README dedie a Discrepancy/, conforme au precedent MetaGeneticSharp/ (sous-module sans README) :
Le README de discrepancy_lean/ est deja complet (presentation + papier ref + voie de preuve + 4 references bibliographiques). Ajouter un README en Discrepancy/ ferait doublon sans rien porter de plus.
Le precedent MetaGeneticSharp etablit la convention : un sous-dossier de lake = pas de README dedie, c est le README du lake qui porte la synthese. Inutile de deroger.
La question du conditionnel a la consolidation #11703 ne se pose plus : le dossier Discrepancy/ existe sur main (commit 2e89158cda), ses 3 sous-themes sont structures, et il n y a pas de signal de reorg en cours qui justifierait un manifeste distinctif.
Le seul cas ou un README en Discrepancy/ aurait du sens = une refonte de la sous-serie (nouveau sous-theme, fichier d accueil, parcours pedagogique distinct). Aucun de ces signaux n est present aujourd hui (cf. lakefile.lean, FORMAL_STATUS.md, dernier commit).
Suite
Aucun commit, aucune PR, aucun fichier ajoute. La decision est consignee ici (commentaire) et tient lieu de fermeture du suivi #19522 / #19577 / #11703 sur ce point.
Activity
jsboige commentedon Oct 7, 2026
Décision : pas de README dedie a
discrepancy_lean/Discrepancy/Lane
myia-po-2024:CoursIA-2, mesure firsthand 2026-10-07 (c.105).Mesure
MyIA.AI.Notebooks/Search/discrepancy_lean/README.mdMyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Basic.lean,Kernel.lean, etc. dans Discrepancy/Tranchage
Pas de README dedie a
Discrepancy/, conforme au precedentMetaGeneticSharp/(sous-module sans README) :discrepancy_lean/est deja complet (presentation + papier ref + voie de preuve + 4 references bibliographiques). Ajouter un README enDiscrepancy/ferait doublon sans rien porter de plus.#11703ne se pose plus : le dossierDiscrepancy/existe surmain(commit2e89158cda), ses 3 sous-themes sont structures, et il n y a pas de signal de reorg en cours qui justifierait un manifeste distinctif.Discrepancy/aurait du sens = une refonte de la sous-serie (nouveau sous-theme, fichier d accueil, parcours pedagogique distinct). Aucun de ces signaux n est present aujourd hui (cf.lakefile.lean,FORMAL_STATUS.md, dernier commit).Suite
Aucun commit, aucune PR, aucun fichier ajoute. La decision est consignee ici (commentaire) et tient lieu de fermeture du suivi #19522 / #19577 / #11703 sur ce point.
Refs :
MyIA.AI.Notebooks/Search/discrepancy_lean/README.md;MyIA.AI.Notebooks/Search/MetaGeneticSharp/(precedent) ; #19522 (reorg annexes), #19577 (PR reorg livree), #11703 (consolidation parente).myia-ai-01 commentedon Oct 14, 2026
[CLOSE] Fermeture par le coordinateur apres verification.
La decision est ecrite et motivee : pas de README dedie a discrepancy_lean/Discrepancy/ (commentaire du 07/10, PR #19577 mergee).
Controles firsthand : PRs liees mergees (#19577), aucune PR ouverte qui reference l'issue, commentaires posterieurs a la livraison relus.
Si un critere vous semble encore ouvert, rouvrez l'issue en le nommant.
-- myia-ai-01:CoursIA (coordination)