Fanf a écrit 276 commentaires

Et bien, je ne connaissais pas, et je dois te remercier ! C'était vraiment _très_ bon.

Juste pour vous mettre l'eau à la bouche : ce sont les prévisions 2005 des principaux évènements du monde informatique... Les revirements de Sun sont particulièrement succulents.

Bref, je le conseille à tous !

> pourquoi c'est pas intégré dans le compilateur directement.

Par ce qu'on peut faire du brouzouf avec et que personne n'a fait quelque chose de si évolué en libre ? :-)

Ou plutot parce que généralement, les outils d'analyse statique sont lents et pas pousse-boutons : il faut beaucoup de calculs pour obtenir des résultats (et donc beaucoup de temps) qui doivent être analysé par la suite. DE plus, il faut parfois rajouter des hypothèses lors de l'analyse pour obtenir un résultat utilsable. Evidemment, pas n'importe quelle hypothèses non plus, et c'est là encore un difficulté (par exemple, donner un invariant de boucle à l'outils qui ne sait généralement pas le trouver, mais qui est essentiel pour vérifier la terminaison de celles-ci).

Bref, tout ça pour dire que tu ne peux pas forcément intégrer les outils d'analyse statique au compilo, mais ça n'empeche pas d'en avoir des libres.

Ok, on est prevenu, c'est beta

En fait, ce n'est même pas encore beta là...
Pour ce qui est de la progression, je suis _très_ optimiste. Il faut voir que les EFL n'ont été annoncées en pr1 qu'il y a ... 4 mois (aout 2004). Le développement de e proprement dit ne s'est fait qu'après.

Bref, je pense de plus en plus sérieusement que 2005 sera, pour le desktop sous linux, l'année d'Enlightenment. Une révolution en marche ?

Et ça marche ! (ne me faites pas dire ce que je n'ai pas dit, ce n'est pas forcément utilisable)

Justement, pour l'instant les applications sont encore très peu utilisables (en gros, entrance marchotte, e pas vraiment, l'image_viewer_dont_j'ai_oublié_le_nom ça va, le reste je n'ai pas vraiment essayé). Mais par contre, on sent bien la puissance sous-jacente (les bibliothèques ont vraiment l'air extrèmement puissantes). Et qu'est ce que c'est bô !

J'ai aussi vu un PC sous Mandrake dans un magasin "Planet Saturn" (disclamer : "plus radin, plus malin"), un magasin "discount" qui vend de l'électroménager, de la hifi-vidéo, informatique, etc... Je n'ai pas regardé les caractéristiques, donc je ne suis pas sûr que le matos soit le même, mais comme le prix était identique, on peut le penser.

Voilà, c'était juste à titre info (pour dire qu'il n'y avait pas que Carrouf qui vendait des PC sous mandrake).

il existe des machines qui arrivent à lire jusqu'à sept couches d'informations écrites sur le disque dur

Oui, et sûrement plus même. C'est pour cela que les institutions Européennes (hmm, je ne sais plus lesquelles, je sais que ça fait un peu argument de force comme ça, désolé...) préconisent 7 réécritures avec des schémas bien précis, puis une destruction physique du disque en particules < 0.5 mm^3 pour les données sensibles. Et là, il parait que c'est sûr "à ce jour".

C'est très (trop?) rigide mais au moins si ta spec est correcte, ton truc sera bon du premier coup - du moins en théorie, et probablement dans la pratique avec beaucoup d'expérience.

En fait, si tu réalise vraiment un développement formel (un complet), ton logiciel correspond aux spec par preuve. Bon, ce qui arrive souvent par contre, c'est que tu fasses une spec, que tu commence les preuves, que tu t'aperçoives qu'elles sont impossibles/ignobles, tu cherches une manière plus élégante de construire ta spec, etc. Le cycle se fait plus à ce niveau. Et pour ce qui est de la rigidité, j'appelerais plutôt cela de la rigueur : tu as un modèle et ton programme y correspond exactement.

Non non, tu ne te trompes pas. La SRAM, même si ça veut dire "static RAM", c'est aussi loin de la Flash qu'un disque dur d'une mémoire à tore. En très gros (du point de vu intéret, pas techno), c'est comme la SDRAM de nos PC, sauf que ça n'efface pas lorsqu'il n'y a plus de courant et que c'est plus rapide. C'est donc très bien... Mais pourquoi n'y en a t-il pas de partout alors ? Ben parce que c'est très cher.
La M-SDRAM devrait être "bon marcher" et très petite, le rêve quoi.

Sinon, ça fait super longtemps que IBM annonce qu'il va sortir la M-SDRAM et que ça va révolutionner le monde de l'informatique (et je veux bien le croire)... Il me semble que les recherches sur le produit se font dans les labos Essonniens d'une jointventure entre IBM et Infeneon, qui doit s'appeller, heu... Altis Semiconductor ?

En fait, je suis exactement dans le même cas : la partie mail est déjà gérée par une solution similaire, mais l'administration resent très fortement le besoin de mettre en place une solution calendrier/contacte/todo-list.
Tout ce que j'ai trouvé pour l'instant (groupwarze diverses) est surdimensionné par rapport aux besoins.
Si tu as des réponses ou si tu trouves une solution intéressante, pourrais-tu m'en informer ?

Ben c'est vrai, tous les plus beaux trolls sont en train de mourir. Avec la vrai arrivée pour de vrai d'E17, c'est encore un de vieux, des anciens, des réspectés qui part. Je verse une larme sur sa tombe.

D'un autre côté E17 n'est -pour l'instant- qu'en CVS, alors il reste un espoir : celui que Rasterman décide de tout reprendre à 0 avec les dernières technologies afin de partir sur des bases saines...

Bon, trève de plaisanteries, ça mériterait presque une nouvelle ça... OK, c'est juste une version même pas alpha, mais une première version CVS attendue comme ça, depuis presque 4 ans, qui a dû générer des millions de lignes de troll et autant de discussions presque sérieuses, je crois que ça n'existe dans aucun autre projet.
Du coup, pour la version finale, on pourrait faire un thème spécial pour tous les sites traitant de linux/LL, et enfin pour son arrivée dans Debian stable il faudrait trouver un truc encore plus imposant. Là, j'ai pas d'idée, mais on a bien 4 ans pour réfléchir, ça devrait aller :)

Je crois que le monsieur utilise LFS... Moi qui pensait que LFS, on se l'installait une fois pour voir, puis qu'on repasser vite vite à une distribution avec une gestion de paquetages moderne, pour éviter les ennuis sus-mentionnés :)

... mais ta signature la bien fait rire. C'était juste pour te remercier de cet instant de bonheur :)

Si tu veux changer la résolution "à la windows", tu peux utiliser la commande xrandr. 'xrandr' te donne les résolutions disponible avec un numéro qui leur est associé, 'xrandr -s le_numero_de_la_résolution_voulue" change pour cette résolution.

Tu peux faire d'autres choses comme des reflexion, man xrandr pour plus d'infos.

Comme d'habitude, le test de la distribution est bien : il révèle en quelques pages les atouts et l'esprit de cette nouvelle distribution.

Pour ma part, je l'ai essayée au moment de sa première release sur mon portable: elle est arrivée juste au moment où je devais réinstaller après un problème matériel. Habitué de Debian, j'ai voulu voir à quoi pouvait ressembler une distribution debian "pour débutant, pour le desktop". Et j'ai été bluffé, à tel point que je l'ai gardée :) J'ai même été agréablement surpris par Gnome 2.8, moi qui était habitué au triplé XFCE + Rox + Gdesklets. (aucun troll ne se cachent dans ses quelques phrases, se sont juste des constations).

Bref, pour un utilisateur "desktop", une bonne distrib qui lui permettra de mettre un pied dans linux/debian sans douleur, d'autant plus que la mailing liste est très active et l'aide aisé à trouver (mais là, je vais commencer à sacrément paraphraser l'article, alors j'arrète).

Non, le Umask est un masque : ça marche par soustraction, ce que l'on voit bien dans le premier exemple : umask = 077 => rxw------

Sinon, les expliqcations sont bien.

Comme dictionnaire français (uniquement, et pas encyclopédique), il y a le trésor de la langue francaise informatisé (tlfi) qui est très bien : c'est ce que j'a vu de mieux sur le net dans sa catégorie : http://atilf.atilf.fr/(...)

Il est vraiment à essayer pour ceux qui ne connaissent pas !

Arf, j'aurais dû être preums sur un post comme ça...

Bon, presque tout est dit. Mais on peut aussi citer Coq, c'est un très gros logiciel dévelopé en OCaml, pour faire de la preuve. Et pis, y'a aussi le compilo ocaml qui est écrit en ocaml, et qui est d'une beauté... Et pis y devrait y avoir d'autres logiciels de calculs massivement parallélisables qui devraient arriver...

Bref. OCaml, c'est bon, mangez-en. Sauf pour les GUI :)

1. j'ai installé debian avec KDE (avec du mal) et KDE ne veut pas se lancer !

Hmmm... As-tu utilisé apt-get pour cela ? Ou si tu préfère, apt-get avec un frontend quelconque (aptitude, synaptic...) ?

il se lance pendant 3secondes et je reviens au menu de selection login/passwd . Quand je suis en mode texte il dit : connection server x lost. mais aucun message d'erreur.. Quand je choisi Gnome au lieu de Kde il se lance correctement !!! pourquoi kde se lance pas ? Que dois-je faire ?

Il n'y pas de messages d'erreurs dans les logs d'XFree non plus ? (dans /var/log/XFree je crois).

2.pour copier un fichier sur une clé USB il faut bien faire :
$mcopy nom_fichier f: ?????
pour copier un fichier sur le dur a partir d une clé USB :
$mcopy f:nom_fichier ???????

C'est sal ce que tu fais là. La façon propre de procéder est de monter ta clés usb dans le système de fichier puis d'y accéder de façon normale (comme tout autre répertoire de ton système) et de démonter le tout avant de la retirer.
Pour monter ta clé, il faut savoir à quel périphérique elle est associé (généralement /dev/sda1). Tu crées un point de montage dans ton arborescence de fichier (par exemple /mnt/removable pour être original) puis un simple "mount /dev/sda1 /mnt/removable " devrait suffire (peut-être faudra-t-il rajouter l'option "-t vfat", mais pas sûr). Pour démonter, tu utilise umount /mnt/removable.

Tu peux automatiser les choses de nombreuses manières, et il existe une litérature abondante sur la chose (le mieux à mon avis étant de passer par hotplug et udev).
Et comme tu m'as l'air d'être plutôt débutant, je te conseille la distribution ubuntu si tu veux avoir une distrib desktop construite sur debian.

Heu en fait non, je n'ai pas le choix car ma copine est en période de rendu de mémoire/dossiers multiples, à rendre pour avant hiers et que je me vois mal lui demander de changer ses habitudes en ce moment. Dans une semaine, je pourrais, mais pas là :)

Nerim ?

Les méthodes semi-formelles et formelles sont toutes les méthodes se basant sur des preuves mathématiques. En gros, tu vas effectuer une spécification à haut niveau dans un langage mathématiques (en général dérivant du lambda-calcul et/ou de la théorie des ensembles), puis tu vas construire ton logiciel en prouvant mathématiquement qu'il est équivalent à la spécification. Résultat : ton logiciel n'a pas de bug.
Bon, ça c'est la théorie, en pratique la complexité est telle qu'on ne peut généralement pas appliquer une méthodologie pure de A à Z. On doit donc faire des consessions, mais globalement les logiciels créés ainsi ne contiennent presque pas de bug. Il faut aussi que la spécification initiale soit bonne, et c'est là aussi un gros chalenge.

En France, notre recherche est plutôt bien positionnée sur le domaine au niveau mondial, avec en particulier des outils : d'une part, la méthode B et son atelier[1], d'autre part l'assistant à la preuve Coq[2].

Pour ce qui est de la méthode B, c'est une méthode de spécification qui marche par pallier en ce basant sur la théorie des ensembles : on comence par modéliser grossièrement, en posant les propriétés qui doivent être vérifiées, puis on raffine, c'est à dire qu'on devient de plus en plus précis, en prouvant l'équivalence entre chaque niveau. Au final, après un certains nombre de pallier la spécification est tellement précise qu'elle peut être exporter dans un langage (Ada par exemple). Cette méthode a été utilisée par Matra pour construire le SI de météor, la ligne 14 automatique du métro parisien (qui n'a à ce jour jamais eu de problèmes informatique).

Pour ce qui est de Coq, c'est un assistant à la preuve, c'est à dire que c'est un logiciel qui permet de spécifier des propriétés puis de prouver qu'elles sont vrai das un contexte donné. Il se fonde sur un lambda-calcul amélioré, qu'on appelle le Calcul des Constructions Inductives : c'est une Lambda-calcul typé + constructeurs de types + types dépendants / polymorphisme + types inductifs. Avec ça, on dispose d'une expressivité consécante.
Avec Coq, on procéde donc à la spécification du logiciel et de ses propriétés que l'on prouve dans l'assistant. Une fois que les preuves sont faite, on peux réaliser l'extraction du logiciel prouvé. Ceci est quelque chose de très nouveau et Coq est le seul logiciel le proposant pour l'instant : à partir de la preuve, on génére automatiquement le code source du logiciel dans un langage cible (en général, OCaml). On obtient alors le logiciel et on a la preuve qu'il vérifie la spécification et ses propriétés. Bref, c'est beau. Aujourd'hui, Coq et l'extraction de programmes sont utilisés dans une grosse action[3] du CÉDRIC et de l'INRIA afin de certifier un compilateur pour C.

Bon, c'était un peu long, désolé...

[1] http://www.atelierb.societe.com/(...)
[2] http://coq.inria.fr/(...)
[3] http://www-sop.inria.fr/lemme/concert/(...)

C'était bien un problème de MTU... Ce qui m'a trompé, c'est que la passerelle est sous windows (je ne peux pas faire autrement, je n'ai pas le choix). Et le driver pppoe fourni par le FAI (neuf.fr) est tout pourri. Sous linux, on peut régler la taille des paquets de base, et je crois même que pppoeconf conseil de mettre le MTU à la bonne valeur.

Bref, après quelques recherches sur le grand Ternet et quelques reboot (pfff), ça marche.

Merci encore à tous pour votre aide.

Je n'ai pas ce paramètre. Par contre, j'ai un "tcp_window_scaling" que j'ai essayé de mettre à 0 sans changement.
Pour ce qui est du noyau, c'est un 2.6.8.1, celui de base de la distrib.

Merci, je vais chercher dans ce sens.

En fait, il a beaucoup souffert (référence culturelle inside)

J'ai un problème, je n'arrive pas à aller sur update.mozilla.org depuis hiers. Est-ce que le problème vient de moi, ou est-ce que c'est le site qui est dans les choux ?