Wiki du LAMA (UMR 5127) - Contributions [fr]

Mise en ligne des calendriers

2010-10-06T06:53:25Z

Tom Hirschowitz : /* Calendrier labo et/ou calendrier personnel en lecture/écriture */

== Introduction ==

Vous pouvez vous abonner aux calendriers suivants :
* votre agenda planète
* calendrier séminaires
* calendrier labo (évènements importants du labo : deadline ANR par exemple)

Pour cela, vous devez configurer un client sur votre machine (voir ci-dessous).
Nous avons testé différents clients et nous recommandons le client Mulberry qui existe sur toutes les plateformes (Linux, Windows et Mac). Les habitués du client Ical sous Mac peuvent aussi le garder.
Dans un calendrier coexistent les notions d'évènements (bien gérés par mulberry) et la notion de tâches (bien pris en charge pour les calendriers personnels mais très mal gérés par la plupart des clients pour les calendriers partagés (celui du laboratoire par exemple), en gros la communication avec le serveur ne se fait que partiellement voire pas du tout).

Pour le calendrier planète : il y a une petite manipulation que Christophe ou Céline doivent faire pour chaque personne.

Vous pouvez aussi stocker vos agendas personnels sur le serveur du labo (voir fin de la doc), ce qui permet de les voir depuis plusieurs postes de travail (y compris i-phone et sans doute Androïd phone).

<font color="#FF0000">News </font>: le client Lightning de Mozilla Thunderbird est disponible pour les architectures 32 et 64 b sous Linux et s'intalle facilement commme extension de Thunderbird (attention à la compatibilité éventuelle avec Thunderbird 3.0). Téléchargement ici : https://help.ubuntu.com/community/ThunderbirdLightning puis suivre les indications pour l'installation (menu Adds-on de Thunderbird).

Pour afficher un agenda type webcalendar avec Lightning : Menu Agenda --> nouvel agenda --> sur le réseau --> type ical --> entrer l'URL pour chaque calendrier en lecture comme c'est indiqué ci-dessous.
Pour les calendriers perso et labo en écriture : idem mais de type caldav et il y a alors une demande d'authentification par le serveur caldav.

== Calendrier planète ==

On peut depuis mi-novembre 2009 avoir accès au calendrier planète !

Il faut donner à Christophe Raffalli ou Céline Acary-Robert votre nom ou pour ceux qui ont des homonymes qui enseignent à UdS, une chaine de caractères permettant de trouver votre agenda dans planète. Une fois que l'on a mis en place l'import du calendrier, l'URL du calendrier est

'''<nowiki>http://www.lama.univ-savoie.fr/ADE/calendar_lachainederecherche.ics</nowiki>'''

Exemple, pour Stéphane Simon, la chaîne "simon s" lui permet de trouver son agenda et l'URL est (il faut parfois remplacer les espaces par '''%20''').

'''<nowiki>http://www.lama.univ-savoie.fr/ADE/calendar_simon%20s.ics</nowiki>'''

Le calendrier est mis à jour une fois par nuit à partir du serveur planète (si celui-ci n'est pas en panne).

== Calendrier séminaires et laboratoire en lecture ==

Un serveur Caldav a été installé sur le serveur du labo. Il permet de gérer des calendriers et de les afficher sur une page web (voir le calendrier du labo [http://www.lama.univ-savoie.fr/index.php?frame=1&titre=Calendrier%20du%20LAMA&height=1200px&page=http://www.lama.univ-savoie.fr/phpicalendar ici]) ou affiché dans un client sur une machine perso.

=== Calendrier séminaires ===

Il s'agit ici d'afficher dans le client choisi un calendrier publié sur le web au format ics. Il faut donc créer un '''web calendar''' qui a pour URL

'''<nowiki>http://www.lama.univ-savoie.fr/icalsem.php</nowiki>'''

avec les options suivantes :

* begin=2003:01:01 (par défaut c'est 100 jours en arrière)
* equipes=lama,edp,logique,geometrie (au choix, par défaut c'est tous les séminaires qui sont affichés)

Exemple, si vous voulez juste le séminaire de géométrie et les sémaire la labo, il faut mettre:

'''<nowiki>http://www.lama.univ-savoie.fr/icalsem.php?equipes=lama,geometrie</nowiki>'''

=== Calendrier laboratoire ===

Un calendrier du laboratoire a été mis en place. Il contiendra des évènements d'intérêt général (deadline ANR, conseil d'UFR, ...)

L'url est '''<nowiki>https://www.lama.univ-savoie.fr/cal/public.php/labo-resources/public</nowiki>''' (attention, c'est du https)

=== Calendrier séminaire et labo sur le Web sans client iCal ou autre ===

Il y a [http://www.lama.univ-savoie.fr/index.php?frame=1&titre=Calendrier%20du%20LAMA&height=1200px&page=http://www.lama.univ-savoie.fr/phpicalendar là un petit calendrier visible sur le site web directement]. IL y a aussi un lien sur ce calendrier à
partir des [https://www.lama.univ-savoie.fr//index.php?use=interne&&lang=fr pages internes du labo]

=== Autres calendriers ===

Calendrier commun avec Plume (le séminaire LIMD-Plume y est dupliqué, mais il y a aussi d'autres évènements spécifiques à Plume) :
'''<nowiki>http://www.google.com/calendar/ical/qe60dn1sjrfk8c1fji62rvi7mo%40group.calendar.google.com/public/basic.ics</nowiki>'''

Calendrier du groupe de lecture Catégories :
'''<nowiki>https://www.lama.univ-savoie.fr/cal/public.php/cat-res/public/</nowiki>'''

== Calendrier labo et/ou calendrier personnel en lecture/écriture ==

Vous pouvez stocker un calendrier sur le serveur du labo (grâce au serveur CALDAV qui y est installé) afin de pouvoir y accéder de partout ...Ces calendriers peuvent être affichés dans un client sur une ou plusieurs machines.
Pour cela, il faut demander la création d'un compte à un administrateur (Christophe Raffalli, Frédéric Mangolte, Céline Acary-Robert, Claudia Billat) et configurer un client calendrier sur votre machine.
Une fois votre compte CALDAV crée sur le serveur, vous avez accès à un calendrier personnel et au calendrier du laboratoire si vous avez le droit. Seul les clients mulberry (linux, windows et OSX) et iCal (OSX) marchent. Sunbird devrait marcher bientôt ...

Sur mulberry, il faut créer un compte de type '''CalDav''' et renseigner le nom du serveur ''www.lama.univ-savoie.fr'', le chemin '''/cal/''' et ensuite son login (le mot de passe est demandé pour authentification sur le serveur). Il faut aussi indiquer que l'on utilise un accès crypté.

Pour iCal, il faut indiquer l'URL suivante (avec parfois des problèmes pour accepter le certificat SSL du serveur) :

'''<nowiki>https://www.lama.univ-savoie.fr:443/cal/caldav.php/votre_login/home/</nowiki>'''

<b>Bien mettre le '/' à la fin.</b>

Pour voir des informations sur son compte dans un navigateur web:

'''<nowiki>https://www.lama.univ-savoie.fr/cal/users.php</nowiki>'''

Le mieux est de demander à Christophe ou Céline ...

Chronique de naissance (liste de mails en français)

2008-02-13T07:50:32Z

Tom Hirschowitz :

== Tom : 18 septembre 2007 15H02 ==

Un petit challenge pour ton systeme de types, est-ce que tu sais
convertir ce code caml (qui ne type pas en caml, mais qui type en
coq) en pml?

type 'var lam = Var of 'var | App of 'var lam * 'var lam | Lam of ('var option) lam

let rec lam f = function
Var x -> Var (f x)
| App (e, e') -> App (lam f e, lam f e')
| Lam e -> Lam (lam (lift f) e)
and lift f = function
| None -> None
| Some x -> Some (f x)

== Christophe : 18 septembre 2007 15H36 ==

Oui ça marche, pourquoi ça coince en OCaml ?

type option(A) = [ None[] | Some[A] ]

type rec lam(var) =
[ Var[var] | App[lam(var) * lam(var)] | Lam[lam(option(var))] ]

val rec lam f = fun
Var[x] -> Var[f x]
| App[e,e'] -> App[lam f e, lam f e']
| Lam[e] -> Lam[lam (lift f) e]

and lift f = fun
None[] -> None[]
| Some[x] -> Some[f x]

== Tom : 24 octobre 2007 8H38 ==

Je sais pas qui ma reponse peut interesser, donc hesitez pas a me
demander de vous degager pour la prochaine fois, mais:

C'est chouette, et ca parait assez naturel de considerer la creation
d'une cloture comme imperative dans le cas du letrec. Aneffet,
comment on compile let rec f x = ... f ...?

1) On alloue le bloc a l'avance sans l'initialiser.

2) On calcule la valeur en pointant vers le bloc (et en esperant ne
pas acceder a ses champs).

3) On met a jour le bloc avec la valeur calculee.

Si ca c'est pas de l'imperatif.

== Christophe : 11 décembre 2007 20H48 ==

Bonsoir,

Cet après-midi, je disais à Pierre que j'étais content car j'avançais
... et je voyais où j'allais ..
mais bon j'en était à devoir écrire la fonction "localise" rendant un
terme clos si possible et donnant une erreur autrement ....
En fait, cette fonction ne sert à rien ! En voici la raison :

val e =: t est l'intersection de deux choses :
- des valeurs "static" (le mot clef du C) dans les records
- des types singletons pour les champs des records.

1°) Examinons d'abord les valeurs "static" avec une nouvelle syntaxe:

mu s. {
....
val static l = t
...
}

Comment les compiler: pour chaque occurrence de static dans le code on
alloue une case mémoire au démarrage du programme
(pour un pointeur), initialisé à NULL. On apellera cette case mémoire
l'adresse de "l"

t ne dépendant pas des variables liées par lambda, la valeur de mu s.t
ne dépend que de la partie de l'environnement contenant
les autres variables et cette partie de l'environement sera toujours la
même et est identifiée à la compilation (en fait dans l'interpréteur de
pml bindlib le fait tout seul).

Lorsque l'on évalue un champs static, on teste si son adresse contient
NULL et si c'est le cas, on crée la clôture <mu s.t, e>
où e est la partie utile de l'environement et on stocke son adresse à la
place allouée.

Pour une projection: si le typage détecte que s.l est un accès à une
valeur static, on sait que le record a été contruit et donc que
l'adresse de l
contient un pointeur sur une clotûre c. On évalue alors (c s). On a ici
un self dynamique, mais on a imposé la restriction qui fait que la
sémantique est la même
que pour le self dynamique. Sauf, pour l'ordre d'évaluation. t étant
gardé par "mu s." il n'est évalué qu'à la projection (il faut que le
programmeur le sache).

2°) Comment tester la contrainte que mu s.t ne dépend pas des lambda :
c'est un test facile sur la typing map:

- On type t sans hypothèse sur s, si t dépend de x:a autrement que via s
alors, il y a une variable de type b typant un sous terme de t tel que
"a inclus dans b" est une des contraintes de la typing map ... Trop facile !
- Ensuite on ajoute les contraintes sur s pour que t soit complètement
typé et en accord avec les types des autres champs qui peuvent dépendre
des variables liées par lambda.

3°) Les types singletons sont nécessairement static. En effet,
considérons le type

Pi x:t.{val static l = x} qui définit une forme d'identité ...C'est la
cas le plus simple de type singleton sous lambda. Il faut bien les type
dépendant pour l'écrire.
Les types dépendants sont totalement incompatible avec PML. Donc pas de
dépendance avec Pi dans les types.

4°) Comment implémenter les types singletons (c'est là que c'est amusant):

Lorsque je type et que je proof-check en même temps, j'ai un contexte
Gamma qui contient des tas d'infos sur les variables libres (leur valeur
parfois) ...

Donc, le type de t dans la signature { ... val static l = t ... } est
donc simplement (t,Gamma) !!!! Il me faut alors une fonction testant si
(t,Gamma) = (t',Gamma').
Il y a de la place pour en écrire des tas, il faut commencer par la plus
simple même si elle est trop stricte ... (Remarque Gamma et Gamma' on en
général un segment initial commun, mais on s'en fout)

5°) On a donc plus de fonction localise, juste une égalité ... mais
cette égalité sera à réutiliser pour la règle de réfléxivité de
l'égalité lorsque PML aura une égalité polymorphe ...

Et ba voilà tout est maintenant très clair, je me mets au boulot !

à demain,
Christophe

== Christophe : 12 février 2008 22H45 ==

En corrigeant un de mes bugs je viens de découvrir ce que sont les
typing maps et l'algo de typage de PML:

(j'ai failli sauté 100 lignes pour le suspence)

ce sont des réseaux et un critère de correction !!!

En lambda-calcul simplement typé intuitionniste avec la flèche et le et,
cela correspondrait à une traduction bizarre du type:

[A -> B] = !([A] -o [B]) (et oui, on copie la fonction !!! j'ai fait un
interprête du lambda-calcul comme ça en DEA)
[A et B] = (![A] tenseur ![B])

Mais attention, on va construire le réseau en faisant plein de choses en
même temps:
- minimiser le nombre des boites et donc le nombre de !
- minimiser le contenu des boites
- normaliser le réseau en testant un critère d'acyclicité ... c'est tout
aussi exponetiel qu'un critère avec switch et acyclicité, sauf que
tester tous les switch
est toujours exponentiel alors que normaliser ne l'est pas toujours.

La vraie question est pourquoi dois-je mêtre des ! dans les & ... car
c'était cela mon bug qui n'acceptait pas assez de programmes (perte de
complétude ?)

Sur ce à demain .. entre mes trois cours/TD.

== Tom ==

C'est vachement attirant comme vision des choses, mais est-ce
que tu sais ''définir'' le tout sous cet angle? Genre, c'est un
peu ce qu'on essayait de faire en voiture au retour de Choco l'autre fois,
sans être allés très loin.

PML

2008-01-18T09:50:20Z

Tom Hirschowitz :

PML : Proved ML or Programmable Mathematical Logic

[http://www.lama.univ-savoie.fr/~raffalli/pml La page web]

[http://www.lama.univ-savoie.fr/~raffalli/pml/manual.pdf User's manual]

[[ Chronique de naissance (liste de mails en français) ]]

==Discussions en cours==

* Compilo? Cible probable LLVM.
* Généralisation.
* Spécifications et preuves.
* Exemples (notamment en utilisant "untyped").
* Mise à jour de la doc.
* Révisions: PML le langage.