Resources

 

Installing the Coq proof assistant

Make sure you have the Coq proof assistant working before the first lecture.

  • There are several ways to install Coq (Version 8.13). Make sure to enable/install the "equations" package. 
    • Linux/macOS/Windows: Install the Coq Platform.
    • Linux/macOS: Install Coq via the the OCaml package manager opam. See also Coq-on-Linux.
    • Windows: Download the Windows installer from the release page.
  • There are three user interfaces for Coq: CoqIDE, Proof General, and VSCode. You can choose which one you want to use.
    • CoqIDE: You can download and install CoqIDE along with the rest of Coq via opam and it is included in the Windows installer. Documentation about CoqIDE can be found here.
    • Proof GeneralProof General is an emacs mode that supports many theorem provers, including Coq. Using Proof General, Company Coq is an extension allowing you to look up lemmas and the Coq Documentation. Both Proof General and Company Coq can be installed via the emacs package archive melpa.
    • VSCode: You can interact with Coq using VSCode using the VSCoq plugin.

 

Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators.