~omrigan/lalambda-env

ref: 3b221ec26828106de836a15e5466578320a0fc64 lalambda-env/readme.md -rw-r--r-- 1.3 KiB
3b221ec2 — Oleg Vasilev fix readme 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. Введите полученные на предыдущих шагах значения. Выведенное число и есть ваш ответ. Его нужно отправить в форму подтверждения участия