~omrigan/lalambda-env

ref: 8378cf74613fc61d623b4dac1a4aaf97b8ccbb9f lalambda-env/README.md -rw-r--r-- 1.3 KiB
8378cf74 — Oleg Vasilev change names 9 months ago

#Настройка окружения

#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. Введите полученные на предыдущих шагах значения. Выведенное число и есть ваш ответ. Его нужно отправить в форму подтверждения участия