Index of /~monin/EnseignementPublic/Misc/MCAL/install_coq_perso

Name	Last modified	Size

Parent Directory		-
README.html	2024-03-31 17:06	2.2K
README.md	2024-03-31 17:06	1.4K
Version_compilee_8.11/	2024-03-31 17:06	-
Version_compilee_8.13/	2024-03-31 17:06	-
Version_compilee_IM2AG_8.9/	2024-03-31 17:06	-
Version_compilee_coq-8.15_OCaml-4.11.1/	2024-03-31 17:06	-
Version_compilee_coq-8.15_OCaml-4.13.1/	2024-03-31 17:06	-
untypedLC.v	2024-03-31 17:06	43K
untypedLC.v.gz	2024-03-31 17:06	9.2K

MCAL λ README install

Il faut avoir préalablement installé Coq en suivant par exemple les instructions données dans

http://www-verimag.imag.fr/~monin/Enseignement/LTPF/robuste/commun/installation/install.html

Ces instructions permettent en fait d’installer un environnement plus complet comprenant, en dehors de coq et de l’interface coqide (disponibles aussi sur les machine IM2AG), une autre interface pour emacs appelée proof-general ainsi que le langage OCaml.

Le présent répertoire contient un fichier coq à utiliser pour expérimenter du λ-calcul non typé en Coq. Attention, vous devez disposer d’une version de Coq suffisamment récente (8.9 ou suivantes). Ce n’est pas forcément le cas de la version de Coq fournie par les paquetages de Debian ou Ubuntu. Il faut au final obtenir un fichier untypedLC.vo (du coq préalablement compilé) dans le répertoire de travail.

Différents formats sont proposés :

à la racine, la version source (ainsi qu’une version compressée par gzip en cas de pbs avec les accents) à compiler chez soi par la commande :

coqc untypedLC.v

(quelques warnings sans importance sont émis).
sous les répertoires Version_compilee_XXX, une version précompilée pour différentes versions de Coq (la version du compilateur OCaml utilisé semble significative aussi, à partir de coq_8.15.)

Version html de cette page produite par :
pandoc -s --metadata pagetitle="MCAL λ README install" -o README.html README.md