jeanas a écrit 170 commentaires

Mon sujet principal est une variante spéculative de HoTT.

https://linuxfr.org/users/ysabeau/liens/fondation-python-the-psf-has-withdrawn-a-1-5-million-proposal-to-us-government-grant-program

Tu fais une thèse en théorie de la démonstration ? ou en calculabilité ?

Théorie des types

Je viens de lire l'article (https://arxiv.org/pdf/2507.22950). Il se trouve que les théorèmes de Gödel font partie des bases de mon propre domaine de recherche (je suis en thèse). Je n'ai pas le temps de développer mais disons simplement que cet article est du vent. Il ne dit strictement rien d'intéressant et ne prouve certainement pas que nous ne vivons pas dans une simulation.

Pour autant que je le sache, la notion de déterminant d'une application linéaire est bien définie uniquement dans le cas particulier où l'espace est de la forme ; et dans ce cas le déterminant est celui de la matrice dans la base canonique.

Pour moi (et Wikipédia), le déterminant d'une application linéaire est par définition le déterminant de sa matrice dans une base quelconque (mais la même au départ et à l'arrivée). On vérifie que ça ne dépend pas de la base.

Pour des démonstrations de Math exigeant la compréhension fine de nombreux concepts, je me demande bien comment l'on peut être sûr de pouvoir valider par soi-même une démonstration sans passer par l'approche de la revue par des pairs reconnus comme experts dans leur domaine.

Rappelons tout de même que le Frido se place au niveau de l'agrégation, qui est un concours d'enseignement, et dont les épreuves orales demandent de présenter un plan de cours sur un sujet au programme. Un niveau, donc, où on est censé savoir en principe reconnaître une démonstration correcte ou non (ce qui n'empêche évidemment pas de se tromper parfois, ça arrive même aux meilleurs) et avoir une maîtrise suffisante des concepts en jeu (qui font partie du cursus mathématique universitaire standard, pas de domaines de recherche très spécialisés) pour appliquer cette compétence de manière raisonnablement efficace sur ces preuves en particulier.

Sur ce point, chatGPT peut en savoir plus que moi. Par exemple je ne voyais pas comment démontrer qu'une transvection est de déterminant 1. C'est chatGPT qui m'a mis sur la piste du lemme des déterminants que je ne connaissais pas.

Ça me paraît bien compliqué. En développant juste le déterminant comme somme sur les permutations, ça marche, non ? (On peut poursuivre cette discussion ailleurs si tu veux.)

Aparté : je n'ai pas compris le lien que tu fais entre mesure et compacité.

Je demande si il est vrai que tout ensemble Dedekin-fini totalement ordonné a un maximum.

À mon avis la preuve donnée par Asaf Karagila (et qui a 5 votes positifs) a au moins un trou ; j'explique dans les commentaires ce qui ne me va pas. Si vous avez une idée de comment compléter, n'hésitez pas.

Je n'ai pas relu la preuve d'Asaf Karagila, mais je viens de poster une nouvelle réponse avec une preuve différente et très détaillée.

Merci mais je ne comprends pas en quoi ça répond à ma question. La sélection primaire de X11, c'est ce qui change dès que tu sélectionnes du texte, sans même le copier. Qu'est-ce que ça a à voir avec les raccourcis clavier, gestes touchpad ou autres interactions qui sont configurés pour copier la sélection ?

Hein ? Mais le fait qu'un clic du milieu fasse ou non un copier-coller dépend de GNOME/KDE/ton window manager, pas du protocole Wayland ou X11 qu'il utilise pour communiquer avec les applications, non ?

Au temps pour moi.

Si les universités belges sont aussi sous-financées que les françaises, c'est un peu normal qu'elles aient à faire des choix budgétaires difficiles. Il y a tout de même une différence entre « fermer la bibliothèque pour faire des étudiants des bons petits consultants obéissants et employables qui n'ont pas besoin de réfléchir donc pas besoin de livres » et « fermer la bibliothèque parce que sinon on ne peut pas remplacer les deux collègues de lettres classiques et trois de maths qui partent à la retraite étant données les dernières coupes budgétaires ».

Avec Nextcloud, tu as une interface Web à ton calendrier et un serveur Caldav, et en prime tu peux facilement y ajouter d'autres usages (Carddav pour les contacts, partage de fichiers, etc.).

Aujourd'hui, beaucoup de sites utilisent des certificats à durée de vie relativement longue, typiquement un an, obtenus de la part du registrar DNS, et renouvelés à la main en demandant un nouveau certificat au registrar et en uploadant le fichier qu'on obtient sur le serveur. Pour eux, ce ne sera plus vraiment tenable, s'il faut faire cette manip tous les mois, donc tout le monde va devoir basculer sur l'autre méthode, celle du renouvellement automatique, qui est déjà très commune parce que Let's Encrypt, la principale autorité de certification à être gratuite, ne fournit déjà que des certificats à durée de vie assez courte.

(Moi, ça m'embête un peu, parce que les outils de renouvellement automatique comme acme.sh et Certbot m'ont causé quelques misères. J'espère que ce sera plus au point pour mes usages d'ici-là.)

C'est une délibération du CA/Browser Forum, un consortium qui rassemble la plupart des navigateurs Web et des autorités de certification qui délivrent les certificats TLS (que tout le monde continue d'appeler SSL), plus quelques autres.

Cette décision signifie donc probablement que presque toutes les CAs vont réduire la durée de validité maximale de leurs certificats, et que les navigateurs vont se mettre à refuser les certificats avec des durées plus longues.

Bonjour,

Prenons un exemple avec des requêtes à LinuxFR.

$ host linuxfr.org
linuxfr.org has address 213.36.253.103
linuxfr.org mail is handled by 50 main.linuxfr.org.

Le serveur de linuxfr.org est joignable à l'adresse IP 213.36.253.103. Pourtant, comme vous l'avez constaté sur d'autres sites, si on essaie de joindre https://213.36.253.103 sans précaution, on n'obtient pas la page d'accueil de LinuxFR. On peut reproduire dans un terminal avec curl ce que fait un navigateur :

$ curl --insecure https://213.36.253.103
<!DOCTYPE html>
<!-- Managed by Ansible, do not edit by hand -->
<html lang="fr">
<head>
<meta charset="utf-8">
<title>Serveur oups.linuxfr.org - LinuxFr.org</title>
</head>

<body><h1>Serveur oups.linuxfr.org - LinuxFr.org</h1>
<p>Si vous êtes arrivé(e) sur cette page, c'est probablement parce que vous kiffez l'HTML 2.</p>
</body>

</html>

La raison à ceci est qu'un même serveur peut, sur une même IP, servir plusieurs sites Web différents. Quand il reçoit une connexion HTTP, il a besoin de savoir à quel site elle se rapporte. Or notre requête ne lui fournit pas cette information. Dans le protocole HTTP, elle est donnée dans l'en-tête Host, qu'on peut demander à curl d'envoyer comme ceci :

$ curl --insecure -H "Host: linuxfr.org" https://213.36.253.103
<!DOCTYPE html>
<html lang="fr">
<head>
<meta charset="utf-8">
<title>Accueil - LinuxFr.org</title>
[…]

Maintenant, il faut que j'explique pourquoi on a eu besoin de --insecure. Dans le bon vieux temps, les requêtes étaient faites en HTTP simple, et le Host suffisait. Mais est arrivé le HTTPS, qui rajoute une couche de chiffrement TLS par dessus le HTTP. Or, dans le début de la connexion TLS, avant même que des données soient transmises, le client est censé vérifier que le serveur a fourni un certificat, qui atteste qu'il est bien le serveur qu'il prétend être. Donc, si un serveur propose plusieurs sites, quand il reçoit une requête, il ne pouvait pas encore savoir quel site voulait le client, et devait forcément fournir un certificat valide pour tous les sites possibles. Le hic, c'est qu'il peut être compliqué, et un peu moins sécurisé aussi, d'obtenir un tel certificat. Pour pallier ce manque est arrivée la SNI, « Server Name Indication », une extension du protocole TLS qui permet au client de spécifier quel site il veut dès le début de la connexion TLS. Avec la commande ci-dessus, curl passe le Host mais pas la SNI, donc se plaint légitimement qu'il n'a pas de certificat valide pour 213.36.253.103 car le certificat envoyé par le serveur de LinuxFR n'est valide que pour linuxfr.org (et j'ai mis le --insecure pour lui demander de l'ignorer).

curl n'a apparemment pas d'option pour régler manuellement le SNI, donc je ne peux pas terminer l'exemple aussi pédagogiquement que je le voudrais, mais dans la requête curl https://linuxfr.org, il utilise l'URL non seulement pour trouver l'IP 213.36.253.103 via DNS, mais aussi pour régler le SNI dans la connexion TLS et le Host dans la connexion HTTP qu'elle chiffre.

Sur Wikipédia : https://en.wikipedia.org/wiki/List_of_HTTP_header_fields#Standard_request_fields et https://en.wikipedia.org/wiki/Server_Name_Indication

HTH

Pour ma part, je ne stocke mon mot de passe maître que dans ma tête.

« the Commission will prioritise […] the preparation of a Technology Roadmap on encryption, to identify and assess technological solutions that would enable law enforcement authorities to access encrypted data in a lawful manner, safeguarding cybersecurity and fundamental rights. »

https://linuxfr.org/users/jeanas/journaux/mon-gestionnaire-de-mots-de-passe-en-50-lignes-de-html

En pratique, mes mots de passe sont enregistrés dans Firefox Sync, donc la plupart du temps je n'ai pas besoin d'ouvrir mon gestionnaire de mots de passe parce qu'ils sont préremplis par la complétion built-in de Firefox.

Quand je veux mon mot de passe pour un service qui n'est pas sur le Web (ma boîte mail, etc.), j'ouvre mon gestionnaire, je rentre le nom du service et mon mot de passe maître, et ça me donne mon mot de passe. Et quand je veux créer un nouveau mot de passe pour n'importe quoi, je l'ouvre aussi et je laisse Firefox l'enregistrer. Et comme noté sur la page du générateur, ça se fait très facilement en ligne de commande aussi.

Donc pour résumer, l'autoremplissage est fourni par Firefox, la synchronisation aussi (Firefox Sync, qui est associé à ton compte Mozilla), et la sûreté contre une panne des services Mozilla + possibilité de retrouver très facilement un mot de passe sur un autre ordinateur que le sien + possibilité de retrouver un mot de passe en ligne de commande et même sans réseau sont fournies par le générateur ultra-simple.

Mon PC actuel ainsi que ceux de ma sœur et mon frère (convertis à Linux par moi) sont achetés sur https://laptopwithlinux.com. J'ai trouvé ça très pratique : plutôt que de lire les specs de zillions de modèles différents, tu as un formulaire à remplir où tu choisis entre plusieurs options le processeur, la taille de RAM, la distribution Linux à préinstaller, la disposition de clavier à imprimer sur les touches, etc., ils l'assemblent et ils te l'expédient. J'en suis très satisfait jusqu'ici.

… il manque un dernier point pour que les comptes Premium soient vraiment la classe : compléter

Les comptes « Open » sont utilisables avec des protocoles normalisés, des formats ouverts et dans le respect de l'interopérabilité.

par

Les comptes « Open » ont accès à LinuxFR.org par IPv6.

----------> []

Je n'ai pas vérifié la configuration de ce réseau (je peux essayer de le faire), mais comme NetworkManager manifestement demande une IPv4 par DHCP et ne l'obtient pas, je ne crois pas que ce soit juste désactivé à son niveau…

Non, le problème ne se produit pas quand elle se connecte directement à la Livebox, seulement sur le répéteur.

Je n'ai pas non plus regardé les autres appareils de mes propres yeux mais elle dit qu'ils fonctionnent bien avec le Wifi du répéteur (en plus de bien fonctionner en mobile et sur le Wifi de la Livebox). Et il n'y a aucun VPN dans l'histoire.

Tu serais surpris de ce qui peut sortir même de chez Google. D'accord, le crawler de Google Search est probablement bon. Mais il y a deux ans, SourceHut a dû menacer de blacklister les serveurs de Google qui maintiennent le cache des paquets Go, parce que ces serveurs mettaient SourceHut sous un quasi-DDoS en faisant des git clone complets (alors qu'il n'en avaient pas besoin), indépendamment sans se coordonner entre eux. Apparemment le même dépôt pouvait se retrouver cloné 2000 fois par jour !

https://linuxfr.org/users/vendrediouletrollsauvage/liens/les-infrastructures-du-libre-attaquees-par-des-entreprises-de-l-ia