Remonter

Consignes pour installer l'environnement de travail en PF et en LT

(filière INFO4)

Les cours LT et PF nécessitent un environnement de travail permettant d'éditer, tester, exécuter et prouver des programmmes fonctionnels, et d'étudier la sémantique de langages de programmation. Cet environnement comporte :
- le langage de programmation fonctionnel OCaml ;
- l'assistant à la preuve Coq, (qui embarque lui-même un langage de programmation proche de OCaml) ;
- l'éditeur de programmes emacs, avec des paquetages convenables pour OCaml et Coq.
Méthode d'installation :
- Méthode directe : via des commmandes à effectuer au terminal.
  C'est la méthode la plus rapide (environ 20mn), qui requiert le moins d'espace et sur laquelle vous avez le plus de contrôle ; elle est plus modulaire, les composants peuvent être installés incrémentalement ; et elle exerce vos compétences en administration de système linux.
Nous recommandons d'utiliser la méthode proposée en suivant les instructions ci-dessous, et en cas de difficulté (dans ce cas, merci de récupérer les diagnostics et de les envoyer aux enseignants), de nous solliciter pour résoudre les problèmes ou essayer des méthodes alternatives.
Méthode directe
Commencer par récupérer le fichier d'initialisation pour emacs ltpf_2020.emacs ainsi que les intructions détaillées dans le pseudo-script instructions_install.pseudo-sh.
Ce fichier log peut être utile en cas de difficulté.
Recopier ltpf_2020.emacs sous ~/.emacs. Il est suggéré de commencer par installer emacs puis son système de packages car c'est le plus rapide.
Installer également opam, le système de packages pour OCaml (et Coq).
L'installation de emacs et de opam se fait via le système de packages de la distribution linux, par exemple apt sur Debian ou Ubuntu.
Lorsque opam est installé, il est facile d'installer OCaml proprement dit puis Coq, ainsi que quelques outils facilitant la programmation comme merlin.
L'éditeur emacs (avec le package proof-general) est un très bon environnement d'édition de script Coq ; on peut aussi utiliser coqide à cet effet, dont l'installation dépend de davantages de packages système ou opam.