Nix: установка ssreflect

Я использую Coq (версии 8.5-6), установленный с Nix. Я хочу установить ssreflect, желательно также с Nix. Единственная информация, которую я нашел об этом, находится здесь. Однако речь идет не об установке ssreflect, а просто о его испытании. Тем не менее, я попытался попробовать это, но в итоге получил сотни предупреждений (о содержимом различных файлов .v и .ml4) и не мог дождаться завершения процесса. Довольно типичное предупреждение выглядело так:

Файл "./algebra/ssralg.v", строка 856, символы 0-39: Предупреждение: неявные аргументы устарели; вместо этого используйте аргументы

Итак, вопрос: как мне установить ssreflect с Nix?

РЕДАКТИРОВАТЬ: после прочтения комментариев ejgallego кажется, что установка ssreflect с Nix - особенно невозможна. если нужно установить только ssreflect без других модулей (fingroup, algebra и т. д.). Итак, у меня также следующий вопрос:

Будет ли стандартная установка Opam или make install ssreflect работать с Coq, установленным Nix?


installation nix coq ssreflect opam
person jaam    schedule 09.06.2017    source источник
comment
Эти предупреждения, к сожалению, нормальны, поскольку разработчики их не исправили. Сборка ssreflect занимает очень много времени, особенно если вы хотите собрать весь пакет и его многочисленные библиотеки. Вы можете либо отредактировать команду ssreflect Make, чтобы удалить некоторые библиотеки, либо просто разделить пакет на части. Это зависит от ваших потребностей, например, OPAM распространяет math-comp в виде 5 отдельных пакетов из-за своего размера.   -  person ejgallego    schedule 10.06.2017
comment
Если вы планируете использовать только плагин тактики, он включен в Coq 8.7, однако обратите внимание, что тактика действительно не очень полезна без хотя бы основной библиотеки.   -  person ejgallego    schedule 10.06.2017

Ответы (1)


arrow_upward
2
arrow_downward

Есть несколько вещей, о которых вам нужно знать:

  • Nix - это менеджер пакетов на основе исходного кода с двоичным кешем. Многие пакеты предварительно собраны и доступны в бинарном кеше, поэтому их установка не занимает много времени; некоторые пакеты (в частности, библиотеки разработки) предварительно не собраны и Nix, при их установке потребуется время, необходимое для их компиляции. Пожалуйста, проявите терпение: вам нужно будет дождаться полной компиляции только в первый раз (и да, math-comp выдает много предупреждений при компиляции); в следующий раз пакет будет уже доступен в вашем местном магазине Nix.

  • Поскольку OPAM также основан на исходном коде, использование OPAM вместо Nix не поможет вам сэкономить время. Вы не можете смешивать Coq, установленный Nix, с SSReflect, установленным в OPAM, потому что последний будет нуждаться в первом в качестве зависимости OPAM.

  • Nix использует библиотеки не для их установки, а для их загрузки с помощью nix-shell. nix-shell "установит" библиотеки и задаст для вас некоторые переменные среды (например, $COQPATH в данном случае).

  • Вы также можете скомпилировать пакет из исходного кода самостоятельно, используя Coq, установленный Nix, но вы не можете запустить make install, потому что это попытается установить SSReflect в том же месте, где установлен Coq, но хранилище Nix не изменяемо. Вместо этого вы можете пропустить этот шаг и настроить $COQPATH вручную.

  • Действительно, составление полной математической компиляции занимает очень много времени. Есть более легкий пакет Coq ssreflect. Получить его можно с помощью:

    nix-shell -p coqPackages_8_6.ssreflect
person Zimm i48    schedule 11.06.2017
comment
Nix использует библиотеки не для того, чтобы устанавливать их, а вместо этого загружать их с помощью nix-shell. Спасибо, это многое объясняет - person jaam; 11.06.2017
comment
Мне потребовалось много времени, чтобы понять это. В частности, в случае с Coq, потому что я не привык думать о нем как о языке программирования. - person Zimm i48; 11.06.2017
comment
У меня есть новый вопрос, связанный с этим - person jaam; 14.06.2017