Forum Programmation.autre Question sur Coq et la tactique induction

Posté par  . Licence CC By‑SA.
Étiquettes :
2
24
oct.
2019

Bonjour à tous

Récemment, j'ai décidé de m'intéresser un peu à la théorie des types et de la démonstration. Quelques vieilles dépêches y sont pour un peu, et le sujet m'avait toujours un peu intrigué.
Après quelques recherches, j'ai trouvé et commencé l'excellent Logic Foundations.
J'en suis arrivé lentement mais sûrement au chapitre sur les propositions inductives (IndProp).
Et là j'ai un petit soucis…

Lemma le_trans : forall m n o, m <= n -> n <= o
(…)

Forum Programmation.autre [Latex] Création de liste dans un template

Posté par  . Licence CC By‑SA.
Étiquettes : aucune
0
7
oct.
2019

Bonjour,
petit problème de latex, j'essaie de faire un template de cv, il me faut une fonction pour générer une liste, le but est d'avoir:

fruit
- poire
- pomme
légume
- carotte
poison
- cyanure
- curare

Bon, ensuite je mettrait ça dans un tableau tout joli, mais pour l'instant je bloque sur la récupération des éléments.

Mon fichier tex contient:

\comp{
    {fruit, {{poire}, {pomme}}},
    {légume, {carotte}},
    {poison, {{cyanure}, {currare}}}
}

Et mon template.cls

% settings comp
\newcommand{\comp}[1]{
    \renewcommand{\givencomp}{
(…)

Forum Programmation.autre Rust, Haskell, composition, monad et arrow

Posté par  . Licence CC By‑SA.
Étiquettes : aucune
0
30
sept.
2019

Salutation à vous,

Tout est dans le titre, en vrac…

Voilà, depuis des années je ne code sérieusement qu'en Haskell, et j'ai envie de voir du pays, pourquoi pas rust ? Je me suis lancé dans un petit projet à base de opencv, et j'ai la tête remplie d'idiomes Haskell. Typiquement, pour appliquer une série de traitement à une image de manière séquentielle, en Haskell on fait :

algorithme = preprocessing >>=
             traitement1 >>=
             traitement2 >>=
             \i -> traitement3
(…)

Forum Programmation.autre Conky et condition (if)

Posté par  . Licence CC By‑SA.
Étiquettes :
0
26
août
2019

Affiche "plop" dans un shell :

if [[ "1" == "1" ]]; then echo "plop";else echo "not good"; fi

Affiche "not good" dans le conky :

${execp if [[ "1" == "1" ]]; then echo "plop";else echo "not good"; fi  }

Pourquoi ?
Comment effectuer une comparaison de deux strings avec bash dans le conky ?

Le but est de faire tourner cette comparaison de deux signatures TLS dans le conky :

${alignc}${font :size=7}${execp certSecure=$( openssl s_client -connect 88.191.250.176:443 -servername
(…)

Forum Programmation.autre question théorique sur l'assembleur

Posté par  . Licence CC By‑SA.
Étiquettes : aucune
1
20
août
2019

bonjour à tous,

je vous donne l'instruction qui me pose probleme, ca sera plus simple pour expliquer :

add ax, PTR BYTE [bp - 0x02]

dans le cas ou j'utilise un processeur 8086 avec un bus d'adresse de 20 bits et un bus de donnés de 16 bits.

comment en une instruction qui ne peut pas dépasser 16 bits, je peux contenir à la fois l'oppcode (ADD), le registre(ax), et l'adresse de 20 bits contenu dans PTR BYTE [bp - (…)

Forum Programmation.autre question sur le processeur 8086 et les cycles d'horloge

Posté par  . Licence CC By‑SA.
Étiquettes : aucune
2
29
juil.
2019

Bonjour,

dans les processeurs 8086, en assembleur quand je fais l'intruction sub a,b :
le compilateur va remplacer cette instruction par un not b + inc b + ADD a,b soit 3 cycles d'horloge pour réaliser la soustraction?

De nos jours avec les processeurs actuels, il y a j'imagine pour optimiser la place dans la RAM une seul instruction pour réaliser une soustraction, mais prend elle toujours 3 cycle d'horloge ?

Merci d'avance pour vos éclaircissements.

Forum Programmation.autre aide en assembleur quand je lance objdump -M intel -DTCs ./a.out

Posté par  . Licence CC By‑SA.
Étiquettes : aucune
0
21
juil.
2019

Bonjour à tous,

Je m'interesse depuis peu à l'assembleur grace à la belle commande objdump. Néanmoins je tombe sur quelques problemes de compréhension au niveau assembleur et j'aurais bien besoin de vos lumieres.

Voici l'extrait de code :

    0000000000000540 <_start>:
     540:   31 ed                   xor    ebp,ebp
     542:   49 89 d1                mov    r9,rdx
     545:   5e                      pop    rsi
     546:   48 89 e2                mov    rdx,rsp
     549:   48 83 e4 f0             and    rsp,0xfffffffffffffff0
     54d:   50                      push   rax
     54e:   54                      push   rsp
     54f:   4c 8d 05
(…)

Forum Programmation.autre Migrer un repo git interne vers gitlab

Posté par  . Licence CC By‑SA.
Étiquettes :
1
13
juil.
2019

Salut à tous,

Je viens d'être embauché comme responsable informatique (sys et dev) par une petite boite qui a fait l'erreur de sous traiter ses developpements à une SSII qui bosse en dehors de nos locaux.
Cette SSII gère le code via un git interne chez eux. J'aimerai qu'ils migrent l'ensemble du code de l'application vers un repo sur gitlab.com.
J'aimerai aussi conserver l'historique des versions dans la branche master et mais aussi les branches en cours.
Vu que je (…)

Forum Programmation.autre Comment écrire un client mail pour Linux ?

Posté par  (site web personnel) . Licence CC By‑SA.
Étiquettes :
0
9
juil.
2019

Bonjour,

J'essaye actuellement de développer un client mail pour GNOME (en GTK). J'aimerais autant que possible ne pas réinventer la roue. Par exemple, j'utilise la libgoa pour les informations de connexion. J'arrive pour le moment à récupérer toutes les informations de l'utilisateur : pour chaque compte, les host IMAP et SMTP ainsi que les information d'authentification.

Maintenant, je dois me mettre aux clients IMAP et SMTP, mais je ne suis pas sûr de la meilleure façon de faire : dois-je (…)

Forum Programmation.autre [Résolu] Conky - Insérer string dans pipe vide

Posté par  . Licence CC By‑SA.
Étiquettes :
1
27
juin
2019

Je souhaiterais insérer "no output" lorsque la pipe suivante est vide, et ne pas l'altérer si elle contient quelque chose.

${execpi 60 nc 10.8.42.42 7634 -w 1 | sed 's/|//m' | sed 's/||/\n/g' | awk -F'|' '{print $3"°"$4 " " $2 " ("$1")" " "}' | sort -r }

Dans un Shell j'y arrive avec la commande suivante

nc 10.8.42.42 7634 -w 1 | sed 's/|//m' | sed 's/||/\n/g' | awk -F'|' '{print $3"°"$4
(…)

Forum Programmation.autre Qt : positionnement "proportionnel" d'un bouton

Posté par  . Licence CC By‑SA.
Étiquettes :
1
24
avr.
2019

Bonjour,
je cherche à faire un truc assez simple avec Qt :
J'ai une fenêtre avec une image comme fond d'écran, et le fond d'écran se redimensionne avec la fenêtre. Jusque là tout va bien.
Je voudrais rajouter un bouton qui se positionne à un endroit précis de l'image, et qui se redimensionne aussi si la fenêtre change de taille (à peu près, on n'est pas au pixel près).
J'ai plus ou moins trouvé une solution assez compliquée avec un (…)

Forum Programmation.autre Polling ou Interrupt ?

Posté par  . Licence CC By‑SA.
Étiquettes : aucune
4
25
mar.
2019

Bonjour,

Dans le cas de lecture socket, sous quelles conditions doit-on préférer faire du polling plutôt que des interruptions ?
J'image peut-être à tort, que le traitement de l'interruption est assez long (Ne serait-ce que le réveil du processus et du chargement de son contexte par le noyau).

Imaginons que cela prenne 4 secondes. Cela donne le schéma suivant : (m==messayge, tt==traitement, p==processus)

                    tt1
                    ^
     p2  ───────xxxx────────────────────────────────>t
                ^              
                │              
                │              
     p1  ───────┴───────────────────────────────────>t
                m1              

Dans le cas du polling :

Polling (…)

Forum Programmation.autre Question grammaire française.

Posté par  . Licence CC By‑SA.
Étiquettes : aucune
0
5
mar.
2019

Bonjour à tous !

je me posais une question assez bête.

Le contexte, nous sommes lundi
A dit à B qu'il ne peut pas aller à un évènement mardi
B rapporte à C ce que A lui a dit :

« il m'a dit que s'il avait pu y aller, il y serait allé »

Pourquoi est-ce qu'on utilise le plus-que-parfait ici ?
Je n'arrive pas à quel cas cela correspond.

Si quelqu'un peut éclairer ma lanterne, je lui dois (…)

Forum Programmation.autre Devops

Posté par  . Licence CC By‑SA.
Étiquettes : aucune
2
4
déc.
2018

Bonjour
Je lance un appel a un devops pour connaître svp une journée type de travail dun devops.
Et plus généralement les technologies ?
Et est ce qu'il faut etre plutot un bon developpeur web ou pas la peine?

Je me pose pas mal la question et si une ame charitable pouvait nous aiguiller la dessus ce serait vraiment formidable.

Merci a vous tous.

Forum Programmation.autre Développement application IOS / Android

Posté par  . Licence CC By‑SA.
Étiquettes :
1
23
oct.
2018

Bonjour,

Quel serait le meilleur moyen pour porter une un site internet de messagerie instantanée HTML5 / socket.io / node.js en application native Android / IOS ?

Avez vous des retours d'expérience de phonegap ou autre point de vue performance, stabilité, push notification ?

Merci.

Forum Programmation.autre [Rust] : lire des données de type i8 depuis un fichier

Posté par  . Licence CC By‑SA.
Étiquettes : aucune
3
22
oct.
2018

Bonjour.

Suite à une discussion récente à propos de Rust sur ce forum, ma curiosité a été piquée et j'ai décidédé de m'y mettre. Je bloque cependant sur un problème et je sollicite votre aide pour pouvoir m'en sortir.

Je suis en train de tenter de lire le contenu d'un fichier qui contient plusieurs types de données. En gros j'essaie de désérialiser ces données.

J'ai lu mes données dans un buffer d'u8:

    let mut header = [0u8; HEADER_SIZE];

    // Opening
(…)

Forum Programmation.autre Github ne supporte pas (les fichiers) libreoffice (en pièces jointes des tickets) ?

Posté par  (site web personnel, Mastodon) . Licence CC By‑SA.
6
17
sept.
2018

Travaillant sur preview-generator (un module python de prévisualisation générique de documents), nous avons un bug sur un document de type "tableur". Quoi de plus naturel que de remonter un ticket sur le dépôt github ? Et d'y joindre - cela va de soi, le fichier en question pour pouvoir reproduire !

Et bien en fait non, le format .ods n'est pas accepté dans les tickets github. Pas grave, on peut mettre un zip.

Oui mais… .xlsx, .docx (…)

Forum Programmation.autre http session sécurité

Posté par  . Licence CC By‑SA.
Étiquettes : aucune
0
24
juin
2018

Salut.

Je voudrais faire un système de session sécurisé pour utiliser en http serveur<->clients.

Donc côté serveur, par défaut chaque visiteur n'ayant pas de cookie dans le http reçu est vu comme visiteur.

S'il veut s'identifier et qu'il fait une bonne combinaison user-password correspondant:
1- je crée un nombre unique et j'envoie au client par http la création d'une cookie ayant comme valeur le nombre unique
2- je crée dans le serveur une session_id chiffré en regroupant:
- le nombre (…)