Как установить SSReflect и MathComp в Linux?

Question

Я успешно установил Coq 8.6 и CoqIDE в Linux (Ubuntu 17.04). Тем не менее, я не знаю, чтобы продолжить, чтобы добавить SSReflect и MathComp к этой установке. Все ссылки, которые я проверил, показались мне очень запутанными. У кого-нибудь есть прямой и простой рецепт к этому? У меня есть опам установлен.

Answer 1

Я на Ubuntu 16.04. Давайте сделаем шаг назад и начнем с установки OPAM:

$ sudo apt update && sudo apt install opam
$ opam --version
1.2.2
$ opam init     # agree to modify your dot-files
$ eval `opam config env`
$ ocamlc -version
4.02.3

Затем вы можете перейти с довольно старой версии Ubuntu на OCaml на более новую. Этот шаг не является обязательным и занимает около 10 минут.

$ opam switch 4.04.1
$ eval `opam config env`
$ ocamlc -version
4.04.1

Теперь давайте добавим следующий репозиторий, чтобы можно было установить math-comp:

$ opam repo add coq-released https://coq.inria.fr/opam/released

И, наконец, установите ssreflect:

$ opam install coq-mathcomp-ssreflect

OPAM выяснит зависимости (включая Coq), скачает и установит то, что мы просили!

Answer 2

Для полноты картины альтернативный способ - использование диспетчера пакетов Nix (вместо OPAM). После его установки (curl https://nixos.org/nix/install | sh), вы можете запустить CoqIDE с Math-Comp, доступным с помощью следующей команды:

nix-shell -p coqPackages_8_6.mathcomp --run coqide

Тогда вы можете просто начать свой файл с From mathcomp Require Import ssreflect.