Syndiquer le contenu
Mis à jour : il y a 23 heures 55 min

Plasma 5.2, l'espace de travail de KDE

2 février, 2015 - 21:51

Plasma 5.2 est sorti le 27 janvier 2015, 2 mois et demi après la sortie de la version 5.1. Pour rappel, Plasma est l’espace de travail (aussi appelé shell) de KDE. Cette version nous apporte de nouveaux composants, un bon nombre de nouvelles fonctionnalités et bien des corrections de bogues.

Découvrez les nouveautés en seconde partie de l'article.

Sommaire Nouveaux composants portés Système

Au menu, en bref : BlueDevil, KSSHAskPass, Muon, configuration de l'apparence du gestionnaire de connexions (SDDM), KScreen, GTK Application Style, KDecoration.

Plus de détails dans la suite de cette dépêche.

BlueDevil

Un ensemble de composants pour gérer les périphériques Bluetooth. Cela configurera votre souris, clavier, l'envoi et la réception de fichiers, et vous pourrez naviguer dans la liste des périphériques.

KSSHAskPass

Si vous accédez à des ordinateurs avec des clés SSH, mais que ces clés ont des mots de passe, alors ce module vous donnera une interface graphique pour entrer des mots de passe.

Muon

Muon permet d’installer et de gérer des logiciels et autres extensions pour votre ordinateur. C'est une interface graphique simplifiée pour apt, il faut donc que votre distribution préférée propose apt, ce qui est possible même avec des rpms.

Login theme configuration (SDDM)

SDDM est désormais le gestionnaire de connexion de choix pour Plasma, et ce nouveau module de Configuration Système vous permet d'en configurer le thème.

KScreen

Kscreen, le module permettant de configurer et de gérer plusieurs écrans, fait un pas en avant, et devient disponible avec cette version de plasma.

Au passage, la gestion de plusieurs écrans a également été améliorée, puisque le code de détection a été porté pour utiliser XRandR directement, corrigeant de multiples bogues dans la foulé.

GTK Application Style

Ce module permet de configurer le thème et le couleurs utilisées par les applications utilisant le cadriciel GTK.

KDecoration

Cette bibliothèque facilite et fiabilise la création de thèmes pour KWin, le gestionnaire de fenêtres de Plasma. On retrouve de grandes amélioration de mémoire, de performances et de stabilité ; le thème Breeze a rendu nécessaire ces améliorations pour être activé par défaut. Si quelques fonctionnalités vous manquent, ne vous inquiétez pas, elles seront au rendez-vous pour la version 5.3.

Autres changements Fonctionnalités

Lors du changement d’un élément du bureau, une notification nous permet d’annuler l’action :

Résultats mieux classés dans KRunner, lancé avec Alt-Espace ou Alt-F2 :

Toujours dans KRunner, il est possible de contrôler le lecteur de musique pour, par exemple, passer à la piste suivante en tapant next.

De nouveaux widgets arrivent, notamment 15 puzzles, un navigateur internet, ou encore montrer le bureau.

L’intégration de logind avec le verrouilleur d'écran a été améliorée pour permettre de s'assurer que l'écran est bien vérouillé avant la mise en veille (cela pouvait se produire juste après la sortie de veille auparavant). En outre, il est maintenant possible de configurer le fond d'écran de l'écran verrouillé. En interne, ça utilise une partie du protocole Wayland, qui est le futur du bureau Linux.

La liste des applications par défaut dans le panneau kickoff a été mise à jour en y ajoutant la messagerie instantanée, Kontact et Kate.

Le retour attendu de l'activation ou de la désactivation du pavé tactile est bienvenu ! (pour les claviers disposant d'une touche dédiée.)

Baloo

Baloo, l’index sémantique de recherche, s'optimise au démarrage : il consomme maintenant de 2 à 3 fois moins de temps processeur au lancement. L'analyseur syntaxique de requêtes ajoute la gestion de la propriété type (ou kind, qui sont synonymes), ce qui permet de filtrer les résultats par type dans KRunner par exemple. Ainsi, day type:audio permet de rechercher tous les fichiers audio dont le nom ou le contenu contient le mot day. Rappelons que baloo est également accessible en ligne de commande grâce à baloosearch.

Pour éviter que certains fichiers non-intéressants soient indexés, Baloo n'indexe plus par défaut les fichiers textes dont la taille est supérieure à 10 mébioctets.

La documentation de Baloo n'étant pas des plus aisées à trouver, voici un petit récapitulatif de sa syntaxe :

# Recherche des fichiers contenant les mots données (insensible à la casse) bouts de mots à trouver # implicitement liés par des ET logiques # Recherche avec ET et OU alpha OR beta # Tri par type de fichiers type:video gone girl # Recherche complexe artist:(queen OR oasis) tracknumber:4

Voici une liste de propriétés que vous pouvez utiliser, en fonction des types de fichiers (d'après le code source) :

Documents Images Audio Author Keywords BitRate Title Width Channels Subject Height Duration Creator AspectRatio Genre Generator FrameRate SampleRate PageCount ImageMake TrackNumber WordCount ImageModel ReleaseYear LineCount ImageDateTime Comment Language ImageOrientation Artist Copyright PhotoFlash Album Publisher PhotoPixelXDimension AlbumArtist Description PhotoPixelYDimension Composer CreationDate PhotoDateTimeOriginal Lyricist PhotoFocalLength PhotoFocalLengthIn35mmFilm PhotoExposureTime PhotoFNumber PhotoApertureValue PhotoExposureBiasValue PhotoWhiteBalance PhotoMeteringMode PhotoISOSpeedRatings PhotoSaturation PhotoSharpness Apparence

Une amélioration du thème Breeze :

  • Décorations de fenêtres ;
  • Nouvelles icônes ;
  • Curseur blanc (dit neige).

En outre, Breeze configure les thèmes GTK dès la première connexion par souci d'homogénéité.

Voici les décorations :

Plus de 300 bogues corrigés dans les modules Plasma.

Voici les icônes :

Conclusion

Plasma 5.3, prévu pour le 28 avril prochain, devrait peaufiner tout ça, même si le bureau est maintenant utilisable sans gros soucis. En parallèle, de nombreuses applications passerons la version Qt 5/Kframeworks par défaut (telle que Dolphin ou encore KCalc).

Amarok sera-t-il porté vers Qt 5 ? C'est difficile à dire. Alors peut-être Clémentine ?

N'hésitez-pas à tester tout ça au sein de votre distribution favorite !

Télécharger ce contenu au format Epub

Lire les commentaires

Revue de presse - février 2015

1 février, 2015 - 23:27

Le mois de janvier fût marqué par des drames que nous ne sommes pas près d'oublier. En France, la presse est libre. Sans la liberté de blâmer, il n'est point d'éloge flatteur ; et comme le rappelle toutes les semaines un canard, la liberté de la presse ne s’use que quand on ne s’en sert pas. Pour ce deuxième mois de l'année, les marchands de journaux disposent encore une fois de nombreux titres dans leurs rayons et cet hiver, la sécurité semble être la préoccupation principale.

Comment protéger sa vie privée ? Y a-t-il un danger à se connecter en wifi ? Comment installer un firewall ? Pour le n° 83 de Planète Linux, 2015 est l’année de la sécurité informatique.

Linux Pratique n° 87 vous propose de découvrir comment anonymiser tout votre trafic [réseau] avec Tor. Par ailleurs, d'autres sujets sont abordés comme la sécurisation d'un serveur serveur web avec chroot ainsi que l'utilité d'un pare-feu.

Souhaitez vous optimiser la protection de votre système et de vos applications ? Le hors-série n° 76 Sécurité & Linux devrait vous intéresser. À noter qu'un chapitre est consacré à la sécurité sous Android.

MISC n° 77 propose un dossier sur la sécurité des moyens de paiement. Comment faciliter les échanges tout en évitant la fraude ? Les réponses sont dans MISC.

Hackable n° 4 le magazine des amateurs de tournevis et de fer à souder se recentre une nouvelle fois sur Raspberry Pi et ses nouvelles cartes.

Les pythoneux pointilleux se délecteront du n° 179 de GNU/Linux Magazine. Tandis que les débutants en programmation porteront leur attention sur le n° 182 de Programmez! qui tente de convaincre son lectorat de l'intérêt du métier de développeur. Le magazine a tout de même le mérite de présenter la première version d'Android Studio apparue discrètement en décembre.

Les sommaires complets de chacun de ces magazines sont en ligne via les liens ci-dessous.

Télécharger ce contenu au format Epub

Lire les commentaires

Club de la Presse : Petit déj’ de la com’ « L’utilisation des données numériques dans la presse »

1 février, 2015 - 23:24

Cette fois, nous organiserons un Petit déj’ de la com à 8h30 afin de pouvoir inviter plus de monde, notamment des communicants. Suite à de nombreuses demandes qui nous ont été faites lors de la première journée. Ainsi, pour le gens de Montpel’libre qui veulent venir, ils peuvent contacter directement le Club de la Presse par mail ou téléphone pour s’inscrire.

Une diffusion en directe sera proposée sur le site web du Club, pour permettre aux personnes qui ne peuvent pas se déplacer, de suivre quand même l’intervention.

Comment exploiter les données locales ? Les données numériques, dîtes « data », envahissent notre quotidien jusqu’à être présentées, par les spécialistes du numérique, comme l’une des révolutions les plus importantes qu’aient connu l’humanité. Venez découvrir ce qui se cache derrière ces big, fast, smart, open…data.

Quels sont les enjeux pour la profession de journaliste ? Comment la recherche d’information se doit d’évoluer pour s’adapter à cette avalanche de données ?

Faire face à la menace numérique et juridique.

Jeudi 5 février 2015 de 8h30 à 10h00
1, place du Nombre d’Or 34000 Montpellier

GPS Latitude : 43.608199 | Longitude : 3.887789

Tramway ligne 1, arrêt Antigone

Télécharger ce contenu au format Epub

Lire les commentaires

Rencontres Fedora 21 le 7 février 2015 à Lyon

1 février, 2015 - 22:41

L’association Borsalinux-Fr vous donne rendez-vous le samedi 7 février 2015 à Epitech à Lyon (au 156, rue Paul Bert) pour les Rencontres Fedora 21. Cet événement aura lieu de 14h à 17h et sera suivie par l’assemblé générale de Borsalinux-Fr, association qui fait la promotion de Fedora dans les pays francophones.

Pour cette nouvelle version de Fedora, pleine de nouveautés, ces Rencontres sont l’occasion de découvrir Fedora, sa communauté et d’échanger sur le monde du Logiciel Libre. Lors de cette journée, vous pourrez demander une démonstration et une installation de Fedora 21 mais aussi venir discuter du projet et de son organisation avec la communauté francophone.

Des présentations sur les nouveautés de Fedora seront proposées au cours de l’événement.

Télécharger ce contenu au format Epub

Lire les commentaires

SMI version 1.0.0

1 février, 2015 - 22:40

SMI (Services Maintenance Interventions) est un logiciel libre de gestion et de suivi de maintenance ou gestion de SAV et de services, multi‐professions, développé en PHP / MySQL et placé sous licence GPL.

Cette nouvelle version apporte essentiellement des corrections de bugs mineurs, un passage en UTF-8 (character set et MySQL), l'intégration de JQuery pour améliorer les performances et l'ergonomie, et une amélioration de la gestion des plannings. Elle est également plus compacte et améliore les performances globales.

SMI a été développé sur une base d’expérience de plus de 20 ans dans la maintenance. Il est aujourd’hui utilisé par différents professionnels, de toutes professions, recherchant un logiciel complet de suivi de services et de maintenance auprès de particuliers, de sociétés ou d’établissements publics.

Il permet de mettre en place et de gérer efficacement un service de maintenance, ainsi que de répondre globalement aux demandes de SAV de clients, de services d'une entreprise ou d'une administration, tout en restant simple d'utilisation. Il est proche d’une gestion de maintenance assistée par ordinateur (GMAO), mais n’en reprend pas la complexité, car il est avant tout destiné aux structures et indépendants qui souhaitent utiliser un logiciel simple et rapide d’apprentissage.

SMI a été téléchargé près de 10 000 fois depuis sa création et est utilisé en production dans tous les types et tailles de structures.

Télécharger ce contenu au format Epub

Lire les commentaires

Soirée sur les logiciels libres en santé le jeudi 5 février 2015 à Nice

1 février, 2015 - 21:40

L'association LibreHealthCare organise ce jeudi 5 février une soirée sur les logiciels libres en santé.
Il est important de bien se servir de ses outils ! Tout comme un marteau peut servir à construire un hôpital ou à s'écraser un doigt, les outils informatiques doivent être utilisés à bon escient. Un professionnel de santé a besoin de se servir d'une multitude d'outils pour arriver au mieux à pratiquer son art.

Plus d'infos en seconde partie

Au court-circuit café, le jeudi 5 février à 19h, l'association LibreHealthCare vous propose d'explorer l'univers des outils libres appliqué au milieu de la santé autour d'une bonne bière (ou deux) avec la possibilité supplémentaire de vous sustenter pour environ 8 euros la bonne assiette.

L'informatique est désormais présente dans la pratique professionnelle : logiciels d'aide à la prescription, lecteur d'imagerie médicale, gestion de dossier des patients, jeux autour de la dyslexie, etc. Or c'est un outil sensible puisqu'il peut contenir des données de santé des patients, et il est d'autant plus important de comprendre comment ils fonctionnent au quotidien, et pourquoi les professionnels de santé doivent garder le contrôle sur leur développement.

Pas de panique, nous n'aborderons pas les codes et autres détails de programmation. Le seul pré-requis sera votre bonne humeur :) Nous nous proposons de vous expliquer ce qu'est un logiciel libre, et pourquoi il est primordial de sensibiliser un maximum de professionnels et d'étudiants à cette question pour leur pratique quotidienne.

De plus, Jerôme Pinguet (interne en médecine générale à Marseille) viendra nous présenter comment ces outils peuvent être utilisés concrètement pour gérer son cabinet médical. Nous explorerons enfin la question des principe du Libre dans la recherche scientifique ainsi que l'impression 3D libre appliqués à la santé.

Notons que les dinosaures n'utilisaient pas les outils libres…et ils ont disparu!

Librement vôtre

PS : si vous souhaitez déjà vous renseigner sur la problématique des logiciels libre en santé, nous vous recommandons la lecture de la thèse de Nicolas Floquet (de la faculté de pharmacie de Lille) accessible aux plus profanes d'entre vous ici.

Télécharger ce contenu au format Epub

Lire les commentaires

Atelier Warmux MDA - 7 et 8 Février 2015 Montpellier

1 février, 2015 - 21:37

Cet atelier permet de découvrir les jeux Libres disponibles sous différents systèmes d’exploitation dont GNU/Linux (nous utiliserons Ubuntu…) ainsi que la modification d’un de ces jeux, en l'occurrence Warmux.

Warmux est un jeu vidéo libre dans la famille des jeux vidéo d’artillerie, comme Scorched Earth ou Worms.

Rendez-vous le Samedi 7 février 2015 de 9h00 à 12h00 et de 13h00 à 16h00 et le dimanche 8 février 2015 de 13h00 à 16h00. Maison des Adolescents - MDA34 - 9, rue de la République 34000 Montpellier

Logiciels utilisés pour l’atelier (disponible gratuitement et légalement en téléchargement et en utilisation sous Licence GPL) :

  • Warmux (le jeu)
  • Gimp (montage d’images)
  • Inkscape (dessin vectoriel)
  • Audacity (montage audio)
  • Éditeur de texte simple ou LibreOffice (pour la modification des codes sources)
  • Firefox (pour la navigation sur internet)
  • Dogmazic (pour les téléchargements de musiques et sons)

Matériels utilisés :

  • Ordinateurs en réseau
  • Micro-casques ou microphones pour les bruitages
  • Vidéoprojecteur
  • Imprimante
Télécharger ce contenu au format Epub

Lire les commentaires

Séminaire gratuit "Concevoir un système embarqué Linux avec Yocto"

1 février, 2015 - 13:53

Le projet Yocto, hébergé par la Linux Foundation, est un projet collaboratif fournissant les outils et méthodes pour créer des distributions Linux sur mesure pour le monde de l'embarqué, en prenant en compte des architectures de processeur variées.

Soutenu par de très nombreux fondeurs, tels Intel, AMD, Broadcom, Texas Instruments & Freescale, il sert de base à des solutions Linux commerciales, mais peut également être utilisé par tout développeur qui souhaite bénéficier d'une solution Linux embarqué intégrant des composants logiciels riches. Les outils de build permettent une grande qualité de production de la distribution en assurant fiabilité et reproductibilité.

Le programme Cap'tronic qui vise à réussir l’intégration de solutions électroniques et de logiciel embarqué dans les produits des PME a donc intégré Yocto à son cycle de séminaires pour l'année 2015, et propose un séminaire gratuit dédié à ce sujet, animé par CIO Systèmes Embarqués le 24 février 2015 à Montpellier (Hérault).

Ce séminaire d'une 1/2 journée est l'occasion de faire un point sur les 10 dernières années d'évolution de Linux dans l'embarqué, puis de mettre en avant la nécessité de se doter d'un outil adapté pour créer une distribution embarquée adaptée aux besoins actuels, avant d'entrer plus en détail sur le projet Yocto et l'outil qu'il propose.

Une démonstration de l'utilisation de l'outil sur le poste développeur, et de la distribution générée sur carte ARM intégrant un processeur IMX.6 de Freescale, est prévue en fin de séminaire, ainsi qu'une session de questions / réponses.

La participation au séminaire nécessite une inscription préalable.

Télécharger ce contenu au format Epub

Lire les commentaires

Jeudi du libre du 5 février 2015 à Lyon

29 janvier, 2015 - 19:23

Dans ce monde déchaîné, il est bon d'avoir un peu de régularité. Pour cela, l'ALDIL, le GULL lyonnais, vous propose comme chaque mois un jeudi du libre. Cette fois, c'est Mageia qui est à l'honneur.

Mageia est une distribution GNU/Linux créée en 2010 à partir de Mandriva Linux. Les initiateurs du projet ont voulu en faire une distribution totalement communautaire, d'où la structure (association loi 1901 et le mode d'adhésion gratuite).

L'objet de la distribution est d'essayer de répondre aux besoins du plus grand nombre en laissant le plus de choix possible à l'utilisateur final. Vous découvrirez pendant cette conférence le projet, son histoire et ses spécificités.

C'est Daniel Tartavel qui présentera cette conférence. Il utilise les Logiciels Libres depuis 1996, et Mandrake / Mandriva / Mageia depuis la première version sortie (5.1 en 1998). Samuel Verschelde l'accompagnera. Samuel a été utilisateur puis contributeur sur Mandrake puis Mandriva depuis 2004. Il a rejoint Mageia dès sa création en 2010 et participe dans la mesure de ses moyens. Présent tous les ans avec Daniel sur le stand Mageia aux Journées Du Logiciel Libre organisées par l'ALDIL (JDLL), il est co-créateur du MADB, qui liste les applications disponibles sur Mageia.

La conférence aura lieu le 5 février à partir de 19h30 à la Maison Pour Tous / Salle des Rancy : 249 rue Vendôme - 69003 LYON (Métro Saxe Gambetta). Entrée libre et gratuite.

Télécharger ce contenu au format Epub

Lire les commentaires

Sortie de pfSense 2.2, distribution routeur/pare-feu sur base FreeBSD

29 janvier, 2015 - 11:20

La version 2.2 de pfSense est sortie vendredi 23 janvier. pfSense est une distribution à base de FreeBSD, utilisable comme routeur et pare-feu. Cette version 2.2 passe de FreeBSD 8.3 à FreeBSD 10.1, en plus du changement de démon IPsec racoon remplacé par strongSwan, une mise à jour de la bibliothèque PHP en version 5.5 avec un remplacement de FastCGI vers PHP-FPM pour l'interface graphique, et l'ajout d'Unbound DNS server.

Plus de détails dans la deuxième partie de la dépêche.

Présentation

pfSense est un système d'exploitation orienté routeur et pare-feu dérivé de m0n0wall et basé sur FreeBSD (NanoBSD pour la version embarquée). Il se veut complet, mais également intuitif au travers d'une interface web donnant accès à l'intégralité des fonctionnalités. On peut ainsi établir des tables de routage, des règles pour le pare-feu, faire des VLAN, activer un service DHCP, et bien d'autres choses.

pfSense s'administre depuis une interface web moderne ou via CLI/PHP et est facile à utiliser.

pfSense est léger et peut être embarqué sur du matériel de type mini-ITX (Alix), installé sur carte CompactFlash (la version embarquée charge les composants en mémoire puis n'écrit plus rien). Il peut se substituer à une box domestique ou faire office de pare-feu d'entreprise.

Fonctionnalités
  • gestion des VLAN taggés ;
  • routage IPv4 et (depuis la version 2.1) IPv6, NAT ;
  • filtrage du trafic entrant et sortant pour tout type de trafic (ICMP, UDP, TCP…) ;
  • limitation des connexions pour un pair ;
  • log du trafic avec génération de graphiques ;
  • log sur serveur syslog externe ;
  • load Balancing, Failover ;
  • agrégation de ports, IP virtuelles ;
  • proxy transparent ;
  • serveur ou client PPPoE ;
  • VPN (client ou serveur) IPsec, PPTP, OpenVPN ;
  • DNS Dynamique ;
  • portail captif ;
  • contrôle d'accès par adresses MAC ou authentification RADIUS ;
  • serveur ou relais DHCP / DNS ;
  • ajout de fonctionnalités via des paquets directement installables dans l'interface.
Nouveautés
  • pfSense 2.2 est basé sur FreeBSD 10.1 ce qui apporte non seulement de nombreux correctifs de sécurité, mais aussi une meilleure prise en charge du matériel et de la virtualisation ;
  • pf est désormais SMP friendly, ce qui améliore grandement les performances ;
  • l'interface d'administration fonctionne désormais sous PHP-FPM, ce qui apporte un gain de réactivité ;
  • ajout de nouveaux fournisseurs de DNS Dynamique (City Network, OVH DynHOST, GratisDNS, Euro DNS et CloudFlare) ;
  • Changement de démon IPSec racoon par strongSwan avec la gestion d'IKEv2, AES-GCM entre autres ;
  • et bien d'autres, que vous pouvez lire sur cette liste complète des changements.
Télécharger ce contenu au format Epub

Lire les commentaires

Jorani passe la troisième

29 janvier, 2015 - 08:41

Jorani est un projet de LMS (Leave Management System), une application de gestion des congés et des heures supplémentaires. Disponible sous une licence GPLv3, cette application web (PHP/MySQL) aide les petites et moyennes structures à passer sans douleur d'un processus papier à un processus informatisé.

Jorani est disponible depuis le 21 janvier dernier en version 0.3.0. Après quelques déploiements et la prise en compte des remarques des lecteurs de LinuxFr.org, le projet revient vous présenter les nouveautés de la dernière version :

  • détection des chevauchements de demandes ;
  • calcul du solde de congé à reporter ;
  • calendrier tabulaire ;
  • multiples améliorations ergonomiques et ajouts de pages utilitaires ;
  • API REST (OAuth2) ;
  • authentification LDAP simple ou complexe ;
  • la documentation ainsi que le site du projet ont été traduits en français.
Télécharger ce contenu au format Epub

Lire les commentaires

Prochains meetup Linux embarqué et Android à Toulouse de janvier à mars 2015

28 janvier, 2015 - 22:22

Il y a quelques mois, nous annoncions la création d'un Meetup Linux embarqué et Android à Toulouse, avec deux premières rencontres prévues (sur Yocto et sur le Device Tree).

Ces deux premiers rendez-vous ayant eu un fort succès, nous avons reprogrammé 3 nouveaux événements en ce début 2015:

N'hésitez pas à vous inscrire à ces événements, dont l'entrée est gratuite. Ils ont lieu à La Cantine Toulouse. Nous sommes également à l'écoute de vos propositions d'interventions.

Télécharger ce contenu au format Epub

Lire les commentaires

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

28 janvier, 2015 - 09:44

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.

Sommaire Coq, en résumé

Développé depuis trois décennies, la version 1 datant de 1984, Coq vient d'être consacré dans la cour des grands l'année dernière, en recevant le très prestigieux prix ACM Software System Award de l'ACM, côtoyant ainsi Unix, TCP/IP, TeX, Java, Make et d'autres grands noms faisant partie de notre quotidien  —  LLVM avait ainsi été récompensé l'année précédente.

Les logiciels de méthodes formelles

Un « assistant de preuve » fait partie d'une famille plus large de logiciels visant à établir la vérité (ou la fausseté) d'un énoncé mathématique donné. Par exemple, une égalité entre deux expressions mathématiques, ou un énoncé décrivant le fait qu'un certain système formalisé ne tombe jamais dans un état de panne, ou encore le fait qu'il existe une infinité de nombres premiers. Il existe une grande diversité d'approches selon la nature des énoncés concernés et la nature plus ou moins automatique de l'obtention du résultat :

  • On parle de « prouveurs automatiques de théorèmes » pour les logiciels très automatisés qui prennent l'énoncé en entrée et répondent soit « vrai », soit « faux », soit parfois « je ne sais pas » sans aucune information supplémentaire. Par exemple, les solveurs SAT ou SMT essaient de prouver des énoncés logiques utilisant un langage restreint (logique pure, arithmétique, tableaux, un peu de quantificateur, …). Ils ne savent répondre automatiquement que si la réponse peut être trouvée de façon assez « bête », mais peuvent traiter des formules énormes qu'un humain ne saurait pas manipuler ; ils sont donc de plus en plus utilisés dans l'industrie. Le model checking utilise ces outils pour vérifier automatiquement des propriétés de systèmes physiques ou virtuels ayant un nombre d'états possibles fini.

  • Les « analyseurs de programmes » sont une classe d'outils spécialisés pour l'étude des programmes informatiques. Les systèmes de typage statiques en font partie, mais aussi par exemple les outils utilisant l'interprétation abstraite. Ils peuvent garantir l'absence d'une classe d'erreurs variées, allant de l'absence de confusion pointeurs/entiers à l'absence de division par zéro, par exemple. Certains outils permettent d'annoter les programmes avec des invariants et contrats supplémentaires pour prouver des propriétés plus proches encore de la spécification formelle du programme.

  • Les « assistants de preuves » sont des logiciels qui permettent de manipuler des énoncés trop compliqués pour que l'ordinateur les vérifie seul. Ils se présentent comme un langage qui permet de décrire à l'ordinateur non pas un programme informatique, mais les étapes de raisonnement pour justifier un énoncé mathématique. Si le code fourni est accepté par l'assistant, la preuve est correcte et l'énoncé est vrai.

La plupart des théories mathématiques et des énoncés concernant des langages de programmation Turing-complets, ne sont pas décidables automatiquement (il n'existe pas d'algorithme qui peut toujours répondre « oui » ou « non » sans se tromper). Les outils de preuve automatique ont donc toujours un risque de répondre « je ne sais pas ». De même, quand on conçoit un outil d'analyse de programme, il faut accepter qu'il « ne sache pas » dans certains cas ; selon ses priorités, on décidera alors de rejeter des programmes valides (si on veut garantir l'absence d'erreur) ou d'accepter des programmes incorrects (si on veut prévenir l'utilisateur seulement quand il y a vraiment une erreur).

Si on veut pouvoir travailler sur des énoncés mathématiques ou programmes quelconques, une idée de plus en plus réaliste est d'utiliser les assistants de preuve pour décrire les parties difficiles d'une preuve, et laisser des prouveurs plus automatiques décider les sous-parties les plus évidentes. Ou bien utiliser un outil d'analyse de programme, mais faire parfois appel à un assistant de preuve sur les quelques cas trop difficiles à gérer entièrement automatiquement.

Un assistant de preuve

Coq est un assistant de preuve. Il manipule des preuves, dans un sens mathématique. L'utilisateur énonce des théorèmes et il doit ensuite fournir une preuve formelle de ceux-ci, sous forme d'étapes de raisonnement élémentaires dans la plupart des cas. Une fois la preuve donnée, le logiciel vérifie qu'il s'agit bien d'une preuve correcte, sans erreur de raisonnement, puis la marque comme validée. On peut ainsi construire de manière incrémentale une bibliothèque de preuves vérifiées mécaniquement par ordinateur.

Le choix de la dénomination « bibliothèque » dans la phrase précédente n'est pas due au hasard. Pour une raison fondamentale, dont on discutera par la suite, l'ingénierie de la preuve est très similaire à l'ingénierie logicielle. Pour l'instant, il est raisonnable de se figurer que des preuves dépendent d'autres preuves de la même manière que les fonctions d'un programme dépendent de fonctions définies auparavant.

Coq est un assistant de preuve, mais c'est aussi un langage de programmation. En particulier, il fournit un système de modules qui ressemble à celui d'OCaml. L'exemple qui suit définit une fonction multiplicity récursive (mot-clé Fixpoint) qui renvoie le nombre de fois qu'apparaît l'entier n dans une liste l. Ensuite il prouve une propriété simple sur la fonction : la multiplicité de n dans la concaténation de deux listes est la somme des multiplicités de n dans chaque liste.

(* import de modules pour les listes et l'arithmétique *) Require Import List Arith. Fixpoint multiplicity (n : nat) (l : list nat) : nat := (* filtrage par motifs sur la liste "l" *) match l with (* cas où la liste est vide *) | nil => 0 (* cas où on a un élément "a" en tête de liste, "l'" le reste *) | a :: l' => (* test d'égalité de "n" avec l'élément "a" *) if eq_nat_dec n a (* appel récursif suivi de la fonction successeur d'un entier *) then S (multiplicity n l') else multiplicity n l' end. Lemma multiplicity_app (n : nat) (l1 l2 : list nat) : multiplicity n (l1 ++ l2) = multiplicity n l1 + multiplicity n l2. Proof. induction l1. reflexivity. simpl. destruct eq_nat_dec; auto. rewrite IHl1. auto. Qed.

Une des caractéristiques des fonctions récursives en Coq, liée au fait que Coq n'est pas Turing-Complet, est qu'elles terminent — ou autrement dit, s'arrêtent forcément à un moment donné. En effet, Coq vérifie que les arguments de l'appel récursif sont plus petits : il accepte l'exemple, car la liste l' est obtenue à partir de la liste l en lui enlevant son premier élément. Il arrive que certaines fonctions récursives terminent, mais que Coq ne soit pas capable de le deviner : savoir si un objet est plus petit qu'un autre n'est pas toujours évident. Dans ces cas, il faut l'aider un peu pour qu'il accepte la fonction.

Voici deux preuves plus compliquées, reposant sur des définitions précédentes et bibliothèques de théorèmes. La première énonce qu'un petit langage de programmation est déterministe : si le programme c, partant de l'état mémoire st, peut arriver soit dans l'état st1 soit dans l'état st2, alors ces deux états sont égaux.

Theorem ceval_deterministic: ∀c st st1 st2, c / st ⇓ st1 → c / st ⇓ st2 → st1 = st2. Proof. introv E1 E2. gen st2. induction E1; intros; inverts× E2; tryfalse. forwards*: IHE1_1. subst×. forwards*: IHE1_1. subst×. Qed.

La seconde fait partie d'une preuve qu'il y a une infinité de nombres premiers : pour tout nombre entier m, on peut trouver un nombre entier premier p strictement supérieur à m.

Lemma prime_inf m : {p | m < p & prime p}. Proof. pose c := pdiv m`!.+1. have Pc : prime c by apply/pdiv_prime/fact_gt0. exists c => //. have [cLm|//] := leqP. have /Euclid_dvd1 := Pc. have /eqP<- := coprimenS (m`!). rewrite dvdn_gcd pdiv_dvd. by have /fact_div-> : 0 < pdiv m`!.+1 <= m by rewrite prime_gt0. Qed. Écosystème

À l'instar des langages de programmation, il existe différents assistants de preuves, qui ne reposent pas tous sur la même base théorique, diffèrent au niveau de la syntaxe ou de l'expressivité. Citons quelques noms à la louche :

  • ACL2 ;
  • PVS ;
  • La famille HOL (HOL4, HOL Light…) ;
  • Isabelle, successeur de HOL ;
  • Agda, qui est probablement l'un des plus proches cousins de Coq à l'état naturel.

La preuve assistée par ordinateur est une pratique qui se répand de plus en plus, avec aussi bien des théorèmes légendaires formalisés que des systèmes informatiques complexes certifiés sans bugs. Citons deux projets époustouflants et révélateurs de ce qui se fait déjà à l'heure actuelle :

  • Le projet Flyspeck, en HOL Light sous licence BSD, qui visait à prouver la conjecture de Kepler, vient d'arriver à son terme l'été dernier. Cette conjecture, évidente pour n'importe quel vendeur d'oranges, avait tout de même été énoncée en 1611 !
  • Le système d'exploitation seL4 prouvé de bout en bout en Isabelle (et open sourcé GPL / BSD, de surcroît).

Parmi les gros développements en Coq, on peut citer :

Il faut savoir que les deux premiers théorèmes ont été prouvés par Georges Gonthier et son équipe, après une quantité impressionnante de travail acharné (6 ans pour Feit-Thompson).

Usage industriel

Les débouchés industriels des outils de preuve formelle sont nombreux. L'industrie a adopté en premier les outils de démonstration automatique et de model checking qui sont les plus automatisés et donc les plus faciles à utiliser (voir par exemple l'article A short survey of automated reasoning de John Harrison, 2007). Par exemple, les concepteurs de micro-processeurs utilisent très lourdement des outils de vérification formelle pour garantir la correction des futurs modèles à différents moments de leur conception.

Les assistants de preuves ont longtemps été réservés à un usage par une petite poignée d'experts (utilisation de la méthode B sur le logiciel critique embarqué de la ligne 14 de métro automatique), mais commencent à se diffuser. En particulier, les industries manipulant des logiciels critiques s'intéressent aux logiciels prouvés corrects utilisant ces méthodes. Par exemple, Airbus s'intéresse à l'usage du compilateur prouvé correct Compcert. Le micro-noyau Sel4 (prouvé correct avec l'assistant Isabelle) a lui été utilisé par un groupe de chercheurs et d'industriels pour construire l'hélicoptère télécommandé « le plus sécurisé au monde » (un projet qui intéresse beaucoup les militaires…).

Quelques nouveautés de Coq 8.5

Plus de deux ans et demi après la version 8.4, sortie en août 2012, la version 8.5 de Coq marque de grands changements. Elle intègre en effet quatre branches apportant des fonctionnalités remarquables.

  • Sous le capot, le moteur de tactiques (recherche de preuve) a été refait de fond en comble. Le langage de surface a été changé le moins possible, mais cela constitue une nouvelle base qui ouvre la voie à des changements / structurations / simplifications importantes dans le futur. (Arnaud Spiwack)
  • Le modèle de compilation / vérification des preuves est maintenant asynchrone ; au lieu de vérifier un fichier de preuves ligne par ligne, Coq trace maintenant les dépendances pour calculer en parallèle les résultats indépendants, et recalculer incrémentalement ce qui est nécessaire après un changement. (Enrico Tassi)
  • un nouveau mécanisme d'évaluation des termes, native_compute est disponible : au lieu d'interpréter le calcul ou de le compiler vers un bytecode, il produit des programmes OCaml qui sont compilés à la volée en code natif. Ce mécanisme accélère beaucoup les très gros calculs, mais n'est pas rentable pour les opérations simples où le coût de compilation dominerait. (Maxime Dénès)
  • La logique sous-jacente a été étendue avec de nouvelles notions avancées : polymorphisme d'univers (plus modulaire) et projections natives (plus efficace). (Matthieu Sozeau)

Quelques autres changements importants sont:

  • Une construction $(...)$ qui permet d'intégrer des bouts de tactique directement dans des programmes  —  on ne pouvait auparavant faire que l'inverse avec la tactice refine. C'est très très pratique.
  • Une restriction de la condition de garde (qui vérifie que les programmes terminent) pour corriger une incompatibilité de la logique avec des axiomes désirables (l'extensionnalité des propositions, et des conséquences de l'univalence).
  • Une nouvelle option -type-in-type qui rend la logique incohérente (on peut prouver False) mais est pratique pour prototyper des idées sans avoir à gérer les niveau d'univers dans un premier temps.
  • Une tactique cbn qui remplace avantagement simpl.
  • Un nouveau motif introductif = x1 .. xn qui applique injection au vol (inspiré de SSReflect, un jeu alternatif de tactiques de base pour Coq)
  • De nouvelles constructions uconstr:c et type_term c pour programmer des tactiques manipulant des termes pas encore typés.

Le Changelog complet est disponible. La partie cachée de l'iceberg contient de nombreuses modifications et bugfixes (avec en particulier Pierre Boutillier, Hugo Herbelin, Pierre Letouzey et Pierre-Marie Pédrot).

Preuves et programmes : deux faces de la même pièce

Cette partie plus historique détaille un aspect important et intéressant de la conception de l'assistant de preuve Coq, qui repose sur une correspondance entre preuves et programmes. Attention à ne pas en faire une idéologie : tous les assistants de preuve ne reposent pas sur ces mêmes bases, et les bons outils obtenus aujourd'hui sont au final assez proches à l'usage, quelle que soit leur tradition scientifique.

Coq possède une particularité que ne présentent pas la majorité des autres assistants de preuve : il est basé sur la fameuse correspondance de Curry-Howard. Sous ce nom à priori barbare se cache une révolution paradigmatique de la logique, d'importance probablement comparable à l'introduction de la relativité générale en physique. Par un remarquable double effet Kiss-Cool, cette révolution est aussi d'une importance capitale pour l'informatique[1] !

Un peu d'histoire

Pour avoir une idée de l'importance de cette révolution, je me permets de faire un détour par la logique, en espérant ne pas perdre le valeureux lecteur en route. Revenons pour cela quelques malheureux 2500 ans en arrière.

À cette époque, un type nommé Aristote cherche à justifier le raisonnement logique conduisant à produire des énoncés vrais. La logique de cette époque est en effet essentiellement perçue à travers le prisme du langage et de la rhétorique, d'où le nom même de « logique », qui vient en fait du mot λόγος (logos) signifiant « parole ».

Ce nommé Aristote écrit l'Organon, qui deviendra jusqu'au XIXe siècle à la logique ce que The C Programming Language est au langage C. On y apprend des choses fort intéressantes, dont voici un exemple afin d'en jauger la teneur :

  • Socrate est un homme.
  • Tous les hommes sont mortels.
  • Donc Socrate est mortel.

Si l'Organon a fait le délice des étudiants en scolastique médiévaux, il faut attendre la fin du XIXè siècle pour que les mathématiques s'emparent vraiment de la logique comme un objet à étudier formellement. Commence alors le règne encore inachevé de la théorie des ensembles.

Les grands ancêtres

Le début du XXe siècle est une période fertile pour les progrès de la logique formelle[2]. Le développement du logicisme permet l'élaboration incrémentale d'une théorie permettant de décrire les théories mathématiques sans ambiguïté ni possibilité d'erreurs : la théorie des ensembles. L'histoire n'étant pas un long fleuve tranquille, la formulation de cette théorie fut plusieurs fois mise en défaut. Un des paradoxes les plus connus et les plus simples à expliquer est sans aucun doute le paradoxe de Russell, publié en 1903. Malgré sa mise en équations, la logique conserve alors encore sa nature aristotélicienne, c'est-à-dire qu'on pouvait la résumer à un ensemble de règles à appliquer qui garantissent la correction du raisonnement.

À peu près à la même époque et pour des raisons liées, se posent les premières questions de la définition de ce qu'on appellait alors « méthodes effectives », mais que l'on appellerait plus volontiers aujourd'hui « algorithmes ». Plusieurs tentatives de création de systèmes capturant physiquement la notion abstraite de calcul mènent à l'élaboration de deux célèbres modèles de calcul encore utilisés de nos jours.

Si les machines de Turing peuvent être vaguement considérées comme la source d'inspiration des langages de programmation impératifs, le λ-calcul est quant à lui l'ancêtre direct des langages de programmation fonctionnels. Les deux paradigmes ont rapidement été démontrés équivalents, menant à la notion de Turing-complétude. Un langage est dit Turing-complet s'il est aussi expressif qu'une machine de Turing  —  ou que le lambda-calcul. Cela signifie qu'on peut y écrire tous les algorithmes raisonnables.

Des systèmes de types aux systèmes de preuves

Les premiers langages fonctionnels comme LISP ne présentaient pas de systèmes de types statiques, conduisant à une sémantique similaires aux langages dynamiques comme Python. Étonnamment, s'il faut attendre 1972 et la publication du langage ML pour obtenir un système de types satisfaisant pour l'usage quotidien, le λ-calcul avait été doté quasiment dès ses origines d'un système de types simple. ML a justement été conçu comme langage pour programmer l'un des premiers assistants de preuves, LCF, et son typage servait à garantir que les utilisateurs ne pouvaient pas manipuler le langage pour fabriquer de « fausses preuves » d'un énoncé. Coq poursuit cette tradition : c'est un descendant de LCF implémenté dans un descendant de ce ML des origines.

La correspondance de Curry-Howard est la découverte fortuite par Haskell Curry en 1958 puis William Alvin Howard en 1969 que le système de types primitif du λ-calcul correspondait en fait exactement à un système logique minimaliste, la bien nommée logique propositionnelle minimale. C'était là la découverte d'une véritable pierre de Rosette des fondements de l'informatique, comblant le fossé qui séparait la théorie de la calculabilité (et de là l'informatique) avec la logique mathématique (et avec elle les mathématiques).

La correspondance de Curry-Howard énonce ainsi que :

  • Les preuves mathématiques sont les programmes des langages fonctionnels ;
  • Les formules logiques que démontrent ces preuves sont les types de ces programmes.

Il ne s'agit pas d'une vague ressemblance : dès lors qu'on a trouvé le bon angle sous lesquels les regarder, ces objets sont exactement les mêmes. Ainsi, on peut donner quelques traductions à travers cette pierre de Rosette pour éclairer le lecteur perdu.

Informatique Mathématiques Type Formule Programme Preuve Primitive système Axiome Fonction de A vers B Preuve de « A implique B » Paire de A et B Preuve de « A et B » Type somme sur A et B Preuve de « A ou B » Interpréteur Théorème de correction Décompilateur Théorème de complétude

Un des intérêts de cette équivalence est que l'on peut faire des va-et-vient d'un monde à l'autre. Ainsi, certaines primitives venant de la programmation sont traduites comme des lois logiques nouvelles et inversement. Ce changement paradigmatique marque aussi la naissance de la théorie de la démonstration moderne. Puisque les preuves sont des programmes, elles calculent et, donc, deviennent intéressantes en soi.

De nouvelles fondations

Peu à peu, des systèmes logiques de plus en plus riches se sont développés sur ce terreau fertile. Coq est ainsi une extension du calcul des constructions (de son petit nom CoC) développé par Thierry Coquand à la fin des années 1980. Il convient de citer aussi la théorie des types de Martin-Löf (MLTT), qui lui est similaire, sur laquelle se base Agda.

Ce courant de recherche se veut une alternative à la théorie des ensembles du siècle passé, permettant d'unifier logique et calcul en un seul et même formalisme. Le recours à l'ordinateur laisse aussi espérer l'adaptation des techniques du génie logiciel au génie de la preuve, et le passage à l'échelle des mathématiques.

Tout récemment, le petit monde de la théorie de la démonstration a été secoué par les idées de Vladimir Voïevodski, médaille Fields 2002, qui s'est rendu compte que la théorie des types était un excellent langage pour écrire les preuves d'homotopie. La théorie homotopique des types (HoTT) était née. Coq est un des langages dans laquelle cette théorie est implémentée. On pourra se réferer au pavé collaboratif de quelques 600 pages, le HoTT Book[4].

Méli-mélo de Coq au Curry-Howard

Coq est le résultat de ce courant de recherche fondamentale. En effet, il n'y a pas de différence formelle en Coq entre une preuve et un programme. Les deux objets vivent dans le même langage, à tel point qu'on peut calculer avec une preuve et, inversement, enrichir un programme avec des morceaux de preuves. Voici un exemple très simple de la fonction prédécesseur :

Definition pred : forall n : nat, {m : nat | n = 0 \/ n = S m} := fun (n : nat) => (** analyse de cas sur n *) match n return {m : nat | n = 0 \/ n = S m} with (** n vaut zéro *) | 0 => exist _ 0 (or_introl eq_refl) (** n est de la forme n' + 1 *) | S n' => exist _ n' (or_intror eq_refl) end.

Ce fragment se lit ainsi :

  • Version informatique : on définit la fonction pred qui prend en argument un entier naturel n et qui renvoie un entier naturel m tel que soit n vaut zéro, soit n = m + 1.
  • Version mathématique : le théorème pred affirme que pour tout entier naturel n, il existe un entier naturel m tel que n vaut zéro ou n = m + 1.

Et effectivement, on peut calculer le résultat de l'application de cette fonction-théorème (proj1_sig est la fonction qui extrait le témoin de l'existentielle).

Eval compute in proj1_sig (pred 42). = 41 : nat

Coq propose aussi un langage externe dit « de tactiques » qui permet d'écrire des preuves par méta-programmation, appelé Ltac. Un script de preuve n'est pas une preuve, c'est un programme qui manipule des morceaux de preuves pour construire un terme de preuve. Malheureusement, on ne sait pas encore concevoir des langages propres pour faire cela, et le langage actuel est impératif, non-typé et mal compris. Le résultat est aussi sordide que le langage interne de Coq est élégant. On pourra se le figurer comme l'hybride démoniaque entre TeX et PHP, pour les connaisseurs. Le programme précédent peut s'écrire à l'aide de Ltac comme suit.

Definition pred : forall n : nat, {m : nat | n = 0 \/ n = S m}. Proof. intros n; destruct n. + exists 0; left; reflexivity. + exists n; right; reflexivity. Defined.

Le terme produit par cette séquence de commandes est le même que celui qu'on a écrit à la main auparavant. L'avantage de Ltac est qu'il permet d'écrire des morceaux de preuves aisément, au prix d'un moins grand contrôle sur le terme produit.

Agda, le seul autre assistant de preuve mainstream aussi proche de l'idée de correspondance preuve-programme, a fait un choix différent, qui est de n'avoir qu'un langage de termes (et pas de méta-programmes), et d'essayer de le rendre le plus propre possible pour permettre de l'utiliser directement. Cela a conduit à des idées intéressantes, mais pour l'instant le résultat est moins adapté à l'automatisation des preuves et donc aux formalisations de grande ampleur. (Les utilisateurs Agda essaient de compenser par un mode Emacs de folie qui ré-écrit les termes de preuve pour eux; il y a du bon et du moins bon dans cette approche.)

Un langage exotique

En tant que langage de programmation, Coq fait malgré tout figure d'alien aux yeux des programmeurs lambda.

En premier lieu, Coq est un langage de programmation purement fonctionnel, et ce, encore plus que Haskell. Il n'y a en effet aucun effet de bord possible et cela inclut aussi bien la mémoire mutable que l'affichage sur la ligne de commande. Eh oui, on ne peut même pas écrire le Hello World des familles en Coq ! Imaginez le désarroi de ses promoteurs quand on le leur demande… Pas non plus d'exceptions, de primitives systèmes, etc. On peut cependant toujours se débrouiller en encodant ces effets dans une monade, comme en Haskell.

Pire encore, quand nous disons que Coq est plus pur que Haskell, cela n'est pas pour rien. Il est en effet impossible en Coq d'écrire un programme qui ne termine pas. Coq est très strict sur les fonctions qu'il accepte et demande souvent un peu de gymnastique au programmeur. Le point positif de cette rigidité est que les programmes sont garantis de respecter leur spécification. En un sens, Coq rend vrai l'adage souvent appliqué à OCaml et à Haskell : « quand ça compile, c'est que ça marche ».

Une conséquence inattendue de ce fait : Coq n'est pas Turing-complet. Il existe donc des programmes qu'on ne peut pas écrire en Coq. Ce n'est pas un bug, c'est une feature ! Cette restriction permet de passer outre les limitations dues au théorème d'incomplétude de Gödel  —  mais complique l'écriture de programme dont on ne sait pas prouver la terminaison ou la productivité[3].

Le futur ?

Les gens qui travaillent sur les assistants de preuves imaginent un monde où les mathématiciens et mathématiciennes travaillent directement avec des assistants de preuve et où l'on n'a plus jamais besoin de corriger un résultat qui s'avère faux après sa publication. C'est encore une utopie, même si les mathématiciens sont de plus en plus nombreux à prendre ces outils au sérieux. Aujourd'hui, les assistants de preuves restent trop difficiles à utiliser pour des « mathématiques de tous les jours » et il faudra encore des efforts de simplification et d'ergonomie pour rendre cette idée réaliste.

Des bibliothèques importantes de mathématiques formalisées existent déjà (par exemple le journal Formalized Mathematics présente les nombreux résultats formalisés dans la Mizar Mathematical Library), mais elles soulèvent de nombreuses questions d'ingénérie des preuves et d'inter-opérabilité entre les différents langages de description de preuves.

La formalisation assistée par ordinateur laisse malgré tout entrevoir la possibilité de faire des mathématiques que l'esprit humain ne saurait appréhender aisément aujourd'hui. Ainsi, une des barrières à la preuve, aussi bien du théorème des quatre couleurs que de la conjecture de Kepler, était la quantité dantesque de cas particuliers à vérifier à la main, que l'ordinateur a pu traiter rapidement. Une nouvelle ère des mathématiques est probablement en train de s'ouvrir sous nos yeux.

Par ailleurs, on voit fleurir des outils permettant de vérifier formellement que les programmes informatiques respectent une spécification. Alors qu'on peut imaginer que les preuves mathématiques aient toute vocation à être vérifiées, personne ou presque n'espère réellement que tous les logiciels écrits soient un jour prouvés corrects. D'une part, certains logiciels n'ont pas de spécification claire, stable ou que l'on sait exprimer (comment spécifier un économiseur d'écran ?) ; d'autre part, les facteurs économiques jouent contre les preuves formelles. En effet, même si la preuve formelle devenait un jour la façon la plus économique d'éviter les bugs dans les logiciels, cela restera toujours plus difficile et donc plus coûteux que d'écrire du logiciel buggué. On peut cependant rêver au fait que, d'ici quelques dizaines d'années, le dessous de l'iceberg (les bibliothèques standards, compilateurs, runtime, noyaux de système d'exploitation ou navigateurs web) sur lequel reposent les programmes grand-publics soient spécifiés le plus précisément possible et prouvés corrects par rapport à cette spécification.

L'assistant de preuve Coq, en permettant à chacun de se former à la preuve formelle (ou à la preuve tout court) et de se lancer dans des formalisations qui commencent à être de grande ampleur, est un des outils phare de cette (r)évolution.

Notes

[0] Plus précisément, c'est en cherchant à modéliser ce sous-système dans Coq que Masashi Kikuchi a découvert ce défaut de conception. La démarche de la preuve formelle revient à soumettre tout un système à un tyran de rigueur insatiable. Il révèle ses erreurs, ses points faibles et force l'utilisateur à une compréhension au centimètre près. Si la présentation n'est pas structurée et élégante, la preuve en est d'autant plus difficile. Les assistants de preuves poussent à la simplicité et permettent souvent la production de documents pédagogiques remarquables, car leur clarté vient non des détails qu'ils passent sous le tapis, mais de la rigueur qui leur a été imposée. C'est souvent dans un article de la forme Comment prouver formellement X que vous trouverez l'exposition la plus claire du sujet X.

[1] Peut-être presque autant que la sortie de l'iPhone n + 1, pour un n bien choisi.

[2] Je recommande la lecture de la captivante BD Logicomix à ceux qui sont intéressés.

[3] Dans les faits, 99,99% des programmes imaginables peuvent s'écrire en Coq. On dit aussi souvent que cela empêche aussi d'écrire un interpréteur de Coq en Coq, mais cela est plus compliqué en pratique. On pourrait écrire une fonction qui effectue une étape de réduction (et laisser l'utilisateur pédaler), ou imaginer bootstrapper à l'aide d'un axiome bien choisi.

[4]Quand un mathématicien déclare son amour à git et à l'esprit du libre.

Télécharger ce contenu au format Epub

Lire les commentaires

Atelier Musique Assistée par Ordinateur le 14 mars 2015 à Argenteuil

28 janvier, 2015 - 09:43

Le Gull StarinuX vous convie à l'atelier « La musique assistée par ordinateur (MAO) sous GNU/Linux », qui aura lieu le samedi 14 mars 2015 de 9h à 18h, aux Bains-douches Silicone-banlieue, 9 rue de Calais, 95018 Argenteuil (5 min de la gare de d'Argenteuil, directe 10 min St Lazare).

Vous êtes musicien(ne), vous souhaitez vous enregistrer, créer vos propres compilations, arranger vos morceaux… et librement avec un logiciel de MAO sous Linux ? On dit souvent que la musique assistée par ordinateur, c'est le domaine réservé de Windows et MacOS. En fait, non : GNU/Linux aussi c'est bien pour faire de la musique ! Alors venez le découvrir et l'apprendre avec des outils Libres !

Cet atelier sera animé par Yann Collette, un musicien féru de Linux. Le programme prévoit d'aborder plusieurs logiciels musicaux, comme Guitarix, Ardour ou Mixxx.

Comme à l'accoutumée pour les ateliers StarinuX, il vous est demandé de vous inscrire sur la page prévue à cet effet, sachant que la participation (annuelle) de 20 euros est valable pour plus de 17 ateliers !

Concernant les commodités, un bar est disponible sur place et lunch sera facile à la pause de midi.

Au plaisir de vous rencontrer le 14 mars !

Télécharger ce contenu au format Epub

Lire les commentaires

Musique libre : Moquettes&Tapis par Sebkha-Chott

28 janvier, 2015 - 00:03

Sebkha-Chott est un groupe de musique libre, faite avec des logiciels libres.

Le groupe, qui se compose trois musiciens et de beaucoup de machines, a été en grande partie renouvelé avec l'arrivée d'un nouveau batteur et d'un nouveau guitariste, bassiste, ainsi que divers objets sonores. Il est notamment doté d'une guitare DIY rotative assez singulière.

"Moquettes&Tapis", leur 6ème album est annoncé en prévente pour le 1er avril 2015.

Les prémices de ce nouvel album ont pu être découvertes l'été dernier à l'occasion du concert des RMLL 2014 à Montpellier. Ce nouvel album est intitulé "Moquettes&Tapis", est dans la ligne du précédent album ("the Ne[xxx]t Epilog") : mélange d'instruments électriques et électroniques, rock parfois très dur, rythmes fouillés… avec toutefois de nouveaux musiciens et de nouvelles compositions (Sebkha-Chott ayant habitué ses fans aux multiples orchestrations radicalement différentes des mêmes morceaux).

Le groupe finance en partie sa production par la pré-commande de CD. L'album sera placé comme toujours sous licence libre (licence art libre 1.3 pour la partie artistique et GPL pour la technique).

"Moquettes&Tapis" bénéficie de la participation de nombreux invités dont les plus illustres sont :

  • Ike Willis (Frank Zappa),
  • Yom (Yom),
  • Fred Gastard (Musiques à Ouïr, Brigitte Fontaine, Melosolex, Journal Intime),
  • Mathieu Metzger (Klone, Marc Ducret, Louis Sclavis, Anthurus d'Archer…)
  • Gabriel Yacoub (Malicorne)

Un clip a été réalisé pour l'occasion, pour donner un avant goût de ce sixième album.

Télécharger ce contenu au format Epub

Lire les commentaires

Mettre en place un serveur Jabber avec du TLS et du Forward Secrecy

27 janvier, 2015 - 10:19

J'ai publié il y a quelques mois un tuto pour mettre en place "facilement" un serveur XMPP/Jabber avec Prosody et du SSL/TLS plutôt bien configuré sous Debian, j'ai eu pas mal de retours positifs depuis et je pense qu'il pourrait intéresser d'autres personnes.

Sommaire Installation

Pour installer Prosody sous Debian, il suffit de rajouter le dépôt dans son sources.list, on peut utiliser la ligne suivante pour le faire. Elle permet de simplifier énormement la manipulation (pour les détails, c'est ici) :

echo "deb http://packages.prosody.im/debian $(lsb_release -sc) main" | sudo tee -a /etc/apt/sources.list

Puis on ajoute la clé GPG du dépôt :

wget https://prosody.im/files/prosody-debian-packages.key -O- | sudo apt-key add -

On met à jour les dépôts, puis on installe Prosody :

aptitude update && aptitude install prosody

Le paquet lua-sec dans Debian est légèrement… ancien, si vous voulez les derniers algorithmes de chiffrement et que le Perfect Forward Secrecy soit pris en compte, il faut le mettre à jour.

Sur Debian Wheezy :

echo "deb http://ftp.debian.org/debian wheezy-backports main" >> /etc/apt/sources.list aptitude update && aptitude -t wheezy-backports install lua-sec-prosody Configuration

L'ensemble de la configuration se fait dans un seul fichier :

/etc/prosody/prosody.cfg.lua

La première partie est commune à l'ensemble des VirtualHosts que vous allez mettre en place. Ce qui sera écrit sous chaque VirtualHost "exemple.com" (en bas) sera propre à chaque VirtualHost.

Ce qui veut dire que si vous mettez votre configuration SSL dans la première partie, elle sera commune à tous les VirtualHosts. Faites attention aux répercussions que ça peut avoir ;-)

La première brique

Ouvrez le fichier avec votre éditeur préféré (pour moi ça sera vim)

vim /etc/prosody/prosody.cfg.lua

Il faut modifier/compléter les champs suivants (avec évidemment vos informations à la place de example.tld) :

Qui est administrateur du serveur (tout en haut du fichier) ?

admins = {"admin@exemple.tld"}

Voulez-vous autoriser les inscriptions sur votre serveur ? À moins de savoir ce que vous faites, je vous conseille grandement de le mettre sur false afin d'éviter de servir aux spammeurs et aux bots.

allow_registration = false;

Quel domaine voulez-vous utiliser (tout en bas du fichier) ? N'oubliez pas de changer example.tld pour votre domaine.

VirtualHost "example.tld" enabled = true Les logs

C'est très important (et déjà partiellement configuré). Ils permettent de trouver où est le problème quand ça ne marche pas (pour plus de détails sur la configuration : logging), la modification par rapport au fichier original consiste à mettre le prosody.log en warn et non plus en info et à faire la même manipulation pour le syslog :

log = { warn= "/var/log/prosody/prosody.log"; error = "/var/log/prosody/prosody.err"; { levels = { "error" }; to = "syslog"; };

Si vous avez un problème à régler, je vous conseille de rechanger le premier warn pour debug, puis de redémarrer prosody (via la commande prosodyctl restart), vous aurez alors toutes les informations qu'il vous faut dans /var/log/prosody/prosody.log et bien plus encore pour trouver d'où ça vient.

Un minimum de sécurité

De base, Prosody enregistre les mots de passe des comptes en clair sur le serveur, pour qu'ils soient hashés, il faut modifier la ligne authentication = "internal_plain" par la ligne suivante :

authentication = "internal_hashed" prosodyctl

Prosody vient avec une commande qui aide à communiquer avec lui facilement : prosodyctl, et qui s'utilise sous la forme suivante :

prosodyctl COMMAND [OPTIONS]

COMMAND peut être :

  • adduser - exemple@exemple.tld - crée le compte utilisateur
  • passwd - exemple@exemple.tld - configure le password de l'utilisateur
  • deluser - exemple@exemple.tld - supprime l'utilisateur
  • start - démarre Prosody
  • stop - arrête Prosody
  • restart - redémarre Prosody
  • reload - recharge la configuration de Prosody
  • status - indique le status actuel de Prosody

Plutôt utile non ? :]

Nous allons ajouter un utilisateur (il vous demandera un mot de passe), puis nous rechargerons la configuration pour prendre en compte les changements (exemple.tld doit être le même que vous avez mis pour votre VirtualHost) :

prosodyctl adduser exemple@exemple.tld prosodyctl reload

Et là, c'est l'instant de plaisir, si vous essayez de vous connecter avec un client jabber (comme pidgin), ça devrait se connecter. Si ce n'est pas le cas (faire dans l'ordre) :

  • voir les logs de prosody,
  • voir les logs de votre client jabber,
  • changer les logs de prosody de info à debug,
  • boire un thé (ou une bière)
  • vérifier votre firewall,
  • rebrancher la box,
  • reprendre un thé,
  • changer de FAI.
Les modules

Comme vous pouvez le voir dans le fichier de configuration, il y a déjà un certain nombre de modules qui sont activés par défaut (roster, saslauth, tls, posix…). ils sont dans la partie modules_enabled = { }.

Si je vous parle de ça, vous vous doutez que ce n'est pas pour rien, il existe beaucoup de modules, dont un pour Tor :

Chiffrons tout pour tout le monde Manifesto - *[A public statement about ubiquitous encryption on the XMPP network.](https://github.com/stpeter/manifesto)*

Si vous ne connaissez pas (ou mal) le SSL/TLS, je ne peux que vous conseiller d'attaquer le sujet par la conférence de Benjamin Sonntag dans le cadre du cycle de conférence « Il était une fois Internet ».

Création du certificat Si votre certificat n'est pas reconnu « valide » par votre client jabber, par exemple en cas de certificat auto-signé, il demandera autorisation pour l'utiliser. La méthode simple (et vraiment rapide)

La méthode « simple » consiste à la création d'un certificat auto-signé avec l'aide de prosodyctl :

# exemple.tld étant le domaine que vous avez mis dans prosody.cfg.lua prosodyctl cert generate exemple.tld
  • vérifier l'emplacement des certificats une fois qu'ils sont générés
  • vous pouvez les bouger dans /etc/prosody/certs/ si vous avez envie (on part du principe que c'est le cas pour la suite)
  • N'oubliez pas les deux lignes suivantes :
chmod 600 /etc/prosody/certs/exemple.tld.key chown prosody:prosody /etc/prosody/certs/exemple.tld.key chown prosody:prosody /etc/prosody/certs/exemple.tld.crt

Pour aller plus loin :

La méthode un peu moins simple mais qui est vachement mieux

Nous allons créer ce dont nous avons besoin en faisant une requête à startssl.com :

openssl req -sha256 -out /etc/prosody/certs/exemple.csr -new -newkey rsa:2048 -nodes -keyout /etc/prosody/certs/exemple.key

Cette commande génère (openssl req -out) une CSR (-new) ainsi qu'une nouvelle clé RSA de 2048 bits (-newkey rsa:2048) qui ne sera pas chiffrée (-nodes). Si vous voulez encore plus de détails, c'est sur openssl.org.

Je vous laisse sur startssl.com réaliser les différentes étapes pour s'inscrire (bonne chance !), il faut choisir la première formule (celle qui est gratuite). Après la création de votre compte, la validation de votre nom de domaine, etc. etc. nous pouvons passer à la suite.

  • Après votre authentification sur le site, cherchez l'onglet « Certificates Wizard » qui se trouve normalement vers la gauche de votre écran,
  • il vous demande alors pourquoi vous voulez un certificat ("Select Certificate Purpose"), vous choisissez donc XMPP (jabber) SSL/TLS certificate,
  • le site vous demande de créer une clé privée ("Generate Private Key") : VOUS NE LE FAITES PAS !, vous appuyez au contraire sur skip (nous avons créé la clé privée quelques lignes au dessus),
  • vous arrivez maintenant sur la page de demande de certificat ("Submit Certificate Request (CSR)"), toujours dans un terminal, vous devez taper la commande suivante :
cat /etc/prosody/certs/exemple.csr

Cette commande vous donnera un résultat qui devrait ressembler à

-----BEGIN CERTIFICATE REQUEST----- MIIChjCCAW4CAQAwQTELMAkGA1UEBhMCRlIxCzAJBgNVBAgMAkZSMQswCQYDVQQH DAJGUjELMAkGA1UECgwCRlIxCzAJBgNVBAsMAkZSMIIBIjANBgkqhkiG9w0BAQEF AAOCAQ8AMIIBCgKCAQEAsoJcj6/bwl9naKG9C9seKt4HjBicV5o96zqoO0YxtJAe X9k2t4KTp0CrzQ85c9DfggY8oAMq/DX/xRFL0cPxamxSwwW5ttVoBQ04wBWDhjEo a2ixpe5UMmfakuY3Q56HsIbhh7Vo4RZS1OtPOv7E2J0CfDVUhrNCpDjZbtM8akTE 9P86BkXdroJgU8tfwONMFDBF2K8ElhN6mqftb89KGIUpgm1fcDq8woRpnFER7A3H OwfCfnlkLrtMWVca1smEWnlutBKw6cgk6uSMK9V9/Y44wMKZHoOrOQE0R26+MGrA MLhprqPaANIvhamq+tSsSASYZDeajDS3R1JWX188awIDAQABoAAwDQYJKoZIhvcN AQEFBQADggEBAHYSpBxHhRP87qmWNqp9Sf8dYz3oQfJLA2cLpQV2MOIfFW0mmOyz JG6TVISKVmiEHZtHqgW4TL3BSKBAWENBM8mjAjmxXCmy2MBSWBVhDVaGz4w+x3hO UMtNMubYxkkc/xgX5vwbuReH6y1sbkMUQm1UETb6Fnmm8dyDzwPI0zV+NdzUqqhI ARjMM2RrwPH7QZ2lSAOiB/X+fXKhwMSg0qUExYiln20JKBi6f58GdyOu6Hp/Fi+m r8xnIcnZ2ZIIyjh4B2bfAfybTOWHHRtOaI9yH8pTP3HnKqgbtxZJYqioTAAAQxjQ hFmXThFFrfhTDnqJ0Fc+bjcoiLoy46FtLz8= -----END CERTIFICATE REQUEST-----

Copiez-le dans la fenêtre en bas (de -----BEGIN CERTIFICATE REQUEST----- à -----END CERTIFICATE REQUEST----- !).
Vous aurez alors votre certificat peu de temps après, transférez-le sur votre serveur, dans /etc/prosody/certs/ avec comme nom « exemple.tld.crt ».

Création d'un certificat chaîné

Pour créer un certificat chaîné, faites la manipulation suivante (startssl.com vous donne les liens vers ces deux certificats juste au dessus du bouton finish »» de la page Save Certificate) :

  • télécharger le certificat intermédiaire de startssl :
wget https://www.startssl.com/certs/sub.class1.server.ca.pem
  • puis le certificat root :
wget https://www.startssl.com/certs/ca.pem
  • puis on forge le certificat chaîné (ne pas oublier les 2 >>) :
cat sub.class1.server.ca.pem >> /etc/prosody/certs/exemple.tld.crt cat ca.pem >> /etc/prosody/certs/exemple.tld.crt Génération du dhparam

Création du dhparam (prosody.im/dhparam) :

openssl dhparam -out /etc/prosody/certs/dh-2048.pem 2048

Java ne peut pas utiliser un dhparam supérieur à 1024 bits, ce qui empêche d'utiliser par exemple le logiciel Jitsi. Pour éviter cela (c'est tout de même un client grandement utilisé), on peut générer un dhparam de 1024 bits avec la commande suivante (ne pas oublier de modifier la configuration pour remplacer dh-2048.pem par dh-1024.pem) :

openssl dhparam -out /etc/prosody/certs/dh-1024.pem 1024 Configuration du SSL/TLS

On retourne dans /etc/prosody/prosody.cfg.lua :

ssl = { key = "/var/lib/prosody/exemple.tld.key"; certificate = "/var/lib/prosody/exemple.tld.cert"; dhparam = "/etc/prosody/certs/dh-2048.pem"; options = { "no_sslv2", "no_sslv3", "no_ticket", "no_compression", "cipher_server_preference", "single_dh_use", "single_ecdh_use" }; ciphers = "EECDH+ECDSA+AESGCM EECDH+aRSA+AESGCM EECDH+ECDSA+SHA384 EECDH+ECDSA+SHA256 EECDH+aRSA+SHA384 EECDH+aRSA+SHA256 EECDH EDH+aRSA !RC4 !aNULL !eNULL !LOW !3DES !MD5 !EXP !PSK !SRP !DSS"; }
  • c2s signifie « Client TO Server »,
  • s2s signifie « Server TO Server ».
c2s_ports = { 5222 } s2s_ports = { 5269 } c2s_require_encryption = true s2s_require_encryption = true s2s_secure_auth = false allow_unencrypted_plain_auth = false;

s2s_secure_auth est sur false pour les raisons suivantes (TL;DR: possibilité de certificat auto-signé en face). Peut marcher avec s2s_auth_fingerprint mais c'est douloureux.

Les options s2s_secure_domains et s2s_insecure_domains peuvent aussi vous intéresser, surtout si vous voulez parler avec des personnes qui sont sur gmail (ce qui veut dire que ça ne sera pas chiffré).

Concernant la ciphersuite, le choix par défaut de Prosody est déjà pas mal :

ciphers = "HIGH+kEDH:HIGH+kEECDH:HIGH:!PSK:!SRP:!3DES:!aNULL";

Il faut tout de même enlever RC4 et eNULL, et tant qu'à faire, autant faire une liste de ciphers avec seulement du PFS (Perfect Forward Secrecy) (c'est à mettre dans le bloc ssl { }) :

ciphers = "EECDH+ECDSA+AESGCM EECDH+aRSA+AESGCM EECDH+ECDSA+SHA384 EECDH+ECDSA+SHA256 EECDH+aRSA+SHA384 EECDH+aRSA+SHA256 EECDH EDH+aRSA !RC4 !aNULL !eNULL !LOW !3DES !MD5 !EXP !PSK !SRP !DSS"; DNS

N'oubliez pas d'ajouter les enregistrements SRV dans vos DNS :

_xmpp-client._tcp.jabber IN SRV 0 5 5222 host.exemple.com. _xmpp-server._tcp.jabber IN SRV 0 5 5269 host.exemple.com. Firewall

En cas de firewall, il faut ouvrir les ports 5269 et 5222 (IN et OUT) en TCP. La configuration pour iptables donne ceci :

iptables -I INPUT -p tcp --dport 5269 -j ACCEPT iptables -I OUTPUT -p tcp --sport 5269 -j ACCEPT iptables -I INPUT -p tcp --dport 5222 -j ACCEPT iptables -I OUTPUT -p tcp --sport 5222 -j ACCEPT Test

Comme SSLLabs pour tester le SSL/TLS sur les serveurs webs, il existe xmpp.net pour les serveurs XMPP. Je vous conseille vivement de tester votre site !

Il faut toujours vérifier, même quand on pense pouvoir avoir confiance.

Si vous vous demandez comment améliorer votre note, c'est là : xmpp.net/about.

Télécharger ce contenu au format Epub

Lire les commentaires

Revue de presse de l'April pour la semaine 4 de l'année 2015

27 janvier, 2015 - 09:11

La revue de presse de l'April est régulièrement éditée par les membres de l'association. Elle couvre l'actualité de la presse en ligne, liée au logiciel libre. Il s'agit donc d'une sélection d'articles de presse et non de prises de position de l'association de promotion et de défense du logiciel libre.

Sommaire

[L'Informaticien] Interdiction des machines à voter? Une proposition de loi est sur la table

Par Emilien Ercolani, le vendredi 23 janvier 2015. Extrait:

«Marginal», «en sursis», «dysfonctionnements»… Le député centriste de la Loire François Rochebloine n'a pas de mots assez durs pour décrire les machines à voter, qu’il souhaite définitivement interdire dans une proposition de loi déposée le 21 janvier.

Lien vers l'article original: http://www.linformaticien.com/actualites/id/35507/interdiction-des-machines-a-voter-une-proposition-de-loi-est-sur-la-table.aspx

Et aussi:

[Le Monde Informatique] L'UE doit-elle obliger les géants de l'Internet à céder leurs clés de chiffrement

Par Serge Leblal, le jeudi 22 janvier 2015. Extrait:

La montée en puissance du terrorisme en Europe relance le débat sur le chiffrement des communications et la création de backdoors réservés aux forces de l'ordre européenne. Le coordinateur antiterrorisme de l'UE, Gilles de Kerchove, demande sans détour un accès aux clefs de chiffrement des géants de l'Internet.

Lien vers l'article original: http://www.lemondeinformatique.fr/actualites/lire-l-ue-doit-elle-obliger-les-geants-de-l-internet-a-ceder-leurs-cles-de-chiffrement-59993.html

Et aussi:

[Libération.fr] Le lobby anti-DRM s’étoffe

Par Camille Gévaudan, le jeudi 22 janvier 2015. Extrait:

Le journaliste et auteur de science-fiction Cory Doctorow est un fervent défenseur du partage en ligne et un grand penseur des technologies, qui ne doivent pas selon lui brider l’accès du public à la culture. On ne s’étonne donc pas de le voir rejoindre l’Electronic Frontier Foundation (EFF) en tant que consultant spécial chargé du lobby anti-DRM.

Lien vers l'article original: http://ecrans.liberation.fr/ecrans/2015/01/22/le-lobby-anti-drm-s-etoffe_1186627

[Numerama] Droit d'auteur: les propositions du rapport de l'eurodéputée pirate Julia Reda

Par Guillaume Champeau, le lundi 19 janvier 2015. Extrait:

L'eurodéputée pirate Julia Reda présentera mardi en commission son rapport sur la mise en oeuvre de la directive de 2001 sur le droit d'auteur dans la société de l'information, dans lequel elle plaide pour un large assouplissement des conditions de réutilisation des oeuvres. Mais sans remettre en cause les fondements du droit d'auteur ni exiger de révolution.

Lien vers l'article original: http://www.numerama.com/magazine/31920-droit-d-auteur-les-propositions-du-rapport-de-l-eurodeputee-pirate-julia-reda.html

Et aussi:

[FrenchWeb] Comaking: les start-up doivent-elles adopter la tendance?

Par Camille Adaoust, le lundi 19 janvier 2015. Extrait:

Le comaking, un phénomène qui nous vient des Etats-Unis. Il s’installe petit à petit en France. Paris, Lyon, Marseille, Bordeaux, dans les grandes villes, ces espaces de production partagés prennent leurs marques.

Lien vers l'article original: http://frenchweb.fr/comaking-les-start-up-doivent-elles-adopter-la-tendance/179886

[Next INpact] Plan e-éducation: davantage de numérique dans les enseignements à partir de 2016

Par Xavier Berne, le lundi 19 janvier 2015. Extrait:

À l’occasion du débat organisé mercredi dernier à l’Assemblée nationale à propos de la stratégie numérique de la France, la secrétaire d’État au Numérique Axelle Lemaire est revenue sur le grand «plan pour le numérique à l’école» promis l’été dernier par François Hollande. Non sans une certaine impression de réchauffé…

Lien vers l'article original: http://www.nextinpact.com/news/91755-plan-e-education-davantage-numerique-dans-enseignements-a-partir-2016.htm

Et aussi:

[Le Monde.fr] Numérique: des images deux fois moins lourdes

Par David Larousserie, le lundi 19 janvier 2015. Extrait:

Un ingénieur français a développé un nouveau format de compression plus efficace que l’incontournable JPEG.

Lien vers l'article original: http://www.lemonde.fr/sciences/article/2015/01/19/des-images-deux-fois-moins-lourdes_4559136_1650684.html

Télécharger ce contenu au format Epub

Lire les commentaires

FOSDEM 2015 ce week-end du 31 janvier à Bruxelles

27 janvier, 2015 - 08:26

C'est devenu une habitude, le premier week-end de février des milliers de développeurs se réunissent dans le cadre du FOSDEM.

Le FOSDEM (Free and Open Source software Developers' European Meeting) est le plus grand congrès gratuit pour les développeurs du Libre, organisé uniquement par des bénévoles.

Le congrès se déroule à Bruxelles dans les locaux de l'ULB sur le campus du Solbosch.

Programme Keynotes Main tracks Developer rooms Lightning talks

Les lightning talks sont de courtes présentations de 15 minutes sur d'un projet pour donner envie aux gens d'y participer. Il y a quarante-et-une présentations de prévues.

Examens

En plus des certifications Linux Professional Institute (LPI), une certification BSD et une certification LibreOffice sont disponibles.

Et, si vous avez un peu de temps disponible, venez donner un coup de main dans l'organisation : il y a des tâches de tout niveau.

Télécharger ce contenu au format Epub

Lire les commentaires

Sortie de vera++ 1.3.0

24 janvier, 2015 - 18:05

Jeudi 22 janvier est sortie la version 1.3.0 de vera++ : programme permettant de faire des vérifications de style de code sur du C++. Il est scriptable et permet également la refactorisation de code.

Vera++ est multi-platforme (Windows, GNU/Linux, Mac, FreeBSD, et même GNU/Hurd au moins jusqu'en 1.2.1).

La version 1.3.0 arrive avec plusieurs nouveautés sympathiques. Notamment l'introduction de Python et Lua dans la liste des langages permettant de scripter vera++, en plus du Tcl initialement disponible. Plusieurs corrections de bugs, l'amélioration des exclusions ainsi que la gestion des profils viennent également avec cette nouvelle mouture de vera++.

Vera++ fait aussi partie des plugins disponibles dans le logiciel de contrôle de qualité SonarQube.

Le paquet Debian devrait prochainement être mis à jour. La 1.2.1 est pour l'instant sélectionnée pour Jessie (8). La 1.3.0 devrait arriver dans Stretch (9) après le freeze.

Télécharger ce contenu au format Epub

Lire les commentaires

Le langage Rust en version 1.0 alpha, on arrête de tout casser !

24 janvier, 2015 - 17:55

Rust est un langage de programmation conçu pour répondre aux problématiques modernes des gros logiciels clients et serveurs utilisant Internet, en particulier la sécurité, le contrôle de la mémoire et la parallélisation.

Comme le rappelle la rétrospective 2014, Rust est un sujet qui a été beaucoup traité l’année précédente. N’oublions pas non plus l’expérimentation avec Rust et ibus qui a fait l’objet d’une dépêche en octobre dernier.

Avec un peu de retard par rapport au communiqué lors de la sortie de la version 0.12, mais comme annoncé le 12 décembre, c'est près de 3 ans après la version 0.1 que l'équipe de Rust publie la version alpha de la version 1.0 du langage ce 9 janvier.

Ça y est, Rust 1.0 alpha est sorti ! Cela signifie que le langage et les bibliothèques ne recevront plus de changements majeurs.

Selon le tableau de bord de stabilité du projet, la bibliothèque standard a désormais 44% de code marqué stable (c’est-à-dire dont l’API ne changera pas) et 52% non stable (2% non marqué). Cela montre une très grande progression par rapport à la dernière version d'octobre 2014 où le code stable représentait seulement 2%, le non stable 12% et 77% pour l'expérimentale, le reste étant déprécié ou non marqué.

Principaux changements

Il y a plus de 2400 modifications, incluant les corrections de bogues, dans cette version alpha, l'ensemble des changements est fourni dans les notes de version.
Le travail a porté principalement sur deux modules : gestion des chemins de fichiers et entrées-sorties. Plusieurs fonctionnalités ont été implémentées dans le langage et la bibliothèque standard. Dans le langage ont été ajoutés la gestion des types de taille dynamique : les « multidispatch traits ». Les conventions de codage ont été appliquées dans la bibliothèque standard.

Les types à taille dynamique (DSTs pour Dynamically-sized types) sont des types dont la taille est fixe mais inconnue à la compilation. Ils souffraient de grosses limitations dans les précédentes versions de Rust, ils sont maintenant largement intégrés dans le langage.

Les types int et uint (les équivalents Rust de intptr_t et uintptr_t en C++) ont été déclarés obsolètes en faveur des nouveaux types isize et usize. Ce renommage a été fait dans le but d’encourager l’utilisation des types à taille fixe (actuellement i8, i16, i32 et i64) pour assurer un fonctionnement cohérent entre différentes plateformes et prendre moins de mémoire. Les noms int et uint pouvaient faire croire à ceux venant du C/C++ qu'il s'agissait des types "par défaut" de Rust.Ce n'est pas le cas: i32 est le type par défaut pour les entiers (f64 pour les flottants), tandisque int et uint seront totalement supprimés d’ici la bêta. Plus d’infos

Une clause where a été ajoutée pour faciliter la déclaration des contraintes de type lors de la déclaration de traits. Pour le développeur, le changement le plus visible est :

impl<K:Hash+Eq,V> HashMap<K, V> { […] } // qui devient impl<K,V> HashMap<K, V> where K : Hash + Eq { […] }

Cela a également permis la suppression de plusieurs traits de la bibliothèque standard, ainsi que quelques autres simplifications bienvenues.

Le système de macro a été largement amélioré pour le préparer à la sortie de la 1.0. C’est un travail de nettoyage, d’arrondissage des angles, d’amélioration de la syntaxe et de modifications de quelques comportements problématiques.

La documentation a bénéficié des efforts portés : elle traite une plus grande partie de l'API, avec plus d'exemples et plus d'explications. Les différents guides ont été rassemblés dans le livre. Le site Rust by Example est désormais maintenu par l'équipe Rust.

Des chiffres ! Projets utilisant Rust

OpenHub tient des statistiques sur l'utilisation de Rust dans les projets qu'il recense, comme pour tout autre langage. On peut ainsi voir que le nombre de personnes qui modifient du code Rust est relativement faible, mais augmente (de 165 projets pour la version 0.12 à 177 dans les projets recensés et 1 025 090 lignes de code). Par ailleurs, le nombre de projets recensés sur GitHub passe de 3262, lors de la sortie de la 0.12, à 4892.

Évènements

De nombreux évènements sont organisés autour de Rust. La rencontre parisienne, régulière, se tient tous les 3è lundis du mois dans les locaux de Mozilla.

Des rencontres ont aussi eu lieu à Lisbonne (16 octobre), Milan (11 novembre), San Francisco (6 novembre et 18 décembre), Seattle (13 octobre, 10 novembre, 8 décembre et 12 janvier).

Liens ''This week in Rust''

Si vous voulez suivre le mouvement de tout ce qui se passe à propos de Rust sans avoir à lire le détail des commits, des annonces sur la liste de diffusion, de Reddit ou de Twitter, le blog This Week in Rust fait une synthèse hebdomadaire des nouveautés et actualités autour de Rust :

Notes de version

Contrairement aux précédentes versions, le fichier RELEASES.md contient directement toutes les informations détaillées sur cette version.

Conclusion

Les exécutables d'installation sont disponibles pour les systèmes Linux, Windows, Mac OS X et le code source reste disponible sur GitHub. À noter que l'équipe de développement de Rust recommande d'utiliser les compilations quotidiennes (''nightly builds'') afin de profiter de tous les changements qui se produiront pendant la phase alpha.
La première sortie Bêta est prévue pour la semaine du 16 février 2015, elle comprendra une réécriture de la bibliothèque std::io.

Télécharger ce contenu au format Epub

Lire les commentaires