Coder but Gamer

C’est un article du 3 Juillet que j’avais posté sur mon précédent blog et que j’ai envie de “sauver” ici.

Warning : Ce tutorial peut être suivi de manière totalement linéaire. Je l’ai rédigé car je n’ai pas trouvé de how-to pour faire quelque chose aussi bateau que cela. Il est basé (niveau documentation) sur les 3 liens qui concluent l’article. Il peut être suivi de la même façon en préfixant les paths de ssh:// pour faire du git sur ssh. Il faut surtout ne pas penser en architecture “clients/serveur” à la CVS/SVN mais penser que l’on a des dossiers avec lesquels on peut se synchroniser. Et donc l’envoi de fichier(s) est distinct du “commit”.

Notation et Contexte : M1 pour Machine 1 qui contiendra le repository “public” et sur laquelle on peut coder également (donc update et commit). M2 pour Machine 2 qui ne fait que coder / update / commit.

Créer un repo sur M2

Ça semble assez logique car c’est là que l’on a les sources mais on pourrait faire dans l’autre sens (mais PAS de manière symétrique !). On commence donc sur M1.

cd mes_sources/
git config --global user.name "my name"
git config --global user.email me\@u.com
git init

Faire le premier commit (import)

git add ce_que_l_on_veut
git commit

(git commit fait récursivement les dossier comme svn)

Mettre en place le dépot (repository) public sur M1

/!\ On est toujours sur M2

git clone --bare ~/mes_sources/ mes_sources.git
touch mes_sources.git/git-daemon-export-ok
scp -r mes_source.git login\@M1:.

(ou où l’on veut, ou n’importe quel moyen de copier de ce dossier de M2 vers M1) Nota : Il peut être avisé de créer un login spécial (du style : “git”) sur M1 afin qu’il puisse être accédé par tout le monde.

Commit depuis M1 sur M1

/!\ On est maintenant sur M1

mkdir codeur_M1 && cd codeur_M1 (optionel)
git clone chemin_vers_repo_public (ou git clone login\@localhost:chemin_vers_repo_public)

Effectuer des envois de fichier

/!\ Restons sur M1

modifiez ce que vous voulez dans votre copie privée du repo (le dossier SANS .git) puis

git commit -a -m "tous les fichiers modifiés"

Note : si on veut seulement envoyer certains fichiers on ne fait que :

• git add fichier1 fichier2 fichier3

• git commit -m "certains fichiers"

git push

Envoie effectivement les fichiers

Travailler la première fois depuis M2

/!\ Nous sommes maintenant sur M2

git pull login\@M1:repo_public.git

faire des changements et un commit

git push login\@M1:repo_public.git

Si on fait un git pull depuis le répertoire (repo privé) où on travaille sur les sources (celui SANS .git) sur M1 on voit que les changements ont été répercutés. On constate par cette commande qu’il n’y a plus besoin de dire de où on pull (pareil pour push) une fois la première commande exécutée : c’est sauvegardé dans .git/config en tant que remote “origin”. On remarque également que l’on peut push à un endroit et pull à un autre. On peut changer les “lieux” des git push/pull à tout moment soit dans le .git/config soit en spécifiant le chemin.

En résumé (schéma tiré du manuel de GIT)

                      you push
your personal repo ------------------> your public repo
      ^                                     |
      |                                     |
      | you pull                            | they pull
      |                                     |
      |                                     |
      |               they push             V
their public repo <------------------- their repo

Quelques commandes

git push

ou

git push login\@machine:repo_public

pour envoyer les fichiers

git pull

ou

git pull login\@machine:repo_public

pour prendre les fichiers

git commit -a

pour faire un

git add

des fichiers modifiés et les commit

Exactement comme pour SVN :

• git rm

• git mv

• git status

• git log

• git blame

Des liens

1. Équivalents GIT/SVN (mais attention au mode de pensée !)
2. Un tutorial assez complet
3. Le manuel entier de GIT

Je me suis librement inspiré d’Intelligence Artificielle de Russel & Norvig, du Polycopié de Logique et Mécanisation de l’Inférence de Ricardo Caferra, et de Wikipedia.

En 1920, David Hilbert a lancé un programme de recherche visant à donner une base formelle aux mathématiques. Un ensemble d’axiomes de base à partir desquels on pourrait prouver tous les théorèmes mathématiques qui sont  des (énoncés de) vérités dans ce “monde imaginaire dont on crée les règles”. Kurt Gödel a démontré, avec son premier théorème d’incomplétude, qu’il existe des énoncés (formules closes) arithmétiques vrais qui sont impossibles à prouver. Ce fut dès lors la fin du rêve d’Hilbert d’unifier les mathématiques sur une base formelle.

Voici une esquisse de la preuve (la preuve complète, de Gödel, fait 30 pages) de ce théorème dans un but de vulgarisation à des personnes ayant des bases de mathématiques mais pas de logique. J’essaye ici de donner plus la forme et l’idée qui devraient permettre de comprendre le résultat de Gödel qu’une preuve formelle qui demanderait des connaissances en logique mathématique. Ceux qui veulent sont toujours à même d’aller consulter Wikipedia pour avoir des définitions formelles ou la preuve complète.

I) Définition d’un langage pour l’arithmétique
Commençons par énumérer les entiers, il nous faut :
• la constante 0
• la fonction S, successeur
S(0) = 1, S(S(0)) = 2 . . . On a construit les entiers. On dit qu’ils sont récursivement énumérables.
On rajoute à ce langage les fonctions ‘+’, ‘x’, ‘exp’ (la mise à la puissance si vous préférez), ainsi que les quantificateurs existentiel et universel et les connecteurs logiques non, et, ou, implication.

II) Numération de Gödel
L’ensemble des énoncés que l’on peut écrire dans ce langage est énumérable. Par exemple si l’on définit un code pour chacun des symboles de base (S()=’1′, +()=’2′, x()=’3′ …), un énoncé peut-être codé par la concaténation des codes des symboles qui le composent. On numérote ainsi les énoncés avec leur nombre de Gödel #E. À chaque énoncé E correspond une ou plusieurs preuves. Une preuve P étant une suite d’énoncés, on peut elle-même la numéroter par son nombre de Gödel G(P).

III) Construction d’un énoncé particulier
Prenons un ensemble A récursivement énumérable d’énoncés vrais à propos des entiers naturels (le point important est que l’on puisse les compter). On peut écrire un énoncé E=(j, A) qui serait : ∀ i, i ≠ G(P(E)) avec {P(E)} ⊆ A et #E=j, qui se lit “pour tout i, i n’est pas le nombre de Gödel de la preuve, utilisant seulement des hypothèses A, d’un énoncé dont le nombre de Gödel est j”.  Autrement dit, un énoncé dont le nombre de Gödel est j est improuvable avec seulement les hypothèses A. Soit F l’énoncé (#F, A) construit comme ci-dessus, c’est un énoncé qui affirme sa propre non-prouvabilité à partir de A. “Un énoncé dont le nombre de Gödel est #F est improuvable avec seulement les hypothèses de A”. F est l’énoncé qui se dit non prouvable à partir de A, nous n’avons pas encore prouvé sa véracité.

IV) “Diagonalisation”, par l’absurde
Montrons maintenant par l’absurde que F n’est pas prouvable à partir de A. Supposons que F soit prouvable à partir de A, alors F est faux (puisqu’on peut le prouver alors qu’il dit le contraire). F est faux et prouvable à partir de A donc A n’est pas constitué seulement d’énoncé vrais, ce qui est en contradiction avec notre hypothèse de départ. (Parenthèse : si l’on accepte de contredire l’hypothèse de départ, notre théorie n’est pas cohérente et n’a donc pas de sens.) Donc F n’est pas prouvable à partir de A et donc F est vrai (c’est ce qu’il affirme).

<< Dans n’importe quelle théorie récursivement axiomatisable, cohérente et capable de « formaliser l’arithmétique », on peut construire un énoncé arithmétique qui ne peut être ni prouvé ni réfuté dans cette théorie. >> (Wikipedia) On peut aussi le voir comme ceci : il n’existe pas d’ensemble d’axiomes de base qui permettent de démontrer l’ensemble des vérités arithmétiques.

Remarque : Le langage arithmétique pourrait (devrait) contenir avoir la comparaison (’<’) et le raisonnement par induction complète mais ça ne fait que complexifier les choses ici.

J’espère avoir écrit quelque chose de digeste …

Quelques autres des photos prises à Londres :

La relève de la garde :

Le museum d’histoire naturelle :

Panoramique depuis l’observatoire de Greenwich (le méridien passe 30m à gauche) :

Et du tower Bridge pour finir …

J’ai récupéré chez mes parents (Noël !) un 50 f/1.7, un 28 f/2.8 et un 70-210 f/3.5 avec macro embrayable (à pompe) de leur vieux ME pour mon K20D.

J’ai shooté en RAW en me disant que je ferais des traitements, des panoramas … j’ai un peu la flemme ! En voici quelques-unes (un bout d’une journée), on commence par des essais de tonemappings :

Je ne suis pas très content de mes tonemaps mais bon, ce sont les premiers ! Plus de tonemapping à présent :

J’ai appris pleins de choses sur mon appareil (Pentax K20D) notament au niveau de la gestion du bruit (on constate qu’ici c’est pas top) et de la dynamique. Et surtout qu’il faut utiliser le 18-55 kit au minimum au profit des 28 et 50 fixes. C’est dommage, j’ai effacé une photo faite au 18-55 en focale 28 du tate modern de nuit et la même avec le 28 fixe, la différence de netteté est saisissante (toutes deux étaient posées sur le parapet). La suite un de ses jours peut-être …