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

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

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

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

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

Будет ли стандартный Opam или make install установка ssreflect работает без установленного Nix Coq?

Источник

1 ответ

Решение

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

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

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

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

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

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

    nix-shell -p coqPackages_8_6.ssreflect
Источник
Другие вопросы по тегам