Sortie de Coq 8.5 bêta, un assistant de preuve formelle

98
28
jan.
2015
Science

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.

Journal Encore un exemple de code spaghetti : Toyota

96
5
mar.
2014
Ce journal a été promu en dépêche : Encore un exemple de code spaghetti : Toyota.

Cher nourjal,

Après les journaux successifs sur l'instruction goto, je reçois un mail d'un de nos professeurs par rapport à une affaire où les freins d'une Toyota ont refusé de fonctionner à cause d'un code spaghetti : http://www.safetyresearch.net/2013/11/07/toyota-unintended-acceleration-and-the-big-bowl-of-spaghetti-code/

L'article est très long et en angliche, ça date du 13 novembre 2013, je vais tenter un résumé :

Jean Bookout et Barbara Schwarz avaient une Toyota Camry de 2005. Le système de freinage est contrôlé par l'électronique du système. Mais voilà (...)

Journal To comment or not to comment. That is the question.

93
23
avr.
2013

Sommaire

Hier, j'ai participé à une discussion fort intéressante, vis à vis de la nécessité, ou non, de commenter son code. Certains étaient contre, d'autres non.

Voici pourquoi moi je suis pour le fait de commenter, et absolument contre la version courante, mauvais dérivé d'XP et des méthodes agiles qui voudrait faire croire que le code est la documentation, justification au fait de ne pas commenter.

Tout a commencé par la lecture de cette présentation faite par (...)

[code] Trouver les erreurs

70
14
jan.
2015
Technologie

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.

Le retour de la Méthode R.A.C.H.E

67
13
jan.
2016
Humour

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…

Journal L'intégration continue chez Debian

47
16
juin
2014

Cher journal,

Debian a mis en place son système d'intégration continue. Il consiste à exécuter les tests des différents logiciels présents dans le système de paquet dès qu'une dépendance du paquet binaire est mise à jour. Cela permet donc de trouver plus rapidement un problème dans une dépendance et de pouvoir prévenir aussi bien l'upstream du paquet dont les tests ont échoués que la dépendance qui les a fait échouer (en fonction d'où vient le problème).

Espérons que ce (...)

Coccigrep, un grep sémantique pour le langage C basé sur Coccinelle

Posté par (page perso) . Modéré par patrick_g. Licence CC by-sa.
45
2
sept.
2011
C et C++

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.

Entretien avec Stefano Zacchiroli, Responsable du Projet Debian

Posté par (page perso) . Modéré par patrick_g.
44
22
août
2010
Debian
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é.

Petit éventail des outils de construction (« builder ») libres

Posté par . Modéré par patrick_g. Licence CC by-sa.
44
5
sept.
2011
Ligne de commande

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.

Journal The Architecture of Open Source Applications

Posté par . Licence CC by-sa.
38
30
mai
2011

Un livre qui n'a pas l'air trop mal vient de sortir sous le titre "The Architecture of Open Source Applications". Il est composé de 25 chapitres et chaque chapitre détaille un logiciel libre, souvent par un de ses contributeurs majeurs. Chaque application est ainsi décortiqué pour nous en montrer les entrailles. Bref, un excellent voyage du côté obscur du code, ce qu'on a rarement l'occasion de voir.

En prime, le livre est lui-même libre (CC-BY), il est disponible sur Lulu (...)

Journal Outils de pseudo gestion de projet et développement

38
7
fév.
2014

Salut Nal,
Mon premier billet ici, après quelques années passées à lire ceux des autres, est pour vous parler des derniers outils que j'ai eu l'occasion de tester.

Je cherchais les outils nécessaires pour développer collaborativement un programme open source, ou fermé dans le cadre d'une petite entreprise. Plus généralement je cherche un workflow efficace qui s'adapte aux diverses situations que je rencontre.

Besoins

Les fonctionnalités recherchées sont :

  • Le versionnage du code source, bien évidemment, mais aussi un moyen (...)

Nouvelle version pour Doxygen

Posté par (page perso) . Modéré par patrick_g. Licence CC by-sa.
36
6
sept.
2011
Doc

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.

Review Board 1.6

34
7
sept.
2011
Technologie

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.

Forum général.petites-annonces [poste pourvu] Poste ingénieur R&D en développement à Grenoble - CDD 6 mois en vue d'un CDI

32
22
mar.
2017

Contexte

Algoo est une société proposant des services de développement d'applications web sur mesure et infogérance. Elle développe et commercialise également le logiciel libre Tracim.

La stratégie à long terme de l'entreprise est de générer des revenus selon 2 axes :

  • les revenus récurrents, liés à la commercialisation de Tracim et à l'infogérance,
  • les revenus non récurrents, liés aux développements sur mesure.

La stratégie à court terme (et directement concernée par cette annonce) est de finaliser la version 1.0 (...)

Bonnes pratiques et qualité du Web

Posté par (page perso) . Édité par Davy Defaud, Benoît Sibaud, Florent Zara et baud123. Modéré par Davy Defaud. Licence CC by-sa.
32
12
oct.
2012
Internet

Le Web évolue. En l’espace d’une quinzaine d’années, la production de services en ligne est passée du stade artisanal au stade industriel. Très vite, les outils se sont affûtés, les métiers se sont spécialisés, les besoins se sont révélés. Les sites optimisés pour IE6 sont devenus obsolètes grâce à l’arrivée de Firefox, de Chrome, de Safari et surtout des smartphones. Grâce aux spécifications élaborées par le W3C, il est maintenant possible de créer des sites Web fonctionnant sans artifice avec tous les navigateurs.

Un site Web passant le test du validateur W3C est un pré‐requis, mais cela ne suffit pas à en faire un bon site, il faut aussi prendre en compte la notion d’accessibilité et évaluer la facilité d’utilisation, tout en pensant à son référencement. Gérer cet ensemble de contraintes pour répondre aux besoins s’appelle la Qualité.

Fort d’une longue et solide expérience, Élie Sloïm, Laurent Denis, Muriel de Dona et Fabrice Bonny viennent de publier le livre Qualité Web. Il est le fruit d’une longue expérience qui l’a conduit, avec Fabrice Bonny, à créer OpenWeb, un site qui explique toutes les techniques à employer sur le Web, puis le projet Opquast, un ensemble de bonnes pratiques (en accès libre et en licence creative commons BY-SA) pour la qualité des services en ligne.