Créer un compteSe connecter
Je vais bientôt faire un programme de recherche avec un assistant de preuve et tout le monde dans le labo utilise emacs.
:Sage_comme_une_image_Long_Version2:

J'utilise pour le moment un plugin vim qui me permet de reproduire plus ou moins l'expérience emacs pour cet assistant de preuve mais je doute fortement que ce sera compatible avec leurs outils
:meh2:


Me conseillez-vous d'installer une distribution préconfiguré ou de me contenter de la version vanilla?
:pepepipe:
La meilleure façon de châtier les hommes est de toujours donner ce qu'ils réclament.
il y a 2 ans
Un assistant de preuve ?
Je vous aime tous
:love:
Tu ne fais pas exception
il y a 2 ans
Un assistant de preuve ?
oui, un langage de programmation permettant de formaliser des arguments mathématiques et de les faire vérifier automatiquement.
Tu peux écrire tes propres définitions ; par exemple ici une syntaxe pour une logique de premier ordre avec des règles d'introduction/évaluation
Image

on peut ensuite démontrer des lemmes ; par exemple ici un cas particulier de cut elimination
Image


Ici j'utilise le langage coq.
:KaguyaCafe:
La meilleure façon de châtier les hommes est de toujours donner ce qu'ils réclament.
il y a 2 ans
emacs ? de ce que je sais, seuls les fanatiques de stallman et quelques universitaires l'utilisent
:fran_ok4:
La meilleure façon de châtier les hommes est de toujours donner ce qu'ils réclament.
il y a 2 ans
je ne bosse pas dans le dev à proprement parler :Konmignon:
il existe une extension vscode pour coq, mais il faut accepter de vendre son âme à microsoft. Puisque personne dans le labo ne l'utilise je préfère rester sur des logiciels libres.
La meilleure façon de châtier les hommes est de toujours donner ce qu'ils réclament.
il y a 2 ans
@Miko tu connais emacs ?
:Cligne:
La meilleure façon de châtier les hommes est de toujours donner ce qu'ils réclament.
il y a 2 ans
:Chat_sad:
La meilleure façon de châtier les hommes est de toujours donner ce qu'ils réclament.
il y a 2 ans
pareil :Konmignon:
c'est agréable de pouvoir préserver sa configuration par ssh
La meilleure façon de châtier les hommes est de toujours donner ce qu'ils réclament.
il y a 2 ans
ils sont particulièrement rapides et peuvent être intégrés facilement dans un environnement tmux
:Possiblement:
La meilleure façon de châtier les hommes est de toujours donner ce qu'ils réclament.
il y a 2 ans
Je vois. Quel était l'autre choix à 42?
:Reflechis:
c'est étrange d'imposer un éditeur de texte
La meilleure façon de châtier les hommes est de toujours donner ce qu'ils réclament.
il y a 2 ans
Yoneda
Yoneda
2 ans
Je vais bientôt faire un programme de recherche avec un assistant de preuve et tout le monde dans le labo utilise emacs.
:Sage_comme_une_image_Long_Version2:

J'utilise pour le moment un plugin vim qui me permet de reproduire plus ou moins l'expérience emacs pour cet assistant de preuve mais je doute fortement que ce sera compatible avec leurs outils
:meh2:


Me conseillez-vous d'installer une distribution préconfiguré ou de me contenter de la version vanilla?
:pepepipe:
J'ai testé emacs doom et le problème c'est que c'est mal documenté donc au final pas si pratique que ce qu'on pourrait éspérer.

Autant rester sur la version de base avec evil pour avoir des raccourcis clavier plus adaptés
:gamerz:
il y a 2 ans
Si tu connais elisp c'est cool par-ce que tu peux faire faire ce que tu veux a emacs, c'est très pratique pour écrire des papiers scientifiques askip
:pepepipe:
il y a 2 ans
J'utilise des print en python et gdb en c (en particulier pour les segfaults)
:lain_sourire2:


Si tu veux une interface, il existe toujours des plugins github.com https://github.com/mfussenegger/nvim-dap
La meilleure façon de châtier les hommes est de toujours donner ce qu'ils réclament.
il y a 2 ans
Yoneda
Yoneda
2 ans
oui, un langage de programmation permettant de formaliser des arguments mathématiques et de les faire vérifier automatiquement.
Tu peux écrire tes propres définitions ; par exemple ici une syntaxe pour une logique de premier ordre avec des règles d'introduction/évaluation
Image

on peut ensuite démontrer des lemmes ; par exemple ici un cas particulier de cut elimination
Image


Ici j'utilise le langage coq.
:KaguyaCafe:
stylé
:base:
il y a 2 ans-PEMT
Yoneda
Yoneda
2 ans
oui, un langage de programmation permettant de formaliser des arguments mathématiques et de les faire vérifier automatiquement.
Tu peux écrire tes propres définitions ; par exemple ici une syntaxe pour une logique de premier ordre avec des règles d'introduction/évaluation
Image

on peut ensuite démontrer des lemmes ; par exemple ici un cas particulier de cut elimination
Image


Ici j'utilise le langage coq.
:KaguyaCafe:
C'est plaisant comme panel de couleurs
:Chiffonne:
La Image Boucle
il y a 2 ans-PEMT
J'ai testé emacs doom et le problème c'est que c'est mal documenté donc au final pas si pratique que ce qu'on pourrait éspérer.

Autant rester sur la version de base avec evil pour avoir des raccourcis clavier plus adaptés
:gamerz:
De ce que j'ai pu comprendre, emacs est plus proche d'un repl Lisp que d'un éditeur de texte.
Evil, c'est pour avoir les raccourcis vim? Il ne risque pas d'y avoir des conflits si j'installe d'autres plugins?
La meilleure façon de châtier les hommes est de toujours donner ce qu'ils réclament.
il y a 2 ans
J'utilise Vim pour a peu près tout perso
:rikadrink:
:kiwi-jmp:
:OrangeRikaContent:
il y a 2 ans
Glock
Glock
2 ans
C'est plaisant comme panel de couleurs
:Chiffonne:
github.com https://github.com/morhetz/gruvbox
:chatfloreuh:
La meilleure façon de châtier les hommes est de toujours donner ce qu'ils réclament.
il y a 2 ans
Merci, je n'y comprend pas grand chose au logiciel mais je vais certainement garder les codes couleurs
:Sage_comme_une_image_Long_Version2:
La Image Boucle
il y a 2 ans
C'est simple mais terriblement efficace
:KaguyaCafe:
La meilleure façon de châtier les hommes est de toujours donner ce qu'ils réclament.
il y a 2 ans