kantien a écrit 1187 commentaires

Ça tombe bien, personne n'a dit ça, et c'est une bêtise.

Je crois que c'est moi qui l'est dit, et ce n'est pas une bêtise : c'est ce qu'offre les langages avec types dépendants. Du moins il dispense de tests unitaires, sauf pour ce qui est des erreurs dans la formalisation des spécifications du code.

L'exemple le plus parlant est celui-ci :

Theorem transform_c_programm_preservation :
  forall p tp beh
  transf_c_program p = Ok tp ->
  program_behaves (Asm.semantics tp) beh ->
  exists beh', programm_behaves (C.semantics p) beh'
            /\ behavior_improves beh' beh

Laissant de côté le mot clef Theorem, le terme transform_c_programm_preservation est un terme du langage dont le type est l'énoncé exprimant que CompCert C est bien un compilateur C optimisant qui préserve la sémantique. Le terme, ou programme, est construit grâce à l'assistant de preuve Coq et il y a bien vérification statique qu'il a le bon type. Comme son type quantifie sur la totalité des programmes C (la varibale p du forall), qui est potentiellement infinie, il garantie des choses inaccessibles aux tests unitaires.

Par contre, il reste la question : la formalisation de la sémantique de l'Asm (utilisée dans le terme Asm.semantics tp) est-elle conforme à la réalité ? Question dont la réponse est inaccessible aux méthodes formelles. De même pour ce qui est de la question sur la correction de la formalisation du C.

Au niveau de la traduction en français, le type s'exprime ainsi : pour tout programme C p, tout programme assembleur tp et tout comportement observable beh, si la fonction transf_c_prgram appliquée à p renvoie le programme tp et que beh est un comportement observable de tp en accord avec la sémantique ASM, alors il existe un comportement observable beh' de p conforme à la sémantique du C et tel que beh améliore beh'.

Autrement dit le type affirme que transf_c_program est un compilateur optimisant du C vers l'ASM.

Ce cas extrême n'était pas pour inciter à l'usage des types dépendants, mais pour montrer que plus on introduit de typage statique et d'expressivité dans le système de types, moins on a besoin de tests unitaires (au point de ne plus en avoir besoin) : ce qui était bien ton propos initial. ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je sais pas si c'est très clair…

Ça l'est : tu veux faire du polymorphisme ad-hoc; mais je ne vois pas où on a besoin de typage dynamique pour cela.

L'idée du polymorphisme ad-hoc est d'avoir des fonctions qui ont le même nom (ici Greeting) mais qui opère sur différents types et selon des logiques différentes (à la différence du polymorphisme paramétrique). Ensuite à l'usage (comme dans ta fonction foo) la fonction effectivement utilisée est choisie en fonction du type du paramètre (type base dispatch). C'est exactement ce que font les type classes de Haskell et les traits du Rust. Cette manière de faire est bien plus intelligente (j'ai envie de dire moins inepte) que l'approche de l'orienté objet. En OCaml on passe par des modules et foncteurs pour faire cela (avec une perte de l'implicite) et il me semble (mais là je suis moins sûr) que les template du C++ peuvent servir à cela.

Pour présenter grossièrement l'idée, il s'agit d'associer à un type un dictionnaire de fonctions pour opérer dessus, c'est l'interface contre laquelle on veut programmer de manière générique. En fonction du type du paramètre, le compilateur choisira le dictionnaire qui lui a été associé. Néanmoins, le système des interfaces du Go reste trop limité à mon goût : j'en ai déjà parlé sur un ancien journal de gasche.

Prenons l'exemple de la structure d'anneaux en mathématiques : un anneau c'est un type de données que l'on peut ajouter, soustraire et multiplier avec deux éléments neutres pour l'addition et la multiplication. Autrement dit, c'est cette interface de module :

module type Anneau = sig
  (* le type des éléments de l'anneau *)
  type t

  (* les éléments neutres *)
  val zero : t
  val one : t

  (* les opérations *)
  val add : t -> t -> t
  val neg : t -> t
  val mul : t -> t -> t
end

Plutôt que de dire que l'on peut les soustraire, je préfère exprimer l'axiomatique en disant que l'addition est une opération inversible d'où la fonction neg. À partir de là, dès que l'on a une telle structure, on peut définir dessus le polynôme :

let f (type a) (module A : Anneau with type t = a) x =
  let (+), ( * ) = A.add, A.mul in
  x * x + x + A.one

Le principe derrière les type classes de Haskell ou les traits de Rust est de dire que pour un type donnée on ne peut définir qu'une interface Anneau sur ce type. Autrement dit, ils considèrent que le type Anneau with type type t = a est un singleton pour tout type a (où plutôt le compilateur garantie que l'on ne définit pas deux valeurs distinctes de ce type), ce qui est trivialement faux mais en pratique largement suffisant. Les interfaces de Go, c'est un peu la même idée mais en beaucoup moins bien : tu ne peux pas définir l'interface Anneau par exemple, il n'est pas possible de définir des opérateurs binaires sur le type t dans les interfaces de Go.

En OCaml, comme le type en question est rarement un singleton, il faut explicitement passer le dictionnaire en argument à la fonction f, même s'il y a déjà eu des propositions pour le rendre implicites dans certaines situations.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Oui mais tu réponds à une comparaison entre C++ et python. Donner un exemple pourquoi pas venir dire que le langage foobar lui il est mieux, c'est hors sujet.

Ce n'est pas vraiment hors-sujet à mon avis. Philippe Fremy répond à rewind en postant une vidéo d'une de ses conférences sur le typage statique en python. Le slide de conclusion est :

Conclusion :

• Type annotation is powerful to bug finder. Use it !
• Type annotation is also good way to document your code.
• Feedback from developpers using type annoation: "It rocks !"
• Some python dynamic constructs are difficult to verify statically

Là où c'est déjà étrange, c'est que dans sa réponse il laisse entendre que rewind cherche à troller, alors que c'est justement ces avantages du typage statique que rewind et chimrod ont cherchait à mettre en avant.

Ensuite, oui cela relève d'une plus grande sûreté que le recours aux tests unitaires. Quand on pousse jusqu'aux systèmes à types dépéndants, non seulement on ne fait plus de tests unitaires mais en plus on obtient une sûreté que ne pourront jamais atteindre ces derniers : un test peut montrer l'existence d'un bug (dans le respect à la spécification) mais jamais son absence.

Typer son code permet effectivement de le documenter (point 2 du slide de conclusion) car le langage de types est un langage formel d'écriture de spécification du code, et permet donc d'exprimer en partie ce que doit faire la fonction. D'où mon point précédent, avec des types dépendants on peut totalement spécifier formellement le code et donc vérifier qu'il est conforme à sa spécification.

Pour le typage structurel, on peut tout à fait faire cela statiquement et sans écrire d'annotation. Quelques exemples issues de la conférence de Philippe Fremy :

(* voir à la 20ème minute *)

(* cas d'un bug détecter statiquement *)
class a ?step_init = object
  val step = step_init
  method get_step = step_init + 1
end;;
Error: This expression has type 'a option
       but an expression was expected of type int

(* première solution on teste la valeur de l'attribut [step] *)
class a ?step_init () = object
  val step = step_init
  method get_step = match step with None -> 0 | Some step-> step + 1
end;;
class a :
  ?step_init:int ->
  unit -> object val step : int option method get_step : int end

(* deuxième solution, on initialise avec une valeur par défaut *)
class a ?(step_init = 0) () = object
  val step = step_init
  method get_step = step + 1 end;;
class a :
  ?step_init:int -> unit -> object val step : int method get_step : int end


(* pour le typage structurel, voire autour de la 30ème minute *)
let validate form data = form#validate data;;
val validate : < validate : 'a -> 'b; .. > -> 'a -> 'b = <fun>

Enfin, pour ce qui est des objets et du typage structurel, la façon dont ils sont globalement utilisés en pratique cela en fait surtout des modules du pauvre. En OCaml on utilisera plutôt des modules, en Haskell des type classes, en Rust des traits et en C++ des template.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

la cuisine cuisine

La cuisine est une pratique récursive qui s'appelle elle-même ? Elle termine ? Est-on garanti d'avoir de quoi manger à l'arrivée ? :-P

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

La liste Ocaml est une fifo pour une très bonne raison d'immutabilité. Mais comprendre pourquoi elle est comme ça et pourquoi c'est très bien ainsi, est bien au delà d'une introduction à l'informatique.

Les listes OCaml sont naturellement en mode LIFO : dernier arrivé, premier sorti. Ensuite c'est juste le principe des entiers unaires : en quoi c'est au-delà d'une introduction à l'informatique ? C'est ce que fait un enfant quand il apprend à compter avec ses doigts. Si des élèves de terminale ne comprennent pas cela, il y a un gros soucis.

Les listes OCaml sont LIFO par construction :

let push x l = x :: l

let l = [] |> push `As |> push `Roi |> push `Dame;;
val l : [> `As | `Dame | `Roi ] list = [`Dame; `Roi; `As]

(* la première à sortir est la dernière arrivée, à savoir `Dame *)
List.hd l;;
- : [> `As | `Dame | `Roi ] = `Dame

Ensuite, si l'on fait abstraction des valeurs contenus dans la liste, on obtient une liste de type unit list :

List.map ignore l;;
- : unit list = [(); (); ()]

et une telle liste c'est les entiers unaires : une liste de bâtons, de traits, de points…

Qu'est-ce qu'on fait, le plus souvent, avec une liste ? On utilise un fold, c'est à dire le principe du raisonnement par récurrence sur les nombres entiers. Il vient en deux versions : fold_left (mode LIFO) et fold_right (mode FIFO).

Non, vraiment, je ne vois pas où est le problème d'aborder ces notions dans une introduction à l'informatique. Cela fait partie des concepts les plus simples à assimiler.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Surtout, ce que tu as décrit (et que j'ai complété, c'est plutôt moi qui l'ai tendu le piège) intervient très rarement dans un process GCL digne de ce nom (à base de PR par exemple)

Si tu parlais en français, ou dans une langue que tout un chacun peut comprendre, cela faciliterait grandement les choses. Je veux parler de ces termes comme « process GCL digne de ce nom » qui chez toi on peut être un sens, mais chez moi c'est : qu'est-ce qu'il dit ? Pour le reste des tes commentaires, cela reste dans la même zone : le fait que le système puisse planter dans des cas tordus, qui ne sont même pas rejeter par Linus (toi tu les rejettes pour cacher la poussière sous le tapis), ne te déranges pas : grand bien t'en fasse, mais je comprends mieux pourquoi il y a tant de bugs dans les logiciels existants; la rigueur intellectuelle ne semble pas être une priorité pour certains.

Honnêtement, si tu penses réellement m'avoir tendu un piège, de quelque forme qu'il soit, il faudra que tu me montres où il se trouve. La seule chose que tu as fait c'est nier un problème que même Linus ne nie pas et auquel il propose une solution pour contourner les limites de git.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je ne comprends pas cette obsession autour de git revert et de l'idée d'annuler des patch.

Ce n'est pas une obsession, c'est juste la continuité de la discussion autour de problème que j'ai posé. Pour ce qui est de l'idéé d'annuler un patch, c'est une des fonctionnalités que tu attends d'un VCS :

est-ce qu'il me permet de défaire ce que j'ai fait?

La solution avec git, sans réécrire l'historique, c'est d'utiliser git revert. Personnellement, c'est la réponse à laquelle je m'attendais (même si la tienne fait la même chose, c'est moins idiomatique) et c'est ce qu'a proposé El Titi.

Néanmoins, le problème que j'ai posé était un piège tendu de ma part. ;-) En utilisant git revert (ou ta commande), vous prenez le risque de mettre 3-way merge dans la panade plus tard. Voilà comment Linus préconise d'annuler un merge foireux : un exemple typique du besoin de lire une bonne pratique pour effectuer une action de base sans avoir de problème.

Ce défaut est propre au VCS qui utilise 3-way merge comme algorithme de fusion, ce qui n'est pas le cas de pijul. D'ailleurs, pour quelqu'un qui aime la précision sémantique des mots utilisés, c'est bien là le problème de tous ces VCS : ils n'ont pas de définition claire de ce qu'est une fusion, un comble pour une opération si fondamentale dans un tel outil ! :-) À ce sujet, tu pourras lire mon commentaire qui traite de la question qu'est-ce qu'une fusion ?

Et au-delà de ce problème (qui reste central dans tous ces VCS), il y a celui de déterminer l'indépendance entre patchs. Dans mon problème, je précisais bien que les modifications des branches B et C étaient indépendantes de celles de la branche A. C'est à cette seule condition (l'indépendance) qu'il suffit de revert le merge entre A et B pour défaire ce qui a été fait. Si l'on souhaite définir formellement (et donc clairement) ce que signifie ce mot indépendance, cela consiste à dire que les patchs commutent. Voilà pourquoi pmeunier insiste tant sur cette notion de commutation de patchs. En conséquence, s'il n'y avait pas commutation il faudrait aussi défaire d'autres patchs que ceux de la branche A (ce que ne saura pas faire git revert ni ta commande : il faudrait résoudre le problème à la main). Par exemple si, après la fusion de la branche C, j'ajoute un patch p qui dépend du travail de la branche A alors il sera aussi défait automatiquement par pijull rollback AB mais pas par git revert (ni ta commande).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Quel va être l'apport de pijul rollback face à un git revert ?

Déjà, on n'aura pas besoin de revert le revert ou faire du rebase dans certaines situations afin de ne pas mettre le 3-way merge dans la panade (mais ça c'est une propriété générale de la fusion sous pijul).

En revanche je me pose la même question que toi : est-ce que pijul rollback se contente d'inverser les patchs passer en arguments ou est-ce qu'il inverse aussi ceux qui en dépendent ? Autrement dit, prend-t-il en compte la relation de dépendance entre patch ?

Si j'ai cet historique :

O -> p -> q -> r -> A

que r dépend de p mais que q commute avec eux, lorsque je fais pijull rollback p, est-ce que r est aussi inversé ? C'est là pour moi un avantage important de pijull face aux autres : ne pas avoir à résoudre manuellement un problème qui peut être fait automatiquement (et qui pourrait s'avérer difficile à résoudre à la main, n'ayant pas nécessairement bien en tête les relations de dépendances entre patchs). C'est-à-dire, pijull rollback p applique p' ou r'; p' (le ' dénote l'inverse) ?

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Autre question ?

Pas spécialement, c'est la réponse à laquelle je m'attendais (utiliser git revert). Mais il semblerait que ce ne soit pas aussi simple que cela, ensuite, pour la gestion future de la branche : how to revert a faulty merge avec explication en détails, par Linus, des pièges à éviter.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Si il faut plus d'une commande, fouiller dans les bonnes pratiques, chercher sur le net pour résoudre une question aussi triviale, alors git (ou autre VCS) a un problème.

La conclusion de cette phrase est dommageable parce que du coup tu digresses (tu le dis d'ailleurs toi-même à la fin). Il aurait été préférable de dire à la place "alors cela vaut peut-être la peine de s'intéresser à un outil qui prétend offrir une approche plus simple et rigoureuse".

Elle est peut être malheureuse, du fait qu'elle a amené une digression de FantastIX, mais je la maintiens. :-P

Je précise que j'ai qualifié ce problème de trivial (il l'est, je donne même la solution juste après) et qu'il fait parti du cœur de métier d'un VCS. Un problème trivial touchant à l'usage même d'un outil devrait être résolu facilement par l'utilisateur, sinon c'est un défaut de conception du logiciel.

Pour l'exemple, il est analogue au cas d'étude du rebasing dans le livre de référence sur git. On a trois branches que l'on rebase :

On peut bien supposer qu'il y a indépendance entre les modifications des parties clients et serveurs. Maintenant supposons, qu'après tous ces rebases on se rende compte que les commits sur le code client ont introduit une faille de sécurité. La correction la plus rapide est de supprimer ces commits en attendant d'analyser le problème et de le résoudre : comment faire avec git vu que les derniers commits présents (ceux du serveur) en dépendent ? On souhaiterait un commande du style git undo client : peut-on l'implémenter simplement autour du cœur de git ? J'en doute, mais je ne demande qu'à être contredit. En tout cas, elle l'est autour de celui de pijul (c'est la solution que j'ai donné manuellement et ce que devrait faire pijull rollback ou pijull unrecord).

Pour bien montrer à quel point le problème est trivial, je vais l'illustrer en prenant des nombres entiers au lieu de fichiers pour les sommets du graphe :

   /-- *2 -> 2 -- *3 -> 6 -- *5 -> 30 ----\
  /                                        \
1 ---- *7-> 7 -- *11 -> 77 -- *13 -> 1001 --> 30030 --> 9699690 -- ?? = /30 -> BC = 323323
  \                                                  /
   \-- *17 -> 17 -> *19 -> 323 ---------------------/

Annuler la branche A c'est annuler la multiplication par 30 c'est à dire diviser par 30. Dans les cas des fichiers c'est pareil : il faut inverser le patch global de la branche A, c'est-à-dire prendre l'inverse du composé de a1; a2; a3 puis l'appliquer à l'état ABC.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Ensuite, j'affirme en effet ne pas avoir de problème avec Git et j'explique (en gros) pourquoi.

Je suis intrigué par cette remarque, alors je pose un cas pratique n'étant pas un fin connaisseur de git. Prenons un historique de cette forme :

   /-- a1 -> A1 -- a2 -> A2 -- a3 -> A3 -\
  /                                       \
O ---- b1 -> B1 -- b2 -> B2 -- b3 -> B3 --> AB --> ABC -- ?? -> BC
  \                                             /
   \-- c1 -> C1 -> c2 -> C2 -------------------/

Les lettres majuscules désignent des instantanés du dépôt et les lettres minuscules des patchs. On a trois branches A, B et C avec leurs patchs et commits successifs. On fusionne A et B, puis ensuite on fusionne C. La dernière fusion génère un conflit qui est résolu. On suppose que les changements de la branche A sont totalement indépendants de ceux des autres branches, le conflit venant seulement de la fusion des modifications de B et C. Question : comment, à partir de ABC, annuler les changements apportés par la branche A ? (hint : avec pijul, une seule commande devrait résoudre le problème).

Si il faut plus d'une commande, fouiller dans les bonnes pratiques, chercher sur le net pour résoudre une question aussi triviale, alors git (ou autre VCS) a un problème. Il s'agit ici uniquement d'appliquer sur l'état ABC le patch inverse du composé de a1; a2; a3.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Un petit complément auquel j'ai pensé après coup.

Je trouve qu'elle explique mieux l'astuce de l'utilisation des graphes et elle n'utilise même pas le terme de graggle, bravo :) (quand je parlais de simplification de la représentation du fichier, c'est exactement ça, mais plus clairement exprimé en partant de la richesse du graphe au lieu de la "simplification/relaxation" de la liste).

Pour le terme de graggle, il semble être propre à Joe Neeman : Pierre-Étienne Meunier ne le connaissait pas. En revanche, un point sur lequel je n'ai pas insisté est que ces graphes de lignes étaient inéluctables pour résoudre la question : qu'est-ce qu'une fusion ? C'est parce que les autres systèmes n'ont pas de définition claire de cette notion qu'ils leur arrivent de se prendre les pieds dans le tapis (comme dans l'exemple donné avec git, où le problème viens de l'agorithme three-way merge si j'ai bien compris).

Revenons un instant sur nos graphes :

On a par exemple une flèche entre les sommets O et A marquée par un patch p. Je dirais que A est un descendant de O par la relation p. Si on prend par exemple des entiers pour sommets, comme dans mon premier commentaire, on dira que 2 est un descendant de 1; ou bien que 6 est un descendant commun de 2 et 3.

Maintenant prenons le graphe qui illustre la propriété fondamentale de la fusion de deux états :

Dans le cas des entiers, je prenais pour fusion le ppcm. Ce qui importe dans le ppcm ce n'est pas qu'il soit le plus petit des multiples communs, mais que tout multiple de A et B soit aussi un multiple de leur ppcm M. Autrement dit : parmi tous les descendants de A et B, il y en a un qui est un ancêtre commun de tous les descendants. C'est cette propriété qui caractérise la fusion.

Dans le cas où l'on travaille sur des fichiers, lorsqu'il y a conflit, c'est cet état de conflit qui est l'ancêtre commun de tous les états futurs du dépôt. Or, pour le représenter, il faut utiliser un graphe de lignes. Et, ce qui est le plus important, lorsque l'on l'on travaille avec des graphes un tel descendant commun existe toujours et c'est lui que l'on appelle la fusion. Mais, ce qu'il y a de pire avec les autres systèmes, c'est que faute d'une telle définition formelle de la fusion ils ne choisissent pas toujours un tel descendant même s'il existe sans conflit (voir l'exemple de pmeunier).

Enfin, comme un état de conflit est un sommet comme les autres dans le graphe de l'historique, résoudre un conflit revient à lui appliquer un patch pour le ramener sur état similaire à une liste, i.e un fichier normal, et pijul garde en mémoire tant l'existence du conflit que sa résolution.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

J'ai juste un doute sur les deux dernières lignes: commit et merge sont bien des fonctions prenant les 2 premiers éléments en paramètre et faisant un résultat du type du dernier élément ?

Plus ou moins. La réponse de barmic est plus proche de la vérité, et c'est effectivement une pratique courante en programmation fonctionnelle (connue sous le nom de curryfication). Si j'écris le type de commit avec des parenthèses, cela donne :

val commit : patch -> (state -> state)

C'est une fonction qui prend un patch et retourne une fonction des états dans les états. Pour prendre une notation utilisée en mathématiques, il faudrait prendre la notation indicée. commit décrit une famille de fonctions indexées par des patchs. Ce qui correspond bien à ce qu'exprime le diagramme :

Les flèches entre sommets sont des transformations indexées par des patchs. Lorsque j'ai écrit :

• A = commit p O

il faudrait lire (en rajoutant des parenthèses) :

• A = (commit p) O

soit la fonction commit p appliquée à O, ou avec des indices :

De la même manière, une suite de fonctions des réels dans les réels a pour type nat -> real -> real.

Il y a bien une correspondance entre cette approche à la Curry et celle où les fonctions prennent un couple. Elle traduit cette égalité algébrique :

L'exponentiel de l'exponentiel est égale à l'exponentiel du produit. C'est liée à l'algèbre des types : là où le produit cartésien correspond au produit, le type des fonctions correspond à l'exponentiel.

Si un type A a 2 éléments et un type B a 3 éléments, alors le type A -> B a 3^2 = 9 éléments (A -> B = B ^ A).

Pour en revenir à la fonction commit, elle associe chaque patch à une fonction des états sur eux-mêmes. Lorsque l'on dit que l'on applique un patch, c'est un abus de langage, en réalité on applique la fonction associée au patch via commit. Et lorsque l'on dit que les patchs sont associatifs, c'est parce que la composition de fonctions est associative. En notant . la composition de fonction on a les égalités :

  (commit r . commit q) . commit p
= commit r . (commit q . commit p)
= commit r . commit q . commit p

Ce qui revient à « appliquer » les patchs dans l'ordre p, q, r.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

⚠ Je ne te demande pas de me le réexpliquer avec d'autres mots, et surtout pas des termes mathématiques! ⚠

En complément du commentaire d'Adrien Dorsaz, je vais quand même essayer. Mais ne t'inquiète pas, ce sera des mathématiques simples : de l'arithmétique élémentaire avec les nombres entiers, et un peu de graphes.

Une image que j'aime bien et qui représente des historiques possibles d'un dépôt est celle-ci :

On peut résumer le cœur d'un gestionnaire de version à cette interface rudimentaire :

type patch
type state
val commit : patch -> state -> state
val merge : state -> state -> state

Il y a deux concepts : les patchs et les états, puis deux fonctions pour appliquer un patch sur un état ou fusionner deux états. Ainsi, sur le graphe du dessus, on a par exemple :

• A = commit p O
• M = merge A B

Plutôt que de travailler avec des fichiers et des répertoires, commençons plus simple et travaillons avec des entiers naturels. Les états (ou sommets du graphes) sont des entiers et les patchs sont aussi des entiers où la fonction de commit est la multiplication. Le graphe relie alors deux entiers s'ils sont multiples et l'arrếte est étiquetée par le coefficient multiplicateur. La fonction de fusion (merge) calcule le plus petit commun multiple.

On peut par exemple partir de l'état initial 1 et prendre pour les trois patchs du graphes les nombres suivants : p = 2, q = 3 et r = 7. Je remets le graphe :

On aura ainsi le sommet A = 2, le sommet B = 3 et leur fusion M = 6. Ce qu'exprime le graphe, c'est que quelque soit le chemin que l'on prenne pour fusionner ces trois patchs, on tombera toujours sur Q = 42. Cela parce que la multiplication est associative et commutative.

La première propriété (associativité) n'est pas satisfaite par les autres CVS : fusionner A et N ou bien fusionner M et C ne donnera pas toujours le même résultat. C'est cela qu'illustre ces deux schémas dans la documentation de pijul :

Le pire étant que ces CVS peuvent fusionner le tout, sans signaler de conflit, et faire n'importe quoi. Tel était l'exemple donné par Pierre-Étienne Meunier.

Ensuite, à la place des nombres entiers, on peut prendre un Rubik's cube. Ici les états seraient ceux du cube, et le patchs les transformations qu'on peut lu faire subir. Avec un tel système, on aura toujours l'associativité des transformations. Que je fasse p ; (q ; r) ou (p; q) ; r cela ne change pas grand chose et l'on dit que l'on a effectué ces trois transformations à la suite p; q; r, sans mettre de parenthèses. Par contre, sur un rubik's cube, deux patchs ne peuvent pas toujours être appliqués dans n'importe quel ordre, lorsqu'ils bougent des zones communes. Dans ce cas, on dit qu'ils ne commutent pas. Il en est de même avec les CVS : des fois ça commute, des fois ça ne commute pas; mais pijul est capable de déterminer si deux patchs commutent ce qui lui permet (non de réécrire l'historique) mais de réécrire le graphe de dépendance entre les patchs pour faciliter la gestion du dépôt : on peut supprimer facilement l'effet d'un patch sans toucher aux modifications qui lui sont postérieures et indépendantes.

Il reste un point à éclaircir : la représentation interne des conflits. Revenons au cas des nombres entiers ou la fonction de merge était le calcul de plus petit commun multiple. Et regardons, ce graphe :

Ici, nos sommets sont toujours des entiers, M est le ppcm de A et B et F est un multiple quelconque de A et B, mais aussi un multiple de M. Ce que fait pijul c'est généraliser cette notion de ppcm aux fichiers. Pour cela, on considère un fichier comme une liste de lignes. Malheureusement, il n'y a pas toujours de ppcm pour deux fichiers : c'est le signe d'un conflit lors d'une fusion.

La solution est de prendre un type plus riche que les liste pour les sommets du graphe : à savoir des graphes de lignes (dont les listes sont un cas particuliers). À ce moment là, deux graphes de lignes ont toujours un « ppcm » que l'on appelle leur fusion. Si ce graphe est similaire à une liste alors il n'y a pas de conflit sinon c'est qu'il y a conflit :

If the two following conditions are both met:

• the graph is acyclic, and contains a path passing through all the vertices.
• for each vertex v, all incoming edges of v have the same label ("alive" vs. "deleted").

Then the task of presenting the file to the user is relatively straightforward: just go along the path and output all alive vertices. Else, we say the file has a conflict, and presenting the state of the file to the user in an intelligible way is not obvious.

pijul documentation

Comme pijul travail avec des états qui sont ces graphes de lignes, il a une représentation interne des conflits (des graphes qui ne sont pas des listes) et peut travailler sur eux comme il le ferait avec des fichiers normaux : on peut leur appliquer des patchs, les fusionner… et les aplatir vers des fichiers (résoudre les conflits) quand on veut.

D'une manière générale, j'aime bien ce principe : Theorise first then implement is the stairway to heaven. Implement first then theorise is the highway to hell. D'autant que Jimmy page était, sans nul doute ni contestation, bien plus fin et subtil qu'Angus Young. :-P

Comme pijul a choisi la première voie, c'est plus simple et plus naturel; les autres systèmes reposant sur une mauvaise analyse de l'algèbre des patchs et des états.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je ne suis pas sûr de savoir ce que sont les graggle, j'imagine que c'est le graphe des lignes.

Oui c'est cela, c'est le nom que leur a donné Joe Neeman. J'avais lu ces articles de blog pour comprendre la théorie derrière pijul, sans avoir à me farcir les articles académiques.

Justement pas trop, parce que le renommage ne produit pas juste une liste.

Là je ne comprends pas trop. Il y a d'autres forme de graphes que les listes pour représenter un état sans conflit ?

Pour ce qui est du dictionnaire de renommage, pourquoi ne pas le mettre comme tag sur le patch ? En admettant qu'il soit facilement décidable à quel sous-type de patch on a affaire : pijul remarque que A propose un patch de renommage, de même que B, et il marque chacun des patch avec leur dictionnaire. Puis lors de la résolution de conflit, pijul spécifie la cause du conflit (conflit de renommage) et propose une solution spécifique : choisir les noms de A ou ceux de B.

Si j'ai bien compris l'idée des patchs sémantiques, le principe est d'avoir un type générique patch avec plusieurs sous-type (déplacement, renommage, indentation…). Le problème étant, en autre, de savoir s'il est facilement décidable de savoir à quel sous-type appartient un patch donné. Mais, si c'est le cas, l'information devrait être attachée au patch et non au graphe de ligne.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

encore une fois, que doit-on faire si Alice et Bob décident en parallèle de renommer la même variable avec deux noms différents ?

Il y a conflit ? Le merge est un graphe qui n'est pas une liste et il y a conflit à résoudre.

Si j'ai bien compris les principes derrière pijul, il y a au fond deux opérations primitives commit : patch -> graggle -> graggle et merge : graggle -> graggle -> graggle. Elles ont de bonnes propriétés algébriques, de telles sorte que le graphe ci-dessous commute :

Mais comme tu le dis dans un autre commentaire, pijul n'a pas besoin de patchs sémantiques pour fonctionner correctement. À la rigueur, cela pourrait être utile pour l'UI et fournir des informations plus détaillées à l'utilisateur lorsqu'il doit résoudre un conflit.

Dans le fond, ces patchs sémantiques sont juste une subdvision du type des patch (des sous-types) mais l'essentiel pour pijul c'est que ce soit des patchs. N'est-ce pas cela ? Dans ce cas, la seule chose que cela peut apporter serait d'ajouter des tags sur les patchs (comme les différentes variantes d'un type somme sont tagguées par un compilateur) et s'en servir pour adapter les messages au niveau de l'interface utilisateur, mais sans rien modifier sous le capot au niveau de la gestion des fusions et conflits.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Dans une économie de marché purement libérale (pas de socialisation de pertes, risque réel pour les prêts), un tel gonflement ne serait pas arrivé et on pourrait comparer une telle approche purement libérale par rapport à l'approche qui décapitalise le logement.

C'est là que j'ai du mal à te suivre. Tu admets qu'un des problèmes c'est l'intervention étatique sur le marché (qui déresponsabilise certains acteurs), et comme solution tu prônes encore plus d'État. Que les marchés puissent être défaillants, c'est certain, mais il y a une chose encore plus défaillante que les marchés : l'administration. L'école de Chicago :-)

En passant, tu demandes des sources à Nicolas Boulay dans un autre commentaire, tu les as dans le lien que te proposais barmic :

Pour remédier à cet état de fait, les auteurs de l'étude recommandent de "réfléchir à des politiques structurelles visant à augmenter l'élasticité de l'offre de logements" par la "simplification et l'accélération des procédures d'autorisation de construction dans un cadre juridique maîtrisé".

[…]

Pour le CAS, "les effets de l'inélasticité de l'offre peuvent être atténués par des politiques visant à favoriser une meilleure allocation du parc de logements". "Celle-ci passe notamment par une réduction des freins à la mobilité résidentielle: distorsions fiscales liées au traitement différentiel des propriétaires et des locataires, et coûts de transaction (droits de mutation)", propose le CAS.

Le problème reste bien celui d'une pénurie d'offre dans certains secteurs.

Sur tes tautologies, j'ai du mal avec la dernière :

« Capitaliser sur le logement, c'est capitaliser sur un bien et droit fondamental. »

J'ai toujours eu du mal avec cette notion de bien et droit fondamental. Quel sens lui donner ? Et quels sont les critères pour qualifier ainsi un bien et un droit ?

Je ne peux me représenter avoir un droit sans qu'autrui est un devoir en contrepartie (et réciproquement, en vertu du principe d'égalité juridique, autrui a ce droit et moi ce devoir), mais quel devoir mettre en face du droit fondamental au logement ?

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je ne veux pas revenir sur l'ensemble de ton commentaire, mais il y a tout de même un passage qui m'a vraiment fait tiquer plus que les autres :

Pourquoi ne ressentons nous pas de mouvement (Et là c'est le pire: Galilée affirme que la mouvement de la terre est en fait la cause les marrées, alors que ça n'a rien à voir)

Là pour moi ce qui est pire est que tu omets totalement le cœur de la question et la solution fondamentale de Galilée. Sa réponse, c'est le principe d'invariance galiléen, autrement appelé principe de relativité restreinte par les physiciens. Ramener cela à la question des marées, c'est au pire de la mauvaise foi, au mieux de l'ignorance.

Il justifia ce principe dans son Dialogue sur les deux grands systèmes du monde à travers des expériences de pensée impliquant un homme enfermé dans sa cabine sur un bateau et qui, à partir des expériences qu'il y mène, ne peut constater le mouvement de son navire. C'est à partir de cela que Newton tira son Principe Fondamental de la Dynamique, et qu'Einstein développa encore plus dans ses deux théories de la relativité (qui est donc son homme enfermé dans sa cabine, pour qui inertie et gravité sont identiques dans leur principe, si ce n'est un lointain cousin du personnage de Galilée ?).

Ceci étant, dans son ouvrage, il y a effectivement un idiot du nom de Simplicio : celui qui s'attache avec acharnement aux principes de la physique d'Aristote et de sa théorie du mouvement.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Les angles y sont corrects. ;)

Que vient faire le fair-play britannique dans cette histoire ? :-P

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

De mon point de vue, se baser sur un document comportant de telles erreurs [mathématiques] n'est pas pertinent, car il ne saurait être considéré comme une source fiable ou crédible.

Ah, mais je partage ton avis sur le document en question, et ce n'est pas que sur le plan mathématique qu'il est douteux, il l'est aussi : philosophiquement (philosophie du droit) et économiquement (du au premier point, mais aussi sur la partie historique en fin d'ouvrage). Seulement, en dehors de lui, je ne connais personne qui emploie le terme monnaie libre, il me semblait donc que c'était à cela que faisait référence El Titi et je répondais alors à la question de Marco.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

si on peut me définir une monnaie libre ça serait sympa aussi

Les principes de la monnaie libre sont présentés dans la théorie relative de la monnaie et pour la définition de monnaie libre c'est, plus particulièrement, ici.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

CNR ? Comité National Révolutionnaire ?

Encore pour PPA, je peux comprendre, c'est un acronyme qui ne doit être compris et connu que dans certains milieux idéologiques. En revanche, pour celui-ci, cela relève de l'histoire de France : Conseil National de la Résistance. Bien qu'il fût initié par De Gaulle sous la direction de Jean Moulin, afin d'unifier les différents mouvements de résistance durant la seconde guerre, son programme politique de 1944 était très empreint de communisme (comme on peut le constater à la lecture des premiers articles sur la presse).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Art. 1. La presse n’est pas un instrument de profit commercial, mais un instrument de culture ; sa mission est de donner des informations exactes, de défendre des idées, de servir la cause du progrès humain.

Intéressant article auquel je propose celui-ci en miroir :

Art. 1. La boulangerie, l'élevage et l'agriculture ne sont pas des instruments de profit commercial, mais des instruments d'alimentation ; leur mission est de donner de la nourriture de qualité, en quantité suffisante, de servir à la survie de l'espèce humaine.

Ce dernier étant, à mon sens, bien plus important que celui du CNR : à quoi sert de pouvoir s'informer si l'on n'est même pas assurer de survivre ?

Il faudra un jour que l'on m'explique ce qu'il y a de malsain, par principe, dans une relation commerciale.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Au-delà de comment quelques individuEs

et c'est tellement peu intuitif que tu l'utilises sur un nom masculin.

Il eut été plus simple d'écrire « Au-delà de comment quelques personnes… »

Ceci étant, avec cette nouvelle écriture, il faudrait écrire comment ?

• unE personnE
• quelques personnEs

ou bien garder la graphie actuelle ? Dans ce cas pourquoi ne toucher que les substantifs génériques du genre masculin ?

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Ça n'est pas parce qu'Indiana Jones ressemble comme deux gouttes d'eau à Harrison Ford

D'autant que, il est nécessaire de le rappeler, Indiana c'était le nom du chien ! Mais ils ont peut être pris aussi des images de chiens pour alimenter leur algorithme… :-D

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.