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.
Cette dépêche est la deuxième d’une série de quatre sur le packaging en Python :
Je vais donc proposer un aperçu plus ou moins complet des différents outils, et de ce qu’ils font ou ne font pas, en essayant de les comparer. Mais je parlerai aussi des fichiers de configuration, des dépôts où les paquets sont publiés, des manières d’installer Python lui-même, et de l’interaction de tout ceci avec les distributions Linux. En revanche, je laisse de côté pour l’instant les paquets écrits en C, C++ ou Rust et la complexité qu’ils apportent.
Quelques dépêches précédentes ont parlé des outils de packaging Python, comme ici, là ou encore là. Je vais chercher à faire un tour complet de la question, non seulement du point de vue de l’utilisateur qui cherche à comprendre quelle est « la bonne » solution (← ha ha ha rire moqueur…), mais aussi en expliquant les choix qui ont été faits, les évolutions, la structure de la communauté autour des outils, et les critiques qui leur sont souvent adressées, à tort ou à raison.