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.
  Deux méthodes d'installation vous sont proposées :
  • 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.
  • Via docker : installation d'une mini-VM toute faite contenant un Ubuntu muni de OCaml, Coq et emacs.
    C'est plus simple, mais bien plus long (les chargements peuvent prendre 1h voire bien plus suivant le débit internet de votre connexion.
    Il faut également prendre des dispositions spéciales pour que les fichiers écrits sous docker soient convenablement sauvegardés et récupérés sur votre espace disque hôte.
  Nous recommandons d'essayer en premier la méthode directe 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 vous rabattre sur docker.

  ---

• 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.

  ---

• Méthode par docker
  Se reporter à docker.html.