# Настройка окружения ## Coq Установите https://github.com/coq/platform/ ### Редакторы - Дима советует: заведите VSCode + VSCoq. - Антон советует: пользуйте Emacs + Proof General. - Олег бурчит: если ничего не работает, сработает CoqIDE. ## TLA Установите Java - Java 16 с https://adoptopenjdk.net/ должна работать ### Редакторы - Дима говорит: рекомендуется VSCode. - Сгодится TLA+ Toolbox. ## Haskell Установите stack # Сдача контеста - Верифицируйте лемму из coq/hello.v. Посмотрите в выводе какую лемма использовал `auto` для доказательства - Сделайте model checking у модели из tla. Посмотрите в выводе сколько всего состояний было использовано - Запустите stack run в папке haskell. Введите полученные на предыдущих шагах значения. Выведенное число и есть ваш ответ. Его нужно отправить в форму подтверждения участия