Linux France

S'abonner à flux Linux France
Mis à jour : il y a 2 heures 11 min

Jorani passe la troisième

Jeudi 29 Janvier

Jorani est un projet de LMS (Leave Mananagement 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

Mercredi 28 Janvier

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

Mercredi 28 Janvier

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 d'apprentissage de la logique dans l'enseignement supérieur.

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.

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é 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 accepter des programmes incorrects (si on ne veut prévenir l'utilisateur que 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 :

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

Mercredi 28 Janvier

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 compilation, 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

Mercredi 28 Janvier

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

Mardi 27 Janvier

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</pre> 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

Mardi 27 Janvier

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

Mardi 27 Janvier

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

Samedi 24 Janvier

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 !

Samedi 24 Janvier

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

1er festival du domaine public, du 16 au 31 janvier 2015 à Paris

Samedi 24 Janvier

Le droit d'auteur n'est finalement qu'une courte exception temporaire au domaine public. Le destin de toute création est de rejoindre un jour le domaine public. C'est pour rappeler, défendre et fêter cela que se déroule actuellement à Paris le 1er festival du domaine public.

Il est à l'initiative de Véronique Boukali (fondatrice de Romaine Lubrique) et Alexis Kauffmann (fondateur de Framasoft) et bénéficie du soutien et de l'implication d'une cinquantaine de structures dont Wikimedia France, SavoirsCom1, La Quadrature du Net, OKF France, CC France, OSM France.

Pourquoi en janvier ? Parce que c'est le 1er de ce mois qu'entrent ensemble dans le domaine public les œuvres des auteurs morts 70 ans auparavant. Et cette année on a du beau monde : Munch, Kandinsky, Mondrian, Maillol, Giraudoux…

La technique permet aujourd'hui comme jamais la libre circulation de la culture. L'interdit est avant tout juridique à cause du droit d'auteur. Or, avec les œuvres du domaine public, on a certes attendu longtemps mais on a enfin le droit d'utiliser, partager, diffuser, modifier, remixer… sans demander autorisation ni s'acquitter de droits. Alors profitons-en !

Du 16 au 31 janvier à Paris et sa région, auront lieu, dans 20 lieux différents, 30 événements, tous libres et gratuits, pour s'informer, se former, se cultiver, pour numériser et créer ensemble, pour aborder le domaine public dans toutes ses formes et sous tous les angles.

Petite sélection « spécial DLFP » :
- Grande fête du Remix, le samedi 24 janvier à Numa ;
- Libre interprétation de Bach et Chopin, le dimanche 25 janvier à l'église Saint-Mérri ;
- Le Petit Prince au pays des Hackers, le lundi 26 janvier au garage de la Quadrature du Net ;
- Brevets, santé, semences… le domaine public et le vivant, le mardi 27 janvier à La Paillasse ;
- Enjeux politiques et juridique du domaine public, en présence d'Isabelle Attard et Lionel Morel, le mercredi 28 janvier à l'ENS ;
- Cérémonie de clôture des « Copyfraud Awards », le samedi 31 janvier à la Recyclerie.

Télécharger ce contenu au format Epub

Lire les commentaires

Repas du Libre le 27 janvier 2015 à Toulouse

Vendredi 23 Janvier

Le groupe d'utilisateurs et utilisatrices de Logiciels Libres de Toulouse Toulibre, en collaboration avec Tetaneutral.net fournisseur d'accès internet et hébergeur libre, proposent aux sympathisants et sympathisantes de se retrouver l'un des mardis ou jeudis de chaque mois pour échanger autour des logiciels Libres, des réseaux libres, discuter de nos projets respectifs et lancer des initiatives locales autour du Libre. Ce repas est ouvert à toutes et à tous, amatrices et amateurs de l'esprit du Libre, débutantes et débutants ou technicien(ne)s chevronné(e)s.

Ce QJELT (Quatrième/Quelconque Jeudi/Jour du Libre Toulousain) aura lieu le mardi 27 janvier 2015 à 20 heures, au restaurant Bois et Charbon situé au 64 rue de la Colombette à Toulouse. C'est à proximité de la place Saint Aubin accessible par le métro à la station Jean Jaurès (ligne A et B). Entrée/plat/dessert + 1/4 de vin à 18€. Pour des raisons de logistique, une inscription préalable avant la veille au soir est demandée.

Inscription demandée avant le lundi soir à l'adresse http://www.toulibre.org/qjelt.

Télécharger ce contenu au format Epub

Lire les commentaires

CodevTT v1.0.2 - Suivi d'activité et gestion de projet avec MantisBT

Vendredi 23 Janvier

CodevTT est un outil de gestion de projet, permettant un suivi détaillé de l'avancement des projets et des activités de l'équipe.

Sa caractéristique principale est d'être en lien direct avec MantisBT — un système de suivi d'anomalies — dont on étendra le périmètre d'activité.

En puisant des informations dans la base de données de MantisBT et en simplifiant au maximum la saisie des comptes-rendus d'activité des utilisateurs, CodevTT réduit considérablement le nombre d'opérations manuelles à effectuer pour générer des rapports, statistiques, alertes, diagramme de Gantt et autres indicateurs de production et de suivi.

Les données de MantisBT étant tenues à jour en permanence par les développeurs, le chef de projet peut avoir une vue en temps réel de l'avancement du projet, sans créer de surcharge de travail pour l'équipe.
Les informations remontées par CodevTT permettent au chef de projet d'identifier plus rapidement les points durs du projet. La réduction d'un grand nombre de tâches récurrentes lui permet de se concentrer davantage sur les parties nécessitant le plus d'attention et d'analyse.

Les statistiques aident à identifier les actions à entreprendre pour améliorer la productivité de l'équipe et permettront d'en mesurer l’efficacité à court, moyen et long terme.
La section Contrats et Commandes permet d'avoir une vue client de l'avancement, et propose des indicateurs qui pourront lui être remontés.

CodevTT est donc un outil de gestion de projet réactif, en lien direct avec le développement, et se fixe comme objectif la maîtrise du suivi et la réduction des coûts de management par la simplification et l'automatisation des processus.

CodevTT est un logiciel libre, soutenu par AtoS qui l'utilise en interne pour gérer ses projets (avec une base d'utilisateurs actuelle d'environ 250 personnes).

Télécharger ce contenu au format Epub

Lire les commentaires

Meetup : Les bonnes pratiques de MariaDB le 29 janvier 2015 chez Mozilla Paris

Jeudi 22 Janvier

LeMug.fr (MySQL/MariaDB User Group France), organise un Meetup avec la contribution de MariaDB, à partir de 18h30 dans les locaux de Mozilla, 16 bis boulevard Montmartre, à Paris. Le thème abordé sera « Les bonnes pratiques avec MariaDB ».

Cet événement est ouvert à l'ensemble des développeurs et développeuses de tous les langages (C, PHP, Python, Java, Perl, Ruby, etc…). Ainsi, vous pourrez rencontrer la communauté de MariaDB.

Comme toujours le rendez-vous est gratuit et ouvert à tous, n’hésitez donc pas en parler autour de vous, et comme toujours… le nombre de places est limité. Alors n'hésitez pas à vous inscrire à partir de la page de l'événement !

Le programme de cette soirée :

  • ouverture des portes à 18h30 (début 19h00) ;
  • première présentation : installer et configurer MariaDB, par William Agasvari ;
  • deuxième présentation : les nouvelles fonctions et fonctionnalités de MariaDB, par Christophe Villeneuve et Stéphane Varoqui ;
  • troisième présentation : tour d’horizon des nouveaux moteurs de stockage, par Serge Frezefond ;
  • networking et cocktail sponsorisé par D4 et MariaDB.
Télécharger ce contenu au format Epub

Lire les commentaires

Apéro Python à Lyon le 28 janvier 2015

Mercredi 21 Janvier

Un apéro Python aura lieu à Lyon le mercredi 28 janvier à partir de 19h à l'Antre Autre (11 rue Terme, Lyon 1er). Un AFPyro est un moment convivial où les pythonistes peuvent échanger librement autour d’un verre ou d’une assiette.

Une présentation sur l’utilisation et les dernières fonctionnalités de Radicale sera donnée par Guillaume Ayoub.

Radicale est un serveur CalDAV/CardDAV permettant de stocker et gérer des données calendaires et de carnets d'addresses.

Télécharger ce contenu au format Epub

Lire les commentaires

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

Mercredi 21 Janvier

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

[Echos judiciaires Girondins] «Les geeks sur La Banquiz»

Par Eric Moreau, le dimanche 18 janvier 2015. Extrait:

À l’heure où la France souhaite mettre en avant ses talents de la nouvelle économie du numérique, une pépinière d’un genre nouveau émerge dans la métropole bordelaise.

Lien vers l'article original: http://www.echos-judiciaires.com/high-tech/-les-geeks-sur-la-banquiz-a11136.html

[L'OBS] Pendant ce temps, la NSA s’arme en vue des cyberguerres

Par Benoît Le Corre, le dimanche 18 janvier 2015. Extrait:

Sur l’offre de stage, il est précisé qu’ils «recherchent des stagiaires qui veulent casser des choses». Ils, c’est la NSA, l’Agence américaine de la sécurité, du renseignement, à travers une cellule de formation appelée Politerain.

Lien vers l'article original: http://rue89.nouvelobs.com/2015/01/18/pendant-temps-nsa-sarme-vue-cyberguerres-257177

Et aussi:

[Le Journal de Montréal] Blackberry, Linux et la sécurité

Par Michel Dumais, le vendredi 16 janvier 2015. Extrait:

En effet, BB détient d’importants brevets dans le domaine de la mobilité qui fait l’envie de nombreux compétiteurs. C’est d’ailleurs pour cette raison (entre autres) que Google a acheté la division mobile de Motorola.

Lien vers l'article original: http://www.journaldemontreal.com/2015/01/16/blackberry-linux-et-la-securite

Et aussi:

[Le Courrier picard] BEAUVAIS La capitale du logiciel libre se prépare

Par Fanny Dolle, le jeudi 15 janvier 2015. Extrait:

Les Rencontres mondiales du logiciel libre (RMLL), philosophie selon laquelle les logiciels peuvent être utilisés, partagés et améliorés, se préparent. La prochaine édition aura lieu du 6 au 10 juillet, à l’antenne universitaire de Beauvais.

Lien vers l'article original: http://www.courrier-picard.fr/region/beauvais-la-capitale-du-logiciel-libre-se-prepare-ia186b0n502061

[Next INpact] Charlie Hebdo n° 1178 : de l'intérêt du papier face aux éditions numériques

Par David Legrand, le mercredi 14 janvier 2015. Extrait:

Aujourd'hui, tout le monde cherche à s'acheter le dernier Charlie Hebdo. Un numéro 1178 qui restera sans doute dans l'histoire, tiré à plusieurs millions d'exemplaires, qui pousse à réfléchir sur l'intérêt du papier et de la presse au format numérique. Mais sur la capacité des lecteurs à soutenir et à financer l'information.

Lien vers l'article original: http://www.nextinpact.com/news/91736-charlie-hebdo-n-1178-interet-papier-face-aux-editions-numeriques.htm

Et aussi:

[Decideo.fr] Les clients d'Oracle se plaignent ouvertement, PostgreSQL en embuscade

Par la rédaction, le mercredi 14 janvier 2015. Extrait:

Campaign for clear Licensing, une organisation à but non-lucratif basée au Royaume-Uni défendant les droits des acheteurs de logiciels d'entreprise, vient d’exhorter Oracle, dans une lettre ouverte adressée à Larry Ellison et ses collègues, «à prendre des mesures pour améliorer la confiance de ses clients et répondre à leurs préoccupations concernant la stratégie de vendor lock-in de l’éditeur s’il veut que sa stratégie actuelle de faire migrer ses clients vers ses services de cloud computing soit couronnée de succès.»

Lien vers l'article original: http://www.decideo.fr/Les-clients-d-Oracle-se-plaignent-ouvertement-PostgreSQL-en-embuscade_a7619.html

Et aussi:

[Numerama] Comment nous pouvons perdre la guerre

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

Il n'y a qu'une seule manière de perdre la guerre contre le terrorisme. Et c'est celle que nous choisissons de plus en plus.

Lien vers l'article original: http://www.numerama.com/magazine/31837-comment-nous-pouvons-perdre-la-guerre.html

Et aussi:

Télécharger ce contenu au format Epub

Lire les commentaires

Install-Party Linux et Logiciels Libres à la Médiathèque de Teyran le 24 janvier 2015

Mardi 20 Janvier

La médiathèque a invité l’association Montpel’libre pour un Café numérique, le 17 janvier 2015 dernier. Cette matinée conviviale fut l’occasion de découvrir et échanger sur l’intérêt suscité par les logiciels libres, la philosophie qu’ils véhiculent, ainsi que leurs nombreux avantages.

Samedi 24 janvier 2015, de 10h à 17h, la médiathèque les reçoit pour la phase 2 : l’install’party !
Médiathèque de Teyran - Place du ballon 34820 Teyran

Bus Hérault Transport ligne 111 au départ de Castelnau-le-Lez station G. Pompidou
GPS : Latitude : 43.683601 | Longitude : 3.925709

Vous êtes décidé à installer Linux sur votre ordinateur et vous avez choisi votre distribution ? Apportez votre ordinateur portable, ainsi qu’une clé USB d’au moins 4 Go et laissez-vous guider par les membres de l’association Montpel’libre.

Le but de cette journée : avoir fait ses premiers pas et repartir avec un ordinateur fonctionnant avec le système d’exploitation Linux, correctement installé, configuré et agrémenté de logiciels libres utiles au quotidien. Le tout gratuitement, librement et légalement.

Télécharger ce contenu au format Epub

Lire les commentaires

Install Party GNU/Linux le 31 Janvier 2015 à Marseille

Lundi 19 Janvier

L'association CercLL (CercLL d'Entraide et Réseau Coopératif autour des Logiciels Libres) vous invite à une install Party GNU/Linux le samedi 31 janvier 2015 de 14h30 à 19h30 dans la salle de la Fabulerie au 4 rue de la bibliothèque, 13001 Marseille.

Vous avez envie de découvrir un système d'exploitation libre, simple d'utilisation, stable, rapide, sécurisé. Une nouvelle façon d'utiliser votre ordinateur. Vous vous sentez une affection naissante pour le Gnou et le Manchot, les mascottes GNU/Linux.

Programme en deuxième partie de dépêche.

Au programme :

  • découverte de l'univers des logiciels libres ;
  • installation d'un environnement GNU/Linux, ainsi que les meilleurs des logiciels libres ;
  • démonstration de jeux vidéo sous Linux.

Venez avec votre ordinateur : il vous sera proposé d'installer une distribution GNU/Linux avec un ensemble de logiciels libres et gratuit pour une utilisation quotidienne.

L'entrée est libre, et une participation de 2 euros est demandée. De plus, l'évènement est accessible aux débutantes et débutants. Vous pourrez aussi adhérer à l'association durant un an, pour un montant de 20 euros.

Plan d'accès : http://www.openstreetmap.org/node/2118530202#map=19/43.29531/5.38390

Télécharger ce contenu au format Epub

Lire les commentaires

pkgsrc 2014Q4 est disponible

Dimanche 18 Janvier

Dans un message à des listes de diffusion pkgsrc et NetBSD, Alistair Crooks a annoncé la disponibilité de la branche pkgsrc-2014Q4. Pkgsrc (prononcer package source) est une infrastructure de construction de logiciels tiers pour NetBSD, ainsi que pour d’autres systèmes de type UNIX. Il permet donc à NetBSD et à d’autres systèmes d’exploitation de disposer de nombreux logiciels sous forme source, mais aussi sous forme binaire.

Les développeurs pkgsrc fournissent une nouvelle version stable chaque trimestre. Comme son nom l’indique, pkgsrc 2014Q4 est donc la dernière sur les quatre de l'année 2014 et est disponible depuis le 2 janvier dernier.

Plus de détails sur cette version en particulier en seconde partie de dépêche, qui reprend grandement le courriel d'annonce.

Si vous ne connaissez toujours pas pkgsrc

À force de publier des dépêches sur le sujet (suivez le tag pkgsrc), espérons que vous commencez à connaître la chanson : pkgsrc, c'est le système de paquets logiciels pour NetBSD, issu d'un fork en 1997 de celui de FreeBSD. Nos amis au drapeau orange étant adeptes de la portabilité, il est logique que leur système de paquets puisse fonctionner ailleurs et compte toujours sa vingtaine de plateformes compatibles, allant des systèmes BSD à Windows (grâce à Cygwin/Interix/Services For Unix) en passant par GNU/Linux, OS X et Solaris.

Pour être plus concret sur la portabilité de pkgsrc, certaines personnes maintiennent des dépôts de paquets binaires en dehors de ceux pour NetBSD. Ainsi, le dépôt de la société Joyent contient des ensembles de paquets pour SmartOS, GNU/Linux mais aussi OS X. Saluons aussi le projet Save OS X, qui en plus de fournir un dépôt pour x86_64 (celui de Joyent est pour i386), propose articles et courtes vidéos introduisant pkgsrc pour le système à la pomme.

Enfin, ces initiatives ne sauraient être couronnées de succès sans pkgin, gestionnaire de paquets maintenu par iMil et dont la version 0.7.0 devrait voir le jour sous peu.

Les chiffres du trimestre

En termes de paquets, pkgsrc-2014Q4 c’est (entre parenthèses la différence avec pkgsrc-2014Q3 lorsque le chiffre était indiqué) :

  • 15510 paquets possibles (+ 324) ;
  • 15049 paquets binaires compilés avec clang pour NetBSD-current/x86_64 (+ 308) ;
  • 12972 13026 paquets binaires compilés avec gcc pour SmartOS/x86_64 (- 54) ;
  • 14430 paquets binaires compilés avec gcc pour NetBSD-6.0/x86_64.

Ce trimestre, en termes de modifications, il y a eu :

  • 156 paquets ajoutés ;
  • 48 paquets retirés, dont 9 avec un successeur ;
  • 1575 paquets mis à jour ;
  • 4 paquets ont été renommés.
Les changements

Parmi les ajouts ou mises à jour notables, on peut remarquer :

  • une amélioration des paquets Haskell ;
  • des mises à jour dans les paquets d'émulation Linux, basés sur SUSE 12.1 ;
  • ainsi que de nombreuses bibliothèques Python, Perl, Haskell et Ruby.

La campagne de nettoyage qui a lieu chaque trimestre permet de supprimer ce qui obsolète, ou non utilisé. Cette fois-ci, c'est au tour de libreoffice3, skype1 et skype21.

Au-delà des paquets en eux-même, l'infrastructure de pkgsrc évolue. Ce trimestre, une nouvelle variable fait son apparition : PKGSRC_KEEP_BIN_PKGS (à placer dans son fichier mk.conf). Elle permet de conserver les paquets binaires de ce qui est compilé.

Un commentaire de la dépêche précédente signalait le travail de Jonathan Perkin sur l'amélioration du temps de compilation de tous les paquets de pkgsrc (ce qu'on appelle des bulk build, ou pbulk, du nom de l'outil). Alistair Crooks mentionne que l'intégration des cwrappers (qui permet cette amélioration) a progressé, et que d'autres progrès sont à attendre pour le trimestre prochain.

Alistair Crooks profite de son courriel d'annonce pour faire le bilan, non seulement de l'année 2014, mais aussi depuis 1997. Sur ces 17 années de publication de pkgsrc, 2014 se situe en troisième position en terme de nombre de changements apportés. L'année la plus faste est 2013, suivie par 2004.

Un coup d'oeil à NetBSD

La dernière dépêche traitant de nouvelles versions de NetBSD abordait les versions 6.1.5 et 6.0.6. Quelques semaines plus tard, les mêmes corrections étaient portées sur la branche 5, permettant de publier NetBSD 5.1.5 et 5.2.3. Toutefois, l'attente continue concernant NetBSD 7 : la branche existe depuis plusieurs mois dans CVS, mais est toujours au stade de beta. Si vous le souhaitez, vous pouvez télécharger et installer une de ces versions pour améliorer la future version 7 stable.

Enfin, sur une note plus personnelle, votre serviteur est maintenant lui aussi développeur NetBSD, et espère ainsi agrandir la liste des mises à jour de pkgsrc que vous pourrez lire chaque trimestre.

Télécharger ce contenu au format Epub

Lire les commentaires

Le plein de frags pour cette nouvelle année 2015 (Unvanquished, ET:Legacy, Xonotic)

Dimanche 18 Janvier

Ce mois de janvier à peine commencé a vu plusieurs jeux annoncer des mises à jour importantes, en voici trois :

Ces trois nouvelles versions sont détaillées en seconde partie de dépêche. À vous de jouer !

Sommaire

Pour ne pas le répéter à chaque fois : tous ces jeux sont désormais passés à la version 2 de la SDL.

Unvanquished 0.35.1

Unvanquished alpha 35 vient de sortir. C'est un jeu qui mêle tir à la première personne et stratégie, où une armée d’humains (armes de tir) et une armée d’extraterrestres monstrueux (corps à corps) défendent leur base et attaquent la base adverse.

Unvanquished maintient son rythme actif d’une publication par mois, mais comme nous n’en avons pas parlé dans ces colonnes depuis avril 2013, c’est l’occasion de rappeler l’avancement pour cette année écoulée !

L’interface du jeu est désormais propulsée par libRocket (une interface HTML/CSS). Plus aucune carte de l’ancien Tremulous n’est utilisée, et ce sont dix cartes originales qui sont distribuées officiellement.

La structure de défense de proximité Générateur Tesla est supprimée, et une nouvelle structure est ajoutée : un Rocket Pod qui tire des missiles à longue distance (le Rocket Pod n’est donc pas vraiment un remplaçant pour le Générateur Tesla).

Beaucoup de modèles ont été refait, comme le Granger, ou leur animation refaite comme pour le Trapper, et certains aliens ont été remplacés, comme la Mantis qui remplace le Basilisk.

Coté serveur, la logique de jeu ne tourne plus sur QVM (Quake Virtual Machine) mais sur NaCl (Google Native Client).

Le protocole unv:// permet de rejoindre une partie depuis un lien sur un site web ou posté sur un canal IRC.

Le tout nouveau « Rocket Pod » vient soutenir la tourelle automatique, ici sur la nouvelle carte « Antares ».

Mais les changements ne s’arrêtent pas au jeu lui-même. Le site web vient d’être complètement refait à neuf, avec beaucoup de soin. La priorité : accueillir convenablement le joueur ! Comme le jeu est encore en version alpha, le projet ne communique pas énormément afin d’éviter de causer des frustrations ou des désillusions auprès du grand public. Toutefois, l’équipe soigne sa petite base de joueurs fidèles.


Au secours !

En plus de ce nouveau site pour vous accueillir, vous êtes invités à rejoindre le canal #unvanquished sur le réseau IRC Freenode où un bot annonce les parties en cours : c’est un moyen très pratique de ne pas rater les meilleures parties ! Cela signifie aussi qu’il suffit souvent de se connecter à un serveur et de commencer à jouer pour que d’autres joueurs rejoignent !

L’équipe organise également un dev game tous les dimanches à 20:00 UTC (21h pour nos lecteurs d’Europe occidentale), afin de tester certains ajustements ou tout simplement pour le plaisir de jouer. Comme le rendez-vous est connu et que beaucoup y sont fidèles (et l’attendent avec impatience), c’est le bon moment à réserver dans sa semaine pour passer une excellente soirée de jeu !

Pour télécharger Unvanquished 0.35.1, c’est par ici.

Enemy Territory:Legacy 2.72

Comme promis, ET:Legacy est sorti en version stable 2.71, et même 2.72… il s'agit d'un projet qui maintient le moteur libre de Wofenstein: Enemy Territory, un jeu multijoueur en équipe qui vous renvoie pendant la seconde guerre mondiale pour mener à bien vos missions ou au contraire, mettre en échec celles du camp adverse !

Cette version 2.72 publiée par ET:Legacy arrive donc près de neuf ans après la dernière version de Wolfenstein: Enemy Territory publiée par Splash Dammage

La majorité des modifications sont des corrections, pas de grands changement majeurs sur la jouabilité (ce n’est pas le but du projet). On peut cependant noter qu’à la manière d’Unvanquished et son protocole unv://, ET:Legacy sait interpréter les url etl:// et puis y a pas que ça tout d’même !

Pour en savoir plus sur ET:Legacy et Wolfestein: Enemy Teritory, et notamment pour tout ce qu’ET:Legacy a apporté au moteur orignal, n’hésitez pas à lire l’article « Enemy Territory: Legacy, en résistance » qui décrit tout cela.


Parviendrez-vous à empêcher l’Axe de charger et amorcer ce canon démesuré ?

ET:Legacy a lui aussi complètement refondu son site et prévoit comme Unvanquished d’organiser des matchs réguliers pour tester le jeu en développement, ainsi que d’utiliser un bot sur #etelegacy@Freenode pour annoncer ces parties. À suivre donc !

Cependant le projet ET:Legacy a déjà une base de joueurs bien plus vaste qu’Unvanquished étant entendu qu’il s’agit de maintenir le moteur d’un jeu préexistant avec sa base de joueurs convaincus.

ET:Legacy est pleinement compatible avec Wolfenstein: Enemy Territory, donc bien que ce soit la première fois qu’ET:Legacy soit publié en version stable, il existe déjà plusieurs centaines de serveurs disponibles en ligne…

Vous pouvez télécharger ET:Legacy 2.72 depuis cette page.

Xonotic 0.8.0

Xonotic est un grand classique du twitch game libre : vous voilà téléporté dans une arène avec un arsenal d’armes aussi variées qu’efficaces afin d’amasser le plus de points pour vous ou votre équipe (frags ou capture de drapeau). Le jeu est rapide et soutenu et mettra à l’épreuve vos meilleurs réflexes ! Xonotic est un fork du jeu Nexuiz fondé sur le moteur Darkplace hérité de Quake2, dont il se place ici en très digne héritier.


La nouvelle arme « Arc » sur la nouvelle carte « Vorix ».

Un an et demi après la version 0.7.0, cette version 0.8.0 apporte notamment une nouvelle arme : Arc, qui rappellera à certains le Lightning Gun de Quake Ⅲ Arena, mais avec une trajectoire souple, et qu’il ne faut pas utiliser trop longtemps sous peine de surchauffe ! Une nouvelle musique accompagnera vos parties : X-Force, et trois nouvelles cartes ont été ajoutées au mode « capture du drapeau » : « Catharsis », « Implosion », et « Vorix ». À la fin d’une partie, il est désormais possible de voter le type de jeu avant de voter la prochaine carte à jouer !


Invasion : Vous n’y survivrez pas !

Un nouveau mode de jeu apparaît, « Invasion », où le joueur doit se battre contre une marée de monstres… Un nouveau système de bonus nommés « Buffs » peut également être activé, qui donne au joueur des pouvoirs spéciaux lorsqu’ils sont ramassés.

Vous pouvez aussi suivre le canal #xonotic sur QuakeNet et organiser des parties de Xonotic sur #xonotic.pickup, après avoir téléchargé Xonotic 0.8.0 à partir de cette page.

Bons frags !

Télécharger ce contenu au format Epub

Lire les commentaires

Pages