Skip to content

Latest commit

 

History

History
19 lines (17 loc) · 1.69 KB

Coq.md

File metadata and controls

19 lines (17 loc) · 1.69 KB
Raw

Coq

Software

Use designated versions of software in this class to avoid version incompatibility. Your submission will not be properly graded if you do not follow this instruction.

  • Use Coq 8.4pl5.
    • Coq is already installed in the lab.
    • For Linux:
      • Install opam, and make sure you can use OCaml 4.01.0.
      • Install libgtk2 by sudo apt-get install libgtk2.0-dev or sudo yum install gtk2-devel.
      • Install lablgtk2 by opam install lablgtk
      • Download tarball file.
      • Extract the tarball, ./configure -coqide opt, make, and then make install.
      • Test by coqc -v in the command line. Check your PATH variable if you get an error.
      • Run CoqIDE by coqide.
    • For Windows / OS X, I recommend you to download those with CoqIDE bundle (for Windows or for OS X).
      • In OS X, at first run, you may see an error message saying "Failed to load coqtop." Then click "No", and then find /Applications/CoqIDE_8.4pl5.app/Contents/Resources/bin/coqtop and open for once. Then goto CoqIDE > Preferences > Externals. And then change coqtop into /Applications/CoqIDE_8.4pl5.app/Contents/Resources/bin/coqtop.
    • For OS X, an alternative way to install Coq is using brew. See #1 for more details.
  • Use software foundations material in this repository (as explained in the Homeworks section below).