Est-ce que l'algo seul peut être prouvé sans que le programme complet soit prouvé ? Je ne sais pas.
Ce n'est pas non plus ce qu'on demande aux autres (dont Git et Mercurial), mais j'avoue qu'on a hésité entre Rust et Idris à un moment, entre autres pour cette raison.
Si les algos sont prouvés, c'est déjà bien mieux que Git par exemple (en plus, quelle spécification donner à Git, vu qu'il fait parfois des bêtises ?).
Je veux bien aider des gens à le prouver, par contre, mais il faut commencer par les fondations (qui nous ont pris plus de temps que le projet lui-même). Exemples :
Sanakirja, un dictionnaire clef-valeur à la LMDB, mais avec des tables forkables efficacement (la complexité est compliquée à expliquer, je l'ai fait là). Le code n'est pas très gros, mais les algos sont un peu tordus : il y a des skiplists et des B trees, mais tout est transactionnel, y compris la gestion de la mémoire. Exemple, si on débranche la machine au milieu d'une transaction qui a alloué plein de blocs dans le fichier, quand on redémarrera, la base de données sera retrouvée exactement dans l'état initial (et Sanakirja n'a rien de spécial à faire, il n'y a pas besoin de journal, c'est seulement que le commit de transaction est atomique).
Oui, c'est possible, enfin, on sait pas trop mais ça doit bien pouvoir se faire, on à même de superbes idées sur comment faire…
Non, en l'occurrence c'est plutôt "c'est déjà implémenté dans la bibliothèque, c'est rétro-compatible, mais il faut écrire plein de commandes supplémentaires, ce qui implique de bike-shedder beaucoup, et il y a plein de trucs d'ingénierie plus urgents à résoudre".
Exemples de trucs d'ingénierie :
s'assurer que notre bibliothèque SSH marche correctement sur toutes les plateformes. Oui, j'ai écrit une bibliothèque SSH, c'est l'un des inconvénients de travailler avec un langage trop jeune.
faire en sorte de lire ~/.ssh/config, et résoudre tous les problèmes avec les clefs protégées par mot de passe.
résoudre les deux ou trois problèmes restants sur nest.pijul.com. Il est tout asynchrone, mais un thread peut parfois se retrouver bloqué par une opération sur un dépôt, sans que le reste de la boucle d'événements puisse avancer pour le débloquer.
Et il y a des trucs qui demandent des algorithmes plus durs à écrire, comme par exemple l'affichage des patchs déjà recordés dans le terminal, ou l'affichage plus complet des contextes des patchs sur nest.pijul.com.
Pas vraiment. Par exemple, dans un projet de petite taille comme Pijul, qui a été essentiellement écrit à deux, on travaillait tous les deux sur quarante trucs à la fois.
On a utilisé Darcs, et presque chaque patch avait une nouvelle fonctionnalité ou une nouvelle résolution de bug. Pour faire la même chose avec Git, il nous aurait effectivement fallu plusieurs dizaines de branches. Pire, il aurait fallu se souvenir, en même temps qu'on démouchait du code, de la branche courante et des interactions potentielles avec toutes les autres branches.
À moins que j'ai vraiment loupé un truc, seule l'attitude de git, s'arrêter et te dire t'es gentil tu corriges tes conneries est valide.
Pijul fait bien entendu la même chose.
Je voudrais juste rajouter que "appliquer les patchs successivement" a un sens, mais Pijul garantit que les applique dans n'importe quel ordre fait la même chose, ce qui permet de laisser les deux développeurs faire un pull de l'autre, et d'aboutir à exactement le même résultat :
Le développeur cool pull un patch qui ajoute des lignes dans un contexte (les lignes autour) qu'il a supprimé, c'est un conflit.
Le développeur pas cool pull un patch P qui supprime des lignes, mais ces lignes supprimées ont du contexte qui ne fait pas partie des dépendances de P. C'est le même conflit.
L'attitude de Git dans ce cas :
dépend du contenu des lignes. Parfois il ne verra pas le conflit, et ajoutera la nouvelle ligne à un autre endroit du code.
dépend de l'ordre dans lequel ces patchs ont été appliqués.
Ce n'est pas complètement raisonnable, en particulier sur des codes plus gros qu'une fonction de trois lignes qui fait un truc simple.
Ce qui est encore moins raisonnable, c'est que Git peut en plus, dans pas mal de cas, indiquer un conflit alors qu'il n'y en a pas, simplement parce que le manuel de bonnes pratiques a dit de faire un rebase il y a trois mois. L'intention du manuel était bonne : il s'agissait juste d'essayer de simuler la commutation de patchs. Mais ça n'a pas trop marché, et maintenant il faut relire un code déjà testé et relu quinze fois auparavant, pour s'assurer encore une fois que tout va bien, alors que ce n'est pas forcément sur ce morceau-là du projet qu'on voudrait travailler maintenant.
Relire du code est absolument essentiel, on est d'accord, mais on peut aussi supposer que les participants au projet ont un temps de travail fini, et des priorités de relecture et de tests décidés par autre chose que par Git. Dans ce cas, c'est une perte de temps.
Ça n'est pas pour te décourager, tu dis toi-même que c'est un projet d'expérimentation, et c'est très bien. Dire que la théorie des patchs, « c'est bien », oui, peut-être, mais je ne vois pas en quoi en pratique ça changera quoi que ce soit : l'exemple donné dans ton premier commentaire est complètement tiré par les cheveux et n'arrivera jamais en pratique.
Oui, sauf que ce problème peut être utilisé pour créer des failles dans un logiciel, même open source, et même en passant les reviews et les tests : aucun test unitaire ne peut garantir l'intégralité d'un code, et d'ailleurs toutes les failles de sécurité qui arrivent (on en découvre tous les jours presque partout) avaient échappé aux tests unitaires dans 100% des cas (encore mieux que 99,999%).
Sur les autres avantages et "Git va être le meilleur", c'est un peu ce qu'on disait de SVN quand Git est sorti.
Il n'est pas 100% honnête (et même pas 99,999% honnête) de dire "Git est supérieur" en oubliant les questions essentielles du temps d'apprentissage et du passage à l'échelle sur de gros dépôts et de grosses équipes.
Dans la vraie vie, on a parlé avec pas mal de monde depuis qu'on a commencé ce projet, et on a déjà entendu (assez rarement quand même) ce "je comprends tout Git, et c'est tellement mieux que votre truc que je ne vais même pas aller regarder ce que c'est".
Par contre, on ne l'a absolument jamais entendu des gens avec qui on a parlé qui travaillent sur de très gros trucs (par exemple chez Apple ou Facebook, ou même des gens qui gèrent les dépôts du noyau Linux).
Et on soupçonne un tout petit peu que les gens qui nous disent ça "oublient" en général de mentionner qu'ils ont passé 10 ans à essayer de le comprendre, lus des quantités ahurissantes de livres, de blogs et de manuels pour essayer de forcer Git à rester dans les clous des axiomes que Pijul garantit au débutant qui fait son premier dépôt avec un pote, sans avoir la moindre idée de ces trucs ni de notre théorie.
Je réponds super en retard (je suis un des auteurs du truc).
En écrivant ça j'ai l'intuition de retrouver ce pourquoi git est si plaisant à utiliser (surtout comparé à SVN qui était dominant à l'époque, il est vrai).
Personne ne conteste que Git est bien mieux que SVN. Mais il est basé sur les mêmes heuristiques "qui marchent souvent", et passe encore moins bien à l'échelle de très gros dépôts (un truc à la mode chez Google et Facebook) que SVN.
Sauf que je ne vois pas comment pijul peut être magiquement mieux.
Pijul n'est pas "magiquement mieux", dans le sens où il n'y a aucune magie, seulement une vraie théorie qui gère tous les cas, donne des axiomes simples et efficaces à l'utilisateur (et des algos avec une meilleur complexité que Git, même s'il y a encore eu moins de micro-optimisation dans Pijul que dans Git).
Une conséquence de ces axiomes est que les conflits ne sont pas (comme dans Git ou même Darcs) des "cas pourris" qu'il faut résoudre avant le prochain commit. Ils sont traités comme le cas normal.
En fait j'aurais plutôt tendance à dire que Git est "magiquement" moins bien, parce qu'il utilise des heuristiques (de la magie) qui marchent souvent. Il n'y a pas de principe qui assure que tout va toujours bien se passer. Au fait, les gens qui font Pijul, c'est-à-dire Florent Becker, moi-même, et les gens qui commencent à nous rejoindre, connaissent très bien Git (et très bien Darcs, et un peu moins Mercurial et SVN).
Si pijul a stocké "alors là tu changes la ligne 3 du fichier 'foo' de 'bar' vers 'baz'" comme patch, par quelle magie, lorsque je le rebase sur un nouveau sommet où précédemment la dite ligne 3 a été modifiée de 'bar' vers 'boo', il recolle les morceaux ? A part en disant "oh merde je m'en fous je colle 'baz' puisque de toute façon on voulait 'baz'". Ou alors en disant "euh au secours conflit !".
C'est effectivement un conflict dans Pijul. Pijul n'utilise pas du tout le contenu des lignes pour appliquer un patch, seulement leur histoire et leur contexte.
Ça n'a rien de magique, il y a simplement des règles pour garantir les axiomes.
Salut ! Je suis un des auteurs de Pijul, et en retard pour répondre.
C'est dommage que sa doc se focalise sur un avantage futile (youpi, mes merges sont supposément plus fiables) plutôt que sur des avantages concrets dans 100% des cas (mon repo est 100% fiable, validable et ne peut pas techniquement être corrompu sans rattrapage possible).
Ces avantages "concrets" sont bien évidemment garantis par notre théorie. L'avantage des merge n'est certes pas le principal avantage, mais l'idée d'avoir une théorie petite, qui garantit un petit nombre d'axiomes simples, est un avantage énorme.
Et d'ailleurs, si on regarde les bonnes pratiques, les "successful workflows" et autres "Pro Git Book" en connaissant ces axiomes, on se rend compte que tout le monde cherche à garantir la même chose.
Maintenant, (sauf dans le cas rare de Git is inconsistent, où Git fait vraiment n'importe quoi), il y a deux façons de garantir ces propritétés : soit c'est la machine qui le fait, soit c'est le programmeur. C'est exactement la même différence qu'entre la programmation fonctionnelle et les autres langages. Il n'est d'ailleurs pas extraordinairement surprenant de voir des utilisateurs de Rust, Haskell, OCaml, Scala etc. désirer mieux que Git.
Notre pari, c'est qu'alors que les langages fonctionnels sont plus difficiles d'accès que Python, pour nous ça a l'air d'être l'inverse : l'utilisateur peut complètement oublier qu'il y a une théorie derrière, tout ce qu'il voit ce que "ça colle à l'intuition" (c'est à ça que servent des axiomes dans toutes les théories) et que "ça va vite".
Salut ! Je suis un des auteurs de Pijul, et je suis super en retard pour répondre.
Ce nom est en effet horrible à taper, encore pire sur un clavier dvorak. Toutes les lettres sont sur la main gauche, sauf le "l" qui est sur l'auriculaire droit, ligne du haut. En plus la main gauche doit changer de ligne à chaque lettre.
On a des idées pour le changer, parce qu'un plus il se prononce différemment dans toutes les langues. Les auteurs le prononcent comme en espagnol, mais les finlandais disent "piyoul", les anglophones "pidjoul", les français "pijul" (prononcé comme en français), et il existe sans doute plein d'autres variantes.
Bref, ce n'est pas la priorité, mais on a des idées pour le changer (peut-être quand il deviendra 1.0).
[^] # Re: Preuves ?
Posté par pmeunier . En réponse au journal Pijul, un nouveau gestionnaire de source. Évalué à 8.
Salut ! Je suis un des auteurs de Pijul.
Ce n'est pas non plus ce qu'on demande aux autres (dont Git et Mercurial), mais j'avoue qu'on a hésité entre Rust et Idris à un moment, entre autres pour cette raison.
Si les algos sont prouvés, c'est déjà bien mieux que Git par exemple (en plus, quelle spécification donner à Git, vu qu'il fait parfois des bêtises ?).
Je veux bien aider des gens à le prouver, par contre, mais il faut commencer par les fondations (qui nous ont pris plus de temps que le projet lui-même). Exemples :
Sanakirja, un dictionnaire clef-valeur à la LMDB, mais avec des tables forkables efficacement (la complexité est compliquée à expliquer, je l'ai fait là). Le code n'est pas très gros, mais les algos sont un peu tordus : il y a des skiplists et des B trees, mais tout est transactionnel, y compris la gestion de la mémoire. Exemple, si on débranche la machine au milieu d'une transaction qui a alloué plein de blocs dans le fichier, quand on redémarrera, la base de données sera retrouvée exactement dans l'état initial (et Sanakirja n'a rien de spécial à faire, il n'y a pas besoin de journal, c'est seulement que le commit de transaction est atomique).
Thrussh, une bibliothèque SSH asynchrone.
[^] # Re: Is it possible to refer to a specific version? Yes. Maybe. In practice, no.
Posté par pmeunier . En réponse au journal Pijul, un nouveau gestionnaire de source. Évalué à 10.
Non, en l'occurrence c'est plutôt "c'est déjà implémenté dans la bibliothèque, c'est rétro-compatible, mais il faut écrire plein de commandes supplémentaires, ce qui implique de bike-shedder beaucoup, et il y a plein de trucs d'ingénierie plus urgents à résoudre".
Exemples de trucs d'ingénierie :
Et il y a des trucs qui demandent des algorithmes plus durs à écrire, comme par exemple l'affichage des patchs déjà recordés dans le terminal, ou l'affichage plus complet des contextes des patchs sur nest.pijul.com.
[^] # Re: Pourquoi du théorie des patch c'est bien
Posté par pmeunier . En réponse au journal Pijul, un nouveau gestionnaire de source. Évalué à 10.
Pas vraiment. Par exemple, dans un projet de petite taille comme Pijul, qui a été essentiellement écrit à deux, on travaillait tous les deux sur quarante trucs à la fois.
On a utilisé Darcs, et presque chaque patch avait une nouvelle fonctionnalité ou une nouvelle résolution de bug. Pour faire la même chose avec Git, il nous aurait effectivement fallu plusieurs dizaines de branches. Pire, il aurait fallu se souvenir, en même temps qu'on démouchait du code, de la branche courante et des interactions potentielles avec toutes les autres branches.
[^] # Re: Pourquoi du théorie des patch c'est bien
Posté par pmeunier . En réponse au journal Pijul, un nouveau gestionnaire de source. Évalué à 10.
Pijul fait bien entendu la même chose.
Je voudrais juste rajouter que "appliquer les patchs successivement" a un sens, mais Pijul garantit que les applique dans n'importe quel ordre fait la même chose, ce qui permet de laisser les deux développeurs faire un pull de l'autre, et d'aboutir à exactement le même résultat :
L'attitude de Git dans ce cas :
Ce n'est pas complètement raisonnable, en particulier sur des codes plus gros qu'une fonction de trois lignes qui fait un truc simple.
Ce qui est encore moins raisonnable, c'est que Git peut en plus, dans pas mal de cas, indiquer un conflit alors qu'il n'y en a pas, simplement parce que le manuel de bonnes pratiques a dit de faire un rebase il y a trois mois. L'intention du manuel était bonne : il s'agissait juste d'essayer de simuler la commutation de patchs. Mais ça n'a pas trop marché, et maintenant il faut relire un code déjà testé et relu quinze fois auparavant, pour s'assurer encore une fois que tout va bien, alors que ce n'est pas forcément sur ce morceau-là du projet qu'on voudrait travailler maintenant.
Relire du code est absolument essentiel, on est d'accord, mais on peut aussi supposer que les participants au projet ont un temps de travail fini, et des priorités de relecture et de tests décidés par autre chose que par Git. Dans ce cas, c'est une perte de temps.
[^] # Re: Pourquoi du théorie des patch c'est bien
Posté par pmeunier . En réponse au journal Pijul, un nouveau gestionnaire de source. Évalué à 10.
Oui, sauf que ce problème peut être utilisé pour créer des failles dans un logiciel, même open source, et même en passant les reviews et les tests : aucun test unitaire ne peut garantir l'intégralité d'un code, et d'ailleurs toutes les failles de sécurité qui arrivent (on en découvre tous les jours presque partout) avaient échappé aux tests unitaires dans 100% des cas (encore mieux que 99,999%).
Sur les autres avantages et "Git va être le meilleur", c'est un peu ce qu'on disait de SVN quand Git est sorti.
Il n'est pas 100% honnête (et même pas 99,999% honnête) de dire "Git est supérieur" en oubliant les questions essentielles du temps d'apprentissage et du passage à l'échelle sur de gros dépôts et de grosses équipes.
Dans la vraie vie, on a parlé avec pas mal de monde depuis qu'on a commencé ce projet, et on a déjà entendu (assez rarement quand même) ce "je comprends tout Git, et c'est tellement mieux que votre truc que je ne vais même pas aller regarder ce que c'est".
Par contre, on ne l'a absolument jamais entendu des gens avec qui on a parlé qui travaillent sur de très gros trucs (par exemple chez Apple ou Facebook, ou même des gens qui gèrent les dépôts du noyau Linux).
Et on soupçonne un tout petit peu que les gens qui nous disent ça "oublient" en général de mentionner qu'ils ont passé 10 ans à essayer de le comprendre, lus des quantités ahurissantes de livres, de blogs et de manuels pour essayer de forcer Git à rester dans les clous des axiomes que Pijul garantit au débutant qui fait son premier dépôt avec un pote, sans avoir la moindre idée de ces trucs ni de notre théorie.
[^] # Re: Pourquoi du théorie des patch c'est bien
Posté par pmeunier . En réponse au journal Pijul, un nouveau gestionnaire de source. Évalué à 10.
Je réponds super en retard (je suis un des auteurs du truc).
Personne ne conteste que Git est bien mieux que SVN. Mais il est basé sur les mêmes heuristiques "qui marchent souvent", et passe encore moins bien à l'échelle de très gros dépôts (un truc à la mode chez Google et Facebook) que SVN.
Pijul n'est pas "magiquement mieux", dans le sens où il n'y a aucune magie, seulement une vraie théorie qui gère tous les cas, donne des axiomes simples et efficaces à l'utilisateur (et des algos avec une meilleur complexité que Git, même s'il y a encore eu moins de micro-optimisation dans Pijul que dans Git).
Une conséquence de ces axiomes est que les conflits ne sont pas (comme dans Git ou même Darcs) des "cas pourris" qu'il faut résoudre avant le prochain commit. Ils sont traités comme le cas normal.
En fait j'aurais plutôt tendance à dire que Git est "magiquement" moins bien, parce qu'il utilise des heuristiques (de la magie) qui marchent souvent. Il n'y a pas de principe qui assure que tout va toujours bien se passer. Au fait, les gens qui font Pijul, c'est-à-dire Florent Becker, moi-même, et les gens qui commencent à nous rejoindre, connaissent très bien Git (et très bien Darcs, et un peu moins Mercurial et SVN).
C'est effectivement un conflict dans Pijul. Pijul n'utilise pas du tout le contenu des lignes pour appliquer un patch, seulement leur histoire et leur contexte.
Ça n'a rien de magique, il y a simplement des règles pour garantir les axiomes.
[^] # Re: Pourquoi du théorie des patch c'est bien
Posté par pmeunier . En réponse au journal Pijul, un nouveau gestionnaire de source. Évalué à 10.
Salut ! Je suis un des auteurs de Pijul, et en retard pour répondre.
Ces avantages "concrets" sont bien évidemment garantis par notre théorie. L'avantage des merge n'est certes pas le principal avantage, mais l'idée d'avoir une théorie petite, qui garantit un petit nombre d'axiomes simples, est un avantage énorme.
Et d'ailleurs, si on regarde les bonnes pratiques, les "successful workflows" et autres "Pro Git Book" en connaissant ces axiomes, on se rend compte que tout le monde cherche à garantir la même chose.
Maintenant, (sauf dans le cas rare de Git is inconsistent, où Git fait vraiment n'importe quoi), il y a deux façons de garantir ces propritétés : soit c'est la machine qui le fait, soit c'est le programmeur. C'est exactement la même différence qu'entre la programmation fonctionnelle et les autres langages. Il n'est d'ailleurs pas extraordinairement surprenant de voir des utilisateurs de Rust, Haskell, OCaml, Scala etc. désirer mieux que Git.
Notre pari, c'est qu'alors que les langages fonctionnels sont plus difficiles d'accès que Python, pour nous ça a l'air d'être l'inverse : l'utilisateur peut complètement oublier qu'il y a une théorie derrière, tout ce qu'il voit ce que "ça colle à l'intuition" (c'est à ça que servent des axiomes dans toutes les théories) et que "ça va vite".
[^] # Re: Un peu de marketing que diable...
Posté par pmeunier . En réponse au journal Pijul, un nouveau gestionnaire de source. Évalué à 8.
Salut ! Je suis un des auteurs de Pijul, et je suis super en retard pour répondre.
Ce nom est en effet horrible à taper, encore pire sur un clavier dvorak. Toutes les lettres sont sur la main gauche, sauf le "l" qui est sur l'auriculaire droit, ligne du haut. En plus la main gauche doit changer de ligne à chaque lettre.
On a des idées pour le changer, parce qu'un plus il se prononce différemment dans toutes les langues. Les auteurs le prononcent comme en espagnol, mais les finlandais disent "piyoul", les anglophones "pidjoul", les français "pijul" (prononcé comme en français), et il existe sans doute plein d'autres variantes.
Bref, ce n'est pas la priorité, mais on a des idées pour le changer (peut-être quand il deviendra 1.0).