Coq Setup

Posted on October 2, 2012

Tags: hacksoft

install opam

sudo bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)"

init opam

opam init
eval $(opam env)

if on RHEL, you will get “error [ERROR] Missing dependencies – the following commands are required for opam to operate: - patch.”

sudo dnf install patch

then try again

1 install vscoq

You must set the path to the installed coqtop from coq

which coqtop
#output may be

DO NOT USE RELATIVE PATH when editing the vscoq preferences
about output is ~/.opam/default/bin/coqtop but we use absolute path and take only the directory of coqtop: /home/rhel/.opam/default/bin/

opam repo add coq-released https://coq.inria.fr/opam/released
opam search compcert
opam install coq-compcert

opam search vst
opam install coq-vst

Change key setting Coq: Interpret to Point Alt+ Right arrow
Ctrl Alt P, >Coq: Interpret to Point click the settings icon next to it
Edit it to Shift + Right arrow

2 Software foundations

Do not open the folder as a workspace