Различные версии одной и той же библиотеки в Coq - PullRequest
Новая
       75

Различные версии одной и той же библиотеки в Coq

0 голосов
/ 18 мая 2018

Можно ли установить несколько версий одной и той же библиотеки в Coq?Если да, как мне выбрать, с какой версией я хочу работать?

Я работаю в Windows, поэтому, к сожалению, любые решения с использованием OPAM мне не помогут.

Ответы [ 2 ]

0 голосов
/ 18 мая 2018

Вы можете использовать -R, чтобы сообщить coq, что определенный каталог соответствует определенному пространству имен.(обратите внимание, что -R принимает два параметра, каталог и пространство имен!)

Давайте создадим два каталога и скомпилируем две версии.Обратите внимание, что мы должны сообщить coqc уже во время компиляции, что файлы в каталоге должны находиться в пространстве имен MyLib, а не в том, что пространство имен по умолчанию оказывается. 

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)

Теперь для использования libv1 для MyLib

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

(для печати a := 1.) и использование libv2 для MyLib

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

(для печати a := 2.)

Вы также можете поместить флаг -R и его параметры в файл _CoqProject, чтобы вам не приходилось постоянно помещать его в командную строку.Это также понимает Proof General.

EDIT: использовать переменную COQPATH, а не флаг -R: 

(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
0 голосов
/ 18 мая 2018

Лучшее решение - установить библиотеки в отдельные каталоги, используя правильную переменную DESTDIR в coq_makefile, а затем установить COQPATH для включения правильных каталогов.Это стиль работы Nix и OPAM.

Непроверенный пример, где Makefile происходит от 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
...