Je ne prétends pas débattre avec le niveau requis, mais peut on encore parler de démonstration quand c'est "trivial" et que cela tient en une ligne ?
Oui, pourquoi pas ? De même que les maths ont fait un bond en avant quand zéro a été reconnu comme un vrai nombre, la logique marche mieux quand on reconnaît aussi les démonstrations triviales comme de vraies démonstrations :-)
De ce que je comprends il y a une sorte de consensus qui considère que les preuves formelles n'ont pas besoin d'aller au delà d'un certain niveau de détail. Les résultats "triviaux" n'ont pas à être démontrés et peuvent simplement être placés dans une bibliothèque.
Je ne sais pas d'où tu tires cette impression mais soit j'ai mal compris ce que tu veux dire, soit c'est faux.
C'est quand même un peu le but de la preuve formelle que tout soit fait dans tous les détails y compris triviaux. Bien sûr, quand on est en plein développement, on peut laisser des lemmes triviaux comme admis pour les prouver plus tard, et il peut arriver qu'on les garde non prouvés dans le résultat fini, mais ce n'est pas commun (et quand c'est le cas, ça va normalement être mentionné explicitement).
Les projets de formalisation réussis que j'ai mentionnés (retournement de la sphère, etc.) n'utilisent aucun lemme admis (seulement des axiomes « logiques » comme le tiers exclu).
Et cette preuve « rfl » de 2+2=4 (plus généralement de l'égalité entre deux termes définitionnellement égaux) est bien une preuve, pas un appel à un lemme admis.
Notons tout de même que l'automatisation se développe énormément, d'abord la théorie des types en contient intrinsèquement une dose (l'égalité définitionnelle), ensuite Rocq comme Lean (et sûrement Agda, mais je connais moins bien) ont des tactiques qui font de la recherche automatique de preuve, et Lean a une tactique « simpl » très appréciée pour simplifier toutes sortes de buts. De manière plus générale, Rocq et Lean ont de grosses bibliothèques de tactiques (voir p.ex. https://rocq-prover.org/doc/V8.20.0/refman/coq-tacindex.html) pour faire plein d'étapes de preuve à la fois.
Par exemple, la preuve de 2+2=4 en Lean est triviale (c'est un exemple d'égalité définitionnelle) :
Lean est dominant dans le domaine de la formalisation des maths, mais Agda avance pas mal aussi, et largement dans une autre direction puisque la plupart des gens qui font de la théorie homotopique des types (dans l'une de ses variantes, p.ex. la théorie cubique des types) le font en Agda (certains le font en Rocq aussi, mais Lean ne le permet pas du tout). Et j'ai l'impression que Rocq reste le plus utilisé pour la vérification de programmes, mais c'est peut-être mon biais d'observation qui fait ça (parce que je suis plus au contact de la recherche qui se fait en France, et Rocq est développé par l'Inria et beaucoup utilisé dans les labos français) ; en tous cas c'est sûr que CompCert et Iris, des outils assez connus, sont construits sur Rocq.
Quoi qu'il en soit, je pense qu'il ne faut pas le voir comme un concours : c'est une bonne chose qu'il y a plusieurs outils en parallèle, parce que ça leur fait explorer des pistes différentes, ça évite le lock-in exclusif à un outil qui empêche l'innovation ensuite, etc.
Quelques différences entre Rocq et Lean :
Lean a une grosse particularité dans sa théorie des types, qui s'appelle la « proof irrelevance définitionnelle », et qui peut être très pratique mais a aussi pour conséquence de casser plein de bonnes propriétés théoriques de la théorie des types. Notamment, le type checking de Lean est une approximation d'un problème indécidable, et contrairement à presque toutes les théories de types, il existe en fait des programmes qui ne terminent pas (des termes non fortement normalisables). Rocq a fini par introduire cette particularité sous une forme plus faible qui n'a pas ces conséquences désagréables, mais pour garder la compatibilité avec l'existant, ils l'ont fait avec un autre univers de propositions, du coup on a deux univers, SProp et Prop, qui coexistent, et SProp n'est pas très agréable en pratique parce que toutes les librairies existantes sont écrites avec Prop.
Globalement, il y a plus de vieilleries dans Rocq, c'est un peu normal vu son âge. Il y a plein de fonctionnalités qui font des choses similaires mais pas tout à fait identiques, souvent pour des raisons de compatibilité. (Ltac vs Ltac2 vs Mtac, tactiques standard vs SSreflect, inductifs simples vs records, classes de type vs instances canoniques, #[refine] vs Program, etc.) De plus la bibliothèque standard de Lean est vraiment beaucoup mieux faite. C'est subjectif mais je pense que la plupart des gens seront d'accord pour dire que Lean est mieux ingéniéré et a tiré des leçons de certains aspects moins bien faits de Rocq.
Comme il s'adresse largement à des matheux qui n'y connaissent rien à la logique intuitionniste, Lean n'a pas peur d'utiliser le tiers exclu, et aussi d'autres axiomes comme l'extensionnalité fonctionnelle, l'extensionnalité propositionnelle, les types quotients et l'axiome du choix. Ça n'empêche pas de raisonner sans ces axiomes en Lean, mais c'est lourdingue parce que toutes les tactiques standard les introduisent même quand elles n'en auraient pas besoin.
Rocq, en plus de permettre de faire de la théorie homotopique des types, a des options « expertes » et parfois expérimentales qui permettent de jouer avec les détails de la théorie des types, que n'a pas Lean.
(Mais comme je l'évoque dans le billet, le ministre a aussi évoqué le terrorisme et la pédophilie, parce qu'il ne faudrait quand même pas oublier les bonnes vieilles recettes de grand-mère.)
Comme me l'a fait remarquer Patrick Massot, la ligne
Lean, créé par Leonardo de Moura et développé depuis 2013 chez Microsoft Research, écrit en C++, placé sous licence Apache 2.0.
contient des infos obsolètes : Leonardo de Moura ne travaille plus chez Microsoft Research, et contrairement à Lean 3, Lean 4 est principalement écrit en Lean 4 (je n'ai pas regardé comment c'était bootstrappé).
Est-ce qu'un modérateur voudrait bien corriger ça ? Merci !
Je ne suis pas développeur moi-même, pourtant je certifie que je passe énormément de temps à découvrir des bugs dans l'intranet de mon école, dans mon émulateur de terminal, dans Firefox, … 🙂 Certes, ce n'est pas moi qui écris les tests. Mais si un modérateur passe par là, on pourrait effectivement changer ça en « tous les développeurs (voire les autres !) passent … »
Entre ce journal, celui-là, celui-là, celui-là et maintenant celui-ci, vous faites un concours du journal le plus moinssé ? Le plus pédant ? Le plus hors-sujet ? Faites un petit effort, merci.
Armin Ronacher et Drew DeVault ont tous les deux écrit des billets de blog sur le marché des imprimantes 3D (je ne suis pas forcément d'accord, je pointe juste qu'ils sont intéressants) :
Personnellement, j'ai moinssé uniquement parce que, toute légitime que soit la cause des personnes victimes de racisme et de violences policières, ça n'a aucun lien même ténu avec le thème du site.
On peut être d'accord ou pas avec l'utilité des lettres de motivation dans la vie adulte. Je ne suis pas sûr d'être d'accord (surtout maintenant que ChatGPT en fait qui sont difficile à distinguer de lettres sincères), mais ce n'est pas le propos. Toujours est-il que le monde professionnel, dans son état actuel, exige ces documents, et qu'ils ont des codes assez stricts, comme ne pas commencer une lettre de motivation par le mot « je », mettre son nom en haut à gauche et le destinataire juste en-dessous à droite, donner ses qualités sans avoir l'air trop prétentieux, conclure par une formule très spécieuse comme « En souhaitant une réponse positive de votre part, je vous prie d'agréer, Madame, Monsieur, mes salutations distinguées » (et d'après certains, mettre « espérer » plutôt que « souhaiter » serait une faute), etc. Tant que ce sera le cas, je trouve que c'est une très bonne chose de former les élèves à cet exercice, et ça fait partie de la découverte du monde professionnel qui après tout est le but de ces stages.
Pour le CV, certes, c'est un peu difficile. Mais il y a quand même des choses qu'on peut mettre, comme tu l'as recommandé dans ton modèle (activités extrascolaires, langues, stages précédents, éléments liés au stage qu'on demande comme « j'ai lu tel livre de maths » ou « je connais tel langage de programmation », …). Et là aussi, l'intérêt est surtout d'apprendre que la mise en forme d'un CV se travaille énormément.
Du coup, le fait que les ados soient obligés de « singer les adultes » est certes un peu ridicule, mais finalement possiblement formateur. (Sinon, comme d'habitude, ce sont ceux qui auront appris ces codes de leur milieu familial qui s'en sortiront…)
Merci pour ce journal ! Je réfléchissais justement à en écrire un sur ma quête un peu désespérée d'un éditeur de texte qui me satisfasse.
J'ai utilisé Emacs plusieurs années, je continue de l'utiliser pour certaines choses et dans l'ensemble j'aime bien, mais je me suis arraché les cheveux avec les n systèmes de paquets différents et la difficulté de configurer un LSP. Le temps perdu m'a un peu refroidi.
Je suis donc passé à Helix pour la plupart des langages. J'aime beaucoup la configuration simple et lisible en TOML et la facilité d'utilisation des LSP. Le seul hic, c'est que je ne suis pas fan de l'édition modale. Je préfère les raccourcis avec Control, Alt et Control-Alt, et j'aime bien garder les bases des zones de texte de toutes les autres applications que mon éditeur de texte, à savoir : sélection avec Shift, mouvement mot par mot avec Control, et les raccourcis clavier de base Control-X, Control-C, Control-V. (Ça rend la navigation entre plusieurs applications plus fluide pour moi.)
Est-ce que quelqu'un connaîtrait une sorte d'équivalent de Helix, mais non-modal ?
(Un autre critère important est que l'éditeur puisse fonctionner dans un terminal, pour les sessions SSH.)
Thank you for contacting DigitalOcean Support. […] I understand your concerns around port 25, but unfortunately at this point of time, we are unable to review our decision to unblock SMTP on your account.
Bonjour, et merci. Je regarderai Scaleway. Je n'ai pas envie d'aller chez Amazon — je n'aime pas les giga-monopoles tout-puissants des GAFAM.
Pour DigitalOcean, il est possible de demander l'utilisation de la porte smtp/25
Comment ? Je n'ai pas trouvé.
Leur doc dit : « SMTP port 25 is blocked on all Droplets for new accounts to prevent spam and other abuses of our platform. » et ne cite pas de procédure pour demander un déblocage.
D'ailleurs, il n'y a aucune syntaxe pour les notes de bas de page dans la spécification CommonMark, même si beaucoup de librairies l'ajoutent en extension, activée par défaut ou non.
Les éditeurs de Markdown, ce n'est pas ça qui manque, et il y a aussi beaucoup d'éditeurs généralistes avec un bon mode Markdown. Je suis sûr que tu trouveras ton compte ailleurs. On peut faire des suggestions si tu précises tes besoins.
Je n'ai pas trouvé que les citations soient sorties de leur contexte, et d'autre part ce sont presque exclusivement des citations de billets sur son blog (pas de vidéos) et le lien vers son blog est toujours donné, donc il suffit de cliquer pour lire plus de contexte si on a un doute.
Je suis complètement d'accord avec le point (1). Pour que les choses soient parfaitement claires, je rappelle néanmoins que le rapport ne présente pas RMS comme un violeur ou un pédophile (« Stallman has also incited numerous controversies for advancing a political agenda which normalizes sexual misconduct and advocates for reforming our social and legal understanding of sexual conduct in a manner which benefits the perpetrators of abuse. »).
C'est probablement le cas en revanche de beaucoup de commentateurs, à tort (malheureusement, sur un sujet explosif, on retrouve habituellement des exagérations et accusations infondées dans tous les sens…).
Sur ton point (2), je suis aussi d'accord sur le fait que certaines accusations du rapport sont exagérées, et notamment sur la pédopornographie (après tout j'écrivais justement récemment qu'on ne peut pas poursuivre la propagation de pédopornographie à tout prix au détriment de toute considération de vie privée). Néanmoins, ce que j'apprécie avec ce rapport est qu'il est sérieusement documenté : toutes les citations sur lesquelles il s'appuie sont données in extenso, rien n'est affirmé sans s'appuyer sur des citations. Ce n'est donc pas une accusation à charge sans preuves, chacun peut lire et se faire une opinion. (À titre personnel, ce qui me choque le plus, et de loin, n'est pas dans les citations sur la pédopornographie mais sur la nécrophilie.)
[^] # Re: Preuves de programme et preuves de théorèmes
Posté par jeanas (site web personnel, Mastodon) . En réponse à la dépêche Programmer des démonstrations : une modeste invitation aux assistants de preuve. Évalué à 2 (+0/-0).
Oui, pourquoi pas ? De même que les maths ont fait un bond en avant quand zéro a été reconnu comme un vrai nombre, la logique marche mieux quand on reconnaît aussi les démonstrations triviales comme de vraies démonstrations :-)
Je ne sais pas d'où tu tires cette impression mais soit j'ai mal compris ce que tu veux dire, soit c'est faux.
C'est quand même un peu le but de la preuve formelle que tout soit fait dans tous les détails y compris triviaux. Bien sûr, quand on est en plein développement, on peut laisser des lemmes triviaux comme admis pour les prouver plus tard, et il peut arriver qu'on les garde non prouvés dans le résultat fini, mais ce n'est pas commun (et quand c'est le cas, ça va normalement être mentionné explicitement).
Les projets de formalisation réussis que j'ai mentionnés (retournement de la sphère, etc.) n'utilisent aucun lemme admis (seulement des axiomes « logiques » comme le tiers exclu).
Et cette preuve « rfl » de 2+2=4 (plus généralement de l'égalité entre deux termes définitionnellement égaux) est bien une preuve, pas un appel à un lemme admis.
[^] # Re: Preuves de programme et preuves de théorèmes
Posté par jeanas (site web personnel, Mastodon) . En réponse à la dépêche Programmer des démonstrations : une modeste invitation aux assistants de preuve. Évalué à 2 (+0/-0). Dernière modification le 24 mars 2025 à 17:45.
Notons tout de même que l'automatisation se développe énormément, d'abord la théorie des types en contient intrinsèquement une dose (l'égalité définitionnelle), ensuite Rocq comme Lean (et sûrement Agda, mais je connais moins bien) ont des tactiques qui font de la recherche automatique de preuve, et Lean a une tactique « simpl » très appréciée pour simplifier toutes sortes de buts. De manière plus générale, Rocq et Lean ont de grosses bibliothèques de tactiques (voir p.ex. https://rocq-prover.org/doc/V8.20.0/refman/coq-tacindex.html) pour faire plein d'étapes de preuve à la fois.
Par exemple, la preuve de 2+2=4 en Lean est triviale (c'est un exemple d'égalité définitionnelle) :
[^] # Re: Lean vs Rock
Posté par jeanas (site web personnel, Mastodon) . En réponse à la dépêche Programmer des démonstrations : une modeste invitation aux assistants de preuve. Évalué à 3 (+1/-0).
Lean est dominant dans le domaine de la formalisation des maths, mais Agda avance pas mal aussi, et largement dans une autre direction puisque la plupart des gens qui font de la théorie homotopique des types (dans l'une de ses variantes, p.ex. la théorie cubique des types) le font en Agda (certains le font en Rocq aussi, mais Lean ne le permet pas du tout). Et j'ai l'impression que Rocq reste le plus utilisé pour la vérification de programmes, mais c'est peut-être mon biais d'observation qui fait ça (parce que je suis plus au contact de la recherche qui se fait en France, et Rocq est développé par l'Inria et beaucoup utilisé dans les labos français) ; en tous cas c'est sûr que CompCert et Iris, des outils assez connus, sont construits sur Rocq.
Quoi qu'il en soit, je pense qu'il ne faut pas le voir comme un concours : c'est une bonne chose qu'il y a plusieurs outils en parallèle, parce que ça leur fait explorer des pistes différentes, ça évite le lock-in exclusif à un outil qui empêche l'innovation ensuite, etc.
Quelques différences entre Rocq et Lean :
Lean a une grosse particularité dans sa théorie des types, qui s'appelle la « proof irrelevance définitionnelle », et qui peut être très pratique mais a aussi pour conséquence de casser plein de bonnes propriétés théoriques de la théorie des types. Notamment, le type checking de Lean est une approximation d'un problème indécidable, et contrairement à presque toutes les théories de types, il existe en fait des programmes qui ne terminent pas (des termes non fortement normalisables). Rocq a fini par introduire cette particularité sous une forme plus faible qui n'a pas ces conséquences désagréables, mais pour garder la compatibilité avec l'existant, ils l'ont fait avec un autre univers de propositions, du coup on a deux univers,
SPropetProp, qui coexistent, etSPropn'est pas très agréable en pratique parce que toutes les librairies existantes sont écrites avecProp.Globalement, il y a plus de vieilleries dans Rocq, c'est un peu normal vu son âge. Il y a plein de fonctionnalités qui font des choses similaires mais pas tout à fait identiques, souvent pour des raisons de compatibilité. (Ltac vs Ltac2 vs Mtac, tactiques standard vs SSreflect, inductifs simples vs records, classes de type vs instances canoniques, #[refine] vs Program, etc.) De plus la bibliothèque standard de Lean est vraiment beaucoup mieux faite. C'est subjectif mais je pense que la plupart des gens seront d'accord pour dire que Lean est mieux ingéniéré et a tiré des leçons de certains aspects moins bien faits de Rocq.
Comme il s'adresse largement à des matheux qui n'y connaissent rien à la logique intuitionniste, Lean n'a pas peur d'utiliser le tiers exclu, et aussi d'autres axiomes comme l'extensionnalité fonctionnelle, l'extensionnalité propositionnelle, les types quotients et l'axiome du choix. Ça n'empêche pas de raisonner sans ces axiomes en Lean, mais c'est lourdingue parce que toutes les tactiques standard les introduisent même quand elles n'en auraient pas besoin.
Rocq, en plus de permettre de faire de la théorie homotopique des types, a des options « expertes » et parfois expérimentales qui permettent de jouer avec les détails de la théorie des types, que n'a pas Lean.
[^] # Re: Ne pas confondre
Posté par jeanas (site web personnel, Mastodon) . En réponse au lien [Mon blog] Recherche adultes pour empêcher le gouvernement de casser Internet. Évalué à 4 (+2/-0).
(Mais comme je l'évoque dans le billet, le ministre a aussi évoqué le terrorisme et la pédophilie, parce qu'il ne faudrait quand même pas oublier les bonnes vieilles recettes de grand-mère.)
# Ce n'est pas nouveau (mais ça reste d'actualité)
Posté par jeanas (site web personnel, Mastodon) . En réponse au lien Des chefs de polices EU demandent aux gouvernement d'agir contre le chiffrement des comm. (2024/09). Évalué à 4 (+2/-0).
Déjà posté ici à l'époque : https://linuxfr.org/users/glandos/liens/europol-s-oppose-aux-messageries-chiffrees
# Petite rectification
Posté par jeanas (site web personnel, Mastodon) . En réponse à la dépêche Programmer des démonstrations : une modeste invitation aux assistants de preuve. Évalué à 2 (+0/-0).
Comme me l'a fait remarquer Patrick Massot, la ligne
contient des infos obsolètes : Leonardo de Moura ne travaille plus chez Microsoft Research, et contrairement à Lean 3, Lean 4 est principalement écrit en Lean 4 (je n'ai pas regardé comment c'était bootstrappé).
Est-ce qu'un modérateur voudrait bien corriger ça ? Merci !
[^] # Re: Clichés
Posté par jeanas (site web personnel, Mastodon) . En réponse à la dépêche Programmer des démonstrations : une modeste invitation aux assistants de preuve. Évalué à 2 (+0/-0).
Merci !
[^] # Re: Clichés
Posté par jeanas (site web personnel, Mastodon) . En réponse à la dépêche Programmer des démonstrations : une modeste invitation aux assistants de preuve. Évalué à 4 (+2/-0).
Je ne suis pas développeur moi-même, pourtant je certifie que je passe énormément de temps à découvrir des bugs dans l'intranet de mon école, dans mon émulateur de terminal, dans Firefox, … 🙂 Certes, ce n'est pas moi qui écris les tests. Mais si un modérateur passe par là, on pourrait effectivement changer ça en « tous les développeurs (voire les autres !) passent … »
[^] # Re: Pour la complétude, j'ajoute le couple SPARK/Ada
Posté par jeanas (site web personnel, Mastodon) . En réponse à la dépêche Programmer des démonstrations : une modeste invitation aux assistants de preuve. Évalué à 3 (+1/-0).
Oui, voilà, ça m'a l'air d'être de la logique de Hoare, pas de la théorie des types.
[^] # Re: Il y a du contexte?
Posté par jeanas (site web personnel, Mastodon) . En réponse au journal Wikipédia:Lettre ouverte : non à l'intimidation des contributeurs bénévoles. Évalué à 5 (+3/-0).
La pétition demande d'être autoconfirmé (automatique au bout de quelques jours), pas autopatrouillé.
# Qu'est-ce qui se passe en ce moment ?
Posté par jeanas (site web personnel, Mastodon) . En réponse au journal HS : La "théorie du clan primal" vu par mon ami virtuel . Évalué à 8 (+7/-0).
Entre ce journal, celui-là, celui-là, celui-là et maintenant celui-ci, vous faites un concours du journal le plus moinssé ? Le plus pédant ? Le plus hors-sujet ? Faites un petit effort, merci.
# Liens
Posté par jeanas (site web personnel, Mastodon) . En réponse au journal Alors ? Vous êtes content de votre imprimante Bambu Lab ?!. Évalué à 3 (+2/-0).
Armin Ronacher et Drew DeVault ont tous les deux écrit des billets de blog sur le marché des imprimantes 3D (je ne suis pas forcément d'accord, je pointe juste qu'ils sont intéressants) :
https://lucumr.pocoo.org/2023/12/25/life-and-death-of-open-source/
https://drewdevault.com/2023/12/26/2023-12-26-Prusa-is-floundering.html
# Mise à jour
Posté par jeanas (site web personnel, Mastodon) . En réponse au journal Pas de milliardaires au FOSDEM. Évalué à 4 (+3/-0). Dernière modification le 20 janvier 2025 à 15:00.
DeVault a écrit un nouveau billet de blog pour s'expliquer davantage : https://drewdevault.com/2025/01/20/2025-01-20-FOSDEM-protest.html
[^] # Re: bloub
Posté par jeanas (site web personnel, Mastodon) . En réponse au lien Ed Zitron sur la merdification. Évalué à 1 (+0/-0).
Ah, désolé, je ne l'avais pas vu passer.
[^] # Re: Moinsage massif ?
Posté par jeanas (site web personnel, Mastodon) . En réponse au lien Victime d’une agression raciste, la police la met en garde à vue. Évalué à 2.
Personnellement, j'ai moinssé uniquement parce que, toute légitime que soit la cause des personnes victimes de racisme et de violences policières, ça n'a aucun lien même ténu avec le thème du site.
# Utilité
Posté par jeanas (site web personnel, Mastodon) . En réponse au journal On n’a pas de CV quand on a 14 ans. Évalué à 8. Dernière modification le 15 novembre 2024 à 17:13.
On peut être d'accord ou pas avec l'utilité des lettres de motivation dans la vie adulte. Je ne suis pas sûr d'être d'accord (surtout maintenant que ChatGPT en fait qui sont difficile à distinguer de lettres sincères), mais ce n'est pas le propos. Toujours est-il que le monde professionnel, dans son état actuel, exige ces documents, et qu'ils ont des codes assez stricts, comme ne pas commencer une lettre de motivation par le mot « je », mettre son nom en haut à gauche et le destinataire juste en-dessous à droite, donner ses qualités sans avoir l'air trop prétentieux, conclure par une formule très spécieuse comme « En souhaitant une réponse positive de votre part, je vous prie d'agréer, Madame, Monsieur, mes salutations distinguées » (et d'après certains, mettre « espérer » plutôt que « souhaiter » serait une faute), etc. Tant que ce sera le cas, je trouve que c'est une très bonne chose de former les élèves à cet exercice, et ça fait partie de la découverte du monde professionnel qui après tout est le but de ces stages.
Pour le CV, certes, c'est un peu difficile. Mais il y a quand même des choses qu'on peut mettre, comme tu l'as recommandé dans ton modèle (activités extrascolaires, langues, stages précédents, éléments liés au stage qu'on demande comme « j'ai lu tel livre de maths » ou « je connais tel langage de programmation », …). Et là aussi, l'intérêt est surtout d'apprendre que la mise en forme d'un CV se travaille énormément.
Du coup, le fait que les ados soient obligés de « singer les adultes » est certes un peu ridicule, mais finalement possiblement formateur. (Sinon, comme d'habitude, ce sont ceux qui auront appris ces codes de leur milieu familial qui s'en sortiront…)
# Précédemment
Posté par jeanas (site web personnel, Mastodon) . En réponse au lien « Un geste politique » : pourquoi Firefox continue d’être utilisé, malgré l’hégémonie de Chrome. Évalué à 4.
L'article fait suite à l'appel à temoignages du Monde qui avait déjà été posté ici : https://linuxfr.org/users/thoasm/liens/lemonde-fr-appel-a-temoignages-vous-etes-ou-avez-ete-utilisateur-de-firefox-racontez-nous
[^] # Re: Pas scaleway...
Posté par jeanas (site web personnel, Mastodon) . En réponse au message Cherche hébergeur pour VPS, avec quelques besoins spécifiques. Évalué à 1.
Merci pour le retour !
# Équivalent non-modal ?
Posté par jeanas (site web personnel, Mastodon) . En réponse au journal Helix, une excellent alternative à vim !. Évalué à 5.
Merci pour ce journal ! Je réfléchissais justement à en écrire un sur ma quête un peu désespérée d'un éditeur de texte qui me satisfasse.
J'ai utilisé Emacs plusieurs années, je continue de l'utiliser pour certaines choses et dans l'ensemble j'aime bien, mais je me suis arraché les cheveux avec les n systèmes de paquets différents et la difficulté de configurer un LSP. Le temps perdu m'a un peu refroidi.
Je suis donc passé à Helix pour la plupart des langages. J'aime beaucoup la configuration simple et lisible en TOML et la facilité d'utilisation des LSP. Le seul hic, c'est que je ne suis pas fan de l'édition modale. Je préfère les raccourcis avec Control, Alt et Control-Alt, et j'aime bien garder les bases des zones de texte de toutes les autres applications que mon éditeur de texte, à savoir : sélection avec Shift, mouvement mot par mot avec Control, et les raccourcis clavier de base Control-X, Control-C, Control-V. (Ça rend la navigation entre plusieurs applications plus fluide pour moi.)
Est-ce que quelqu'un connaîtrait une sorte d'équivalent de Helix, mais non-modal ?
(Un autre critère important est que l'éditeur puisse fonctionner dans un terminal, pour les sessions SSH.)
[^] # Re: Quelques options: AWS, Kamatera, Scaleway...
Posté par jeanas (site web personnel, Mastodon) . En réponse au message Cherche hébergeur pour VPS, avec quelques besoins spécifiques. Évalué à 1.
🙁
[^] # Re: Quelques options: AWS, Kamatera, Scaleway...
Posté par jeanas (site web personnel, Mastodon) . En réponse au message Cherche hébergeur pour VPS, avec quelques besoins spécifiques. Évalué à 1.
Bonjour, et merci. Je regarderai Scaleway. Je n'ai pas envie d'aller chez Amazon — je n'aime pas les giga-monopoles tout-puissants des GAFAM.
Comment ? Je n'ai pas trouvé.
Leur doc dit : « SMTP port 25 is blocked on all Droplets for new accounts to prevent spam and other abuses of our platform. » et ne cite pas de procédure pour demander un déblocage.
# Pas possible
Posté par jeanas (site web personnel, Mastodon) . En réponse au message [Résolu] Qownnotes - renvoi note bas de page. Évalué à 3.
Leur syntaxe Markdown est documentée là : https://github.com/pbek/qmarkdowntextedit/tree/000cc7227866bfc5edbdc68e9412a06c9bb6ec1b?tab=readme-ov-file#supported-markdown-features
Il n'y a pas les notes de bas de page.
D'ailleurs, il n'y a aucune syntaxe pour les notes de bas de page dans la spécification CommonMark, même si beaucoup de librairies l'ajoutent en extension, activée par défaut ou non.
Les éditeurs de Markdown, ce n'est pas ça qui manque, et il y a aussi beaucoup d'éditeurs généralistes avec un bon mode Markdown. Je suis sûr que tu trouveras ton compte ailleurs. On peut faire des suggestions si tu précises tes besoins.
[^] # Re: Ambivalence
Posté par jeanas (site web personnel, Mastodon) . En réponse au journal Publication du "Stallman Report" 2024. Évalué à 4.
Je n'ai pas trouvé que les citations soient sorties de leur contexte, et d'autre part ce sont presque exclusivement des citations de billets sur son blog (pas de vidéos) et le lien vers son blog est toujours donné, donc il suffit de cliquer pour lire plus de contexte si on a un doute.
[^] # Re: Ambivalence
Posté par jeanas (site web personnel, Mastodon) . En réponse au journal Publication du "Stallman Report" 2024. Évalué à 3.
Pourquoi ne pas simplement aller voir ce qu'écrit le rapport ?
[^] # Re: Ambivalence
Posté par jeanas (site web personnel, Mastodon) . En réponse au journal Publication du "Stallman Report" 2024. Évalué à 0.
Je suis complètement d'accord avec le point (1). Pour que les choses soient parfaitement claires, je rappelle néanmoins que le rapport ne présente pas RMS comme un violeur ou un pédophile (« Stallman has also incited numerous controversies for advancing a political agenda which normalizes sexual misconduct and advocates for reforming our social and legal understanding of sexual conduct in a manner which benefits the perpetrators of abuse. »).
C'est probablement le cas en revanche de beaucoup de commentateurs, à tort (malheureusement, sur un sujet explosif, on retrouve habituellement des exagérations et accusations infondées dans tous les sens…).
Sur ton point (2), je suis aussi d'accord sur le fait que certaines accusations du rapport sont exagérées, et notamment sur la pédopornographie (après tout j'écrivais justement récemment qu'on ne peut pas poursuivre la propagation de pédopornographie à tout prix au détriment de toute considération de vie privée). Néanmoins, ce que j'apprécie avec ce rapport est qu'il est sérieusement documenté : toutes les citations sur lesquelles il s'appuie sont données in extenso, rien n'est affirmé sans s'appuyer sur des citations. Ce n'est donc pas une accusation à charge sans preuves, chacun peut lire et se faire une opinion. (À titre personnel, ce qui me choque le plus, et de loin, n'est pas dans les citations sur la pédopornographie mais sur la nécrophilie.)