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

86
28
jan.
2015
Science

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

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

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

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

21
29
jan.
2015
Distribution

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.

pfSense

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

Jeudi du libre du 5 février 2015 à Lyon

Posté par . Édité par Nils Ratusznik. Modéré par tankey. Licence CC by-sa
1
29
jan.
2015
Lug

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.

Jorani passe la troisième

Posté par (page perso) . Édité par Nils Ratusznik et ZeroHeure. Modéré par ZeroHeure. Licence CC by-sa
20
29
jan.
2015
PHP

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.

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

9
28
jan.
2015
Mobile

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.

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

Posté par . Édité par Nils Ratusznik, Nÿco et palm123. Modéré par ZeroHeure. Licence CC by-sa
10
28
jan.
2015
Son

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 !

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

Posté par . Édité par ZeroHeure, palm123, Nÿco et NeoX. Modéré par ZeroHeure. Licence CC by-sa
48
27
jan.
2015
XMPP

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.

Musique libre : Moquettes&Tapis par Sebkha-Chott

Posté par . Édité par NeoX, tankey, Nils Ratusznik et palm123. Modéré par Christophe Guilloux. Licence CC by-sa
17
28
jan.
2015
Culture

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.

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

Posté par (page perso) . Modéré par Nÿco. Licence CC by-sa
21
27
jan.
2015
Internet

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

FOSDEM 2015 ce week-end du 31 janvier à Bruxelles

Posté par (page perso) . Édité par M5oul, BAud, ZeroHeure, palm123 et eggman. Modéré par ZeroHeure. Licence CC by-sa
Tags :
12
27
jan.
2015
Communauté

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.

fosdem

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

Posté par (page perso) . Édité par olivierweb, tankey, reno, BAud, patrick_g, palm123, Nÿco et Nicolas Boulay. Modéré par tankey. Licence CC by-sa
44
24
jan.
2015
Technologie

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.

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

Posté par (page perso) . Édité par NeoX, Nils Ratusznik et Benoît Sibaud. Modéré par Nils Ratusznik. Licence CC by-sa
19
24
jan.
2015
Culture

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.

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

Posté par (page perso) . Édité par NeoX, Pierre Jarillon et palm123. Modéré par patrick_g. Licence CC by-sa
24
23
jan.
2015
PHP

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).

Repas du Libre le 27 janvier 2015 à Toulouse

Posté par (page perso) . Édité par NeoX, Nils Ratusznik et patrick_g. Modéré par patrick_g. Licence CC by-sa
6
23
jan.
2015
Communauté

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.