~omrigan/lalambda-env

Demo projects for coq, haskell and TLA+
8378cf74 — Oleg Vasilev 5 months ago
change names
3b221ec2 — Oleg Vasilev 5 months ago
fix readme
e2dcf986 — Oleg Vasilev 5 months ago
add license

refs

master
browse  log 

clone

read-only
https://git.sr.ht/~omrigan/lalambda-env
read/write
git@git.sr.ht:~omrigan/lalambda-env

You can also use your local clone with git send-email.

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

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