TigerCoq

From PLSwiki

Jump to: navigation, search

Coq on tiger.itu.dk

tiger.itu.dk currently runs Coq 8.2pl1 and ssreflect 1.2.

Setting up Coq

To run Coq, add the following lines to "~/.profile": 

PATH="/opt/coq/bin:$PATH"
export COQTOP="/opt/coq/lib/"
export COQLIB="/opt/coq/lib/"
export COQBIN="/opt/coq/bin/"

and the following line to "~/.emacs": 

(load-file "/opt/ProofGeneral/generic/proof-site.el")

Setting up ssreflect

To run ssreflect, add the following line to "~/.emacs" (or change your existing custom-set-variables command): 

(custom-set-variables '(coq-prog-name "/opt/coq/bin/ssrcoq"))
Retrieved from "http://www.itu.dk/research/pls/wiki/index.php/TigerCoq"
Personal tools