Vue lecture

Programmer des démonstrations : une modeste invitation aux assistants de preuve

24 février 2025 à 12:07

En principe, une démonstration mathématique ne fait que suivre des règles logiques bien définies, et devrait donc pouvoir être encodée informatiquement et vérifiée par un ordinateur. Où en est-on dans la pratique et dans la théorie ? Petit tour au pays des assistants de preuve, des langages de programmation dédiés aux démonstrations, et de leur fondement théorique le plus commun, la théorie des types.

lien nᵒ 1 : Why formalize mathematics? par Patrick Massot

Sommaire

Vérifier des programmes

Comme nous sommes sur LinuxFr.org, je devrais peut-être commencer par ceci : nous passons énormément de temps à découvrir des bugs, et pour les personnes du développement logiciel, à les comprendre, à les résoudre, et de préférence à les éviter en écrivant des tests.

Dans une formation universitaire de base en informatique, on rencontre des algorithmes, mais aussi des méthodes pour prouver que ces algorithmes terminent et répondent bien au problème posé. Les premières introduites sont typiquement les variants de boucle (montrer qu’une certaine valeur décroît à chaque itération, ce qui assure que le programme termine si elle ne peut pas décroître à l’infini), et les invariants de boucle (montrer qu’une certaine propriété vraie au début d’une boucle est préservée entre deux itérations, ce qui assure qu’elle reste encore vraie à la fin de la boucle).

On a donc, d’une part, un algorithme, implémentable sur machine, d’autre part une preuve, sur papier, que l’algorithme est correct. Mais si l’implémentation a une erreur par rapport à l’algorithme sur papier ? Et puisque nous n’arrêtons pas de nous tromper dans nos programmes, il est fort possible que nous nous trompions dans notre preuve (qui n’a jamais oublié qu’il fallait faire quelque chose de spécial dans le cas n = 0 ?).

En tant que programmeurs, on peut imaginer une approche où non seulement l’algorithme est implémenté, mais sa preuve de terminaison et de correction est aussi « implémentée », c’est-à-dire encodée dans un langage qui ressemble à un langage de programmation, pour être ensuite non pas interprétée ou compilée mais vérifiée.

La vérification est un très vaste domaine de l’informatique, dont je ne suis pas spécialiste du tout, et dans lequel il existe énormément d’approches : la logique de Hoare (voir par exemple l’outil why3), qui est essentiellement un raffinement des variants et invariants de boucle, la logique de séparation spécialement conçue pour raisonner sur la mémoire mutable (voir Iris), le model checking qui se concentre sur des programmes d’une forme particulièrement simple (typiquement des systèmes de transition finis) pour en vérifier des propriétés de façon complètement automatisée, etc.

Dans cette dépêche, je vais parler d’une approche avec quelques caractéristiques particulières :

On vérifie des programmes purement fonctionnels (pas d’effets de bord, même si on peut les simuler).
Le même langage mélange à la fois les programmes et leurs preuves.
Plus précisément, le langage ne fait pas (ou peu) de distinction entre les programmes et les preuves.

Vérifier des démonstrations mathématiques

Pour se convaincre de l’ampleur que les démonstrations ont prise dans les mathématiques contemporaines, il suffit d’aller jeter un œil, par exemple, au projet Stacks : un livre de référence sur la géométrie algébrique, écrit collaborativement sur les 20 dernières années, dont l’intégrale totalise plus de 7500 pages très techniques. Ou bien la démonstration du théorème de classification des groupes finis simples : la combinaison de résultats répartis dans les dizaines de milliers de pages de centaines d’articles, et une preuve « simplifiée » toujours en train d’être écrite et qui devrait faire plus de 5000 pages. Ou bien le théorème de Robertson-Seymour, monument de la théorie des graphes aux nombreuses applications algorithmiques : 20 articles publiés sur 20 ans, 400 pages en tout. Ou bien, tout simplement, le nombre de références dans la bibliographie de la moindre thèse ou d’articles publiés récemment sur arXiv.

Inévitablement, beaucoup de ces démonstrations contiennent des erreurs. Parfois découvertes, parfois beaucoup plus tard. Un exemple assez célèbre est celui d’un théorème, qui aurait été très important s’il avait été vrai, publié en 1989 par Vladimir Voedvodsky, un célèbre mathématicien dont je vais être amené à reparler plus bas, avec Mikhail Kapranov. Comme raconté par Voedvodsky lui-même, un contre-exemple a été proposé par Carlos Simpson en 1998, mais jusqu’en 2013, Voedvodsky lui-même n’était pas sûr duquel était faux entre sa preuve et le contre-exemple !

Il y a aussi, souvent, des « trous », qui ne mettent pas tant en danger la démonstration mais restent gênants : par exemple, « il est clair que la méthode classique de compactification des espaces Lindelöf s’applique aussi aux espaces quasi-Lindelöf », quand l’auteur pense évident qu’un argument existant s’adapte au cas dont il a besoin mais que ce serait trop de travail de le rédiger entièrement. Donc, assez naturellement, un but possible de la formalisation des maths est de produire des démonstrations qui soient certifiées sans erreur (et sans trou).

Mais c’est loin d’être le seul argument. On peut espérer d’autres avantages, qui pour l’instant restent de la science-fiction, mais après tout ce n’est que le début : par exemple, on peut imaginer que des collaborations à grande échelle entre beaucoup de mathématiciens deviennent possibles, grâce au fait qu’il est beaucoup plus facile de réutiliser le travail partiel de quelqu’un d’autre s’il est formalisé que s’il est donné sous formes d’ébauches informelles pas complètement rédigées.

Brouwer-Heyting-Kolmogorov

Parmi les assistants de preuve existants, la plupart (mais pas tous) se fondent sur une famille de systèmes logiques rangés dans la famille des « théories des types ». L’une des raisons pour lesquelles ces systèmes sont assez naturels pour être utilisés en pratique est qu’en théorie des types, les preuves et les programmes deviennent entièrement confondus ou presque, ce qui rend facile le mélange entre les deux.

Mais comment est-ce qu’un programme devient une preuve, au juste ? L’idée de base est appelée interprétation de Brouwer-Heyting-Kolomogorov et veut que les preuves mathématiques se comprennent de la façon suivante :

Le moyen de base pour prouver une proposition de la forme « et » est de fournir d’une part une preuve de et une preuve de . En d’autres mots, une preuve de « et » rassemble en un même objet une preuve de et une preuve de . Mais en termes informatiques, ceci signifie qu’une preuve de « et » est une paire d’une preuve de et d’une preuve de .
De même, pour prouver « ou », on peut prouver , ou on peut prouver . Informatiquement, une preuve de « ou » va être une union disjointe : une preuve de ou une preuve de , avec un bit pour savoir dans quel cas on est.
Pour prouver « Vrai », il suffit de dire « c’est vrai » : on a une unique preuve de « Vrai ».
On ne doit pas pouvoir prouver « Faux », donc une preuve de « Faux » n’existe pas.
Et le plus intéressant : pour prouver « si alors », on suppose temporairement et on en déduit . Informatiquement, ceci doit devenir une fonction qui prend une preuve de et renvoie une preuve de .

Curry-Howard

L’interprétation de Brouwer-Heyting-Kolmogorov est informelle, et il existe plusieurs manières de la rendre formelle. Par exemple, on peut interpréter tout ceci par des programmes dans un langage complètement non-typé, ce qui s’appelle la réalisabilité.

Mais en théorie des types, on prend plutôt un langage statiquement typé pour suivre l’idée suivante : si une preuve de et est une paire d’une preuve de et d’une preuve de , alors le type des paires de et peut se comprendre comme le type des preuves de « et ». On peut faire de même avec les autres types de preuves, et ceci s’appelle la correspondance de Curry-Howard. Autrement dit, là où Brouwer-Heyting-Kolmogorov est une correspondance entre les preuves et les programmes, Curry-Howard est un raffinement qui met aussi en correspondance les propositions logiques avec les types du langage, et la vérification des preuves se confond entièrement avec le type checking.

Sur les cas que j’ai donnés, la correspondance de Curry-Howard donne :

La proposition « et » est le type des paires d’un élément de et d’un élément de ,
La proposition « ou » est le type somme de et (comme Either en Haskell et OCaml, les tagged unions en C, et std::variant en C++ : l’un ou l’autre, avec un booléen pour savoir lequel),
La proposition « Vrai » est le type trivial à une seule valeur (comme () en Haskell et Rust, unit en OCaml),
La proposition « Faux » est le type vide qui n’a aucune valeur (comme ! en Rust),
La proposition « si alors » est le type des fonctions qui prennent un argument de type et renvoient une valeur de type .

Quantificateurs et types dépendants

La version de Curry-Howard que j’ai esquissée donne une logique dite « propositionnelle » : il n’y a que des propositions, avec des connecteurs entre elles. Mais en maths, on ne parle évidemment pas que des propositions. On parle de nombres, de structures algébriques, d’espaces topologiques, …, bref, d’objets mathématiques, et des propriétés de ces objets. Les deux types principaux de propositions qui manquent sont ce qu’on appelle les quantificateurs : « Pour tout , … » et « Il existe tel que… ». Ici, ce qui est une évidence en logique devient moins évident, mais très intéressant, du côté des programmes.

Prenons pour l’exemple le théorème des deux carrés de Fermat, qui énonce (dans l’une de ses variantes) qu’un nombre premier impair est de la forme 4n+1 si et seulement s’il peut s’écrire comme somme de deux carrés parfaits. À quoi doit ressembler le type associé à cette proposition ? Par analogie avec les implications, on a envie de dire que cela devrait être une fonction, qui prend un nombre premier impair , et renvoie une preuve de l’équivalence. Problème : ce qui est à droite de l’équivalence est une proposition paramétrée par . Autrement dit, en notant le type des nombres premiers impairs, on ne veut plus un simple type fonction P → E , mais un type fonction où le type de retour peut dépendre de la valeur passée à la fonction, noté par exemple (p : P) → E(p) . Ces types qui dépendent de valeurs sont appelés types dépendants.

Dans les langages de programmation populaires, il est rare de trouver des types dépendants. Mais on en retrouve une forme faible en C avec les tableaux de longueur variable (VLA pour « variable-length arrays ») : on peut écrire

… f(int n) {
  int array[n];
  …
}

qui déclare un tableau dont la taille n est une expression. Néanmoins, en C, même si on dispose de ce type tableau qui est en quelque sorte dépendant, on ne peut pas écrire une fonction « int[n] f(int n) » qui renvoie un tableau dont la longueur est passée en paramètre. Plus récemment, en Rust, il existe les const generics, où des valeurs se retrouvent dans les types et où on peut écrire fn f<const n: usize>() -> [u8; n], ce qui est un vrai type dépendant, mais cette fois avec la restriction assez sévère que toutes ces valeurs peuvent être calculées entièrement à la compilation, ce qui à cause de la façon dont fonctionne ce type de calcul en Rust empêche par exemple les allocations mémoire. (Donc l’implémentation est assez différente, elle efface ces valeurs en « monomorphisant » tous les endroits où elles apparaissent.)

En théorie des types, le langage est (normalement) purement fonctionnel, donc les problèmes d’effets de bord dans les valeurs à l’intérieur des types dépendants ne se pose pas. Le type checking peut déclencher des calculs arbitrairement complexes pour calculer les valeurs qui se trouvent dans les types.

Et le « il existe », au fait, à quoi correspond-il ? Cette fois, ce n’est plus une fonction dépendante mais une paire dépendante : une preuve de « Il existe tel que E(x) » est une paire d’une valeur et d’une preuve de E(x) . La différence avec une paire normale est que le type du deuxième élément peut dépendre de la valeur du premier élément.

Comme on peut commencer à s’en douter, le fait d’avoir des types dépendants est utile pour prouver des affirmations mathématiques, mais aussi, bien qu’il puisse sembler inhabituel, pour prouver des programmes, et plus précisément pour encoder des propriétés des valeurs dans les types. Là où on aurait dans un langage moins expressif une fonction qui renvoie deux listes, avec une remarque dans la documentation qu’elles sont toujours de même taille, dans un langage avec des types dépendants, on peut renvoyer un triplet d’un entier , d’une liste dont le type indique qu’elle est de taille , et une deuxième liste elle aussi de taille . Et là où on aurait un deuxieme_liste[indice_venant_de_la_premiere] avec un commentaire que cela ne peut pas produire d’erreur, car les deux listes sont de même taille, on a un programme qui utilise la garantie que les deux listes sont de même taille, et le typage garantit statiquement que cette opération t[i] ne produira pas d’erreur.

Logique intuitionniste

Reprenons l’exemple du théorème des deux carrés de Fermat. Nous pouvons maintenant traduire cette proposition en un type : celui des fonctions qui prennent un nombre premier impair et renvoient une paire de :

Une fonction qui prend tel que et renvoie deux entiers accompagnés d’une preuve que ,
Réciproquement, une fonction qui prend et une preuve de , et renvoie tel que .

Prouver le théorème des deux carrés de Fermat en théorie des types, c’est donner un élément (on dit plutôt « habitant ») de ce type, soit un programme dont le langage peut vérifier qu’il a ce type. Mais que fait au juste ce programme quand on l’exécute ? On voit qu’il permet notamment de calculer une décomposition d’un nombre premier impair congru à 1 modulo 4 comme somme de deux carrés.

Là, c’est le côté « programmes » qui apporte un élément moins habituel du côté « preuves » : l’exécution d’un programme va correspondre à un processus de simplification des preuves. Notamment, si on a une preuve de « si alors » et une preuve de , on peut prendre la preuve de et remplacer chaque utilisation de l’hypothèse dans la preuve de « si alors », pour obtenir une preuve de qui peut contenir de multiples copies d’une même preuve de . Cette opération de simplification du côté logique correspond naturellement au fait que la manière en théorie des types de prouver à partir d’une preuve de P ⇒ Q et d’une preuve de est tout simplement d’écrire f(x) , et que calculer f(x) , informatiquement, se fait bien en remplaçant le paramètre de à tous les endroits où il apparaît par la valeur et à simplifier le résultat. On dit que la logique de Curry-Howard est constructive, parce qu’elle se prête à une interprétation algorithmique.

Mais ceci peut sembler gênant. Par exemple, il est trivial en maths « normales » de prouver que tout programme termine ou ne termine pas. Mais par Curry-Howard, une preuve que tout programme termine ou ne termine pas doit être une fonction qui prend un programme, et qui renvoie soit une preuve qu’il termine, soit une preuve qu’il ne termine pas. Autrement dit, si cette proposition censément triviale était prouvable dans Curry-Howard, on aurait un algorithme pour résoudre le problème de l’arrêt, ce qui est bien connu pour être impossible.

L’explication à cette différence tient au fait que la preuve « triviale » de cette proposition utilise une règle de déduction qui a un statut un peu à part en logique, dite règle du tiers exclu : pour n’importe quelle proposition , sans aucune hypothèse, on peut déduire « ou (non ) » (autrement dit, que est vraie ou fausse). Or cette règle n’admet pas d’interprétation évidente par Curry-Howard : le tiers exclu devrait prendre une proposition et renvoyer soit une preuve de , soit une preuve que est fausse (ce qui s’encode par « si alors Faux »), autrement dit, le tiers exclu devrait être un oracle omniscient capable de vous dire si une proposition arbitraire est vraie ou fausse, et ceci est bien évidemment impossible.

(Cela dit, si vous voulez vous faire mal à la tête, apprenez que c’est l’opérateur call/cc et pourquoi l’ajouter permet de prouver le tiers exclu. Exercice : call/cc existe dans de vrais langages, comme Scheme, pourtant on vient de voir que le tiers exclu semble nécessiter un oracle omniscient, comment expliquer cela ?)

Pour être précis, la logique sans le tiers exclu est dite intuitionniste (le terme constructive étant un peu flou, alors que celui-ci est précis). On peut faire des maths en restant entièrement en logique intuitionniste, et même si ce n’est pas le cas de l’écrasante majorité des maths, il existe tout de même un certain nombre de chercheurs qui le font, et ceci peut avoir divers intérêts. Il y a notamment l’interprétation algorithmique des théorèmes, mais aussi, de manière beaucoup plus avancée, le fait que certaines structures mathématiques (topos, ∞-topos et consorts) peuvent s’interpréter comme des sortes d’univers mathématiques alternatifs régis par les règles de la logique intuitionniste (techniquement, des « modèles » de cette logique), et que parfois il est plus simple de prouver un théorème en le traduisant à l’intérieur de l’univers et en prouvant cette version traduite de manière intuitionniste.

Pour pouvoir malgré tout raisonner en théorie des types de manière classique (par opposition à intuitionniste), il suffit de postuler le tiers exclu comme axiome. Du point de vue des programmes, cela revient à rajouter une constante qui est supposée avoir un certain type mais qui n’a pas de définition (cela peut donc rendre les programmes impossibles à exécuter, ce qui est normal pour le tiers exclu).

Quelques exemples

Si vous aviez décroché, c’est le moment de reprendre. Parlons un peu des assistants de preuve qui existent. Les plus connus sont :

Rocq, anciennement nommé Coq, développé à l’Inria depuis 1989, écrit en OCaml, sous licence LGPL 2.1. Il est assez lié à l’histoire de la théorie des types, car il a été créé par Thierry Coquand comme première implémentation du calcul des constructions, une théorie des types inventée par Coquand et devenue l’une des principales existantes. (Oui, Coq a été renommé en Rocq à cause de l’homophonie en anglais entre « Coq » et « cock ». J’apprécierais que les commentaires ne se transforment pas en flame war sur ce sujet très peu intéressant, merci.)
Lean, créé par Leonardo de Moura et développé depuis 2013 chez Microsoft Research, écrit en C++, placé sous licence Apache 2.0.
Agda, créé par Ulf Norrell en 1999, écrit en Haskell et sous licence BSD 1-clause.
D’autres que je connais moins, notamment Isabelle et F* (liste sur Wikipédia).

Pour illustrer comment peuvent fonctionner les choses en pratique, voici un exemple très simple de code en Agda :

open import Agda.Primitive using (Level)
open import Data.Product using (_×_; _,_)

swap : {ℓ₁ ℓ₂ : Level} → {P : Set ℓ₁} {Q : Set ℓ₂} → P × Q → Q × P
swap (p , q) = (q , p)

Vue comme un programme, cette fonction swap inverse simplement les deux éléments d’une paire. Vue comme une preuve, elle montre que pour toutes propositions et , si et , alors et . Comme le veut Curry-Howard, les deux ne sont pas distingués. Les types et sont eux-mêmes dans des types $\mathsf{Set}_\ell$ avec un « niveau » $\ell$ , ceci parce que, pour des raisons logiques, il serait incohérent que le type des types soit de son propre type, donc on a un premier type de types $\mathsf{Set}_0$ , qui est lui-même de type $\mathsf{Set}_1$ , et ainsi de suite avec une hiérarchie infinie de niveaux appelés univers. À un niveau plus superficiel, on remarquera qu’Agda a une syntaxe qui ressemble fort à Haskell (et utilise intensivement Unicode).

Voilà la même chose en Rocq :

Definition swap {P Q : Prop} : P /\ Q -> Q /\ P :=
  fun H => match H with conj p q => conj q p end.

La syntaxe est assez différente et ressemble plutôt à OCaml (normal, vu que Rocq est écrit en OCaml et Agda en Haskell). Mais à un niveau plus profond, on voit apparaître un type Prop dont le nom évoque furieusement les propositions. Or j’avais promis que les propositions seraient confondues avec les types, donc pourquoi a-t-on un type spécial pour les propositions ?

En réalité, pour diverses raisons, il peut être intéressant de briser l’analogie d’origine de Curry-Howard et de séparer les propositions et les autres types en deux mondes qui se comportent de façon extrêmement similaire mais restent néanmoins distincts. Notamment, un principe qu’on applique sans réfléchir en maths est que si deux propositions sont équivalentes, alors elles sont égales (extensionnalité propositionnelle), mais on ne veut clairement pas ceci pour tous les types (on peut donner des fonctions bool -> int et int -> bool, pourtant on ne veut certainement pas bool = int), donc séparer les propositions des autres permet d’ajouter l’extensionnalité propositionnelle comme axiome. (Mais il y a aussi des différences comme l'imprédicativité dans lesquelles je ne vais pas rentrer.)

Et voici encore le même code, cette fois en Lean :

def swap {P Q : Prop} : P ∧ Q → Q ∧ P :=
  fun ⟨p, q⟩ => ⟨q, p⟩

À part les différences de syntaxe, c’est très similaire à Rocq, parce que Lean a aussi une séparation entre les propositions et les autres types.

Cependant, en Rocq et Lean, on peut aussi prouver la même proposition de façon différente :

Lemma swap {P Q : Prop} : P /\ Q -> Q /\ P.
Proof.
  intros H. destruct H as [p q]. split.
  - apply q.
  - apply p.
Qed.

def swap {P Q : Prop} : P ∧ Q → Q ∧ P := by
  intro h
  have p := h.left
  have q := h.right
  exact ⟨q, p⟩

Avec Proof. ou by, on entre dans un mode où les preuves ne sont plus écrites à la main comme programmes, mais avec des tactiques, qui génèrent des programmes. Il existe toutes sortes de tactiques, pour appliquer des théorèmes existants, raisonner par récurrence, résoudre des inégalités, ou même effectuer de la recherche automatique de démonstration, ce qui s’avère extrêmement utile pour simplifier les preuves.

Ce mode « tactiques » permet aussi d’écrire la preuve de façon incrémentale, en faisant un point d’étape après chaque tactique pour voir ce qui est prouvé et ce qui reste à prouver. Voici par exemple ce qu’affiche Rocq après le destruct et avant le split :

  P, Q : Prop
  p : P
  q : Q
  ============================
  Q /\ P

Cette notation signifie que le contexte ambiant contient les variables P et Q de type Prop ainsi que p une preuve de P (donc un élément du type P) et q une preuve de Q. Le Q /\ P en dessous de la barre horizontale est le but à prouver, c’est-à-dire le type dont on cherche à construire un élément.

Agda fonctionne assez différemment : il n’y a pas de tactiques, mais il existe néanmoins un système de méta-programmation qui sert à faire de la recherche de preuves (donc contrairement à Rocq et Lean, on n’écrit pas la majeure partie des preuves avec des tactiques, mais on peut se servir d’un équivalent quand c’est utile). Pour écrire les preuves incrémentalement, on met ? dans le programme quand on veut ouvrir une sous-preuve, et Agda va faire le type-checking de tout le reste et donner le contexte à l’endroit du ?.

Quelques succès de la formalisation

En 2025, la formalisation reste très fastidieuse, mais elle a déjà eu plusieurs grands succès :

Le théorème des quatre couleurs, formalisé en Rocq (2005).
Le théorème de Feit-Thompson (étape dans la fameuse classification des groupes finis simples) en Rocq (2012).
Un théorème de Peter Scholze sur les « espaces vectoriels liquides » en Lean (2022).
Le retournement de la sphère en Lean (2022).
La valeur de BB(5) en Rocq (2024).

Actuellement, Lean a réussi à attirer une communauté de mathématiciens qui développent mathlib (1,1 million de lignes de code Lean au moment où j’écris), une bibliothèque de définitions et théorèmes mathématiques qui vise à être la plus unifiée possible.

Les équivalents dans d’autres assistants de preuve se développent même s’ils ne sont pas (encore) aussi gros : citons mathcomp, unimath, agda-unimath entre autres.

Un autre grand succès, dans le domaine de la vérification cette fois, est CompCert (malheureusement non-libre), qui est un compilateur C entièrement écrit en Rocq et vérifié par rapport à une spécification du C également encodée en Rocq.

La recherche en théorie des types

La théorie des types est un domaine de recherche à part entière, qui vise à étudier du point de vue logique les théories des types existantes, et à en développer de nouvelles pour des raisons à la fois théoriques et pratiques.

Historiquement, une grande question de la théorie des types est celle de comprendre à quel type doivent correspondre les propositions d’égalité. Par exemple, on veut que deux propositions équivalentes soient égales, et que deux fonctions qui prennent les mêmes valeurs soient égales, et éventuellement pour diverses raisons que deux preuves de la même proposition soient égales, mais s’il est facile d’ajouter toutes ces choses comme axiomes, il est très compliqué de les rendre prouvables sans obtenir, comme avec le tiers exclu, des programmes qui ne peuvent pas s’exécuter à cause des axiomes qui sont déclarés sans définition.

Vladimir Voedvodsky a fait une contribution majeure en proposant un nouvel axiome, appelé univalence, qui dit très sommairement que si deux types ont la même structure (on peut donner une « équivalence » entre les deux), alors ils sont en fait égaux (résumé simpliste à ne pas prendre au mot). Cet axiome est très pratique pour faire des maths parce qu’on travaille souvent avec des objets qui ont la même structure (on dit qu’ils sont isomorphes), et qui doivent donc avoir les mêmes propriétés, et cet axiome permet de les identifier (même s’il a aussi des conséquences qui peuvent paraître choquantes). Sa proposition a donné naissance à une branche appelée théorie homotopique des types, qui explore les maths avec univalence. Le prix à payer est que les types ne se comprennent plus comme de simples ensembles de valeurs (ou de preuves d’une proposition), mais comme des espaces géométriques munis de toute une structure complexe (techniquement, les égalités sont des chemins entre points, et il y a des égalités non-triviales, des égalités entre égalités, etc.), et la compréhension de ces espaces-types est fondée sur la théorie de l’homotopie. Il y a bien d’autres théories des types, avec univalence ou non : théorie cubique des types, théorie des types observationnelle, etc.

Conclusion

J’espère avoir communiqué un peu de mon enthousiasme pour le domaine (dans lequel je suis probablement parti pour démarrer une thèse). Si vous voulez apprendre un assistant de preuve, une ressource assez abordable est la série Software Foundations avec Rocq. Il existe également Theorem proving in Lean 4 et divers tutoriels Agda. Vous pouvez aussi essayer ces assistants de preuve directement dans votre navigateur : Rocq, Lean ou Agda. Et bien sûr les installer et jouer avec : Rocq, Lean, Agda.

Télécharger ce contenu au format EPUB

Commentaires : voir le flux Atom ouvrir dans le navigateur

Nouvelles de Haiku - Hiver 2024-25

LinuxFr.org : les dépêches

Par :pulkomandy · cli345 · Julien Jorge · orfenor · Benoît Sibaud · palm123 · Ysabeau 🧶

17 février 2025 à 15:01

Haiku est un système d’exploitation pour les ordinateurs personnels. Il s’agit à l’origine d’une réécriture de BeOS. Le projet a démarré en 2001 et est actuellement en phase de beta-test pour une première version stable avec support à long terme. Depuis 2024, l’activité du projet Haiku s’accélère grâce entre autres à l’embauche d’un développeur à plein temps. Les dépêches sur Haiku sont donc désormais publiées tous les 3 mois au lieu de tous les ans pour leur conserver une longueur digeste.

La complète liste des changements survenus pendant ces 3 mois comporte près de 300 commits. La dépêche ne rentre pas dans les détails de chaque changement et met en valeur les plus importants.

Les grosses évolutions sont un nouveau port de Iceweasel (Firefox), et des grosses améliorations sur la gestion de la mémoire.

Comme on est en début d’année, c’est aussi le moment du bilan financier.

lien nᵒ 1 : Rapport d'activité de novembre 2024
lien nᵒ 2 : Repport d'activté de décembre 2024
lien nᵒ 3 : Rapport d'activité de janvier 2025

Sommaire

Rapport financier 2024

Recettes

L’association Haiku inc (association de type 501(c)3 aux USA) publie chaque année un rapport financier. Le rôle de l’association est de récolter les dons et de les redistribuer pour aider au développement de Haiku. Elle ne prend pas part aux décisions techniques sur l’orientation du projet, et habituellement les dépenses sont faites en réponse aux demandes des développeurs du projet.

L’objectif en début d’année 2024 était de récolter 20 000$ de dons. Cet objectif a été largement atteint, il a dû être mis à jour 2 fois en cours d’année et finalement ce sont plus de 31 000$ qui ont été reçus ! Cela en particulier grace à un assez gros don de 7 500$.

Les dons sont récoltés via différentes plateformes: Github Sponsors (intéressant, car il n’y a aucun frais de traitement), PayPal, Liberapay, Benevity (une plateforme de « corporate matching »), ainsi que des paiements par chèque, virements bancaires, et en espèce lors de la tenue de stands dans des conférences de logiciels libres. La vente de T-Shirts et autre merchandising via la boutique Freewear reste anecdotique (une centaine de dollars cette année).

Il faut ajouter à ces dons une contribution de 4 400$ de la part de Google en compensation du temps passé à l’encadrement des participants au Google Summer of Code.

Il faut également ajouter des dons en crypto-monnaies, principalement en bitcoins. Le rapport financier présente les chiffres en détail en tenant une compatibilité séparée en dollars, en euros, et en crypto-monnaies, avant de convertir le total en dollars pour dresser un bilan complet.

Une mauvaise nouvelle tout de même: le service de microdons Flattr a fermé ses portes. L’entreprise propose maintenant un service de bloqueur de publicités payant, qui reverse de l’argent aux sites dont les publicités sont bloquées.

Le compte Flattr de Haiku avait été créé pour recevoir des dons sur la plateforme, mais n’avait jamais été configuré pour transférer ces dons vers le compte en banque de l’association. Malgré un certain temps passé à discuter avec le service client de Flattr et à leur fournir tous les documents demandés, il n’a pas été possible de trouver une solution pour récupérer cet argent. Ce sont donc 800$ qui ne reviendront finalement pas au projet Haiku.

Au final, les recettes sont de 36 479 dollars, de loin la plus grosse somme reçue par le projet en un an.

Dépenses

La dépense principale est le paiement de Waddlesplash, le développeur actuellement employé par Haiku inc pour accélérer le développement du système (les autres développeurs participent uniquement sur leur temps libre, en fonction de leurs autres activités). Cela représente 25 500$, un coût assez faible par rapport au travail réalisé.

Le deuxième poste de dépenses est l’infrastructure, c’est-à dire le paiement pour l’hébergement de serveurs, les noms de domaines, et quelques services « cloud » en particulier pour le stockage des dépôts de paquets.

Le reste des dépenses consiste en frais divers (commission PayPal par exemple), remboursement de déplacements pour la participation à des conférences, ainsi que le renouvellement de la marque déposée sur le logo Haiku.

Le total des dépenses s’élève à 31 467$. C’est moins que les recettes, et l’association continue donc de mettre de l’argent de côté. L’année 2022 a été la seule à être déficitaire, suite au démarrage du contrat de Waddlesplash. Ce contrat est à présent couvert par les donations reçues.

Réserves

L’association dispose de plus de 100 000$ répartis sur son compte en banque, un compte PayPal (qui permet de conserver des fonds en euros pour les paiements en euros et ainsi d’éviter des frais de change), et un compte Payoneer (utilisé pour recevoir les paiements de Google).

Elle dispose également de près de 350 000$ en crypto-monnaies dont la valeur continue d’augmenter. Cependant, actuellement ces fonds ne sont pas accessibles directement, en raison de problèmes administratifs avec Coinbase, l’entreprise qui gère ce portefeuille de crypto-monnaies. Le compte n’est pas configuré correctement comme appartenant à une association à but non lucratif et cela pose des problèmes de déclaration de taxes lorsque on souhaite vendre des crypto-monnaies contre du vrai argent. Cette situation persiste depuis plusieurs années, mais l’association n’a pour l’instant pas besoin de récupérer cet argent, les réserves dans le compte en banque principal étant suffisantes.

Applications

Iceweasel

Le navigateur web Iceweasel est disponible dans les dépôts de paquets (seulement pour la version 64 bits pour l’instant). Il s’agit d’un portage de Firefox utilisant la couche de compatibilité Wayland. Le nom Firefox ne peut pas être utilisé puisqu’il ne s’agit pas d’un produit officiel de Mozilla.

En plus du travail de portage pour réussir à faire fonctionner le navigateur, cela a nécessité un gros travail d’amélioration au niveau de la gestion de la mémoire, une partie du système qui est fortement mise à contribution par ce navigateur. On en reparle plus loin dans la dépêche.

Le navigateur est encore considéré comme expérimental: plusieurs fonctions sont manquantes et il peut y avoir des plantages. WebPositive (le navigateur natif basé sur WebKit) reste donc le navigateur installé par défaut avec Haiku, mais les deux sont complémentaires. Par exemple, Iceweasel permet d’afficher les vidéos Youtube avec des performances acceptables.

Tracker

Tracker est le gestionnaire de fichiers de Haiku. Il implémente une interface « spatiale », c’est-à-dire que chaque dossier s’ouvre dans une fenêtre séparée et enregistre sa position à l’écran.

Le code du Tracker fait partie des composants qui ont pu être récupérés de BeOS. Cela signifie que certaines parties du code ont été développées il y a près de 30 ans, dans un contexte où l’élégance du code n’était pas la priorité (il fallait pour les développeurs de BeOS, d’une part livrer un système fonctionnel dans un temps raisonable, et d’autre part, fonctionner sur les machines relativement peu performantes de l’époque).

Les évolutions sur le Tracker nécessitent donc souvent du nettoyage dans de nombreuses parties du code, et provoquent souvent des régressions sur d’autres fonctionnalités. Toutefois, les choses s’améliorent petit à petit.

Ce trimestre, on a vu par exemple arriver la correction d’un problème avec l’utilisation de la touche « echap ». Cette touche peut servir à plusieurs choses:

Fermer une fenêtre de chargement ou d’enregistrement de fichier,
Annuler le renommage d’un fichier,
Annuler une recherche rapide « type ahead » qui consiste à taper quelques lettres et voir immédiatement la liste de fichiers du dossier courant se réduire à ceux qui contiennent cette chaîne de caractères.

Ces différentes utilisations peuvent entrer en conflit. Plus précisément, lorsqu’on utilise le filtrage « type ahead », puis qu’on change d’avis et qu’on appuie sur la touche « echap », il ne faut pas que cela ferme la fenêtre en même temps.

Un autre changement concerne plutôt la validation des données: Tracker interdit l’insertion de caractères de contrôle ASCII dans le nom de fichiers. Ce n’est pas strictement interdit (ni par Haiku, ni par ses systèmes de fichiers, ni par POSIX) en dehors de deux caractères spéciaux: le '/' et le 0 qui termine une chaîne de caractères. Mais, c’est très probablement une mauvaise idée d’avoir un retour à la ligne ou un autre caractère de contrôle enregistré dans un nom de fichier. Le Tracker interdit donc désormais de le faire et si vous êtes vraiment résolu à y parvenir, il faudra passer par le terminal.

Enfin, une nouvelle fonctionnalité dans le Tracker est la mise à jour en temps réel des menus pop-up. Cela peut se produire pour plusieurs raisons, par exemple, l’appui sur la touche « command » modifie le comportement de certains menus. Avant ce changement, il fallait ré-ouvrir le menu (command + clic droit) pour voir ces options modifiées. Maintenant, on peut d’abord ouvrir le menu, puis maintenir la touche command enfoncée pour voir les options modifiées.

Cela a nécessité une refonte complète de la gestion de ces menus (qui proposent de nombreuses autres choses comme la navigation « rayons X »). Au passage, certaines options qui étaient uniquement disponibles au travers de raccourcis claviers ou de la barre de menu des fenêtres du Tracker sont maintenant aussi affichées dans le menu pop-up.

TeamMonitor

TeamMonitor est le gestionnaire d’applications affiché quand on utilise la combinaison de touches Ctrl+Alt+Suppr. Il permet de stopper des programmes, de redémarrer la machine, et autres manipulations d’urgence si le système ne fonctionne pas comme il faut.

Les processus lancés par une même application sont maintenant regroupés et peuvent être tous arrêtés d’un seul coup. Ce changement est nécessaire suite à l’apparition de IceWeasel, qui crée beaucoup de processus en tâche de fond pour une seule instance du navigateur web.

HaikuDepot

HaikuDepot est l’interface graphique pour le système de paquets de Haiku. Il se présente comme un magasin d’applications, permettant non seulement d’installer et de désinstaller des logiciels, mais aussi de les évaluer avec une note et un commentaire.

Ajout d’un marqueur sur les icônes des paquets qui sont déjà installés, et remplacement du marqueur utilisé pour indiquer les applications « natives » (utilisant le toolkit graphique de Haiku, par opposition à Qt et GTK par exemple).
Affichage plus rapide de l’état « en attente d’installation » lorsqu’on demande l’installation d’un paquet.
L’interface pour noter un paquet est masquée si l’attribution de notes n’est pas possible.

Préférences

Diverses améliorations dans les fenêtres de préférences:

Correction d’un crash dans les préférences d’affichage (korli).
Les préférences de fond d’écran n’acceptent plus le glisser-déposer d’une couleur sur un contrôle de choix de couleur désactivé. La modification de la position X et Y de l’image de fond se met à jour en temps réel quand on édite la valeur des contrôles correspondants.
Ajout de réglages supplémentaires (vitesse, accélération, défilement) dans les préférences des pavés tactiles. Ces options étaient déjà implémentées dans l’input_server, mais configurable uniquement pour les souris.
Suppression de code mort et amélioration de la gestion des polices de caractères dans les préférences d’apparence.

Plusieurs améliorations sur les préférences de sons de notifications:

La fenêtre de sélection de fichiers retient le dernier dossier utilisé,
Elle permet également d’écouter un son avant de le sélectionner,
Les menus de sélection rapide de sons affichent uniquement les fichiers et pas les dossiers,
Certains sons ont été renommés.

La plupart des sons ne sont cependant toujours pas utilisés par le système.

Expander

Expander est un outil permettant d’extraire plusieurs types de fichiers archivés.

Peu de changement sur cet outil qui est assez simple et fonctionnel. La seule amélioration ce mois-ci concerne un changement des proportions de la fenêtre pour éviter un espace vide disgracieux.

Cortex

Cortex est une application permettant de visualiser et de manipuler les nœuds de traitement de données du Media Kit.

Le composant « logging consumer » qui reçoit des données d’un autre noeud et les enregistre dans un fichier de log pour analyse a été amélioré pour enregistrer un peu plus d’informations.

Icon-O-Matic

L’éditeur d’icônes vectoriels Icon-O-Matic évolue peu, après un projet Google Summer of Code qui a ajouté la plupart des fonctionnalités manquantes. Ce trimestre, un seul changement: l’ajout d’une entrée menu pour supprimer un « transformeur ».

PowerStatus

L’application PowerStatus affiche l’état de la batterie. Cela peut se présenter comme une icône dans la barre des tâches. L’icône est de taille réduite, et les différents états n’étaient pas forcément bien visibles. Ce problème a été corrigé avec des nouveaux marqueurs pour l’état de la batterie (en charge ou inactive).

StyledEdit

StyledEdit est un éditeur de texte simple, permettant tout de même de formater le texte (un peu comme WordPad pour Windows).

L’application reçoit une nouvelle option pour écrire du texte barré. Le code nécessaire a également été ajouté dans app_server, puisque cette possibilité était prévue, mais non implémentée.

WebPositive

Le navigateur WebPositive reçoit peu d’évolutions en ce moment, en dehors de la maintenance du moteur WebKit. On peut tout de même mentionner l’ajout d’un menu contextuel sur les marque-pages, permettant de les renommer et de les supprimer. Ce développement est issu d’un vieux patch réalisé par un candidat au Google Summer of Code, qui ne fonctionnait pas et n’avait jamais été finalisé.

Mode sombre et configuration des couleurs

Depuis la version Beta 5, Haiku dispose d’un nouveau système de configuration des couleurs, permettant d’obtenir facilement un affichage en « mode sombre ». Cependant, cet affichage est loin d’être parfait, et de petits ajustements sont à faire petit à petit dans toutes les applications qui n’avaient pas été pensées pour cela. En particulier, le changement de couleurs se fait en direct lorsqu’on change les réglages. On trouve ces trois derniers mois des changements dans DeskBar, Tracker, HaikuDepot, l’horloge, ainsi que la classe BTextView.

Outils en ligne de commande

pkgman peut rechercher les paquets installés et qui n’ont aucun autre paquet dépendant d’eux. Cela permet de trouver des paquets inutiles qui peuvent être désinstallés (il manque encore la possibilité de marquer un paquet comme étant « installé manuellement » avant de pouvoir automatiser le nettoyage).

La commande route accepte la syntaxe utilisée par openvpn pour la configuration d’une route par défaut, ce qui facilite l’utilisation de VPN avec Haiku.

Correction d’un problème dans le compilateur de ressources: la commande rc -d ne savait pas décompiler la structure app_version des applications Haiku, uniquement le format plus ancien utilisé par BeOS.

La commande screenmode permet maintenant de récupérer la valeur actuelle du réglage du rétro-éclairage (en plus de permettre de changer cette valeur).

Kits

La bibliothèque de fonctions de Haiku est découpée en « kits » qui regroupent un ensemble de classes et de fonctionnalités liées.

Application kit

L’Application Kit permet, comme son nom l’indique, de lancer des applications. Il offre également toutes les fonctionnalités de boucles d’évènements, et d’envoi de messages entre applications et entre composants d’une application.

Correction d’un problème de suppression d’un port dans la classe BApplication.

Debug kit

Le Debug Kit fournit les services nécessaires au Debugger pour débugger une application. Cela consiste d’une part en un accès privilégie à l’espace mémoire d’une application, et d’autre part en outils pour analyser les fichiers ELF des exécutables et bibliothèques.

Le Debug Kit reçoit ce trimestre plusieurs évolutions et corrections permettant le décodage des stack traces dans les programmes compilés avec clang et lld. Par exemple, les fichiers ELF générés par ces outils sont découpés en plusieurs segments, alors que ce n’est pas le cas pour gcc.

Device Kit

Le Device Kit regroupe tout ce qui concerne l’accès direct au matériel et aux entrées-sorties depuis l’espace utilisateur: ports série, accès direct aux périphériques USB, accès aux joysticks et manettes de jeu.

Les ports série RS232 peuvent être configurés avec des valeurs en baud personnalisées (pour l’instant uniquement pour les adaptateurs série USB).

Interface kit

L’Interface Kit regroupe tout ce qui concerne l’affichage de fenêtres et de vues à l’écran et les interactions avec ces fenêtres.

Ajout de constructeur « move » et d’opérateur d’assignation pour BRegion et BShape pour améliorer les performances en évitant les copie d’objet immédiatement suivies de suppression.
Ajout d’un constructeur pour BRect avec deux arguments (largeur et hauteur) pour les rectangles alignés en haut à gauche ou dont la position n’a pas d’importance.
Remise en place d’un cas particulier dans BBitmap::SetBits pour la gestion du canal alpha afin d’avoir un comportement plus proche de celui de BeOS.
BColorControl réagit correctement et déclenche les évènements nécessaires lorsqu’on modifie sa couleur par glisser-déposer.

Media Kit

Correction d’une assertion vérifiant la mauvaise condition dans BTimeSource.

Réécriture de la classe BTimedEventQueue pour améliorer ses performances en évitant d’allouer de la mémoire dynamique.

Amélioration de l’affichage des « media controls » (sliders de contrôle de volume par exemple) en mode sombre.

libshared

La « libshared » contient plusieurs classes expérimentales, en cours de développement, mais déjà utilisées par plusieurs applications. Il s’agit d’une bibliothèque statique, ce qui permet de changer facilement son contenu sans casser l’ABI des applications existantes.

Ajout de la classe ColorPreview qui existait en plusieurs exemplaires dans le code de Haiku (préférences d’apparence et Terminal). Cette classe permet d’afficher une couleur dans un petit rectangle. Elle est utilisée à plusieurs endroits dans des contrôles de choix de couleur plus complexes, tels que des listes ou des menus.

Servers

Les servers sont des processus systèmes implémentant différentes fonctionnalités de Haiku. Le concept est similaire à celui des daemons dans UNIX, ou des services dans Windows NT et systemd.

app_server

L’app_server s’occupe de l’affichage des applications à l’écran.

Suppression de code inutilisé depuis longtemps permettant l’accélération matérielle d’opérations de dessin en 2D (blit, tracé de lignes, remplissage de rectangles…).

Sur les cartes graphiques PCI, ces opérations étaient souvent réalisées plus rapidement par le CPU qui tourne à une fréquence bien plus rapide que la carte. Sur les cartes AGP, l’accès en lecture à la mémoire vidéo par le CPU est très lent, et il était donc plus intéressant de faire ces opérations en RAM centrale avant d’envoyer un buffer prêt à afficher à la carte graphique. Enfin sur les cartes PCI express modernes, ces fonctions d’accélération ont disparu ou en tout cas n’ont pas du tout une interface compatible avec les besoins de Haiku. Il est donc temps de jeter ce code.

Modification de la façon dont les applications récupèrent la palette de couleurs en mode graphique 256 couleurs: elle utilise maintenant une mémoire partagée, et il n’est plus nécessaire que chaque application demandent au serveur graphique d’en obtenir une copie.

input_server

L’input_server se charge des entrées souris et clavier. Cela comprend les méthodes d’entrée de texte (par exemple pour le Japonais) ainsi que des filtres permettant de manipuler et d’intercepter ces évènements d’entrée avant leur distribution dans les applications.

Améliorations du filtre PadBlocker pour bloquer le touchpad quand le clavier est en cours d’utilisation sur les PC portables: gestion des répétitions de touches, blocage uniquement du touchpad et pas des autres périphériques de pointage.

net_server

Le net_server se charge de la configuration des interfaces réseau.

Arrêt du client d’autoconfiguration (DHCP par exemple) lors de la perte du lien sur un port Ethernet, pour ne pas essayer d’envoyer des paquets alors que le câble est débranché.

notification_server

notification_server se charge de l’affichage de panneaux de notification pour divers évènements tels que la connexion et déconnexion d’interfaces réseau, un niveau dangereusement bas de la batterie, la fin d’un téléchargement…

La fenêtre de notification a été retravaillée pour mieux s’adapter à la taille de police d’affichage choisie par l’utilisateur.

mail_daemon

mail_daemon permet d’envoyer et de recevoir des e-mails. Les messages sont stockés sous forme de fichiers avec des attributs étendus pour les métadonnées (sujet, expéditeur…). Plusieurs applications clientes permettent de rédiger ou de lire ces fichiers. Ainsi chaque application n’a pas besoin de réimplémenter les protocoles IMAP ou SMTP.

Amélioration de la fenêtre de logs pour la compatibilité avec le mode sombre.

runtime_loader

Le runtime_loader est l’outil qui permet de démarrer un exécutable. Il se charge de trouver toutes les bibliothèques partagées nécessaires et de les placer dans la mémoire.

Ajout du flag PF_EXECUTE qui rend exécutable uniquement les sections ELF qui le nécessitent (auparavant, toutes les sections qui n’étaient pas accessibles en écriture étaient exécutables). Cela est utilisé en particulier par clang, qui sépare une zone en lecture seule (pour les constantes) et une autre en lecture et exécution (pour le code). Avec gcc, les deux sont habituellement regroupées dans la même section.

Drivers

Périphériques de stockage

Correction de bugs dans la couche SCSI (utilisée également pour d’autres périphériques de stockage qui encapsulent des commandes SCSI). Des drapeaux d’état n’étaient pas remis à 0 au bon moment, ce qui causait des kernel panic avec le message « no such range! ».

Cela a été l’occasion de faire du ménage : suppression de champs inutilisés dans des structures de données, et suppression du module d’allocation mémoire locked_pool qui n’était utilisé que par la pile SCSI. À la place, utilisation des fonctions d’allocation mémoire standard du noyau, qui sont amplement suffisantes pour répondre aux besoins de ce module (waddlesplash).

Cartes son

Correction d’erreurs dans le code de gestion mémoire des pilotes es1370 et auvia. Ces drivers utilisaient deux copies d’un code d’allocation identique, mais avaient divergé l’un de l’autre. Ils ont été réunifiés mais cela a provoqué quelques régressions, avec des difficultés pour trouver des machines permettant de tester chacune des cartes son concernées. Haiku peut heureusement compter sur des utilisateurs « avancés » qui testent régulièrement les nightly builds pour détecter ce type de régression (korli).

Réseau

Correction d’une fuite mémoire lors de l’utilisation de sockets « raw » permettant d’envoyer et de recevoir directement des paquets ethernet (en contournant la couche IP).

Pilotes FreeBSD

Une grande partie des pilotes de carte réseau de Haiku sont en fait ceux de FreeBSD ou d’OpenBSD. Une couche de compatibilité permet de réutiliser ces pilotes avec très peu de changement dans leur code source. Ainsi, les évolutions et corrections peuvent être partagées avec l’un ou l’autre de ces systèmes. La collaboration avec les *BSD pour les pilotes réseau se passe de mieux en mieux : suite au développement d’une couche de compatibilité permettant d’utiliser les pilotes OpenBSD dans Haiku, les développeurs de FreeBSD étudient la possibilité de réutiliser également ces pilotes. De plus, les développeurs de Haiku et d’OpenBSD sont en contact pour coordonner les mises à jour et les tests.

Génération de statistiques plus fiables sur les paquets réseaux dans la couche de compatibilité FreeBSD et remontée des statistiques générées par les pilotes associés.

Synchronisation du pilote realtekwifi avec la version de FreeBSD et reconnaissance d’un identifiant de périphérique USB supplémentaire dans ce pilote.

Amélioration de la couche de compatibilité pour se comporter plus précisément comme FreeBSD, et suppression de patchs correspondants dans les pilotes qui sont devenus superflus.

Amélioration des performances de la couche de compatibilité: retrait de comparaisons de chaînes de caractères et d’allocations inutiles.

Pilotes spécifiques à Haiku

Amélioration du comportement du pilote USB RNDIS (partage de connexion sur USB de certains téléphones Android) lorsque le câble USB est déconnecté. Le pilote incluait du code pour tenter de restaurer la connexion existante si le même appareil est reconnecté, mais les périphériques RNDIS utilisent des adresses MAC aléatoires qui changent à chaque connexion, donc cela ne pouvait pas fonctionner. De plus, certains transferts USB n’étaient pas correctement annulés pour laisser la pile USB dans un état propre après la déconnexion du périphérique.

USB

Ajout d’une annulation de transferts de données en attente dans le pilote pour les périphériques de stockage USB, ce qui corrige un kernel panic lors de l’utilisation de lecteurs de disquettes USB. Arrêt immédiat des opérations (au lieu de ré-essayer pendant quelques secondes) si le périphérique indique « no media present » (CD ou disquette éjectée de son lecteur par exemple).

Ajout d’une vérification de pointeur NULL et de libération de mémoire manquantes dans la pile USB, ce qui corrige des fuites de mémoires (qui étaient là depuis longtemps) et une assertion qui se déclenchait (introduite plus récemment).

Le pilote de webcam UVC est mis à jour pour utiliser des constantes (identifiants de types de descripteurs…) partagées avec le reste du système au lieu de toutes les redéfinir une deuxième fois. L’affichage des descripteurs dans listusb est également complété pour décoder toutes les informations disponibles. Le pilote n’est toujours pas complètement fonctionnel: l’établissement des transferts au niveau USB fonctionne, mais pour l’instant le pilote ne parvient pas à décoder les données vidéo reçues correctement.

Le pilote HID sait reconnaître les « feature reports », qui permettent de configurer un périphérique. Par exemple, cela peut permettre de configurer un touchpad en mode multi-point (dans lequel le système doit effectuer lui-même le suivi de chaque doigt sur la surface tactile pour convertir cela en mouvements de pointeur de souris) ou en mode émulation de souris (où on ne peut utiliser qu’un doigt à la fois, mais avec un pilote beaucoup plus simple).

Le pilote pour les tablettes Wacom reconnaît la tablette CTH-470.

PS/2

Les ports PS/2 ont disparu de la plupart des machines ces dernières années, mais le protocole reste utilisé pour le clavier des ordinateurs portables, ainsi que pour certains touchpads. Malheureusement, le protocole est seulement émulé au niveau de l’« embedded controller » (le microprocesseur qui se charge de l’interfaçage de divers composants annexes). Le résultat est que l’implémentation du protocole et des registres d’interface peut s’éloigner considérablement des documents officiels.

Amélioration de la détection des contrôleurs PS/2 supportant le protocole « active multiplexing » permettant de connecter à la fois une souris et un touchpad. La procédure de détection officielle peut générer des faux positifs: certains contrôleurs répondent bien à cette commande, mais n’implémentent en fait pas du tout le protocole. Cela provoquait un long délai au démarrage alors que le pilote tente d’énumérer des périphériques de pointage qui n’existent pas. Une vérification supplémentaire après l’activation du mode multiplexé permet de détecter ce cas.

virtio_pci

virtio est un standard matériel pour les machines virtuelles. Plutôt que d’émuler un vrai matériel (carte réseau, carte graphique…), une machine virtuelle peut émuler un matériel qui n’a jamais été fabriqué, mais dont la programmation est beaucoup plus simple. Cela permet également des opérations inimaginables sur du matériel réel, comme la possibilité de changer la taille de la RAM en cours d’exécution pour mieux partager la mémoire de l’hôte entre différentes machines virtuelles.

Le pilote virtio_pci est à la racine du système virtio. Il détecte la « carte PCI » virtio et implémente les primitives de base d’envoi et de réception de messages entre l’hôte et la machine virtualisée (du côté virtualisé, pour le côté hôte, c’est le virtualisateur, par exemple QEMU, qui s’en charge).

Correction de plusieurs problèmes avec les numéros de files virtio qui rendaient les pilotes instables.

ACPI

ACPI est un cadriciel pour la gestion de l’énergie et l’accès au matériel. Le fabricant du matériel fournit (dans la ROM du BIOS) un ensemble de « tables » contenant une description du matériel disponible, ainsi que des méthodes compilées en bytecode pour piloter ce matériel. Le système d’exploitation doit fournir un interpréteur pour ce bytecode, puis réaliser les entrées-sorties vers le matériel demandé lors de l’exécution.

Haiku utilise actuellement ACPICA, une bibliothèque ACPI développée principalement par Intel.

Correction d’un problème d’accès à de la mémoire non cachée. Une modification faite pour les machines ARM a déclenché un problème sur les machines x86.

Sondes de température

Ajout d’un nouveau pilote amd_thermal, ajout de ce dernier ainsi que des pilotes pch_thermal et acpi_thermal dans l’image disque par défaut. Ces pilotes devraient permettre de récupérer la température du processeur sur la plupart des machines. Il reste maintenant à intégrer cela dans les outils en espace utilisateur pour faire un bon usage de ces informations.

Pilotes graphiques

Ajout de deux nouvelles générations de cartes graphiques dans le pilote intel_extreme.

Le pilote VESA est capable de patcher le BIOS de certaines cartes graphiques à la volée pour y injecter des modes graphiques supplémentaires (la spécification VESA permettant à l’OS uniquement de choisir un mode parmi une liste fournie par la carte graphique, liste souvent assez peu fournie). Ce mode est désormais activé par défaut sur les cartes graphiques où il a pu être testé avec succès.

Systèmes de fichiers

FAT

FAT est un système de fichier développé par Microsoft et qui remonte aux premiers jours de MS-DOS. Il est encore utilisé sur certaines clés USB et cartes SD, bien que exFAT tend à le remplacer petit à petit. Il est également utilisé pour les partitions systèmes EFI.

Le pilote de Haiku a été récemment réécrit à partir de celui de FreeBSD. L’amélioration de ce nouveau pilote se poursuit, avec ce mois-ci :

Les noms de volumes FAT sont convertis en minuscules comme le faisait l’ancien pilote FAT,
Le cache de blocs implémente maintenant un mécanisme de prefetch pour récupérer plusieurs blocs disque d’un coup, et le pilote FAT utilise cette nouvelle possibilité pour améliorer en particulier le temps de montage,
Correction de problèmes dans le cache de fichiers si deux applications accèdent au même fichier mais avec des noms différents par la casse (le système de fichier ignorant ces différences).

BFS

BFS est le système de fichier principal de BeOS et de Haiku. Il se distingue des autres systèmes de fichiers par une gestion poussée des attributs étendus, avec en particulier la possibilité de les indexer et d’effectuer des requêtes pour trouver les fichiers correspondants à certains critères.

Clarification de la description des options disponibles lors de l’initialisation d’un volume BFS.

Correction des fonctions d’entrées/sorties asynchrones pour référencer correctement les inodes, ce qui corrige un très ancien rapport de bug. Des corrections similaires ont été faites également dans les pilotes FAT et EXFAT.

Correction des requêtes sur l’attribut « dernière modification », et amélioration de la gestion du type « time » pour éviter les conversions inutiles (ce type d’attribut est historiquement stocké en 32 bits mais migré en 64 bits lorsque c’est possible pour éviter le bug de l’an 2038, aussi le code doit être capable de traiter ces 2 formats de stockage).

packagefs

Le système de fichier packagefs est au centre de la gestion des paquets logiciels dans Haiku. Les paquets ne sont pas extraits sur le disque, mais montés dans un système de fichier spécifique (qui implémente une version tout-en-un de ce qui pourrait être réalisé sous Linux avec squashfs et overlayfs).

Ce système de fichier se trouve donc sur le chemin critique en termes de performances, ce qui fait que même de petites optimisations peuvent déboucher sur de gros gains de performance.

Optimisation de la gestion de la mémoire: utilisation d’un allocateur dédié pour allouer et désallouer très rapidement de la mémoire de travail avec une durée de vie courte.

Ajout d’une vérification manquante sur la présence du dossier parent, qui pouvait déclencher un kernel panic.

NFS4

Le pilote NFS4 permet de monter des partages réseau NFS. Cependant, le pilote ne fonctionne pas toujours, et certains utilisateurs doivent se rabattre sur le pilote NFS v2 (ancienne version du protocole de moins en moins utilisée), ou encore sur des systèmes de fichiers FUSE comme SMB ou sshfs.

Le pilote NFS4 peut maintenant être compilé avec userlandfs (équivalent de FUSE pour Haiku) pour s’exécuter en espace utilisateur. Cela facilitera le déboguage.

ramfs et ram_disk

ram_disk est un périphérique de stockage qui stocke les données en RAM, il a une taille fixe et doit être formaté avec un système de fichiers avant de pouvoir être utilisé.
ramfs est un système de fichier stockant les données directement en RAM sans passer par un périphérique de stockage de type bloc. Sa taille est dynamique en fonction des fichiers qui sont stockés dedans.

Ces deux pilotes ont reçu divers nettoyages et corrections, suite à des problèmes mis en évidence par des assertions ajoutées précédemment dans le code.

Dans le ramfs, nettoyage de code dupliqué, réduction de la contention sur les verrous, amélioration de la fonction readdir pour retourner plusieurs entrées d’un coup au lieu de les égréner une par une.

Ajout de la gestion des fichiers « spéciaux » (FIFOs nommés, sockets UNIX) dans ramfs.

Autres

Refonte de l’algorithme de « scoring » des requêtes sur les systèmes de fichiers. Cet algorithme permet d’estimer quels sont les termes de la requête les moins coûteux à évaluer, afin de réduire rapidement le nombre de fichiers répondant aux critères, et d’effectuer les opérations complexes seulement sur un petit nombre de fichiers restants. Les requêtes s’exécutent ainsi encore plus rapidement (waddlesplash).

Réécriture du code pour identifier les partitions dans mount_server. Ce code permet de re-monter les mêmes partitions après un redémarrage de la machine, mais l’ancien algorithme pouvait trouver de faux positifs et monter des partitions supplémentaires (OscarL et waddlesplash).

Correction d’une option de debug pour intercepter les accès aux adresses non initialisées (0xcccccccc) ou déjà libérées (0xdeadbeef). Cela permet de détecter certains accès à des pointeurs invalides. Cette option ne fonctionnait correctement que sur les systèmes 32 bit, maintenant, l’adresse correspondante pour les machines 64 bit est également protégée.

libroot

La libroot est la librairie C de base de Haiku. Elle regroupe les fonctions parfois implémentées dans les libc, libm, libpthread, librt et libdl pour d’autres systèmes. Haiku choisit une approche tout-en-un, car il est excessivement rare qu’une application n’ait pas besoin de toutes ces bibliothèques.

Du fait de la grande diversité des services rendus par cette bibliothèque, il est difficile de présenter les changements de façon cohérente et organisée.

Correction de quelques cas particuliers dans le traitement des tableaux de descripteurs de fichiers pour select() et déplacement d’une partie des définitions de sys/select.h vers des en-têtes privés non exposés aux applications (waddlesplash).

Ajout d’une fonction manquante dans les « stubs » de la libroot, qui sont utilisés lors de la compilation de Haiku en mode « bootstrap » (sans aucune dépendance précompilée externe). Les stubs sont normalement générés à l’aide d’un script, mais celui-ci n’avait pas pris en compte une fonction nécessaire seulement sur les architectures x86.

Poursuite du travail d’unification des fonctions de manipulation des temps d’attentes pour toutes les fonctions de la libroot qui peuvent déclencher un timeout. Correction d’un cas où la fonction pthread_testcancel retournait NULL au lieu de la valeur attendue PTHREAD_CANCELED.

Optimisation de la fonction strcmp, remplacement d’autres fonctions avec de meilleures implémentations provenant de la bibliothèque C musl.

Compatibilité POSIX-2024

La spécification POSIX Issue 8 a été publiée et comporte de nombreux changements. Après la version 7, la façon de travailler est devenue plus ouverte, avec un outil de suivi de bugs permettant de proposer des améliorations. Cela conduit à la standardisation de nombreuses extensions qui sont communes entre les systèmes GNU et BSD, rendant plus facile d’écrire du code portable entre tous les systèmes compatibles POSIX.

Ajout de fonctions qui ouvrent des descripteurs de fichiers avec le drapeau O_CLOEXEC activé par défaut (dup2, pipe3)
Ajout de reallocarray (un mélange de calloc et realloc)
Ajout de memmem (recherche d’une suite d’octets dans une zone de mémoire)
Ajout de mkostemp
Ajout de posix_devctl et modifications de l’implémentation de ioctl
Ajout de pthread_getcpuclockid pour mesurer le temps CPU consommé par un thread
Ajout de la constante d’erreur ESOCKTNOSUPPORT bien qu’elle ne soit jamais utilisée (cela facilite le portage d’applications qui attendent l’existence de ce code d’erreur)
Correction d’une boucle infinie dans pipe2
Suppression des fonctions *randr48_r des en-têtes publics. Il s’agit d’une extension disponible uniquement dans la glibc, et qui ne devrait donc pas être disponible dans la libroot. Cependant, l’implémentation est conservée pour assurer la compatibilité d’ABI avec les applications existantes.

ioctl et posix_devctl

La fonction ioctl existe depuis le début de UNIX et permet de réaliser des opérations spéciales sur les descripteurs de fichiers (tout ce qui n’est pas une simple lecture ou écriture). En particulier, elle est beaucoup utilisée pour les pilotes de périphériques qui exposent une interface sous forme de fichiers dans /dev.

L’existence de cette fonction était demandée dans la spécification POSIX, mais son fonctionnement n’était pas documenté à l’exception de quelques cas particuliers. La documentation spécifie une fonction avec un nombre d’arguments variable : un numéro de descripteur de fichier, un identifiant de l’opération à effectuer, puis des paramètres qui dépendent de l’opération. On trouve des opérations avec aucun, un, ou deux paramètres.

Dans UNIX et la plupart de ses dérivés, la liste des opérations possibles est définie à l’avance, et le format des numéros identifiants permet de déterminer de façon prédictible quel est le nombre de paramètres attendus. Ce n’est pas le cas dans Haiku : les pilotes de périphériques ont le choix d’assigner n’importe quelle valeur à n’importe quelle opération, et la même valeur numérique peut donc avoir une signification différente selon le type de fichier.

L’opération ioctl est donc en réalité implémentée avec toujours 4 arguments pour Haiku : en plus des deux déjà mentionnés, il faut ajouter un pointeur vers une zone de mémoire, et un entier indiquant la taille de cette zone. Des acrobaties à base de macros permettent de remplir ces deux paramètres avec des valeurs par défaut lorsqu’ils ne sont pas nécessaires (au moins pour les programmes écrits en C ; en C++, ces deux paramètres sont simplement déclarés avec une valeur par défaut).

Heureusement, ces problèmes avec ioctl vont être résolus, puisque POSIX a introduit une nouvelle fonction en remplacement : posix_devctl. Celle-ci fonctionne comme l’implémentation de ioctl dans Haiku, mais les arguments doivent toujours être spécifiés explicitement. Cela va donc permettre de disposer d’une interface réellement portable pour ces opérations.

Kernel

Correction de la taille du tampon mémoire par défaut de la classe KPath qui permet au noyau de manipuler des chemins dans le système de fichiers (waddlesplash).

VFS

Le VFS (virtual filesystem) est l’interface entre les appels systèmes d’accès aux fichiers (open, read, write…) et les systèmes de fichiers proprement dit. En plus de ce travail d’interfaçage (par exemple : convertir un chemin de fichier absolu en chemin relatif à un point de montage), cette couche regroupe un ensemble de fonctionnalités qui n’ont pas besoin d’être réimplémentées par chaque système de fichier: vérification des permissions, mémoire cache pour limiter les accès au disque.

Si les systèmes de fichiers identifient chaque objet par un inode (en général lié à la position de l’objet sur le disque ou dans la partition de stockage), le VFS travaille lui avec des vnode qui existent uniquement en RAM et sont alloués dynamiquement pour les fichiers en cours d’utilisation.

D’autre part, les systèmes de fichiers peuvent se reposer sur un cache de blocs. Ce dernier se trouve plutôt à l’interface entre un système de fichier et le support de stockage correspondant, puisqu’il fonctionne au niveau des blocs de données stockées sur disque. Mais son intégration avec le VFS est nécessaire pour savoir quels sont les fichiers en cours d’utilisation et les opérations prévisibles sur chacun (par exemple, il est utile de pré-charger la suite d’un fichier lorsque un programme demande à en lire le début, car il est probable que ces informations vont bientôt être nécessaires).

Le VFS est donc un élément central en particulier pour obtenir de bonnes performances sur les accès aux fichiers, en minimisant les accès aux vrais systèmes de fichiers qui doivent maintenir beaucoup d’informations à jour sur les disques. Tout ce qui peut être traité en utilisant uniquement la RAM grâce à la mise en cache est beaucoup plus rapide.

Investigation et amélioration des performances de la commande git status qui prenait beaucoup plus de temps à s’exécuter que sur d’autres systèmes (waddlesplash):

Meilleure gestion des vnodes inutilisés à l’aide d’une liste chaînée 'inline' protégée par un spinlock, à la place d’un mutex peu performant dans ce code très fréquemment appelé.
Modification de la structure io_context pour utiliser un verrou en lecture-écriture (permettant plusieurs accès concurrents en lecture, mais un seul en modification).
Ajout d’un chemin rapide dans le cas le plus simple de la recherche de vnode.

Avec ces changements, les performances sont améliorées au moins lorsque les données nécessaires sont déjà disponibles dans le cache disque.

Nettoyage et corrections dans les fonctions d’entrées-sorties vectorisées et asynchrones do_iterative_fd_io et do_fd_io utilisées par les systèmes de fichiers: meilleure gestion des références et prise en compte de certains cas particuliers. Cela permet de simplifier un peu le code de pré-remplissage du cache de blocs (waddlesplash).

La prise en compte des drapeaux O_RDONLY|O_TRUNC lors de l’ouverture d’un fichier est maintenant faite directement dans le VFS, il n’est plus nécessaire de transmettre la requête au système de fichier. Cette combinaison de drapeaux est un comportement indéfini dans POSIX, et supprime le contenu du fichier dans Linux. Dans Haiku, elle remonte une erreur.

Correction du comportement de l’ouverture d’un symlink invalide (ne pointant pas sur un fichier) avec le flag O_CREAT.

Le parser de requêtes pouvait essayer de lire des données invalides (la taille de clé d’un index inexistant) dans certains cas particuliers.

Nettoyage de logs dans tous les systèmes de fichiers qui affichaient un message lors de chaque tentative d’identification. On avait donc un message de chaque système de fichier pour chaque partition. Maintenant, le cas le plus courant (le système de fichier ne reconnaît pas du tout la partition) ne déclenche plus de logs.

Correction d’une erreur dans userlandfs sur la fonction file_cache_read pour les tentatives d’accès après la fin d’un fichier (cas particulier nécessaire pour implémenter correctement mmap).

Correction d’une mauvaise gestion du errno dans le cache de blocs, qui pouvait aboutir à un kernel panic.

Diverses améliorations, nettoyages et corrections de fuites mémoire: dans la gestion des fichiers montés comme image disques, dans les entrées-sorties asynchrones, dans l’enregistreur d’évènements scheduling recorder.

Console et affichage

Unification du code d’affichage du splash screen (par le bootloader) et des icônes de la séquence de démarrage (par le kernel) pour éviter qu’ils prennent des décisions différentes sur le positionnement (par exemple si l’un est compilé pour afficher le logo de Haiku, et l’autre en version « dégriffée » sans ce logo qui est une marque déposée) (waddlesplash).

Initialisation de la console framebuffer beaucoup plus tôt dans le démarrage du noyau, ce qui permet d’afficher un message à l’écran en cas de kernel panic y compris dans les premières étapes du démarrage (par exemple, l’initialisation de la mémoire virtuelle). Auparavant, ces informations étaient disponibles uniquement dans le syslog (inaccessible si le système ne démarre pas) ou via un port série (en voie de disparition sur les machines modernes) (waddlesplash).

Réseau

Remontée des données annexes (ancillary data) en une seule fois lorsque c’est possible. Ces données sont utilisées en particulier dans les sockets de domaine AF_UNIX pour permettre d’échanger des descripteurs de fichiers entre processus. Ce regroupement de données n’est pas exigé par la spécification POSIX, mais c’est le comportement attendu par le code de communication interprocessus de Firefox et de Chromium (ils utilisent tous les deux le même code) (waddlesplash).

Gestion de la mémoire

Comme indiqué plus haut dans la dépêche, l’apparition du navigateur Iceweasel a mis en évidence de nombreux problèmes autour de la gestion de la mémoire. Cela a donc été l’objet d’un gros travail de stabilisation et d’amélioration.

Le cache d’objets du noyau pouvait parfois ignorer le paramètre indiquant la réserve minimum d’objets devant toujours être disponibles (waddlesplash)
Amélioration de l’implémentation de la famille de fonctions autour de mprotect, qui permettent une gestion fine et bas niveau de la mémoire. En particulier, plusieurs problèmes se posaient lors de l’utilisation de ces fonctions lors d’un appel à fork, les deux processus se retrouvant dans un état incohérent,
Suppression de logs présents dans les méthodes de défaut de page, qui sont peu appelées pour les applications classiques, mais exploitées volontairement par d’autres applications (machines virtuelles Java ou Javascript par exemple). Les logs étaient donc superflus dans ce cas (waddlesplash),
Optimisation de l’écriture par lot de plusieurs pages de mémoire vers le swap,
Meilleure gestion des permissions d’accès page par page,
Correction de plusieurs problèmes conduisant à un blocage ou fort ralentissement du système quand il n’y a plus assez de mémoire libre,
Amélioration de la stratégie d’allocation de la table des descripteurs de fichiers,
Regroupement de code dupliqué pour chaque plateforme qui était en fait générique.

Ce travail se poursuit avec un remplacement de l’allocateur mémoire actuel, qui est basé sur hoard2. Cette implémentation est assez ancienne et montre aujourd’hui ses limites. Des essais sont en cours avec l’implémentation de malloc d’OpenBSD, ainsi qu’avec mimalloc de Microsoft, pour déterminer lequel des deux sera utilisé. D’autres allocateurs ont été rejetés, car ils ne répondent pas au besoin de Haiku, en particulier la possibilité de fonctionner efficacement sur un système 32 bits ou l’espace d’adressage est une ressource limitée.

Autres

Sécurisation des permissions sur les zones mémoire partagées: une application ne peut pas ajouter des permissions en écriture aux zones mémoire d’une autre application. Une application qui n’est pas lancée par l’utilisateur root ne peut pas inspecter la mémoire d’une application lancée par l’utilisateur root. Ajout toutefois de cas particuliers pour permettre au Debugger de faire son travail (il a besoin d’accéder à la mémoire d’autres applications).

Ajout et amélioration de commandes dans le debugger noyau pour investiguer l’état de l’ordonnanceur d’entrées-sorties, qui se charge de programmer les accès disque dans un ordre le plus efficace possible (waddlesplash).

La fonction vfork n’appelle plus les fonctions pre-fork. Haiku n’implémente pas complètement vfork, mais peut se permettre des optimisations sur le travail qu’un duo fork + exec classique demanderait normalement.

La configuration de la randomization de l’espace mémoire (ASLR) est maintenant faite par la libroot et pas par le noyau. Ainsi une application peut utiliser une version différente de la libroot pour avoir une politique de randomization différente.

Optimisation de l’accès par un thread à sa propre structure Thread

Chargeur de démarrage

L’écran de démarrage s’affiche correctement sur les systèmes EFI utilisant un mode écran avec une profondeur de couleur 16 bits (korli).

Affichage de la taille des partitions démarrables dans le menu de démarrage, pour faciliter leur identification (waddlesplash).

Activation des warnings du compilateur sur les chaînes printf invalides.

Augmentation de la zone de mémoire utilisée pour la décompression de l’archive de démarrage lors du boot sur le réseau, l’archive était devenue trop grosse suite à l’ajout de nouveaux pilotes.

Refactorisation du code de gestion de la mémoire entre le bootloader et le runtime_loader, ajout de tests pour cette implémentation, et optimisation de l’utilisation mémoire du bootloader.

Amélioration du comportement si le device tree définit un port série sans spécifier de baudrate: le bootloader suppose que le baudrate est déjà configuré, et utilise le port sans essayer de le réinitialiser.

Outils de compilation

La compilation de Haiku est un processus relativement complexe: il faut utiliser deux compilateurs pour Haiku lui-même (un gcc récent plus une version plus ancienne pour assurer la compatibilité avec BeOS) ainsi que un compilateur pour le systême hôte de la compilation (qui peut être Linux, BSD, Mac OS ou Windows) pour générer des outils nécessaires à la compilation elle-même. L’outil retenu est Jam, une alternative à Make avec une meilleure gestion des règles génériques réutilisables.

Ajout de vérification pour éviter d’avoir un build partiellement configuré, avec des ConfigVars définies mais vides.
Retrait d’un warning incorrect dans l’outil de build jam si on spécifie à la fois un profil et une cible de compilation sur la ligne de commande.
Reconnaissance des processeurs hôtes ARM et RISC-V pour la compilation croisée, correction d’autres problèmes avec les architectures non-x86.
Ajout de dépendances manquantes dans les règles de compilation de packagefs.
Suppression de fichiers de licence fournis avec Haiku mais concernant du code qui avait été supprimé de Haiku auparavant.
Amélioration de la remontée d’erreur du script configure si un interpréteur Python n’a pas été trouvé.
Correction de messages d’avertissement de awk pour l’utilisation de fonctions qui n’existent plus dans le traitement des fichiers d’identifiants matériels USB et PCI.

Documentation

Documentation interne

Ajout de documentation sur les détails d’implémentation de ioctl et posix_devctl et les spécificités de Haiku pour la première (PulkoMandy).

Correction de fautes de frappe dans l’introduction au launch_daemon.

Remplacement de toutes les références à "OpenBeOS" par "Haiku".

Documentation d’API

Ajout de documentation pour les méthodes GetFontAndColor et SetFontAndColor de BTextView.

Ajout de documentation pour les classes BShelf et BGameSound.

Réorganisation de la liste des caractères de contrôles dans la documentation du clavier, ajout d’entrées manquantes dans cette liste et ajoute de commentaires indiquant à quelles combinaisons de touches ces caractères sont normalement associés.

Traductions de Haiku

La traduction du système dans différentes langues est un facteur important d’inclusivité et d’accessibilité (même si la communication avec l’équipe de développeurs pour le support n’est pas toujours simple).

Haiku est disponible dans 30 langues, la trentième étant le coréen, pour lequel il y a un nouveau responsable des traductions (le précédent avait cessé toute activité et laissé la traduction inachevée).

Haiku recherche des volontaires pour s’occuper des traductions en biélorusse, croate, bulgare, hindi, punjabi et slovène, pour lesquelles les précédents responsables de relectures n’ont plus le temps d’assurer le rôle. Ainsi bien sûr que de l’aide pour la traduction du système, du manuel d’utilisation, et des applications tierces, que ce soit pour ajouter de nouvelles langues ou pour renforcer les équipes s’occupant de langues existantes. Le point d’entrée est le portail d’internationalisation de Haiku.

La traduction du système Haiku s’effectue avec Pootle. L’outil n’est plus développé et des investigations sont en cours pour le remplacer par Weblate. La traduction du manuel d’utilisation s’effectue avec [un outil spécifiquement développé pour cela](https://github.com/haiku/userguide-translator. La traduction des applications s’effectue également avec un outil personnalisé nommé Polyglot.

Télécharger ce contenu au format EPUB

Commentaires : voir le flux Atom ouvrir dans le navigateur

GIMP 3.0 RC2 est sorti

LinuxFr.org : les dépêches

Par :Jona · Jehan · BAud · Benoît Sibaud · Florent Zara · cli345 · Julien Jorge

8 janvier 2025 à 15:12

Note : cette dépêche est une traduction de l'annonce officielle de la sortie de GIMP 3.0 RC2 du 27 décembre 2024 (en anglais).

Après la première série de retours de la communauté, nous sommes heureux de partager la deuxième version candidate de GIMP 3.0 ! Les gens nous ont donné des commentaires très utiles sur la première version candidate et nous avons pu corriger de nombreux bugs.

C’est notre petit cadeau sous le sapin 🎄 pour vous tous ! (NdM: disons fourré dans la galette/le gâteau des rois désormais ?)

GIMP 3.0 RC2: écran de démarrage

Écran de démarrage de la nouvelle version candidate, par Sevenix (CC by-sa 4.0) - GIMP 3.0 RC2

lien nᵒ 1 : Annonce officielle de la sortie de GIMP 3.0 RC2 du 27 décembre 2024
lien nᵒ 2 : GIMP 3.0 RC1 est sorti (LinuxFr.org)

Sommaire

Corrections de bugs importantes

Plusieurs correctifs ont été apportés depuis la version RC1. Nous souhaitons mettre en évidence les bugs les plus importants afin que les utilisateurs en soient informés et puissent effectuer des tests supplémentaires. Pour plus de détails sur les autres correctifs de bugs, veuillez consulter notre page NEWS sur GitLab.

Migration des paramètres de la 2.10

Lors des tests communautaires, nous avons découvert que les paramètres des utilisateurs de la 2.10 n’étaient pas migrés vers GIMP 3.0 en raison de certaines hypothèses incorrectes dans le code d’importation. Étant donné que la plupart des développeurs utilisent exclusivement GIMP 3.0 depuis un certain temps, nous n’avions pas remarqué ce problème. Le bug devrait maintenant être corrigé, nous demandons donc des rapports de bugs si des préférences 2.10 ne sont pas importées correctement dans RC2. Notez que si vous avez déjà utilisé 3.0 RC1, vous devrez d’abord supprimer ces configurations, sinon RC2 n’essaiera pas d’importer les préférences 2.10 (assurez-vous de sauvegarder vos paramètres bien sûr !).

Console Windows

Dans les versions de développement 2.99, les versions Windows lançaient automatiquement un affichage de console en plus de GIMP lui-même. C’est très utile pour les développeurs Windows pour voir les messages de débogage, mais la console n’était pas destinée à être affichée pendant les versions stables. Comme nous avons modifié notre processus de construction pour utiliser Meson au lieu d’Autotools, nous avons appris que nous devions apporter des modifications supplémentaires pour empêcher l’affichage de la console. Cela devrait être corrigé maintenant grâce à Jehan - si vous voyez toujours la console sous Windows, veuillez remplir un nouveau rapport de bogue !

Problèmes de polices d’interface utilisateur manquantes sur macOS

Il y a un problème de longue date où certains utilisateurs de macOS ne voyaient que des symboles « Unicode manquants » au lieu des textes d’interface dans GIMP (à la fois dans la version 2.10 et dans la version 3.0). Cela était dû à un bug dans Pango, la bibliothèque que nous utilisons pour les mises en page de texte. Ce problème a été résolu avec la récente version Pango 1.55.0, nous encourageons donc tous les empaqueteurs macOS tiers à mettre à jour vers cette version lorsqu’ils construisent GIMP pour le distribuer.

GIMP 3.0.0 RC2 : le package officiel de macOS contient désormais Pango sans polices cassées

Si vous aviez ce problème de polices cassées sur macOS (à gauche), il est désormais résolu (à droite) - captures d’écran de rapporteurs de bug - GIMP 3.0.0 RC2

Intégration de darktable

Après la sortie de la version 3.0 RC1, nous avons reçu des rapports de certains utilisateurs indiquant qu’ils ne pouvaient toujours pas importer et exporter d’images entre GIMP et darktable. Nous avons travaillé avec les développeurs de darktable pour éliminer les bugs restants, de sorte que l’intégration entre darktable 5.0.0 et GIMP 3.0 RC2 devrait désormais fonctionner pour tout le monde. Cependant, veuillez déposer un nouveau rapport de bogue si vous continuez à rencontrer des problèmes pour connecter les deux !

Améliorations

Bien que l’objectif principal du développement de la version 3.0 RC2 ait été la correction de bugs et le peaufinage, certaines nouvelles fonctionnalités ont également été implémentées.

API de filtre GEGL

De nombreux anciens wrappers d’API pour les opérations GEGL ont été supprimés dans la version RC1. Bien que cela ait réduit la dette technique, cela a également causé des problèmes à de nombreux développeurs de greffons et de scripts tiers qui souhaitaient porter leurs greffons vers la version 3.0. Alors que notre plan initial était d’implémenter la nouvelle API publique de filtre après la sortie de la version 3.0, les commentaires de la communauté nous ont convaincu de l’ajouter pour la version 3.0 RC2.

Application de filtres via l’API libgimp 3.0.0 (Script-fu et al.) - GIMP 3.0.0 RC2

Le travail de Jehan permet aux développeurs d’appliquer des effets de filtre soit immédiatement, soit de manière non destructrice. Vous pouvez voir des exemples de la manière de procéder en C, Python et Script-Fu dans la requête de fusion, ou en recherchant gimp-drawable-filter dans le navigateur de procédures de GIMP. Nous avons également commencé à utiliser l’API de filtre dans nos scripts Python pour créer automatiquement des effets d’arrière-plan flou pour le programme d’installation Windows, et avec cette même API en C, Alx Sa a ajouté la prise en charge de l’importation de l’ancien style de calque Color Overlay de Photoshop.

Nous sommes preneurs des retours et des rapports de bugs d’auteurs de greffons et de scripts qui utilisent la nouvelle API de filtrage dans leur travail ! Nous avons également prévu d’autres mises à jour pour GIMP 3.0.

Espaces de fusion de calques et composition dans les fichiers XCF

Les discussions entre les experts en science des couleurs Elle Stone et Øyvind Kolås ont révélé un autre domaine nécessitant des améliorations dans le cadre de notre projet Color Space Invasion. Plus précisément, les images avec des profils de couleurs qui ont des courbes de reproduction des tons non perceptives peuvent ne pas être rendues correctement lorsqu’elles sont définies sur certains modes de calque.

Øyvind a implémenté une correction pour ce problème en ajoutant un espace perceptuel approprié par défaut à des modes de calque spécifiques. Bien que nous pensions que cette amélioration ne devrait pas avoir d’impact sur les fichiers XCF plus anciens, n’hésitez pas à rapporter tous problèmes de compatibilité avec la version 3.0 RC2 !

Paquets

AppImage

Grâce aux efforts continus de Bruno Lopes et avec l’aide de Samueru et de la communauté AppImage, notre AppImage expérimentale fonctionne désormais sur la plupart des distributions Linux. Nous souhaitons encourager davantage de tests, dans l’espoir de pouvoir la proposer comme une autre version Linux en plus de notre Flatpak. Vous pouvez consulter les instructions pour installer les paquets expérimentaux AppImage sur notre page de téléchargement des versions de développement.

Flatpak

Notre flatpak journalier a maintenant un App-ID dédié org.gimp.GIMP.Nightly. Cela signifie principalement qu’il peut être installé côte à côte avec le flatpak stable tandis que les deux sont visibles dans vos menus (plus besoin de sélectionner quelle version doit être affichée avec flatpak make-current).

Mais cela signifie également que tous ceux qui avaient le flatpak journalier jusqu’à présent ne verront pas de mise à jour arriver de sitôt. Afin de continuer à utiliser le flatpak journalier, désinstallez celui existant et installez le nouveau avec ces commandes :

flatpak uninstall org.gimp.GIMP//master
flatpak install https://nightly.gnome.org/repo/appstream/org.gimp.GIMP.Nightly.flatpakref

⚠️ Rappel : le flatpak journalier contient le code de développement actuel tel qu’il se présente dans le dépôt source. Parfois, il peut même être très cassé ou rendre vos fichiers de projet invalides. Nous ne le recommandons pas pour la production ! Utilisez cette version pour nous aider à déboguer en signalant les problèmes ou si vous aimez vraiment les risques pour tester les dernières fonctionnalités.

Améliorations du greffon BMP

Le nouveau contributeur Rupert Weber a été très occupé depuis la dernière mise à jour avec de nouvelles mises à jour de notre greffon BMP. Quelques points de son travail à mettre en avant :

Les fichiers BMP sont désormais importés sans perte dans leur précision d’origine, plutôt que d’être convertis en précision entière de 8 bits.
Le greffon prend désormais en charge le chargement de fichiers BMP avec compression RLE24 et Huffman.
Nous chargeons désormais les fichiers BMP par morceaux plutôt que d’essayer de charger l’image entière en une seule fois. Des travaux connexes nous permettent également de charger des fichiers BMP beaucoup plus volumineux.
Rupert a également effectué beaucoup de nettoyage et de maintenance du code, afin de rendre le greffon plus facile à maintenir à l’avenir.

Mises à jour diverses

Jehan a apporté quelques améliorations d’usage de la console Python. Vous pouvez désormais utiliser les raccourcis Ctrl+R et Ctrl+S pour parcourir votre historique de commandes, et Page précédente et Page suivante vous permettent désormais de faire défiler l’historique en plus des touches fléchées Haut et Bas.

Recherche dans l’historique de commande (console Python) - GIMP 3.0.0 RC2

Alx Sa a implémenté le chargement des fichiers CMJN PAM dans le greffon PNM.
Sous Windows, nous avons également ajouté la possibilité d’ouvrir des images via des raccourcis Windows (fichiers .lnk) directement depuis la boîte de dialogue de sélection de fichiers. Ce travail est également réalisé par Alx Sa.
D’autres modifications et améliorations ont été apportées au thème. En particulier, le style du « curseur compact » a été considérablement amélioré après les commentaires et le travail de Denis Rangelov. Denis a également créé de nouvelles icônes pour la boîte de dialogue de navigation ancrable, remplaçant les doublons par des symboles distincts. Anders Jonsson a également révisé le thème et supprimé certaines solutions de contournement qui étaient nécessaires dans GIMP 2.10, mais qui ne sont plus nécessaires avec nos nouveaux thèmes 3.0.
Idriss Fekir a apporté des améliorations à notre code de chargement de polices XCF, pour améliorer la compatibilité lors de l’importation d’anciens fichiers XCF.

Aperçu des changements depuis la version 2.10

Pour ceux qui n’ont pas suivi de près le développement de GIMP, cet article ne couvre que les changements progressifs depuis la dernière version. Ils ne répertorient pas tous les changements ou améliorations apportés à GIMP 3.0 - ce serait un article très long !

Bien que nous aurons des notes de version complètes pour la version finale 3.0, nous avons pensé qu’il serait utile de résumer quelques-uns des changements majeurs apportés au cours du processus de développement de la version 2.99 :

GEGL

Tout comme pour GIMP, la version 0.4.52 de GEGL a été corrigée. Øyvind Kolås a corrigé certaines étiquettes génériques « Entrée auxiliaire » pour qu’elles soient plus significatives. Elles seront également visibles dans les filtres de GIMP. Il a également amélioré la précision du traitement des couleurs de certains filtres. Thomas Manni, contributeur de longue date, a également corrigé les plantages lorsque certains filtres étaient exécutés sur de très petits calques.

Statistiques de sortie

Depuis GIMP 3.0 RC1, dans le dépôt principal de GIMP :

73 rapports ont été fermés comme CORRIGÉS.
71 demandes de fusion ont été acceptées.
277 commits ont été poussés.
18 traductions ont été mises à jour : bulgare, catalan, chinois (Chine), chinois (Taïwan), danois, finnois, géorgien, islandais, italien, letton, lituanien, norvégien nynorsk, persan, portugais, russe, slovène, suédois, ukrainien.

35 personnes ont contribué à des modifications ou des correctifs à la base de code de GIMP 3.0.0 RC2 (l’ordre est déterminé par le nombre de commits ; certaines personnes sont dans plusieurs groupes) :

12 développeurs pour le code principal : Jehan, Alx Sa, Michael Schumacher, Anders Jonsson, Lloyd Konneker, Øyvind Kolås, Idriss Fekir, Andre Klapper, Jacob Boerema, Michael Natterer, Rupert Weber, Thomas Manni.
11 développeurs de plug-ins ou modules : Jehan, Lloyd Konneker, Alx Sa, Rupert Weber, Daniel Novomeský, Jacob Boerema, Aki, Bruno, Ryan Sims, Simon Munton.
19 traducteurs : Alan Mortensen, Cheng-Chia Tseng, Kolbjørn Stuestøl, Rūdolfs Mazurs, Jiri Grönroos, Sveinn í Felli, Alexander Shopov, Aurimas Černius, Marco Ciampa, Danial Behzadi, Hugo Carvalho, Jordi Mas, Anders Jonsson, Ekaterine Papava, Julia Dronova, Luming Zh, Martin, Michael Schumacher, Youri Chornoivan.
2 concepteurs de thèmes : Alx Sa, Anders Jonnson.
2 contributeurs à la documentation : Jehan, Bruno.
5 contributeurs pour la compilation, l’empaquetage ou l’intégration continue : Bruno, Jehan, Lloyd Konneker, Alx Sa, Jacob Boerema, Rupert Weber.

Contributions sur d’autres dépôts du GIMPverse (l’ordre est déterminé par le nombre de commits) :

GEGL 0.4.52 est composé de 31 commits de 16 contributeurs : Øyvind Kolås, Sam L, Thomas Manni, lillolollo, Alan Mortensen, Anders Jonsson, Ekaterine Papava, Hugo Carvalho, Jordi Mas, Juliano de Souza Camargo, Kolbjørn Stuestøl, Lukas Oberhuber, Luming Zh, Marco Ciampa, Martin, Yuri Chornoivan.
ctx a enregistré 48 commits depuis la sortie de la RC1 par 1 contributeur : Øyvind Kolås.
gimp-data a enregistré 6 commits de 5 contributeurs : Anders Jonsson, Jehan, Sevenix, Alx Sa et Denis Rangelov.
gimp-test-images (nouveau référentiel pour les tests de prise en charge des images) a enregistré 2 commits de 1 contributeur : Rupert.
La version gimp-macos-build (scripts d’empaquetage pour macOS) a reçu 5 commits de 1 contributeur : Lukas Oberhuber.
La version flatpak a reçu 4 commits de 2 contributeurs : Bruno Lopes, Jehan.
Notre site Web principal a reçu 29 commits de 3 contributeurs : Jehan, Alx Sa, Andrea Veri.
Notre site Web de développement a reçu 16 commits de 2 contributeurs : Jehan, Bruno Lopes.
Notre documentation pour GIMP 3.0 a reçu 157 commits de 10 contributeurs : Andre Klapper, Kolbjørn Stuestøl, Jacob Boerema, Alan Mortensen, Anders Jonsson, Marco Ciampa, Jordi Mas, Yuri Chornoivan, Alx Sa, Jiri Grönroos.

N’oublions pas de remercier toutes les personnes qui nous aident à trier dans Gitlab, à signaler les bugs et à discuter des améliorations possibles avec nous. Notre communauté est également profondément reconnaissante envers les guerriers d’Internet qui gèrent nos différents canaux de discussion ou comptes de réseaux sociaux tels que Ville Pätsi, Liam Quin, Michael Schumacher et Sevenix !

Remarque : compte tenu du nombre de parties dans GIMP et de la façon dont nous obtenons des statistiques via les scripts git, des erreurs peuvent se glisser dans ces statistiques. N’hésitez pas à nous dire si nous avons oublié ou mal classé certains contributeurs ou contributions.

Autour de GIMP

Miroirs de téléchargement

GNOME a abandonné l’utilisation de miroirs lors de sa dernière mise à jour d’infrastructure. Comme nos miroirs de téléchargement sont hébergés par eux, on nous a demandé si nous voulions également faire la même chose. En tant que projet communautaire, nous apprécions tous ceux qui contribuent un miroir pour rendre GIMP plus accessible dans leur région. Par conséquent, nous avons décidé de continuer à utiliser des miroirs pour distribuer GIMP.

Si vous souhaiter contribuer à un miroir pour votre région, voici la nouvelle procédure :

Comment devenir un miroir officiel (mise à jour de la procédure)

Créez une demande de miroir sur le tracker gimp-web
Dites-nous pourquoi vous souhaitez créer un miroir de GIMP, pour quels autres logiciels libres vous en contribuez déjà un, quelle est votre configuration, l’emplacement du serveur…
Parlez-nous de vous : êtes-vous une organisation ou un particulier ? Donnez-nous le nom et l’URL spécifiques à afficher dans la liste des sponsors de miroir.
Une fois que nous aurons terminé de vérifier votre organisation, les identifiants rsync seront échangés de manière sécurisée, vous permettant de synchroniser votre miroir avec le serveur source
Il n’y a rien de particulier à faire pour apparaître sur la page des sponsors qui sera mise à jour régulièrement via des scripts. Pourtant, cela peut prendre quelques jours, voire quelques semaines parfois. Ne vous inquiétez donc pas si le nom de votre organisation n’apparaît pas immédiatement !

🛈 Nous vérifions automatiquement à intervalles aléatoires que les miroirs sont mis à jour suffisamment rapidement et que les données correspondent pour des raisons de sécurité évidentes.

Changements dans les miroirs

De plus, depuis la publication de la nouvelle 3.0RC1, un nouveau miroir a été ajouté :

Sahil Dhiman, Mumbai, Inde

Les miroirs sont importants, car ils aident le projet en répartissant la charge des dizaines de milliers de téléchargements quotidiens. De plus, en ayant des miroirs répartis dans le monde entier, nous garantissons que tout le monde peut avoir un accès rapide au téléchargement de GIMP.

Financer des exécuteurs ("runner") GitLab

Le dépôt de code de GIMP est également hébergé sur la plateforme GitLab de GNOME. Andrea Veri a demandé si nous pouvions financer un exécuteur [NDA: un "runner" est une sorte de serveur dédié à la compilation ou à l’intégration continue de manière générale] sur la plateforme, ce qui permet à tout projet sur la plateforme de tester la construction de son logiciel avant, pendant et après les modifications de code. Après un vote du comité de GIMP, nous avons accepté et sommes désormais les sponsors d’un exécuteur CI/CD x86 !

Télécharger GIMP 3.0 RC2

Vous trouverez toutes nos versions officielles sur le site officiel de GIMP (gimp.org) :

Paquets Linux flatpaks pour x86 et ARM (64 bits)
Installateur Windows universel pour x86 (32 et 64 bits) et pour ARM (64 bits)
Paquet MSIX (aperçu GIMP) pour x86 et ARM (64 bits)
Paquets macOS DMG pour le matériel Intel
Paquets macOS DMG pour le matériel Apple Silicon

D’autres paquets réalisés par des tiers devraient évidemment suivre (paquets de distributions Linux ou *BSD, etc.).

🛈 Notes:

Les 2 paquets DMG macOS seront probablement en retard, car nous attendons la validation de la mise à jour Apple par la Fondation GNOME avant de pouvoir signer nos paquets.
Le paquet MSIX prend généralement quelques jours ouvrables de validation par Microsoft. (le paquet MSIX est disponible)

Et ensuite ?

Grâce au grand nombre de retours que nous avons reçus pour notre premier candidat à la version finale, nous sommes en mesure de vous présenter cette deuxième version qui en est d’autant plus robuste. Comme vous l’avez vu, quelques surprises supplémentaires 🎁 sont arrivées avec les corrections de bugs, notamment la nouvelle API de filtre, qui a déclenché la prise en charge de l’importation de l’ancien effet Color Overlay de PSD, des modes de fusion et de composition améliorés, et plus encore. Nous avons pensé que cela valait la peine de rompre le gel des fonctionnalités pour ces changements et que cela fera toute la différence !

Avec cette deuxième version candidate, nous sommes plus proches que jamais de la version 3.0.0 de GIMP. Comme d’habitude, nous attendons avec impatience les nouveaux rapports de problèmes de la communauté qui nous permettront de finaliser la version 3.0.0 ! 🤗

N’oubliez pas que vous pouvez faire un don et financer personnellement les développeurs de GIMP, afin de donner en retour et d’accélérer le développement de GIMP. L’engagement de la communauté aide le projet à se renforcer ! 💪🥳

🎅🎄🎉 Et bien sûr, toute l’équipe vous souhaite de ~~joyeuses fêtes de fin d’année~~ (MAJ de Jehan) nos meilleurs vœux pour la nouvelle année ! 🥳🥂🎆

Télécharger ce contenu au format EPUB

Commentaires : voir le flux Atom ouvrir dans le navigateur