weakmemory.github.io

К странице курса

Для решения упражнений на Coq необходимо подготовить окружение.
Удобнее всего работать с доказательствами будет, если Вы установите всё необходимое напрямую в свою систему.
Другой, более быстрый способ - использовать виртуальную машину.

Установка вручную

Для установки вручную должна подойти любая ОС, поддерживающая opam (однако мы тестировали этот процесс только для Linux). В процессе установки может оказаться, что необходимо установить дополнительные пакеты в зависимости от Вашей системы.

  1. Установите opam (мы тестировали установку с версией 2.1.0).
  2. Инициализируйте opam, выполнив opam init -a. Ключ -a вносит изменения в ~/.profile, облегчающие пользование opam, поэтому мы рекомендуем его оставить.
  3. Создайте отдельное окружение opam, переключитесь него и обновите текущую оболочку: opam switch create semantics 4.12.0; opam switch set semantics; eval $(opam env). Создание окружения займёт некоторое время.
    • Если Вы пользуетесь Mac и собираетесь работать в CoqIDE, рекомендуем вместо версии 4.12.0 ставить версию 4.11.1.
  4. Загрузите локальную копию своего репозитория с задачами.
  5. Установите зависимости проекта.
    Сначала убедитесь, что работаете в нужном окружении opam: команда opam switch должна выделить только что созданное окружение semantics и не должна вывести предупреждений. Если это не так (что может случиться, если Вы открыли другое окно терминала), выполните opam switch semantics; eval $(opam env).
    Теперь, перейдите в каталог с локальным репозиторием Git и выполните в нём ./configure. Это добавит новые репозитории в текущее окружение opam и установит зависимости. Этот процесс займёт некоторое время.
  6. На данном шаге окружение должно быть готово. Запустите make и убедитесь, что при сборке файла src/b1.v выводится ошибка Tactic failure: tauto failed.
  7. Для редактирования доказательств Вы можете использовать любой редактор, доступный для Вашей системы. Убедитесь, что в выбранном редакторе Вы можете пошагово исполнить (см. последнюю секцию) файл src/b1.v вплоть до леммы nat_eq_tests_pass, доказательство которой должно прерываться с упомянутой выше ошибкой. Список редакторов и ссылки на инструкции к ним расположены в следующей секции.
    • Помимо редакторов общего назначения, Вы можете использовать CoqIDE - специализированную среду для работы с Coq.
      Она может быть установлена через opam командой opam install coqide.8.13.2. Обратите внимание, что устанавливаемая версия CoqIDE должна совпадать с установленной версией Coq. Её можно узнать, выполнив команду opam list | grep coq.
      Кроме того, Вам могут понадобиться пакеты вне opam (например, для Ubuntu 18 - libgtk-3-dev, libgtksourceview-3.0-dev и pkg-config).
    • В Emacs некоторые символы, используемые в доказательствах, отсутствуют в шрифте по умолчанию. В Debian-based дистрибутивах это исправляется установкой пакета ttf-ancient-fonts; для других дистрибутивов также должны существовать аналогичные пакеты.

Использование виртуальной машины

Самый простой способ подготовить окружение - использовать виртуальную машину (файл coq-sirius21-env.ova).

  1. Установите VirtualBox (мы используем версию 6.1), а также Oracle VM VirtualBox Extension pack.
  2. Откройте VirtualBox and перейдите в File/Import Appliance. Укажите путь к файлу coq-sirius21-env.ova и следуйте инструкциям установщика.
  3. Запустите только что созданную виртуальную машину.
    • В случае ошибки “RawFile#0 failed to create the raw output file …” попробуйте отключить последовательные порты (щелчок ПКМ по виртуальной машине -> Settings -> Serial Ports -> отключите поле "Enable Serial Port"). Также см. обсуждение связанной проблемы.
  4. Войдите в систему с именем пользователя и паролем “vagrant”.
  5. Клонируйте свой репозиторий с задачами в виртуальную машину.
  6. Убедитесь, что make -j 4 проходит по файлам *.v.
  7. В виртуальной машине доступны все редакторы, перечисленные в следующей секции.

Редакторы для интерактивной работы с доказательствами

Программы в Coq удобно исполнять пошагово, чтобы наблюдать за текущим состоянием доказательства. Такую возможность предоставляют редакторы, перечисленные ниже. Для каждого из них также указано, как выполнить в них команду “сделать шаг в доказательстве”, чтобы убедиться в правильности установки.