On Windows and MacOS

Install Coq

Use the official windows and mac installers downloadable here: https://coq.inria.fr/download

Install Pactole

The Pactole package dedicated to those tutorials (zip archive) is available here. Uncompress it in a directory that you can read, say, /full/path/to/pactole. The library must be compiled for coq-8.6.1.

Start coqide

You should be able to start coqide from the graphical interface of windows and macos. You will need a few more steps to be able to use pactole from coqide, see Section Start a pactole-ready coqide.

On Linux

opam is a packaging system and the easiest way to install coq nowadays. It allows one to update coq versions and switch between versions. The coq opam page is here.

Installing opam

Lots of linux distributions have a package for opam.

On Debian:

sudo apt-get update
sudo apt-get install opam

Other distribs

See there: http://opam.ocaml.org/doc/Install.html if your distrib has a package or how to install it another way.

Installing coq

DON'T USE YOUR DISTRIB PACKAGE SYSTEM,
Most of them are not up to date.

opam init # y to accept modifying .profile and .ocamlinit

opam pin add coq 8.6.1
# y to confirm
# compiles coq and its libraries
# takes ~ 5mn (up to 10mn on slow laptops)

opam pin add coqide 8.6.1
# y to confirm
# take 1-3mn

Add opam directory to your path

PATH=~/.opam/system/bin:$PATH
#(put this in your favorite shell init file)



The example file for the Coq tutorial is available here.

Install Pactole

The Pactole package for the tutorials is available here. Uncompress it in a directory that you can read, say /full/path/to/pactole. The library must be compiled for coq-8.6.1.

Test Coq and pactole in a hurry

coqide -R /absolute/path/to/rep-pactole Pactole  myfirstcoq.v

(note that if opam is not in your path you can try ~/.opam/system/bin/coqide -R ...)

Write the following line in the buffer:

Require Import Pactole.Robots.

Hit [ctrl-down], if the line becomes blue and then green with no error, you are ready to go!

See the next section to make coqide easier to call.

Start a pactole-ready coqide

Have the coq options in a _CoqProject

Create a text file called (exactly) _CoqProjectin the directory dedicated to you coq dev. Put the coq option

-R /absolute/path/to/pactole Pactole

in this file and save it. (Unix shell users can do this with this commands: cd my-coq-dev ; echo "-R /absolute/path/to/pactole Pactole" > _CoqProject) From now on files located in the same directory as _CoqProjectwill be able to use pactole libraries.

Unix shell users: after these last steps calling coqide will need: coqide my-coq-dev/myfirstcoq.v.