CODEWITHSUNDEEP
librariescoqmultiple-versions
Rincewind
Rincewind

Reputation: 317

Diffent versions of same library in Coq

Is it possible to install several versions of the same library in Coq? If yes, how do I choose which version I want to work with?

I work in Windows so any solutions using OPAM are unfortunately not going to help me.

Upvotes: 1

Views: 255

Answers (2)

larsr
larsr

Reputation: 5811

You can use -R to tell coq that a certain directory corresponds to a certain name space. (note that -R takes two parameters, the directory and the namespace!)

Let's create two directories, and compile the two versions. Note that we must tell coqc already at compilation time that the files in the directory should be in the MyLib name space, not in what default namespace happens to be.

D1=~/Desktop/libv1
D2=~/Desktop/libv2

mkdir $D1; echo "Definition a:=1." > $D1/MyLib.v
(cd $D1; coqc -R . MyLib MyLib.v)

mkdir $D2; echo "Definition a:=2." > $D2/MyLib.v
(cd $D2; coqc -R . MyLib MyLib.v)

Now to use libv1 for MyLib

echo "Require Import MyLib. Print a." | \
coqtop -R $D1 MyLib

(that will print a := 1.) and to use libv2 for MyLib

echo "Require Import MyLib. Print a." | \
coqtop -R $D2 MyLib

(that will print a := 2.)

You can also put the -R flag and its parameters in a _CoqProject file so you don't have to put it on the command line all the time. It is also understood by Proof General.

EDIT: to use the COQPATH variable and not the -R flag:

(cd $D1; coqc MyLib.v) # compile without -R
(cd $D2; coqc MyLib.v)

# specify the dir using COQPATH
echo "Require Import MyLib. Print a." | COQPATH=$D1 coqtop

# or add it to the LoadPath when you're in coqtop interactively
echo "Add LoadPath \"$D1\". Require Import MyLib. Print a." | coqtop

Upvotes: 0

ejgallego
ejgallego

Reputation: 6852

The best solution is to actually install the libraries in separate directories, using the proper DESTDIR variable in coq_makefile and then set COQPATH to include the right directories. This is the style Nix and OPAM work.

Non-tested example where Makefile comes from coq_makefile:

$ ( cd lib-v1 && DESTDIR=~/coqlib/lib-v1 make install )
$ ( cd lib-v2 && DESTDIR=~/coqlib/lib-v2 make install )

$ export COQPATH=~/coqlib/lib-v1:$COQPATH
$ coqtop

Upvotes: 2

Related Questions