L'assistant de preuve Coq, deux fois primé l'année dernière, vient de sortir en version 8.5 bêta. Attendue depuis plus d'un an déjà, on trouvera au menu de cette version un nombre certain de changements en profondeur.

Coq est un assistant de preuve sous licence LGPL 2.1, développé entre autres à l'INRIA. Issu des travaux sur la correspondance de Curry-Howard, Coq peut être vu aussi bien comme un langage de programmation que comme un système de preuves mathématiques. Il est, de fait, employé par les deux communautés. Parmi les développements en Coq, on peut citer par exemple le compilateur C certifié CompCert sur le versant informatique et la preuve du Théorème de Feit et Thompson sur le versant mathématique. Plus récemment, une des failles d'OpenSSL a été découverte grâce à Coq[^0] . Il est aussi de plus en plus utilisé comme système interactif pour l'apprentissage de la logique dans l'enseignement supérieur.

On rappellera dans le reste de la dépêche les grands principes qui sous-tendent Coq, ce qu'il est, ce qu'il n'est pas, puis on détaillera les changements introduits dans cette version.

Le récent problème d'OpenSSL et de ses failles peut nous avoir rendu dubitatifs quant à la supposée meilleure qualité des logiciels libres.

Cette dépêche se veut un petit rappel sur ce qui impacte la qualité d'un programme informatique, et de ce que l'on peut en déduire pour la communauté libre, et open source.

Il y a plus de 10 ans maintenant, en lisant le journal d'un certain mmh, je découvrais la Méthode R.A.C.H.E de l’International Institute of La RACHE. Il ne s'est pas passé une année depuis sans qu'un collègue ou moi-même y fasse allusion face à un projet à l'issue incertaine. Malheureusement, le domaine n'a pas été renouvelé en 2013 par le propriétaire, et un site parking plein de liens moisis y a pris place.

Malgré la déception, j'ai finalement réussi à racheter le domaine et à le remettre en route…

Lorsque l'on travaille sur un projet C comportant un certain nombre de fichiers et de lignes de code, il arrive fréquemment que l'on se pose des questions comme "Mais où est modifié le champ data de ma structure Packet ?". grep ne suffit pas pour répondre à ce genre de questions car ne comprenant pas C, il ne sait pas, par exemple, que la variable monbopkt est une structure Packet.

coccigrep, basé sur coccinelle qui est un outil très puissant de recherche et de modification automatique de code, est un logiciel libre chargé de répondre à ce genre de questions. Il vient d'être publié en version 1.0rc1, sous licence GPL v3. Il est écrit en Python et s'interface avec les éditeurs Vim et Emacs, ce qui permet de faire les recherches depuis l'éditeur.

Stefano Zacchiroli (Zack) a été élu Responsable du Projet Debian en avril dernier. Il est actuellement en post-doctorat au laboratoire "Preuves, Programmes et Systèmes" de l'université Paris 7 (où travaille également Roberto Di Cosmo). Son travail s'inscrit au sein du projet européen de recherche Mancoosi qui vise à améliorer les gestionnaires de paquets des distributions.

Au sein de Debian, Zack s'occupe des paquets liés au langage de programmation OCaml et il est aussi très impliqué dans tout ce qui touche l'assurance qualité. En septembre 2009, il a également lancé l'initiative "Release Critical Bugs of the Week" qui se propose de corriger chaque semaine des bugs bloquants du projet Debian.

En lisant ce qui précède, on comprend que Zack est quelqu'un de très occupé. Pour ajouter à son fardeau, j'ai essayé de collecter les questions se trouvant dans la proposition d'entretien initiée par Florent, j'en ai ajouté quelques-unes et j'ai envoyé le tout par mail. Il a eu la gentillesse d'accepter de répondre à cet entretien pour les lecteurs de LinuxFr. Qu'il en soit chaudement remercié.

Je vous propose dans cette dépêche de revenir sur la panoplie d'outils de construction qui s'offre à nous (c'est à dire les outils permettant d'automatiser les étapes de préprocessing, compilation, éditions des liens, etc).
Je ne cherche pas à faire un comparatif, mais juste à les décrire pour en faire ressortir les avantages et inconvénients ainsi que les cas d'utilisation. Cette dépêche peut être vue comme un état de l'art allégé des outils de construction libres.

Je tiens à remercier les contributeurs de cette dépêche :

• GeneralZod
• tiennou
• NedFlanders
• claudex

Ce sont eux qui ont écrit la majeure partie de cette dépêche et qui l'ont améliorée et complétée grâce à leurs connaissances et au temps qu'ils y ont consacré.

Cette dépêche a pour objectif de faire découvrir ou redécouvrir des outils de constructions. Si vous en connaissez d'autres n'hésitez pas à en parler en commentaire.

Doxygen est un générateur de documentation à partir du code source de différents langages. Il est disponible pour les langages suivants : C, C++, C#, Fortran, Java, Objective-C, PHP, Python, IDL, VHDL, TCL et D. Les formats de sorties sont : HTML, LaTeX, RTF, PostScript, PDF (avec les hyperliens), HTML compressé et les pages de manuel Unix.

La liste des utilisateurs est grande, on retrouve KDE, Drupal, DotClear, LLVM, OpenTTD…

Doxygen est compatible avec les conventions de JavaDoc et celles de Qt. Il permet aussi de générer des graphes d’utilisation et d’héritage. Il s’utilise de la manière suivante (exemple en C++) :

/*! Classe d'exemple 
 * @author Xavier Claude
*/
public class Exemple {

    protected:
        /*! la description d'un attribut */
        std::string s;
    public:
        /*! La description d'une classe
         * @param newS la nouvelle valeur de s
         * @return true en cas de succès
         */
         bool setS(std::string newS);
}

Comme cela fait longtemps que les nouvelles versions de Doxygen n’ont pas été évoquées sur LinuxFr.org, un résumé des nouveautés des dernières versions est disponible en deuxième partie. Il y a bien sûr eu, en plus, beaucoup de corrections de bogues et quelques changements de comportement.

Onedev est une application web tout‑en‑un, simple et puissante pour héberger vos dépôts Git avec gestion des bogues, des fusions et construction des binaires. Dans son esprit de simplicité, le Readme du dépôt Onedev présente le fonctionnement par des copies d’écran animées. Onedev, qui porte bien son nom, est quasiment l’œuvre d’une seule personne, Robin Shine, qui le développe sporadiquement depuis 2012 (en Java). Bien sûr, le projet est auto‑hébergé. La version 3.0.5 de Onedev vient de sortir. Le projet est sous licence MIT.

N. D. M. : il existe déjà diverses alternatives (sur toutes ou partie des fonctionnalités) libres à GitLab comme Gogs, Gitea, Phabricator, Trac, Tuleap, etc.

Review Board est une application web libre de revue de code collaborative. Originellement initiée chez VMware, elle est développée en Python/Django, et publiée sous licence MIT. Review Board se repose sur SVN et Git, mais aussi le vénérable CVS, ainsi que Bazaar et Mercurial (et accessoirement les proprios Perforce et ClearCase).

La revue de code étant un des parents pauvres du développement logiciel par son côté rébarbatif, un outil centralisé et collaboratif se révèle bien évidemment très largement supérieur à des méthodes empiriques par courriel et bavardages en ligne éparpillés. De plus, il amène un côté convivial et fun, couplé à un début d’effet social. Si la « sauce » prend dans une équipe de taille moyenne, cela peut beaucoup apporter en termes de qualité de code, entre autres.

La version 1.6 vient d’être publiée et apporte beaucoup de nouveautés : la liste est trop longue pour être détaillée ici. Pour ceux qui ne connaissent pas, jetez un rapide coup d’œil sur les copies d’écran. Review Board permet de gérer les requêtes de revue, les revues en elles‐mêmes, les diffs et les commentaires. En outre, ce logiciel propose un tableau de bord avec statistiques.