Lionel Draghi a écrit 119 commentaires

Et voilà, quand on fait des commentaires en béotien, on tombe à côté :-)

Ce n'est probablement pas lié à la définition de SPARK himself, mais je crois que gnatprove utilise Why3.
Je ne comprends pas ce que cela implique, mais comme tu l'as associé à la logique de Hoare dans ton intro, ça semble confirmer.

Ca ne va pas compléter la pyramide animale des musiciens de Brême, ni contribuer à ce très intéressant état de l'art mathématique sur le sujet, mais pour l'anecdote j'ajoute l'exemple de la spécification de la procedure Swap avec le prouveur SPARK et le langage Ada :

    procedure Swap (A, B : in out Integer)
       with Post => A = B'Old and B = A'Old;

Intéressant au passage de voir comment la syntaxe des langages, en utilisant plus ou moins de symboles, se destine plus à des mathématiciens ou à des béotiens informaticiens.

PS1 : je ne fais pas partie des spécialistes de SPARK
PS2 : je fais partie des béotiens :-)

Par contre je n'ai pas compris l'intérêt d'avoir les cas de tests et les résultats attendus dans la doc.

En réalité, ça dépend de quelle doc on parle. Il y a une grande souplesse avec ce système.

Par exemple dans les tests de bbt, j'ai séparé en plusieurs répertoires.
1. les fonctions du logiciel : elles sont dans le répertoire features. Il s'agit en réalité de la totalité des tests d'acceptation. Ce n'est pas une doc utilisateur, qui doit être plus synthétique : ici, il y a plein de cas, y compris des tests de robustesses, et ce n'est pas structuré pour être pédagogique.
2. les exemples : je ne veux pas que la doc donne des tests qui ne marchent plus, à cause d'une typo ou d'une évolution. Le problème est réglé comme ça, les exemples sont dans la suite de tests.
3. les tests de non reg : en réalité ceux la n'ont rien à faire dans le répertoire docs (je vais les remettre dans le répertoire tests). C'est très utile, mais c'est pour les devs, pas pour les utilisateurs.

Et dans le répertoire features, il y un sous répertoire proposed_features, qui permet de discuter de fonction non encore implémentées.

Donc rien n'empêche d'avoir un guide utilisateur avec quelques exemples dans un doc, un cahier de recette avec des tests d'acceptation dans un autre doc, des tests qui ne passent pas encore dans un doc de backlog, etc.

J'ai justement un outil à tester, je vais voir si ça colle

Dis moi si je peux aider!

PS : attention, l'exemple que tu sites (run_error_msg.md) n'est pas dans la suite de tests, c'est du travail en cours. Tout ce qui est exécuté se trouve dans les sous-répertoires de docs, et principalement dans le répertoire features.

Mais j'imagine l'équivalent d'une page de manuel comme celle de ls, ce serait un peu indigeste , non ?

Je ne sais pas, ça serait à explorer, j'attends d'avoir un bon use case!

J'ai fait un embryon de ce que ça pourrait être avec le début de test de rpl qui se trouve dans les exemples.
Je ne l'ai fait que pour une option, mais il me semble que ça pourrait s'étendre à plus.

Je suis d'accord que les Given/When/Then sont un peu lourd dans une doc utilisateur.
Ça ne dispensera pas de faire plus tard un truc court pour tdlr, de faire une man page, une faq, un guide utilisateur, etc.

Mais dans un premier temps, le rapport temps passé pour avoir une doc quand même lisible et les tests qui vont avec me parait imbattable. Et pour plein de projet il n'y aura jamais besoin d'aller plus loin.

Drôle, le deuxième lien sur la discussion, c'est vieux de vingt ans mais j'y avais participé!

Comme aujourd'hui, je ne devais pas être convaincu par la machine à gaz du literate programming, qui était le sujet initial, et j'étais parti sur une façon pragmatique de générer de la doc à partir du code (ce qui n'est pas du literate programming).

Bref, je ne sais pas ce qu'est le literate programming, mais je vois un point commun avec bbt : la documentation contient des tests, avec une description malgré tout formelle, au milieu d'un texte libre.

Et une différence : il y a bien un mélange entre formel et informel (Donald Knuth parle de la nécessité d'avoir les deux pour que ce qu'il y a à comprendre rentre bien dans le crâne du lecteur). Mais sur la partie formelle (c'est à dire en gros les steps) on essaie d'être en anglais, aussi lisible que la partie informelle.

Ce qui a bien changé pour moi depuis cette discussion d'il y a 20 ans, c'est que j'ai réalisé à quel point l'exercice de génération de documentation à partir du code était vain.

1. Je ne lis jamais ces docs. Déjà à l'époque, tout les IDE (moi j'étais sous emacs) permettaient de sauter directement à la déclaration de la fonction truc, ou se trouvaient les commentaires permettant de générer la doc. Donc la doc ne servaient à rien.

2. Au contraire, les tags mis dans les commentaires pour effectuer la génération viennent rendre la code moche et moins lisible. C'est pourquoi je faisais l'apologie de NaturalDocs à l'époque (et de Markdown maintenant) : embellir, OK, mais l'original doit rester lisible, tant que ce sera la que l'on travaillera en premier lieu.

3. La doc la plus intéressante contient justement ce qui ne figure pas dans le code, ce que le code ne peut pas transcrire (cf. le niveau sémantique dont je parlais plus haut). Et, petit parallèle avec literate programming, il n'y a pas forcément d'endroit idéal dans le code pour mettre ces infos en commentaire.
   Des choix d'architecture, par exemple, pourquoi les mettres dans un source plutôt qu'un autre? Leurs place n'est en fait pas dans un source, mais dans un doc qui s'appele "choix d'architecture".

4. je n'utilise plus de header systématique de fichier ou de fonction, qui stimule l'écriture de commentaires à 80% insipide. Si j'ai quelque chose à dire, je le dis. Dans la spec si ça concerne l'utilisateur, dans le body si ça concerne le mainteneur.

Donc, j'essaie :
1. d'écrire un code clair (quel pied quand il n'y a pas besoin de commentaire!)
2. je mets des commentaires là ou il faut, et pas plus.
3. je n'extrait plus rien du code, si tu veux voir le code, ben va voir le code!
Mon code est beau :-), il n'a rien à cacher et n'a pas besoin de maquillage. Ton IDE est génial, tu peux naviguer avec, pas besoin d'html.
4. la documentation qui m'intéresse le plus sur un outil, c'est celle qui m'explique ce que je peux faire avec. Or, et là on rejoint le sujet, cette doc donne généralement des exemples, des limitations et des cas d'erreurs, que l'on retrouve également dans les tests.
Donc, terminé d'écrire deux fois les choses : maintenant, avec bbt, j'écris un seul des deux.

Mais peut-être que dans encore 20 ans je dirai tout autre chose :-)

(Si GPT 13.z me laisse encore programmer).

pas idiot du tout, débat très intéressant au contraire!

C'est le problème éternel du niveau sémantique.
Le besoin du client n'est pas complètement traduit pas dans le code. Le LLM va être très bon pour décrire la logique du code (ca marche déjà très bien et c'est bien intégré dans vscode et autre).
Mais pour le reste il va inventer, et si le code est faux, il va se tromper.

Même la conception du logiciel n'est pas complètement traduite dans le code. Je prends un exemple qui provient du README du projet sur lequel j'utilise justement bbt pour faire les tests, acc : si le concepteur définit un logiciel en couches, couche C1 avec les modules A et B au dessus d'une couche C2 avec les modules C et D, le code n'embarque pas cette sémantique.
Le LLM verra dans le code qu'il y a un include de C dans A, de D dans C, mais il ne verra pas forcément qu'il y a une architecture en couche.

Parce que, en changeant de niveau sémantique, il y a perte d'information.

Si on laisse les LLM faire ce qui nous amuse, c'est à dire le code, alors je pense qu'il est plus efficace de procéder dans l'autre sens : il vaut mieux générer le code à partir d'une description du besoin plutôt que de lui demander de reconstituer le besoin à partir du code.

La différence avec l’approche présentée dans le billet est juste que le langage de test est clairement séparé et plus formel.

En fait, la différence essentielle est la nature du besoin, ce que j'ai évoqué dans ma réponse précédente. L'objectif n'est pas ici de faire du test unitaire, de définir, documenter ou prouver formellement le comportement du code.

L'objectif est de décrire le comportement de l'appli vue de l'utilisateur. bbt est destiné au test "end-to-end", pas aux tests unitaires ou aux test d'intégration ou autre.

Je viens de regarder Catala, très intéressant. C'est un DSL spécialisé, il y a bien un rapport avec bbt.
Mais bbt fait en sorte que son DSL se fonde dans la langue anglaise (en masquant un cadre Gherkin et une syntaxe spécifique), Catala utilise une syntaxe très informatique, avec des if then else.

Mais le use case de Catala est beaucoup plus complexe que celui de bbt, me semble-t-il, car pour l'analyse de texte juridique, si on a pas une modélisation formelle comme celle proposée par Catala, on doit en passer par des LLM, avec pas mal de verrous technologiques à la clé. Je sais que l'activité sur ce sujet est vraiment intense, mais je ne suis pas un spécialiste et je ne veux pas commenter.

pour ma part j'aime beaucoup l'approche d'une doc rédigée directement dans le code, avec des exemples qui sont testés

Merci pour le retour.
Je ne vise pas en fait ce type de documentation, qui explicite le code et le design, et donc est légitime à être dans le code, et qui se destine aux personnes qui doivent intervenir dans le code ou la conception.

Je cible plutôt une documentation vraiment "utilisateur", qui décrit le comportement attendu (cf. BDD, ATDD).

Y a-t-il des plans pour sortir du modèle "appeler un binaire" et permettre l'exécution des tests dans un code de test ?

A partir du moment ou tu te positionnes dans un code de test, ce n'est plus le créneau de bbt : tu peux utiliser des solutions existantes, et le fait d'exprimer le besoin en anglais plutôt que dans tel ou tel langage de programmation perd de son intérêt.

Ou alors, je n'ai pas compris ce que tu proposes.

Du coup, en partant de la supposition qu'il y aura fatalement des cas demander une telle complexité, ton outil propose-t-il des fonctionnalités du même genre qu'expect, ou est-ce prévu ?

Merci pour le retour. Oui Expect est dans le radar.

J'ai fait une petite liste des choses intéressantes que j'ai trouvé sur le net, qui m'ont inspirées pour des détails de syntaxe ou pour les fonctionnalités : https://github.com/LionelDraghi/bbt/blob/main/docs/comparables.md

La constante, c'est que tous ces outils utilisent un langage trop éloigné à mon goût de l'anglais pour figurer directement dans une doc. Mon point principal c'est le chemin direct de la doc au test. Et faire une surcouche à Expect pourrait être une solution, mais le contraire est également possible (et a déjà été discuté), c'est à dire utiliser une librairie Ada qui offre une API Expect.

Sur la roadmap, la fonction d'interaction (être capable de répondre yes ou no quand ça prompte) est prévue. Je n'en ai pas (encore) besoin pour mes applications, mais j'en ai besoin pour tester bbt lui-même, car il prompte l'utilisateur pour confirmer des effacements. Et pour l'instant, je ne teste pas ces comportements.

De façon générale, les outils disponibles, et en particulier ceux que je liste ci-dessus, offrent plus de fonctionnalité que bbt. Mais bbt vient sur un créneau spécifique, dont la simplicité est une composante importante, et je ne souhaite pas le rendre trop complexe, ni imiter l'existant.

Petit témoignage

Malgré plusieurs tentatives, je n'ai pas réussi à faire passer le nom "slashbin" pour un de mes chats ou pour mon chien, la démocratie familiale me mettant systématiquement en minorité.
(Pourtant, moi ça me faisait beaucoup rire par anticipation de l'appeler "Slashbin" en le promenant!)

Et puis la chance à tourné, à l'occasion d'une adoption ou on nous a proposé un deuxième chat, la famille n'étant pas sûr que je valide, j'ai fait un peu de chantage et j'ai monnayé mon oui contre le fait de l'appeler Linux, tout simplement.

Quelques semaines plus tard, le premier des deux frères nous a abandonné. Il a posé ses valises chez une voisine (chez qui il est le seul chat), cet ingrat, ce Tanguy.

Et Linux, lui, est resté.

Moralité : Linux, c'est fiable.

PS : merci d'insérer à la prochaine occurrence du sondage la réponse "mon Chien s'appelle Slashbin".
Ca me donnera un moyen de revenir à la charge et de dire à ma femme tu vois bien que c'est pas de la maltraitance!

Merci pour le pointeur, je vais regarder ce que sait faire inotify.

Incidemment, le cas d'usage de lk-reducer est très intéressant: Il s'agit, si j'ai bien compris, de nettoyer une arborescence kernel de tous les fichiers qui trainent mais ne servent plus.
On lance sous monitoring un make et un make mrproper, et ensuite on repère les fichiers qui n'ont pas été accédé pendant le make, et qui ne sont pas nettoyé par le make mrproper.

Je ne me suis intéressé qu'aux fichiers lus ou écrits, mais en effet, dans ce cas les fichiers non accédés sont une info intéressante! Je le note comme un ajout fonctionnel possible à smk: après un build, on pourrait demander à smk quels fichiers d'une arborescence n'ont pas été concerné par ce qui a été exécuté.

L'autre point pas inintéressant, c'est le mode interactif: je lance un shell, et c'est tout ce qui est exécuté pendant que je suis dans ce shell qui est observé. Le fichier de log qui classe les fichiers en "Accessed, Untouched, or Generated" est écrit à la sortie du shell. Les commandes sont donc analysées comme une opération unique, puisque c'est ce qui nous intéresse ici.

Pas encore sûr d'en faire quelque chose, mais je le note!

Bonjour Benoar,

On ne peut pas dire que smk "oublie", puisque ce que tu décrit n'est pas du tout la cible visée par l'outil, et que c'est indiqué clairement à plein d'endroit sur le site, dans l'article et dans mes réponses. Je rappelle le créneau : simplicité, universalité.
Je n'ai aucune intention de refaire un bmake.

(D'ailleurs, si le créneau n'était pas celui là, j'aurai juste arrêté le projet et conseiller l'usage de fabricate, que j'ai découvert par les réponses dans ce journal).

La ou je suis moins pessimiste que toi sur l'utilité même pour un grand programme, c'est que je vois très bien en revanche un smkfile lister les commandes à exécuter pour le packaging, l'installation et la désinstallation, etc.

Je te dirais même que pour la désinstallation par exemple, comme smk connait tous les fichiers qui ont été créé par l'installation, y a moyen que ce soit redoutablement simple.
Merci pour l'idée, je vais voir si je peux en faire un cas de test (qui ne sera pas simple, car comment gérer les updates de fichiers existant?, mais bon, bonne idée en tout cas).

Oui, je suis d'accord sur la politique générale: offrir un voie pour permettre de faire tout ce que tu n'as pas envie de prendre en compte directement permet de ne pas bloquer l'usage de l'outils à cause d'une impossibilité fonctionnelle.

Je vais garder le cas d'usage du re-run de Latex de chimrod dans la whish list, auquel j'essaierai surement d'arriver par des étapes plus simples.

Hello Nokomprendo, oui, il pourrait.
Mais le but est ici pédagogique, faire clair avant de faire court. Si dans mon tuto une commande est lancée, j'aime autant qu'elle apparaisse en clair dans le Makefile ainsi que les fichiers concernés.

Et pour les variables, j'en utiliserai dans le Makefile d'exemple dès que smk saura les traiter (ce que j'ai annoncé vaillamment pour Noël un peu plus haut!).

Ah oui, très bonnes idées!
Et pour moi pour illustrer l'utilisation de smk sans faire dans le gcc!

Ça me fait penser que j'ai un cas aussi : j'utilise rapid photo downloader pour renommer et classer toutes les photos que j'archives.
Quelque soit l'origine, je déverse tout dans le même répertoire tmp "à classer", et rapid s'occupe du reste.

Je vais tester smk:
- répertoire tmp vide, ne doit rien faire
- répertoire tmp plein de photos déjà traitées, ne doit rien faire
- répertoire tmp avec des photos inconnues -> run

Et pour le besoin d'outils type backintime, qui sauvegardent leur propre configuration et que l'on peut lancer quasiment sans options sur la ligne de commande, pas la peine de faire un fichier smkfile, je vais prévoir le lancement directement en ligne de commande, type smk backintime --backup-job.

Merci pour les idées!

Oui, on m'en a parlé quand je suis sorti du bois il y a un mois avec mon idée.

Mais même si le système est très intéressant, il oblige à créer un tupfile.
Par exemple pour
"gcc hello.c -o hello", le tupfile contiendra
": hello.c |> gcc hello.c -o hello |> hello"

C'est donc l'utilisateur qui donne la règle de production avec ce format source|commande|target.
C'est une syntaxe différente Make, mais c'est la même idée.

smk vise à se passer complètement de cette description.

Merci pour le papier mtime comparison considered harmful, j'ai appris plein de chose, et découvert qu'un des défauts que je mettais dans limitations est aussi un défaut de make.

Je ne suis pas rentré dans le mécanisme de redo, je n'ai pas trouvé d'explication claire et concise.

redo's design fundamentally depends on keeping a database of targets, if only to remember which files were produced by redo and which were not. From there, it's easy enough to extend that database to include mtime information about sources.

Ca à l'air de ressembler à ce que stocke smk, mais je ne peut pas en dire plus.

Le mécanisme à l'air très safe, mais la syntaxe est trop compliqué pour moi. Quand je vois dans l'intro ce qu'il faut écrire pour lancer un pauvre gcc, ça ne me donne pas envie d'aller plus avant.

Je comprends que le mécanisme permet d'éviter qu'une source soit considérée comme valide alors qu'il s'agit d'un fichier intermédiaire (parce que la compilation a été interrompue au milieu, par exemple).
Pour les cas simples que je vise, cela ne justifie pas la complexité ajoutée autour de la commande gcc.

Après, sur le fait d'avoir les cibles all clean etc. éclatés en plusieurs fichier script dans le répertoire courant, je ne suis pas hostile, et je propose de faire la même chose avec smk, mais le contenu des fichiers doit rester très simple.

Pour répondre à ta question : en effet, je m'appuie sur mtime pour savoir si un fichier a été modifié depuis la dernière exécution de la commande, mais pas pour distinguer les inputs des outputs. C'est ce que faisait ma première version, date fichier < heure d'exécution => source, date fichier > heure exécution => target. Mais la ça dysfonctionnait carrément pour les problèmes évoqué dans l'article, au moins celui de granularité faible du mtime).

Il n'en reste pas moins que la version actuelle souffre encore (marginalement) de ce défaut dans un cas bien précis également décrit dans l'article:

Computers are now so fast that you can save foo.c in your editor, and then produce foo.o, and then compile foo, all in the same one-second time period. If you do this and, say, save foo.c twice in the same second (and you have one-second granularity mtimes), then make can't tell if foo.o and foo are up to date or not.

Comme c'est ce que je fait dans les tests de smk, j'ai du mettre à deux endroits "sleep 1" dans le Makefile pour ne pas tomber dans ce bug. Mais grâce à ton lien, je vois ce que fait redo pour éviter ça (par exemple stocker et comparer également la taille), c'est une très bonne source, merci.

Merci à toi pour l'info (et à Michaël).
L'exploration de bmake et du méta mode a été très intéressante!

Voici mon retour:

• l'outil repose sur filemon. filemon est un device spécial qui permet de collecter toutes les opérations fichier d'un process et de ses fils.
  Il a été pensé exprès pour l'usage d'outils de build, et il est expliqué que ktrace permet de le faire, mais que ktrace capture tout, et qu'il faudrait ensuite filtrer dans un énorme log (info peut-être pas à jour). (sur Linux, strace traite le problème, puisqu'on lui dit sur la ligne de commande "-e trace=file"). Il est dit également que le proto de bmake utilisait un autre équivalent de strace, DTrace. Mais celui-ci exigeait des privilèges root.
  Pour info, existe sur GitHub un port de filemon sur Linux.

• bmake est pensé pour reconstruire FreeBSD sur toutes les plateformes. Autant dire que c'est au antipode de smk en terme de complexité de cible:

  While meta mode may be the coolest thing since sliced bread, it may not be for everyone. It does provide a simple solution to some rather complex problems

Mais surtout bmake reste un make : sa syntaxe relève du grand art, (tu l'écrit le lundi, le mardi tu ne comprends plus ce que tu as écrit, le mercredi tu te demande qui est le con qui a été piqué ce code dans un obfuscation contest!). Personne n'a envie de ça pour un outils simple.
Et vice versa, smk ne fera jamais la moitié de ce que fait bmake.

• j'ai trouvé également intéressant de voir ce que stockait bmake dans ses fichiers .meta (l'équivalent des runfiles smk). Comme pour smk, y sont stockés la commande et ses options, et les fichiers classés en read et write, mais aussi quelques autres infos, comme le répertoire d'exécution. Je retiens l'idée d'un format de fichier en clair (texte), pour faciliter le debug. Pour l'instant, smk c'est du binaire. Je vérifierai l'impact en performance de ce changement, mais si c'est faible, je ferais le switch.
  

fabricate a un argumentaire de vente que je pourrais reprendre tel quel :-)
J'ai bien noté l'utilisation de strace, ou des time tags, ainsi que celle de MD5 pour vérifier si un fichier a changé, intéressant.
De même que l'autoclean, évidemment.

C'est l'outil le plus proche de smk que j'ai vu a date, et il est bien plus puissant. Mais il s'agit plus d'une lib que d'un exe (même si on peut l'invoquer en ligne en lui passant tout en paramètre) : pour l'utiliser dans toute ses possibilités, il faut écrire son script de build en Python.
(Même remarque pour Shake-Forward, sauf que la il faut scripter en haskell).

Donc ça confirme que l'on peut faire smk depuis au moins dix ans. Reste la forme, je pense qu'ils ne sont pas sur le même créneau simplicité - universalité.

Malheureusement, ça ne marchera pas, car smk ne sait pour l'instant lancer que des commandes. Or, là, c'est du shell…

Lancer un shell réglerait ce problème et pas mal d'autres, mais j'hésite à cause des perfs.

Merci Guillaum, très intéressant, je vais aller voir les références.

Pour ce qui est du problème du build initial, effectivement, convertir un énorme projet à cette approche peut poser problème si le temps total de build est en jours (même si on peut toujours réfléchir à une conversion progressive, en insérant progressivement smk dans les makefiles existants).

Par contre, le stockage de smk est fait ainsi :
pour chaque smkfile, chaque couple sources/cibles est indexé par la ligne de commande. Donc si tu rajoutes une commande, ça rajoute une entrée, et si tu modifies une commande, idem. Il n'y a donc pas a ré-exécuter tout à chaque mise à jour du smkfile, et donc pas de problème pour croître avec le projet.

Il faut juste que j'ajoute dans ma suite un test pour vérifier que le runfile n'enfle pas quand on le fait de façon répétitive avec des lignes de commandes "mortes" qui ne figurent plus dans le smkfile. Je vais m'enregistrer une issue pour penser à traiter ce problème.

Ca rejoint également ce que disait liberf0rce plus haut : utiliser gcc -MM
Je vais potasser ça!

OK, à discuter.

A priori, ce n'est pas dans mon idée de développer un tel mécanisme, je préférerais garder une syntaxe simple, et compatible shell script.