UP | HOME

Installation et test de Coq

Table of Contents

Installation de coq - Version 8.10

  • Instructions : voir https://github.com/coq/coq/releases/tag/V8.10.2.
    • Mac os x : utiliser l'installateur fourni.
    • Windows : utiliser l'installateur fourni.
    • Linux
      • Installer opam (OCaml Package Manager) : voir https://opam.ocaml.org/doc/Install.html.
      • Installer Coq en utilisant Opam : voir https://coq.inria.fr/opam-using.html.

        > opam init ou > opam init --disable-sandboxing (si bwrap absent)
          - accepter la modification du fichier de configuration du shell bash_profile 
        > eval $(opam env)   
        > opam switch create avec_coq 4.05.0 (si version courante d'Ocaml < 4.05)
        > opam switch avec_coq
        > eval $(opam env)
        > opam pin add coq 8.10.2 (pin évite les mises à jour automatiques)
        
  • Vérification :

    > coqc -v
    

Environnements de développement

Solution 1 - Installation de Visual Studio Code - Version 1.41

Solution 2 - Installation de CoqIDE - Version 8.10

  • Instructions : voir https://github.com/coq/coq/releases/tag/V8.10.2.
    • Mac os x : utiliser l'installateur fourni.
    • Windows : utiliser l'installateur fourni.
    • Linux
      • Installer CoqIDE en utilisant Opam.

        > opam install coqide (requiert le paquet libgtksourceview-3.0-dev)
        

Solution 3 - Utilisation mixte - Recommandé

  • Il est possible d'utiliser CoqIDE avec un éditeur externe. Il suffit de configurer correctement les préférences (Externals > External Editor) puis d'ouvrir cet éditeur externe lors de l'édition d'un fichier avec la commande Edit > External editor.
  • Un fonctionnement mixte est possible :
    • édition avec code,
    • sauvegarde dans code,
    • mise à jour du fichier dans CoqIDE, par la commande File > revert all buffers,
    • exécution avec CoqIDE.
  • Enfin, pour formater joliment un fichier .v, faute d'outil dans code ou CoqIDE, on peut procéder ainsi.
    • Dans CoqIDE, créer un makefile : Compile > Make makefile.
    • Dans le répertoire où se trouve le makefile, lancer la cible beautify.

      > make beautify
      

Test

  • Dans un répertoire, ouvrir l'environnement de développement.

    code

    > code . &
    

    coqide

    > opam switch avec_coq # sous Linux
    > eval $(opam env)     # sous Linux
    > coqide &
    
  • Créer un nouveau fichier, d'extension .v (pour vernacular, le langage de commandes de Coq). Y copier le code suivant.
Definition F1 : nat -> nat.
  fix REC 1.
  intro n.
  (destruct n as [| pn]).
  {
    exact 1.
  }
  {
    exact (S pn * REC pn).
  }
Defined.

Eval vm_compute in F1 5.
Print F1.

Fixpoint F2 (n : nat) : nat := match n with
                               | 0 => 1
                               | S pn => n * F2 pn
                               end.
  • L'exécuter pas à pas par la commande Alt+Flèche-Bas avec code ou la flèche pointant vers le bas, dans la barre des outils, avec CoqIDE. D'autres commandes sont disponibles : voir la palette, en cherchant Coq, avec code ou la barre des outils avec CoqIDE.
  • Dans la fenêtre Sortie ou Messages, les résultats apparaissent.
  • Que font ces fonctions ?

Author: Hervé Grall
Version history: v1: 2019-12-20.
Comments or questions: Send a mail.
The webpage content is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.