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